inductive Circuit (n : ℕ) : Type

• input {n : ℕ} (i : Fin n) : Circuit n
• not {n : ℕ} (c : Circuit n) : Circuit n
• and {n : ℕ} (cs : List (Circuit n)) : Circuit n
• or {n : ℕ} (cs : List (Circuit n)) : Circuit n

def Circuit.eval {n : ℕ} (v : Vector Bool n) : Circuit n → Bool

Equations

• Circuit.eval v (Circuit.input i) = v.get i
• Circuit.eval v c.not = !Circuit.eval v c
• Circuit.eval v (Circuit.and cs) = Circuit.evalAnd v cs
• Circuit.eval v (Circuit.or cs) = Circuit.evalOr v cs

def Circuit.evalAnd {n : ℕ} (v : Vector Bool n) : List (Circuit n) → Bool

Equations

• Circuit.evalAnd v [] = true
• Circuit.evalAnd v (c :: cs) = (Circuit.eval v c && Circuit.evalAnd v cs)

def Circuit.evalOr {n : ℕ} (v : Vector Bool n) : List (Circuit n) → Bool

Equations

• Circuit.evalOr v [] = false
• Circuit.evalOr v (c :: cs) = (Circuit.eval v c || Circuit.evalOr v cs)

def Circuit.depth {n : ℕ} : Circuit n → ℕ

Equations

• (Circuit.input i).depth = 0
• c.not.depth = c.depth
• (Circuit.and cs).depth = 1 + Circuit.maxDepth cs
• (Circuit.or cs).depth = 1 + Circuit.maxDepth cs

def Circuit.maxDepth {n : ℕ} : List (Circuit n) → ℕ

Equations

• Circuit.maxDepth [] = 0
• Circuit.maxDepth (c :: cs) = max c.depth (Circuit.maxDepth cs)

def Circuit.size {n : ℕ} : Circuit n → ℕ

Equations

• (Circuit.input i).size = 1
• c.not.size = c.size
• (Circuit.and cs).size = 1 + Circuit.sumSize cs
• (Circuit.or cs).size = 1 + Circuit.sumSize cs

def Circuit.sumSize {n : ℕ} : List (Circuit n) → ℕ

Equations

• Circuit.sumSize [] = 0
• Circuit.sumSize (c :: cs) = c.size + Circuit.sumSize cs

def parity {n : ℕ} (v : Vector Bool n) : Bool

Equations

• parity v = List.foldl xor false v.toList