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

Equations

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

inductive Pointer (m : ℕ) : Type

Pointer to a BDD node or terminal

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

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

Equations

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

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

Equations

• instDecidableEqPointer = decEqPointer✝

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

Equations

• instReprPointer = { reprPrec := reprPointer✝ }

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

Equations

• instHashablePointer = { hash := hashPointer✝ }

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

Equations

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

inductive Pointer.le {m : ℕ} : Pointer m → Pointer m → Prop

• terminal_le_terminal {m : ℕ} {b c : Bool} : b ≤ c → (terminal b).le (terminal c)
• terminal_le_node {m : ℕ} {b : Bool} {j : Fin m} : (terminal b).le (node j)
• node_le_node {m : ℕ} {j i : Fin m} : j ≤ i → (node j).le (node i)

instance Pointer.instLE {m : ℕ} : LE (Pointer m)

Equations

• Pointer.instLE = { le := Pointer.le }

instance Pointer.instDecidableLe {m : ℕ} : DecidableLE (Pointer m)

Equations

• (Pointer.terminal a).instDecidableLe (Pointer.terminal a_1) = match a.instDecidableLe a_1 with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯
• (Pointer.terminal a).instDecidableLe (Pointer.node a_1) = isTrue ⋯
• (Pointer.node a).instDecidableLe (Pointer.terminal a_1) = isFalse ⋯
• (Pointer.node a).instDecidableLe (Pointer.node a_1) = match a.decLe a_1 with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯

structure Node (n m : ℕ) : Type

BDD node

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

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

Equations

• instDecidableEqNode = decEqNode✝

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

Equations

• instReprNode = { reprPrec := reprNode✝ }

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 instDecidableEqBdd {n✝ m✝ : ℕ} : DecidableEq (Bdd n✝ m✝)

Equations

• instDecidableEqBdd = decEqBdd✝

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

Equations

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

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} {p : Pointer m} : M[j].low = p → Edge M (Pointer.node j) p
• high {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} {p : Pointer m} : M[j].high = p → Edge M (Pointer.node j) p

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.

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_eq {b : Bool} {n m : ℕ} (w : Vector (Node n m) m) : toVar w (terminal b) = ↑n

@[simp]

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

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

def Pointer.MayPrecede {n m : ℕ} (M : Vector (Node n m) m) (p q : Pointer m) : Prop

Equations

• Pointer.MayPrecede M p q = (Pointer.toVar M p < Pointer.toVar M q)

theorem Pointer.not_terminal_MayPrecede {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {p : Pointer n✝¹} : ¬MayPrecede M (terminal b) p

Terminals must not precede other pointers.

theorem Pointer.MayPrecede_node_terminal {b : Bool} {n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} : MayPrecede w (node j) (terminal b)

Non-terminals may precede terminals.

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

Equations

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

theorem Pointer.Reachable.trans {n✝ n✝¹ : ℕ} {v : Vector (Node n✝ n✝¹) n✝¹} {a b c : Pointer n✝¹} (hab : Reachable v a b) (hbc : Reachable v b c) : Reachable v a c

@[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 }

instance Bdd.instDecidableEqRelevantPointer {n✝ m✝ : ℕ} {B : Bdd n✝ m✝} : DecidableEq B.RelevantPointer

Equations

• Bdd.instDecidableEqRelevantPointer x✝¹ x✝ = decidable_of_iff (↑x✝¹ = ↑x✝) ⋯

def Bdd.toRelevantPointer {n m : ℕ} (B : Bdd n m) : B.RelevantPointer

Equations

• B.toRelevantPointer = ⟨B.root, ⋯⟩

@[reducible, inline]

abbrev Bdd.RelevantEdge {n m : ℕ} (B : Bdd n m) (p q : B.RelevantPointer) : Prop

The Edge relation lifted to RelevantPointers.

Equations

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

theorem Bdd.relevantEdge_of_edge_of_reachable {n m : ℕ} {p q : Pointer m} {B : Bdd n m} (e : Edge B.heap p q) (hp : Pointer.Reachable B.heap B.root p) : B.RelevantEdge ⟨p, hp⟩ ⟨q, ⋯⟩

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

The MayPrecede relation lifted to RelevantPointers.

Equations

• B.RelevantMayPrecede p q = Pointer.MayPrecede B.heap ↑p ↑q

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 = Subrelation B.RelevantEdge B.RelevantMayPrecede

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

Terminals induce Ordered BDDs.

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

def OBdd (n m : ℕ) : Type

Equations

• OBdd n m = { B : Bdd n m // B.Ordered }

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

Equations

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

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

Equations

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

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

Equations

• O.var = ↑(↑O).var

def OBdd.rav {n m : ℕ} (B : OBdd n m) : ℕ

Equations

• B.rav = n - B.var

theorem OEdge.wellFounded {n m : ℕ} : WellFounded OEdge

The OEdge relation between Ordered BDDs is well-founded.

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

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

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

Equations

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

theorem Bdd.reachable_of_edge {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {p q : Pointer n✝¹} : Edge M p q → Pointer.Reachable M p q

theorem Bdd.ordered_of_relevant' {n m : ℕ} {v : Vector (Node n m) m} {q p : Pointer m} {B : Bdd n m} {h : B.heap = v} {r : B.root = q} : B.Ordered → Pointer.Reachable v q p → { heap := v, root := p }.Ordered

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

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

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

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

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

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

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

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

Equations

• O.high x✝ = ⟨(↑O).high x✝, ⋯⟩

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

Equations

• O.low x✝ = ⟨(↑O).low x✝, ⋯⟩

@[simp]

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

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

@[simp]

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

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

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

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

@[irreducible]

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

Equations

• O.toTree = match h : (↑O).root with | Pointer.terminal b => DecisionTree.leaf b | Pointer.node j => DecisionTree.branch (↑O).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_cast {n m n' : ℕ} {I : Vector Bool n'} {O : OBdd n m} (h : n = n') : (h ▸ O).evaluate I = O.evaluate (⋯ ▸ I)

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

Equations

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

def OBdd.Similar {n m : ℕ} : OBdd n m → OBdd n m → Prop

Equations

• OBdd.Similar = OBdd.HSimilar

instance OBdd.instDecidableSimilar {n m : ℕ} : DecidableRel Similar

Similarity of Ordered BDDs is decidable.

Equations

• O.instDecidableSimilar U = decidable_of_decidable_of_iff ⋯

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

Equations

• O.SimilarRP p q = OBdd.Similar ⟨{ heap := (↑O).heap, root := ↑p }, ⋯⟩ ⟨{ heap := (↑O).heap, root := ↑q }, ⋯⟩

instance OBdd.instDecidableSimilarRP {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {l r : (↑O).RelevantPointer} : Decidable (O.SimilarRP l r)

Equations

• OBdd.instDecidableSimilarRP = id inferInstance

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

Isomorphism of Ordered BDDs is an equivalence relation.

Equations

• ⋯ = ⋯

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 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).NoRedundancy ∧ Subrelation O.SimilarRP (InvImage Eq Subtype.val))

theorem transGen_iff_single_and_reflTransGen {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {a b : α✝} : Relation.TransGen r a b ↔ ∃ (c : α✝), r a c ∧ Relation.ReflTransGen r c b

def RelevantPointer.var {n m : ℕ} {B : Bdd n m} (p : B.RelevantPointer) : ℕ

Equations

• RelevantPointer.var p = ↑(Pointer.toVar B.heap ↑p)

def RelevantPointer.gap {n m : ℕ} {B : Bdd n m} (p : B.RelevantPointer) : ℕ

Equations

• RelevantPointer.gap p = n - RelevantPointer.var p

theorem RelevantEdge.flip_wellFounded {n✝ m✝ : ℕ} {B : Bdd n✝ m✝} (o : B.Ordered) : WellFounded (flip B.RelevantEdge)

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

Equations

• RelevantEdge.instWellFoundedRelation O = { rel := flip (↑O).RelevantEdge, wf := ⋯ }

@[irreducible]

instance OBdd.instDecidableReflTransGen {n m : ℕ} (O : OBdd n m) (p : (↑O).RelevantPointer) (q : Pointer m) : Decidable (Relation.ReflTransGen (Edge (↑O).heap) (↑p) q)

Equations

• O.instDecidableReflTransGen p q = ⋯.mpr (decidable_of_iff (q = ↑p ∨ Relation.TransGen (Edge (↑O).heap) (↑p) q) ⋯)

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

Equations

• Pointer.instDecidableReachable O = O.instDecidableReflTransGen ⟨(↑O).root, ⋯⟩

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

Equations

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

instance OBdd.instFintypeRelevantPointer {n m : ℕ} (O : OBdd n m) : Fintype (↑O).RelevantPointer

Equations

• O.instFintypeRelevantPointer = ⋯.mpr (Subtype.fintype (Pointer.Reachable (↑O).heap (↑O).root))

instance Pointer.instDecidableEitherReachable {n m : ℕ} (O U : OBdd n m) (h : (↑O).heap = (↑U).heap) : DecidablePred fun (q : Pointer m) => Reachable (↑O).heap (↑O).root q ∨ Reachable (↑O).heap (↑U).root q

Equations

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

instance OBdd.instFintypeEitherRelevantPointer {n m : ℕ} (O U : OBdd n m) (h : (↑O).heap = (↑U).heap) : Fintype { q : Pointer m // Pointer.Reachable (↑O).heap (↑O).root q ∨ Pointer.Reachable (↑O).heap (↑U).root q }

Equations

• O.instFintypeEitherRelevantPointer U h = ⋯.mpr (Subtype.fintype fun (q : Pointer m) => Pointer.Reachable (↑O).heap (↑O).root q ∨ Pointer.Reachable (↑O).heap (↑U).root q)

instance OBdd.instReducedDecidable {n m : ℕ} : DecidablePred Reduced

Reduced is decidable.

Equations

• x✝.instReducedDecidable = instDecidableAnd

theorem eq_of_constant_eq {α : Sort u_1} {β : Sort u_2} {c c' : β} [Inhabited α] : Function.const α c = Function.const α c' → c = c'

The output of equal constant functions with inhabited domain is equal.

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 }

@[irreducible]

theorem OBdd.init_inductionOn {n m : ℕ} (t : OBdd n m) {motive : OBdd n m → Prop} (base : ∀ (b : Bool), motive ⟨{ heap := (↑t).heap, root := Pointer.terminal b }, ⋯⟩) (step : ∀ (j : Fin m) (hl : { heap := (↑t).heap, root := (↑t).heap[j].low }.Ordered), motive ⟨{ heap := (↑t).heap, root := (↑t).heap[j].low }, ⋯⟩ → ∀ (hh : { heap := (↑t).heap, root := (↑t).heap[j].high }.Ordered), motive ⟨{ heap := (↑t).heap, root := (↑t).heap[j].high }, ⋯⟩ → ∀ (h : { heap := (↑t).heap, root := Pointer.node j }.Ordered), motive ⟨{ heap := (↑t).heap, root := Pointer.node j }, ⋯⟩) : motive t

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

Equations

• O.isTerminal = ∃ (b : Bool), (↑O).root = Pointer.terminal b

theorem not_OEdge_of_isTerminal {n m : ℕ} {U O : OBdd n m} : O.isTerminal → ¬OEdge O U

theorem Bdd.terminal_relevant_iff {b : Bool} {n m : ℕ} {B : Bdd n m} (h : B.root = Pointer.terminal b) (S : B.RelevantPointer) {motive : Pointer m → Prop} : motive ↑S ↔ motive (Pointer.terminal b)

The graph induced by a terminal BDD consists of a sole terminal pointer.

theorem Bdd.eq_terminal_of_relevant {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {B : Bdd n m} (h : B = { heap := v, root := Pointer.terminal b }) (S : B.RelevantPointer) : ↑S = Pointer.terminal b

theorem OBdd.reduced_of_terminal {n m : ℕ} {O : OBdd n m} : O.isTerminal → O.Reduced

Terminal BDDs are reduced.

theorem OBdd.reduced_of_relevant {n m : ℕ} {O : OBdd n m} (S : (↑O).RelevantPointer) : O.Reduced → Reduced ⟨{ heap := (↑O).heap, root := ↑S }, ⋯⟩

Sub-BDDs of a reduced BDD are reduced.

theorem OBdd.reachable_of_edge {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {p q : Pointer n✝¹} : Edge w p q → Pointer.Reachable w p q

theorem OBdd.ordered_of_edge {n m : ℕ} {v : Vector (Node n m) m} {q : Pointer m} {O : OBdd n m} {h : (↑O).heap = v} {r : (↑O).root = q} (p : Pointer m) : Edge v q p → { heap := v, root := p }.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

@[simp]

theorem OBdd.evaluate_node {n m : ℕ} {v : Vector (Node n m) m} {I : Vector Bool n} {j : Fin m} {h : { heap := v, root := Pointer.node j }.Ordered} : evaluate ⟨{ heap := v, root := Pointer.node j }, h⟩ I = if I[v[j].var] = true then evaluate ⟨{ heap := v, root := v[j].high }, ⋯⟩ I else evaluate ⟨{ heap := v, root := v[j].low }, ⋯⟩ I

Spell out OBdd.evaluate for non-terminals.

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

@[simp]

theorem OBdd.evaluate_terminal {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {h : { heap := v, root := Pointer.terminal b }.Ordered} : evaluate ⟨{ heap := v, root := Pointer.terminal b }, h⟩ = Function.const (Vector Bool n) b

Spell out OBdd.evaluate for terminals.

theorem OBdd.evaluate_terminal' {b : Bool} {n m : ℕ} {O : OBdd n m} : (↑O).root = Pointer.terminal b → O.evaluate = Function.const (Vector Bool n) b

@[simp]

theorem OBdd.toTree_terminal {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {h : { heap := v, root := Pointer.terminal b }.Ordered} : toTree ⟨{ heap := v, root := Pointer.terminal b }, h⟩ = DecisionTree.leaf b

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

theorem OBdd.HSimilar_of_terminal {n m m' : ℕ} {b : Bool} {O : OBdd n m} {U : OBdd n m'} : (↑O).root = Pointer.terminal b → (↑U).root = Pointer.terminal b → O.HSimilar U

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

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

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

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

@[irreducible]

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

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

Equations

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

theorem OBdd.size_zero_of_terminal {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} : O.isTerminal → O.size' = 0

theorem OBdd.high_reduced {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).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).root = Pointer.node j} : O.Reduced → (O.low h).Reduced

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

theorem OBdd.evaluate_high_eq_evaluate_low_of_independentOf_root {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} : Nary.IndependentOf O.evaluate (↑O).heap[j].var → (O.high h).evaluate = (O.low h).evaluate

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

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

theorem OBdd.evaluate_high_eq_of_evaluate_eq_and_var_eq' {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} {i : Fin m'} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} : O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.high ho).evaluate = (U.high hu).evaluate

theorem OBdd.evaluate_high_eq_of_evaluate_eq_and_var_eq {n m : ℕ} {O U : OBdd n m} {j i : Fin m} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} : O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.high ho).evaluate = (U.high hu).evaluate

theorem OBdd.evaluate_low_eq_of_evaluate_eq_and_var_eq' {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} {i : Fin m'} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} : O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.low ho).evaluate = (U.low hu).evaluate

theorem OBdd.evaluate_low_eq_of_evaluate_eq_and_var_eq {n m : ℕ} {O U : OBdd n m} {j i : Fin m} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} : O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.low ho).evaluate = (U.low hu).evaluate

theorem OBdd.not_reduced_of_sim_high_low {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : (↑O).root = Pointer.node j) : (O.high h).Similar (O.low h) → ¬O.Reduced

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

Equations

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

def OBdd.Isomorphism {n m : ℕ} : OBdd n m → OBdd n m → Prop

Equations

• OBdd.Isomorphism = OBdd.HIsomorphism

def OBdd.RelevantIsomorphism {n m : ℕ} (O : OBdd n m) (p q : (↑O).RelevantPointer) : Prop

Equations

• O.RelevantIsomorphism p q = OBdd.Isomorphism ⟨{ heap := (↑O).heap, root := ↑p }, ⋯⟩ ⟨{ heap := (↑O).heap, root := ↑q }, ⋯⟩

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

Equations

• O.Reduced' = ((↑O).NoRedundancy ∧ Subrelation O.RelevantIsomorphism (InvImage Eq Subtype.val))

@[irreducible]

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.HSimilar U

Reduced OBDDs are canonical.

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

The only reduced BDD that denotes a constant function is the terminal BDD.

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

@[irreducible]

theorem OBdd.not_oedge_reachable {n m : ℕ} {O U : OBdd n m} : OEdge O U → ¬Pointer.Reachable (↑O).heap (↑U).root (↑O).root

An acyclicity lemma: an edge from O to U implies that O is not reachable from U.

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 : ℕ} {p : Pointer m} {O : OBdd n m} : Pointer.Reachable (↑O).heap (↑O).root p → (↑O).root = p ∨ ∃ (j : Fin m) (h : (↑O).root = Pointer.node j), Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem not_isTerminal_of_root_eq_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : ¬O.isTerminal

def OBdd.OReachable {n m : ℕ} (a : OBdd n m) : OBdd n m → Prop

Equations

• OBdd.OReachable = Relation.ReflTransGen OEdge

theorem OBdd.low_oreachable {n m : ℕ} {j : Fin m} {O U : OBdd n m} {U_root_def : (↑U).root = Pointer.node j} : O.OReachable U → O.OReachable (U.low U_root_def)

theorem OBdd.high_oreachable {n m : ℕ} {j : Fin m} {O U : OBdd n m} {U_root_def : (↑U).root = Pointer.node j} : O.OReachable U → O.OReachable (U.high U_root_def)

theorem OBdd.card_RelevantPointer_le {n m : ℕ} {O : OBdd n m} : Fintype.card (↑O).RelevantPointer ≤ m + 2

theorem OBdd.card_relevantPointer_eq_one_of_isTerminal {n m : ℕ} {O : OBdd n m} : O.isTerminal → Fintype.card (↑O).RelevantPointer = 1

theorem OBdd.reachable_node_iff {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : Pointer.Reachable (↑O).heap (↑O).root = fun (q : Pointer m) => Pointer.Reachable (↑O).heap (↑O).root q ∧ ¬Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∧ ¬Pointer.Reachable (↑O).heap (↑(O.high h)).root q ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∧ ¬Pointer.Reachable (↑O).heap (↑(O.high h)).root q ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root q ∧ ¬Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∧ Pointer.Reachable (↑O).heap (↑(O.high h)).root q

instance OBdd.instFintypeReachableFromNode {n m : ℕ} {j : Fin m} (O : OBdd n m) (h : (↑O).root = Pointer.node j) : Fintype { q : Pointer m // q = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root q }

Equations

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

theorem OBdd.reachable_from_node_iff' {n m : ℕ} {j : Fin m} {p : Pointer m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : Pointer.Reachable (↑O).heap (↑O).root p ↔ p = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem OBdd.card_reachable_node' {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : Fintype.card { p : Pointer m // Pointer.Reachable (↑O).heap (↑O).root p } = Fintype.card { p : Pointer m // p = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p }

theorem OBdd.eq_root_disjoint_reachable_low_or_high {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : Disjoint (fun (x : Pointer m) => x = (↑O).root) fun (p : Pointer m) => Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem OBdd.card_reachable_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) : Fintype.card { q : Pointer m // Pointer.Reachable (↑O).heap (↑O).root q } = 1 + Fintype.card { q : Pointer m // Pointer.Reachable (↑(O.low h)).heap (↑(O.low h)).root q ∨ Pointer.Reachable (↑(O.high h)).heap (↑(O.high h)).root q }

theorem Bdd.ordered_of_low_high_ordered {n m : ℕ} {j : Fin m} {B : Bdd n 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

@[irreducible]

theorem Bdd.ordered_of_ordered_heap_not_reachable_set {n m : ℕ} (O : OBdd n m) (i : Fin m) (N : Node n m) : ¬Pointer.Reachable (↑O).heap (↑O).root (Pointer.node i) → { heap := (↑O).heap.set (↑i) N ⋯, root := (↑O).root }.Ordered

theorem Pointer.mayPrecede_of_reachable {n m : ℕ} {p : Pointer m} {B : Bdd n m} : B.Ordered → Reachable B.heap B.root p → toVar B.heap B.root ≤ toVar B.heap p

theorem OBdd.reduced_var_dependent {n m : ℕ} {O : OBdd n m} {p : Fin n} : O.Reduced → (∀ (i : Fin ↑p), Nary.IndependentOf O.evaluate ⟨↑i, ⋯⟩) → ↑↑p ≤ (↑O).var

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 : ℕ} {j : Fin m} {i : Fin n} {B : Bdd n m} {h : B.root = Pointer.node j} : (B.high h).usesVar i → B.usesVar i

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

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

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

@[irreducible]

theorem OBdd.dependsOn_of_usesVar_of_reduced {n m : ℕ} {j : Fin m} {i : Fin n} {O : OBdd n m} : O.Reduced → Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → (↑O).heap[j].var = i → ∃ (v : Vector Bool n), O.evaluate v ≠ O.evaluate (v.set (↑i) true ⋯)

@[irreducible]

theorem OBdd.usesVar_of_dependsOn {n m : ℕ} {v : Vector Bool n} {b : Bool} {O : OBdd n m} {i : Fin n} : O.evaluate v ≠ O.evaluate (v.set (↑i) b ⋯) → (↑O).usesVar i

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

theorem OBdd.usesVar_iff {n m : ℕ} (i : Fin n) (O : OBdd n m) : (↑O).usesVar i ↔ ∃ (j : Fin m) (hj : (↑O).root = Pointer.node j), (↑O).heap[j].var = i ∨ (↑(O.low hj)).usesVar i ∨ (↑(O.high hj)).usesVar i

@[irreducible]

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

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

instance OBdd.instDecidableUsesVar {n m : ℕ} {O : OBdd n m} : DecidablePred (↑O).usesVar

Equations

• OBdd.instDecidableUsesVar i = id inferInstance

theorem Pointer.eq_terminal_of_reachable {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {p : Pointer n✝¹} : Reachable w (terminal b) p → p = terminal b

theorem Bdd.terminal_of_zero_vars {n m : ℕ} {B : Bdd n m} : n = 0 → ∃ (b : Bool), B.root = Pointer.terminal b

theorem Bdd.terminal_of_zero_heap {n m : ℕ} {B : Bdd n m} : m = 0 → ∃ (b : Bool), B.root = Pointer.terminal b

theorem Pointer.toVar_lt_of_trans_edge_of_ordered {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {x y : Pointer n✝¹} : { heap := M, root := x }.Ordered → Relation.TransGen (Edge M) x y → toVar M x < toVar M y