@[instance_reducible]

instance instToStringVector_bdd {k : ℕ} {α : Type u} [ToString α] : ToString (Vector α k)

Equations

• instToStringVector_bdd = { toString := fun (v : Vector α k) => v.toList.toString }

Bdd

Pointer, Node and Bdd

inductive Pointer (m : ℕ) : Type

Pointer to a BDD node or terminal

• terminal {m : ℕ} : Bool → Pointer m
• node {m : ℕ} : Fin m → Pointer m

@[instance_reducible]

instance instFintypePointer {m✝ : ℕ} : Fintype (Pointer m✝)

Equations

• instFintypePointer = Fintype.ofEquiv (Bool ⊕ Fin m✝) (Pointer.proxyTypeEquiv m✝)

@[instance_reducible]

instance instDecidableEqPointer {m✝ : ℕ} : DecidableEq (Pointer m✝)

Equations

• instDecidableEqPointer = instDecidableEqPointer.decEq

def instDecidableEqPointer.decEq {m✝ : ℕ} (x✝ x✝¹ : Pointer m✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPointer.decEq (Pointer.terminal a) (Pointer.terminal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqPointer.decEq (Pointer.terminal a) (Pointer.node a_1) = isFalse ⋯
• instDecidableEqPointer.decEq (Pointer.node a) (Pointer.terminal a_1) = isFalse ⋯
• instDecidableEqPointer.decEq (Pointer.node a) (Pointer.node b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprPointer {m✝ : ℕ} : Repr (Pointer m✝)

Equations

• instReprPointer = { reprPrec := instReprPointer.repr }

def instReprPointer.repr {m✝ : ℕ} : Pointer m✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def instHashablePointer.hash {m✝ : ℕ} : Pointer m✝ → UInt64

Equations

• instHashablePointer.hash (Pointer.terminal a) = mixHash 0 (hash a)
• instHashablePointer.hash (Pointer.node a) = mixHash 1 (hash a)

@[instance_reducible]

instance instHashablePointer {m✝ : ℕ} : Hashable (Pointer m✝)

Equations

• instHashablePointer = { hash := instHashablePointer.hash }

@[instance_reducible]

instance Pointer.instToString {m : ℕ} : ToString (Pointer m)

Equations

• One or more equations did not get rendered due to their size.

structure Node (n m : ℕ) : Type

BDD node

• var : Fin n
• low : Pointer m
• high : Pointer m

@[instance_reducible]

instance instDecidableEqNode {n✝ m✝ : ℕ} : DecidableEq (Node n✝ m✝)

Equations

• instDecidableEqNode = instDecidableEqNode.decEq

def instDecidableEqNode.decEq {n✝ m✝ : ℕ} (x✝ x✝¹ : Node n✝ m✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instReprNode {n✝ m✝ : ℕ} : Repr (Node n✝ m✝)

Equations

• instReprNode = { reprPrec := instReprNode.repr }

def instReprNode.repr {n✝ m✝ : ℕ} : Node n✝ m✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Node.instToString {n m : ℕ} : ToString (Node n m)

Equations

• Node.instToString = { toString := fun (N : Node n m) => "⟨" ++ toString N.var ++ ", " ++ toString N.low ++ ", " ++ toString N.high ++ "⟩" }

structure Bdd (n m : ℕ) : Type

Raw BDD

• heap : Vector (Node n m) m
• root : Pointer m

@[instance_reducible]

instance instDecidableEqBdd {n✝ m✝ : ℕ} : DecidableEq (Bdd n✝ m✝)

Equations

• instDecidableEqBdd = instDecidableEqBdd.decEq

def instDecidableEqBdd.decEq {n✝ m✝ : ℕ} (x✝ x✝¹ : Bdd n✝ m✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqBdd.decEq { heap := a, root := a_1 } { heap := b, root := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Bdd.instToString {n m : ℕ} : ToString (Bdd n m)

Equations

• Bdd.instToString = { toString := fun (B : Bdd n m) => "⟨" ++ toString B.heap ++ ", " ++ toString B.root ++ "⟩" }

Bdd.low and Bdd.high

def Bdd.low {n m : ℕ} (B : Bdd n m) {j : Fin m} : B.root = Pointer.node j → Bdd n m

Equations

• B.low x = { heap := B.heap, root := B.heap[j].low }

theorem Bdd.low_eq {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : B.low h = { heap := B.heap, root := B.heap[j].low }

theorem Bdd.low_heap_eq_heap {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : (B.low h).heap = B.heap

theorem Bdd.low_root_eq_low {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : (B.low h).root = B.heap[j].low

def Bdd.high {n m : ℕ} (B : Bdd n m) {j : Fin m} : B.root = Pointer.node j → Bdd n m

Equations

• B.high x = { heap := B.heap, root := B.heap[j].high }

theorem Bdd.high_eq {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : B.high h = { heap := B.heap, root := B.heap[j].high }

theorem Bdd.high_heap_eq_heap {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : (B.high h).heap = B.heap

theorem Bdd.high_root_eq_high {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} : (B.high h).root = B.heap[j].high

Edge

inductive Edge {n m : ℕ} (M : Vector (Node n m) m) : Pointer m → Pointer m → Prop

• low {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : Edge M (Pointer.node j) M[j].low
• high {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : Edge M (Pointer.node j) M[j].high

theorem edge_iff {n m : ℕ} {M : Vector (Node n m) m} {p q : Pointer m} : Edge M p q ↔ ∃ (j : Fin m), p = Pointer.node j ∧ (q = M[j].low ∨ q = M[j].high)

theorem not_terminal_edge {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {q : Pointer n✝¹} : ¬Edge w (Pointer.terminal b) q

Terminals have no outgoing edges.

theorem Bdd.edge_low {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : Edge B.heap B.root (B.low h).root

theorem Bdd.edge_high {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : Edge B.heap B.root (B.high h).root

Reachability

def Pointer.Reachable {n m : ℕ} (v : Vector (Node n m) m) (a : Pointer m) : Pointer m → Prop

Equations

• Pointer.Reachable v = Relation.ReflTransGen (Edge v)

theorem Pointer.Reachable.refl {n m : ℕ} {v : Vector (Node n m) m} {p : Pointer m} : Reachable v p p

theorem Pointer.Reachable.trans {n m : ℕ} {v : Vector (Node n m) m} {p q r : Pointer m} : Reachable v p q → Reachable v q r → Reachable v p r

theorem Pointer.Reachable.ofEdge {n m : ℕ} {v : Vector (Node n m) m} {p q : Pointer m} : Edge v p q → Reachable v p q

theorem Pointer.Reachable.cons {n m : ℕ} {v : Vector (Node n m) m} {p q r : Pointer m} : Edge v p q → Reachable v q r → Reachable v p r

theorem Pointer.Reachable.snoc {n m : ℕ} {v : Vector (Node n m) m} {p q r : Pointer m} : Reachable v p q → Edge v q r → Reachable v p r

theorem Pointer.Reachable.eq_of_eq_edge {m n : ℕ} {v : Vector (Node n m) m} {n' : ℕ} {v' : Vector (Node n' m) m} : Edge v = Edge v' → Reachable v = Reachable v'

theorem Pointer.Reachable.iff_eq_or_cons {n m : ℕ} {v : Vector (Node n m) m} {p q : Pointer m} : Reachable v p q ↔ p = q ∨ ∃ (p' : Pointer m), Edge v p p' ∧ Reachable v p' q

theorem Pointer.Reachable.cases_snoc {n m : ℕ} {v : Vector (Node n m) m} {p : Pointer m} {motive : (q : Pointer m) → Reachable v p q → Prop} {q : Pointer m} (h1 : Reachable v p q) (refl : motive p ⋯) (snoc : ∀ {q r : Pointer m} (h1 : Reachable v p q) (h2 : Edge v q r), motive r ⋯) : motive q h1

theorem Pointer.Reachable.cases_cons {n m : ℕ} {v : Vector (Node n m) m} {q : Pointer m} {motive : (p : Pointer m) → Reachable v p q → Prop} {p : Pointer m} (h1 : Reachable v p q) (refl : motive q ⋯) (cons : ∀ {p r : Pointer m} (h1 : Edge v r p) (h2 : Reachable v p q), motive r ⋯) : motive p h1

theorem Pointer.Reachable.recOn {n m : ℕ} {v : Vector (Node n m) m} {p : Pointer m} {motive : (q : Pointer m) → Reachable v p q → Prop} {q : Pointer m} (h1 : Reachable v p q) (refl : motive p ⋯) (snoc : ∀ (q r : Pointer m) (h1 : Reachable v p q) (h2 : Edge v q r), motive q h1 → motive r ⋯) : motive q h1

theorem Pointer.Reachable.recOn' {n m : ℕ} {v : Vector (Node n m) m} {q : Pointer m} {motive : (p : Pointer m) → Reachable v p q → Prop} {p : Pointer m} (h1 : Reachable v p q) (refl : motive q ⋯) (cons : ∀ (p r : Pointer m) (h1 : Edge v r p) (h2 : Reachable v p q), motive p h2 → motive r ⋯) : motive p h1

@[simp]

theorem Pointer.Reachable.terminal_iff {n m : ℕ} {v : Vector (Node n m) m} {b : Bool} {q : Pointer m} : Reachable v (terminal b) q ↔ q = terminal b

theorem Bdd.reachable_node_iff {n m : ℕ} {B : Bdd n m} {j : Fin m} {q : Pointer m} : Pointer.Reachable B.heap (Pointer.node j) q ↔ q = Pointer.node j ∨ Pointer.Reachable B.heap B.heap[j].high q ∨ Pointer.Reachable B.heap B.heap[j].low q

@[simp]

theorem Bdd.reachable_low {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : Pointer.Reachable B.heap B.root B.heap[j].low

@[simp]

theorem Bdd.reachable_high {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : Pointer.Reachable B.heap B.root B.heap[j].high

RelevantPointer

@[reducible, inline]

abbrev Bdd.RelevantPointer {n m : ℕ} (B : Bdd n m) : Type

B.RelevantPointer is the subtype of pointers reachable from B.root.

Equations

• B.RelevantPointer = { q : Pointer m // Pointer.Reachable B.heap B.root q }

def Bdd.Relevant {n m : ℕ} (B : Bdd n m) (p : Pointer m) : Prop

Equations

• B.Relevant p = Pointer.Reachable B.heap B.root p

theorem Bdd.relevant_iff_reachable {n m : ℕ} {B : Bdd n m} {p : Pointer m} : B.Relevant p ↔ Pointer.Reachable B.heap B.root p

theorem Bdd.relevant_root {n m : ℕ} (B : Bdd n m) : B.Relevant B.root

Pointer.toVar and Bdd.MayPrecede

def Pointer.toVar {n m : ℕ} (M : Vector (Node n m) m) : Pointer m → Fin n.succ

Equations

• Pointer.toVar M (Pointer.terminal a) = Fin.last n
• Pointer.toVar M (Pointer.node a) = ⟨↑M[a].var, ⋯⟩

@[simp]

theorem Pointer.toVar_terminal {b : Bool} {n m : ℕ} (w : Vector (Node n m) m) : toVar w (terminal b) = ⟨n, ⋯⟩

@[simp]

theorem Pointer.toVar_node {n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} : ↑(toVar w (node j)) = ↑w[j].var

theorem Pointer.toVar_heap_set {n m : ℕ} {M : Vector (Node n m) m} {N : Node n m} {i j : Fin m} : i ≠ j → toVar (M.set (↑i) N ⋯) (node j) = toVar M (node j)

def Pointer.toVarD {n m : ℕ} (M : Vector (Node n m) m) : Pointer m → ℕ → ℕ

Equations

• Pointer.toVarD M (Pointer.terminal a) x✝ = x✝
• Pointer.toVarD M (Pointer.node j) x✝ = ↑M[j].var

@[simp]

theorem Pointer.toVarD_terminal {n m : ℕ} (w : Vector (Node n m) m) {b : Bool} {i : ℕ} : toVarD w (terminal b) i = i

@[simp]

theorem Pointer.toVarD_node {n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} {i : ℕ} : toVarD w (node j) i = ↑w[j].var

def Bdd.MayPrecede {n m : ℕ} (B : Bdd n m) (p q : Pointer m) : Prop

Equations

• B.MayPrecede p q = (Pointer.toVar B.heap p < Pointer.toVar B.heap q)

theorem Bdd.mayPrecede_iff {n m : ℕ} {B : Bdd n m} {p q : Pointer m} : B.MayPrecede p q ↔ ∃ (j : Fin m), p = Pointer.node j ∧ ∀ (j' : Fin m), q = Pointer.node j' → B.heap[j].var < B.heap[j'].var

theorem Bdd.mayPrecede_eq_of_heap_eq {n m : ℕ} {B1 B2 : Bdd n m} : B1.heap = B2.heap → B1.MayPrecede = B2.MayPrecede

@[simp]

theorem Bdd.mayPrecede_node {n m : ℕ} {B : Bdd n m} {j j' : Fin m} : B.MayPrecede (Pointer.node j) (Pointer.node j') ↔ B.heap[j].var < B.heap[j'].var

Ordered

def Bdd.Ordered {n m : ℕ} (B : Bdd n m) : Prop

A BDD is Ordered if all edges relevant from the root respect the variable ordering.

Equations

• B.Ordered = ∀ (p q : Pointer m), Pointer.Reachable B.heap B.root p → Edge B.heap p q → B.MayPrecede p q

theorem Bdd.ordered_iff {n m : ℕ} {B : Bdd n m} : B.Ordered ↔ ∀ (p q : Pointer m), Pointer.Reachable B.heap B.root p → Edge B.heap p q → B.MayPrecede p q

theorem Bdd.ordered_iff' {n m : ℕ} {B : Bdd n m} : B.Ordered ↔ ∀ (p q : Pointer m), Pointer.Reachable B.heap B.root p → Edge B.heap p q → Pointer.toVar B.heap p < Pointer.toVar B.heap q

theorem Bdd.no_self_edge_of_ordered {n m : ℕ} {B : Bdd n m} {p : Pointer m} : B.Ordered → B.Relevant p → ¬Edge B.heap p p

theorem Bdd.ordered_of_terminal {n m : ℕ} {b : Bool} {B : Bdd n m} : B.root = Pointer.terminal b → B.Ordered

Terminals induce Ordered BDDs.

theorem Bdd.ordered_of_reachable {n m : ℕ} {B : Bdd n m} {p : Pointer m} : B.Ordered → Pointer.Reachable B.heap B.root p → { heap := B.heap, root := p }.Ordered

theorem Bdd.ordered_of_edge {n m : ℕ} {B : Bdd n m} {p : Pointer m} : B.Ordered → Edge B.heap B.root p → { heap := B.heap, root := p }.Ordered

theorem Bdd.high_ordered {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : B.Ordered → (B.high h).Ordered

theorem Bdd.low_ordered {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : B.Ordered → (B.low h).Ordered

OBdd

structure OBdd (n m : ℕ) : Type

• bdd : Bdd n m
• ordered : self.bdd.Ordered

@[simp]

theorem OBdd.mk_eq_self {n m : ℕ} {O : OBdd n m} {h : { heap := O.bdd.heap, root := O.bdd.root }.Ordered} : { bdd := { heap := O.bdd.heap, root := O.bdd.root }, ordered := h } = O

@[simp]

theorem OBdd.eq_iff_bdd_eq {n m : ℕ} {O U : OBdd n m} : O = U ↔ O.bdd.heap = U.bdd.heap ∧ O.bdd.root = U.bdd.root

OBdd.low and OBdd.high

def OBdd.low {n m : ℕ} (O : OBdd n m) {j : Fin m} : O.bdd.root = Pointer.node j → OBdd n m

Equations

• O.low x✝ = { bdd := O.bdd.low x✝, ordered := ⋯ }

@[simp]

theorem OBdd.mk_eq_low {n m : ℕ} {O : OBdd n m} {j : Fin m} {ho : { heap := O.bdd.heap, root := O.bdd.heap[j].low }.Ordered} (h : O.bdd.root = Pointer.node j) : { bdd := { heap := O.bdd.heap, root := O.bdd.heap[j].low }, ordered := ho } = O.low h

theorem OBdd.low_eq {n m : ℕ} (O : OBdd n m) {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.low h = { bdd := O.bdd.low h, ordered := ⋯ }

theorem OBdd.bdd_low {n m : ℕ} (O : OBdd n m) {j : Fin m} {h : O.bdd.root = Pointer.node j} : (O.low h).bdd = O.bdd.low h

@[simp]

theorem OBdd.low_heap_eq_heap {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : (O.low h).bdd.heap = O.bdd.heap

@[simp]

theorem OBdd.low_root_eq_low {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : (O.low h).bdd.root = O.bdd.heap[j].low

def OBdd.high {n m : ℕ} (O : OBdd n m) {j : Fin m} : O.bdd.root = Pointer.node j → OBdd n m

Equations

• O.high x✝ = { bdd := O.bdd.high x✝, ordered := ⋯ }

@[simp]

theorem OBdd.mk_eq_high {n m : ℕ} {O : OBdd n m} {j : Fin m} {ho : { heap := O.bdd.heap, root := O.bdd.heap[j].high }.Ordered} (h : O.bdd.root = Pointer.node j) : { bdd := { heap := O.bdd.heap, root := O.bdd.heap[j].high }, ordered := ho } = O.high h

theorem OBdd.high_eq {n m : ℕ} (O : OBdd n m) {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.high h = { bdd := O.bdd.high h, ordered := ⋯ }

theorem OBdd.bdd_high {n m : ℕ} (O : OBdd n m) {j : Fin m} {h : O.bdd.root = Pointer.node j} : (O.high h).bdd = O.bdd.high h

@[simp]

theorem OBdd.high_heap_eq_heap {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : (O.high h).bdd.heap = O.bdd.heap

@[simp]

theorem OBdd.high_root_eq_high {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : (O.high h).bdd.root = O.bdd.heap[j].high

sub-Bdds

theorem OBdd.ordered_of_reachable {n m : ℕ} {O : OBdd n m} {p : Pointer m} : Pointer.Reachable O.bdd.heap O.bdd.root p → { heap := O.bdd.heap, root := p }.Ordered

theorem OBdd.ordered_of_relevant {n m : ℕ} (O : OBdd n m) (S : O.bdd.RelevantPointer) : { heap := O.bdd.heap, root := ↑S }.Ordered

All BDDs in the graph of an Ordered BDD are Ordered.

def OBdd.subBdd {n m : ℕ} (O : OBdd n m) (p : O.bdd.RelevantPointer) : OBdd n m

Equations

• O.subBdd p = { bdd := { heap := O.bdd.heap, root := ↑p }, ordered := ⋯ }

theorem OBdd.subBdd_eq {n m : ℕ} (O : OBdd n m) (p : O.bdd.RelevantPointer) : O.subBdd p = { bdd := { heap := O.bdd.heap, root := ↑p }, ordered := ⋯ }

@[simp]

theorem OBdd.heap_subBdd {n m : ℕ} {O : OBdd n m} (p : O.bdd.RelevantPointer) : (O.subBdd p).bdd.heap = O.bdd.heap

@[simp]

theorem OBdd.root_subBdd {n m : ℕ} {O : OBdd n m} (p : O.bdd.RelevantPointer) : (O.subBdd p).bdd.root = ↑p

@[simp]

theorem OBdd.subBdd_root {n m : ℕ} (O : OBdd n m) : O.subBdd ⟨O.bdd.root, ⋯⟩ = O

theorem OBdd.reachable_low_of_subBdd {n m : ℕ} {O : OBdd n m} {p : O.bdd.RelevantPointer} {j : Fin m} (h : (O.subBdd p).bdd.root = Pointer.node j) : Pointer.Reachable O.bdd.heap O.bdd.root O.bdd.heap[j].low

@[simp]

theorem OBdd.low_subBdd {n m : ℕ} {O : OBdd n m} {p : O.bdd.RelevantPointer} {j : Fin m} {h : (O.subBdd p).bdd.root = Pointer.node j} : (O.subBdd p).low h = O.subBdd ⟨O.bdd.heap[j].low, ⋯⟩

theorem OBdd.reachable_high_of_subBdd {n m : ℕ} {O : OBdd n m} {p : O.bdd.RelevantPointer} {j : Fin m} (h : (O.subBdd p).bdd.root = Pointer.node j) : Pointer.Reachable O.bdd.heap O.bdd.root O.bdd.heap[j].high

@[simp]

theorem OBdd.high_subBdd {n m : ℕ} {O : OBdd n m} {p : O.bdd.RelevantPointer} {j : Fin m} {h : (O.subBdd p).bdd.root = Pointer.node j} : (O.subBdd p).high h = O.subBdd ⟨O.bdd.heap[j].high, ⋯⟩

var

def Bdd.var {n m : ℕ} (B : Bdd n m) : Fin n.succ

Equations

• B.var = Pointer.toVar B.heap B.root

theorem Bdd.var_eq {n m : ℕ} (B : Bdd n m) : B.var = Pointer.toVar B.heap B.root

theorem Bdd.var_node {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : B.var = B.heap[j].var.castSucc

def OBdd.var {n m : ℕ} (O : OBdd n m) : ℕ

Equations

• O.var = ↑O.bdd.var

theorem OBdd.var_eq_bdd_var {n m : ℕ} (O : OBdd n m) : O.var = ↑O.bdd.var

theorem OBdd.var_eq {n m : ℕ} (O : OBdd n m) : O.var = ↑(Pointer.toVar O.bdd.heap O.bdd.root)

theorem OBdd.var_node {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : O.var = ↑O.bdd.heap[j].var

theorem OBdd.var_le {n m : ℕ} (O : OBdd n m) : O.var ≤ n

theorem OBdd.var_lt_high_var {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.var < (O.high h).var

theorem OBdd.var_lt_low_var {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.var < (O.low h).var

Termination

def Bdd.InvEdge {n m : ℕ} (B : Bdd n m) (p q : B.RelevantPointer) : Prop

Equations

• B.InvEdge p q = Edge B.heap ↑q ↑p

theorem invEdge_wellFounded {n m : ℕ} (O : OBdd n m) : WellFounded O.bdd.InvEdge

@[instance_reducible]

instance RelevantPointer.instWellFoundedRelation {n m : ℕ} (O : OBdd n m) : WellFoundedRelation O.bdd.RelevantPointer

Equations

• RelevantPointer.instWellFoundedRelation O = { rel := O.bdd.InvEdge, wf := ⋯ }

def OEdge {n m : ℕ} (O U : OBdd n m) : Prop

Equations

• OEdge O U = (O.bdd.heap = U.bdd.heap ∧ Edge O.bdd.heap O.bdd.root U.bdd.root)

theorem OEdge.flip_wellFounded {n m : ℕ} : WellFounded (flip OEdge)

The OEdge relation between Ordered BDDs is converse well-founded.

@[instance_reducible]

instance OEdge.instWellFoundedRelation {n m : ℕ} : WellFoundedRelation (OBdd n m)

Equations

• OEdge.instWellFoundedRelation = { rel := flip OEdge, wf := ⋯ }

@[simp]

theorem oedge_of_low {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {j : Fin m✝} {h : O.bdd.root = Pointer.node j} : OEdge O (O.low h)

@[simp]

theorem oedge_of_high {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {j : Fin m✝} {h : O.bdd.root = Pointer.node j} : OEdge O (O.high h)

Induction

theorem Bdd.terminal_or_node {n m : ℕ} (B : Bdd n m) : (∃ (b : Bool), B.root = Pointer.terminal b ∧ B = { heap := B.heap, root := Pointer.terminal b }) ∨ ∃ (j : Fin m), B.root = Pointer.node j ∧ B = { heap := B.heap, root := Pointer.node j }

theorem OBdd.init_inductionOn {n m : ℕ} (t : OBdd n m) {motive : OBdd n m → Prop} (base : ∀ (b : Bool) (B : OBdd n m), B.bdd.heap = t.bdd.heap → B.bdd.root = Pointer.terminal b → motive B) (step : ∀ (B : OBdd n m) (j : Fin m), B.bdd.heap = t.bdd.heap → ∀ (h : B.bdd.root = Pointer.node j), motive (B.low h) → motive (B.high h) → motive B) : motive t

toTree and evaluate

@[irreducible]

def OBdd.toTree {n m : ℕ} (O : OBdd n m) : DecisionTree n

Equations

• O.toTree = match h : O.bdd.root with | Pointer.terminal b => DecisionTree.leaf b | Pointer.node j => DecisionTree.branch O.bdd.heap[j].var (O.low h).toTree (O.high h).toTree

theorem OBdd.toTree_terminal {n m : ℕ} {O : OBdd n m} {b : Bool} (h : O.bdd.root = Pointer.terminal b) : O.toTree = DecisionTree.leaf b

theorem OBdd.toTree_eq_leaf_iff_terminal {n m : ℕ} {O : OBdd n m} {b : Bool} : O.toTree = DecisionTree.leaf b ↔ O.bdd.root = Pointer.terminal b

theorem OBdd.toTree_node {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : O.toTree = DecisionTree.branch O.bdd.heap[j].var (O.low h).toTree (O.high h).toTree

def OBdd.evaluate {n m : ℕ} : OBdd n m → Vector Bool n → Bool

Equations

• OBdd.evaluate = DecisionTree.evaluate ∘ OBdd.toTree

theorem OBdd.evaluate_def {n m : ℕ} {O : OBdd n m} : O.evaluate = O.toTree.evaluate

theorem OBdd.evaluate_cast {n m n' : ℕ} {I : Vector Bool n'} {O : OBdd n m} (h : n = n') : (h ▸ O).evaluate I = O.evaluate (⋯ ▸ I)

@[simp]

theorem OBdd.evaluate_terminal {n m : ℕ} {O : OBdd m n} {b : Bool} : O.bdd.root = Pointer.terminal b → O.evaluate = fun (x : Vector Bool m) => b

Spell out OBdd.evaluate for terminals.

@[simp]

theorem OBdd.evaluate_node {n m : ℕ} {O : OBdd n m} {I : Vector Bool n} {j : Fin m} (h : O.bdd.root = Pointer.node j) : O.evaluate I = if I[O.bdd.heap[j].var] = true then (O.high h).evaluate I else (O.low h).evaluate I

Spell out OBdd.evaluate for non-terminals.

theorem OBdd.evaluate_node' {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : O.evaluate = fun (I : Vector Bool n) => if I[O.bdd.heap[j].var] = true then (O.high h).evaluate I else (O.low h).evaluate I

theorem OBdd.not_dependsOn_lt_root {n m : ℕ} {O : OBdd n m} {I J : Vector Bool n} (h : ∀ (i : Fin n), O.var ≤ ↑i → I[i] = J[i]) : O.evaluate I = O.evaluate J

theorem OBdd.independentOf_lt_root {n m : ℕ} (O : OBdd n m) (i : Fin O.var) : Nary.IndependentOf O.evaluate (Fin.castLE ⋯ i)

Similarity

def OBdd.Similar {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') : Prop

Equations

• O.Similar U = (O.toTree = U.toTree)

theorem OBdd.similar_iff {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} : O.Similar U ↔ O.toTree = U.toTree

theorem OBdd.similar_low {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} (h1 : O.bdd.root = Pointer.node j) {j' : Fin m'} (h2 : U.bdd.root = Pointer.node j') : O.Similar U → (O.low h1).Similar (U.low h2)

theorem OBdd.similar_high {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} (h1 : O.bdd.root = Pointer.node j) {j' : Fin m'} (h2 : U.bdd.root = Pointer.node j') : O.Similar U → (O.high h1).Similar (U.high h2)

def OBdd.SimilarRP {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} (p : O.bdd.RelevantPointer) (q : U.bdd.RelevantPointer) : Prop

Equations

• OBdd.SimilarRP p q = (O.subBdd p).Similar (U.subBdd q)

theorem OBdd.similarRP_iff {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {p : O.bdd.RelevantPointer} {q : U.bdd.RelevantPointer} : SimilarRP p q ↔ (O.subBdd p).toTree = (U.subBdd q).toTree

theorem OBdd.Similar.instEquivalence {n m : ℕ} : Equivalence Similar

Isomorphism of Ordered BDDs is an equivalence relation.

theorem OBdd.Similar_of_terminal {n m m' : ℕ} {b : Bool} {O : OBdd n m} {U : OBdd n m'} : O.bdd.root = Pointer.terminal b → U.bdd.root = Pointer.terminal b → O.Similar U

OBdd.Reduced

inductive Pointer.Redundant {n m : ℕ} (M : Vector (Node n m) m) : Pointer m → Prop

A pointer is redundant if it point to node N with N.low = N.high.

• red {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : M[j].low = M[j].high → Redundant M (node j)

@[instance_reducible]

instance Pointer.Redundant.instDecidable {n m : ℕ} (w : Vector (Node n m) m) : DecidablePred (Redundant w)

Equations

• One or more equations did not get rendered due to their size.

def Bdd.NoRedundancy {n m : ℕ} (B : Bdd n m) : Prop

Equations

• B.NoRedundancy = ∀ (p : B.RelevantPointer), ¬Pointer.Redundant B.heap ↑p

def OBdd.Reduced {n m : ℕ} (O : OBdd n m) : Prop

A BDD is Reduced if its graph does not contain redundant nodes or distinct similar subgraphs.

Equations

• O.Reduced = (O.bdd.NoRedundancy ∧ Subrelation OBdd.SimilarRP (InvImage Eq Subtype.val))

theorem OBdd.reduced_of_terminal {n m : ℕ} {O : OBdd n m} {b : Bool} (h : O.bdd.root = Pointer.terminal b) : O.Reduced

Terminal BDDs are reduced.

theorem Bdd.reduced_of_terminal {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {o : { heap := M, root := Pointer.terminal b }.Ordered} : { bdd := { heap := M, root := Pointer.terminal b }, ordered := o }.Reduced

theorem OBdd.high_reduced {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.Reduced → (O.high h).Reduced

theorem OBdd.low_reduced {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : O.Reduced → (O.low h).Reduced

Size

@[instance_reducible]

instance OBdd.instDecidableReachable {n m : ℕ} (O : OBdd n m) : DecidablePred (Pointer.Reachable O.bdd.heap O.bdd.root)

Equations

• O.instDecidableReachable = OBdd.decidableReachable✝ O

def OBdd.size {n m : ℕ} (O : OBdd n m) : ℕ

The number of nodes in O reachable from the root.

Equations

• O.size = Fintype.card { j : Fin m // Pointer.Reachable O.bdd.heap O.bdd.root (Pointer.node j) }

theorem OBdd.size_eq_card_reachable {n m : ℕ} (O : OBdd n m) : O.size = Fintype.card { j : Fin m // Pointer.Reachable O.bdd.heap O.bdd.root (Pointer.node j) }

@[simp]

theorem OBdd.size_terminal {b : Bool} {n m : ℕ} {O : OBdd n m} (h : O.bdd.root = Pointer.terminal b) : O.size = 0

def OBdd.size' {n m : ℕ} : OBdd n m → ℕ

The number of nodes in the unraveling of O

Equations

• OBdd.size' = DecisionTree.size ∘ OBdd.toTree

theorem OBdd.size'_node {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : O.size' = 1 + (O.low h).size' + (O.high h).size'

theorem OBdd.evaluate_high_eq_evaluate_set_true {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : (O.high h).evaluate = O.evaluate ∘ fun (I : Vector Bool n) => I.set (↑O.bdd.heap[j].var) true ⋯

theorem OBdd.evaluate_low_eq_evaluate_set_false {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} : (O.low h).evaluate = O.evaluate ∘ fun (I : Vector Bool n) => I.set (↑O.bdd.heap[j].var) false ⋯

theorem OBdd.Canonicity {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} (ho : O.Reduced) (hu : U.Reduced) : O.evaluate = U.evaluate → O.Similar U

Reduced OBDDs are canonical.

theorem OBdd.Canonicity_reverse {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} : O.Similar U → O.evaluate = U.evaluate

Lemmas about Ordered

theorem OBdd.ordered_of_low_edge {n n✝ : ℕ} {v : Vector (Node n✝ n) n} {j : Fin n} : { heap := v, root := Pointer.node j }.Ordered → { heap := v, root := v[j].low }.Ordered

theorem OBdd.ordered_of_high_edge {n n✝ : ℕ} {v : Vector (Node n✝ n) n} {j : Fin n} : { heap := v, root := Pointer.node j }.Ordered → { heap := v, root := v[j].high }.Ordered

theorem Bdd.ordered_of_low_high_ordered {n m : ℕ} {B : Bdd n m} {j : Fin m} (h : B.root = Pointer.node j) : (B.low h).Ordered → B.var < (B.low h).var → (B.high h).Ordered → B.var < (B.high h).var → B.Ordered

Lemmas about reachability

theorem OBdd.not_edge_reachable {n m : ℕ} {O : OBdd n m} {p q : Pointer m} : Pointer.Reachable O.bdd.heap O.bdd.root p → Edge O.bdd.heap p q → ¬Pointer.Reachable O.bdd.heap q p

An acyclicity lemma: an edge from p to q implies that p is not reachable from q.

theorem OBdd.not_reachable_low_root {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : ¬Pointer.Reachable O.bdd.heap O.bdd.heap[j].low O.bdd.root

theorem OBdd.not_reachable_high_root {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : O.bdd.root = Pointer.node j) : ¬Pointer.Reachable O.bdd.heap O.bdd.heap[j].high O.bdd.root

theorem Pointer.Reachable_iff {n m : ℕ} {r p : Pointer m} {M : Vector (Node n m) m} : Reachable M r p ↔ r = p ∨ ∃ (j : Fin m), r = node j ∧ (Reachable M M[j].low p ∨ Reachable M M[j].high p)

theorem OBdd.reachable_or_eq_low_high {n m : ℕ} {O : OBdd n m} {p : Pointer m} : Pointer.Reachable O.bdd.heap O.bdd.root p → O.bdd.root = p ∨ ∃ (j : Fin m) (h : O.bdd.root = Pointer.node j), Pointer.Reachable O.bdd.heap (O.low h).bdd.root p ∨ Pointer.Reachable O.bdd.heap (O.high h).bdd.root p

Bdd.usesVar

def Bdd.usesVar {n m : ℕ} (B : Bdd n m) (i : Fin n) : Prop

Equations

• B.usesVar i = ∃ (j : Fin m), Pointer.Reachable B.heap B.root (Pointer.node j) ∧ B.heap[j].var = i

theorem Bdd.usesVar_of_high_usesVar {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} {i : Fin n} : (B.high h).usesVar i → B.usesVar i

theorem Bdd.usesVar_of_low_usesVar {n m : ℕ} {B : Bdd n m} {j : Fin m} {h : B.root = Pointer.node j} {i : Fin n} : (B.low h).usesVar i → B.usesVar i

theorem OBdd.usesVar_of_high_usesVar {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} {i : Fin n} : (O.high h).bdd.usesVar i → O.bdd.usesVar i

theorem OBdd.usesVar_of_low_usesVar {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : O.bdd.root = Pointer.node j} {i : Fin n} : (O.low h).bdd.usesVar i → O.bdd.usesVar i

theorem OBdd.usesVar_iff_dependsOn_of_reduced {n m : ℕ} {O : OBdd n m} {i : Fin n} : O.Reduced → (O.bdd.usesVar i ↔ Nary.DependsOn O.evaluate i)

theorem OBdd.toTree_usesVar {n m : ℕ} {i : Fin n} {O : OBdd n m} : O.bdd.usesVar i ↔ DecisionTree.usesVar i O.toTree

@[instance_reducible]

instance OBdd.instDecidableUsesVar {n m : ℕ} {O : OBdd n m} : DecidablePred O.bdd.usesVar

Equations

• OBdd.instDecidableUsesVar i = (usesVar_helper✝ O i O.bdd.root ⋯ ⟨Std.HashSet.emptyWithCapacity, ⋯⟩).1

Raw Bdds

Pointer.equiv and Node.equiv

def Pointer.equiv {m m' : ℕ} (p : Pointer m) (p' : Pointer m') : Prop

Equations

• p.equiv p' = ((∀ (b : Bool), p = Pointer.terminal b → p' = Pointer.terminal b) ∧ ∀ (j : Fin m), p = Pointer.node j → ∃ (j' : Fin m'), p' = Pointer.node j' ∧ ↑j = ↑j')

theorem Pointer.equiv_refl {m : ℕ} (p : Pointer m) : p.equiv p

theorem Pointer.equiv_symm {m m✝ : ℕ} {q : Pointer m✝} {p : Pointer m} : p.equiv q → q.equiv p

def Node.equiv {n m n' m' : ℕ} (N : Node n m) (N' : Node n' m') : Prop

Equations

• N.equiv N' = (↑N.var = ↑N'.var ∧ N.low.equiv N'.low ∧ N.high.equiv N'.high)

theorem Node.equiv_refl {n m : ℕ} (N : Node n m) : N.equiv N

theorem Node.equiv_symm {n✝ m✝ : ℕ} {N : Node n✝ m✝} {n✝¹ m✝¹ : ℕ} {M : Node n✝¹ m✝¹} : N.equiv M → M.equiv N

theorem OBdd.toTree_eq_toTree_of_ordered_heap_all_reachable_eq {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') : (∀ (j : Fin m'), Pointer.Reachable U.bdd.heap U.bdd.root (Pointer.node j) → ∃ (hj : ↑j < m), O.bdd.heap[↑j].equiv U.bdd.heap[j]) → U.bdd.root.equiv O.bdd.root → O.toTree = U.toTree

theorem OBdd.evaluate_eq_evaluate_of_ordered_heap_all_reachable_eq {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') : (∀ (j : Fin m'), Pointer.Reachable U.bdd.heap U.bdd.root (Pointer.node j) → ∃ (hj : ↑j < m), O.bdd.heap[↑j].equiv U.bdd.heap[j]) → U.bdd.root.equiv O.bdd.root → O.evaluate = U.evaluate

RawPointer and RawNode

inductive RawBdd.RawPointer : Type

• terminal (b : Bool) : RawPointer
• node (n : ℕ) : RawPointer

structure RawBdd.RawNode (n : ℕ) : Type

• va : Fin n
• lo : RawPointer
• hi : RawPointer

def RawBdd.RawPointer.Bounded (m : ℕ) (p : RawPointer) : Prop

Equations

• RawBdd.RawPointer.Bounded m p = ∀ {i : ℕ}, p = RawBdd.RawPointer.node i → i < m

theorem RawBdd.RawPointer.bounded_iff {m : ℕ} {p : RawPointer} : Bounded m p ↔ ∀ {i : ℕ}, p = node i → i < m

theorem RawBdd.RawPointer.bounded_terminal {m : ℕ} {b : Bool} : Bounded m (terminal b)

theorem RawBdd.RawPointer.bounded_node_iff {m n : ℕ} : Bounded m (node n) ↔ n < m

theorem RawBdd.RawPointer.bounded_of_le {m m' : ℕ} {p : RawPointer} (hm : Bounded m p) (h : m ≤ m') : Bounded m' p

def RawBdd.RawPointer.cook {m : ℕ} (p : RawPointer) (h : Bounded m p) : Pointer m

Equations

• (RawBdd.RawPointer.terminal b).cook h_2 = Pointer.terminal b
• (RawBdd.RawPointer.node i).cook h_2 = Pointer.node ⟨i, ⋯⟩

theorem RawBdd.RawPointer.cook_terminal {b : Bool} {m : ℕ} {h : Bounded m (terminal b)} : (terminal b).cook h = Pointer.terminal b

theorem RawBdd.RawPointer.cook_node {n m : ℕ} {h : Bounded m (node n)} : (node n).cook h = Pointer.node ⟨n, ⋯⟩

theorem RawBdd.RawPointer.cook_equiv {m1 : ℕ} {p : RawPointer} {m2 : ℕ} {h1 : Bounded m1 p} {h2 : Bounded m2 p} : (p.cook h1).equiv (p.cook h2)

def RawBdd.RawPointer.fromPointer {m : ℕ} : Pointer m → RawPointer

Equations

• RawBdd.RawPointer.fromPointer (Pointer.terminal a) = RawBdd.RawPointer.terminal a
• RawBdd.RawPointer.fromPointer (Pointer.node a) = RawBdd.RawPointer.node ↑a

structure RawBdd.RawNode.Bounded {n : ℕ} (m : ℕ) (N : RawNode n) : Prop

• lo_bounded : RawPointer.Bounded m N.lo
• hi_bounded : RawPointer.Bounded m N.hi

theorem RawBdd.RawNode.bounded_iff {n m : ℕ} {N : RawNode n} : Bounded m N ↔ RawPointer.Bounded m N.lo ∧ RawPointer.Bounded m N.hi

theorem RawBdd.RawNode.bounded_of_le {n m m' : ℕ} {N : RawNode n} (hm : Bounded m N) (h : m ≤ m') : Bounded m' N

def RawBdd.RawNode.cook {n m : ℕ} (N : RawNode n) (h : Bounded m N) : Node n m

Equations

• N.cook h = { var := N.va, low := N.lo.cook ⋯, high := N.hi.cook ⋯ }

theorem RawBdd.RawNode.cook_eq {n m : ℕ} {N : RawNode n} {h : Bounded m N} : N.cook h = { var := N.va, low := N.lo.cook ⋯, high := N.hi.cook ⋯ }

theorem RawBdd.RawNode.cook_equiv {n✝ : ℕ} {N : RawNode n✝} {m✝ : ℕ} {h1 : Bounded m✝ N} {m✝¹ : ℕ} {h2 : Bounded m✝¹ N} : (N.cook h1).equiv (N.cook h2)

theorem RawBdd.cook_low {n m : ℕ} {rn : RawNode n} {h1 : RawNode.Bounded m rn} : (rn.cook h1).low = rn.lo.cook ⋯

theorem RawBdd.cook_high {n m : ℕ} {rn : RawNode n} {h1 : RawNode.Bounded m rn} : (rn.cook h1).high = rn.hi.cook ⋯

theorem RawBdd.cook_inj {m : ℕ} {p q : RawPointer} {hp : RawPointer.Bounded m p} {hq : RawPointer.Bounded m q} : p.cook hp = q.cook hq ↔ p = q

def RawBdd.cook_heap {n c : ℕ} (v : Vector (RawNode n) c) (hh : ∀ (i : Fin c), RawNode.Bounded (↑i) v[i]) : Vector (Node n c) c

Equations

• RawBdd.cook_heap v hh = Vector.ofFn fun (i : Fin c) => v[i].cook ⋯

theorem RawBdd.cook_heap_eq {n c : ℕ} {v : Vector (RawNode n) c} {hh : ∀ (i : Fin c), RawNode.Bounded (↑i) v[i]} : cook_heap v hh = Vector.ofFn fun (i : Fin c) => v[i].cook ⋯

theorem RawBdd.cook_aux {p : RawPointer} {n m : ℕ} {j : Fin n} {hj : ↑j < m} {h1 : RawPointer.Bounded n p} {h2 : RawPointer.Bounded m p} : p.cook h1 = Pointer.node j → p.cook h2 = Pointer.node ⟨↑j, hj⟩

theorem RawBdd.push_ordered {n✝ n✝¹ : ℕ} {v : Vector (RawNode n✝) n✝¹} {h0 : ∀ (i : Fin n✝¹), RawNode.Bounded (↑i) v[i]} {p : RawPointer} {h1 : RawPointer.Bounded n✝¹ p} {N : RawNode n✝} {h2 : ∀ (i : Fin (n✝¹ + 1)), RawNode.Bounded (↑i) (v.push N)[i]} {h3 : RawPointer.Bounded (n✝¹ + 1) p} : { heap := cook_heap v h0, root := p.cook h1 }.Ordered → { heap := cook_heap (v.push N) h2, root := p.cook h3 }.Ordered

theorem RawBdd.push_evaluate {n m : ℕ} {O : OBdd n (m + 1)} {v : Vector (RawNode n) m} {N : RawNode n} {h0 : ∀ (i : Fin (m + 1)), RawNode.Bounded (↑i) (v.push N)[i]} {p : RawPointer} {hp : RawPointer.Bounded (m + 1) p} {h1 : ∀ (i : Fin m), RawNode.Bounded (↑i) v[i]} {hp' : RawPointer.Bounded m p} {ho : { heap := cook_heap v h1, root := p.cook hp' }.Ordered} (h_heap : O.bdd.heap = cook_heap (v.push N) h0) (h_root : O.bdd.root = p.cook hp) : O.evaluate = { bdd := { heap := cook_heap v h1, root := p.cook hp' }, ordered := ho }.evaluate