Complete this form and hit the "Save Changes" button!
Total atoms: 0 - Specified : 0 — Verified: 0.
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
-- REGION: load private
--Annotation: private input
def advice_0_0: Prop := c.Advice 0 0 = a
def advice_0_1: Prop := c.Advice 0 1 = b
def advice_0_2: Prop := c.Advice 0 2 = c
-- REGION: add
def selector_0_3: Prop := c.Selector 0 3 = 1
--Annotation: lhs
def advice_0_3: Prop := c.Advice 0 3 = a
def copy_0: Prop := c.Advice 0 3 = c.Advice 0 0
--Annotation: rhs
def advice_1_3: Prop := c.Advice 1 3 = b
def copy_1: Prop := c.Advice 1 3 = c.Advice 0 1
--Annotation: lhs + rhs
def advice_0_4: Prop := c.Advice 0 4 = (a) + (b)
-- REGION: mul
def selector_1_5: Prop := c.Selector 1 5 = 1
def advice_0_5: Prop := c.Advice 0 5 = (a) + (b)
def copy_2: Prop := c.Advice 0 5 = c.Advice 0 4
def advice_1_5: Prop := c.Advice 1 5 = c
def copy_3: Prop := c.Advice 1 5 = c.Advice 0 2
--Annotation: lhs * rhs
def advice_0_6: Prop := c.Advice 0 6 = ((a) + (b)) * (c)
def copy_4: Prop := c.Advice 0 6 = c.Instance 0 0
------GATES-------
def gate_0: Prop := ∀ row : ℕ, c.Selector 0 row * (c.Advice 0 (row) + c.Advice 1 (row) - c.Advice 0 (row + 1)) = 0
def gate_1: Prop := ∀ row : ℕ, c.Selector 1 row * (c.Advice 0 (row) * c.Advice 1 (row) - c.Advice 0 (row + 1)) = 0
