@[implicit_reducible]

instance Reduce.instLinearOrderRawPointer : LinearOrder RawBdd.RawPointer

Equations

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

def Reduce.leKeyPair (a b : RawBdd.RawPointer × RawBdd.RawPointer) : Bool

Equations

• Reduce.leKeyPair a b = if a.1 = b.1 then decide (a.2 ≤ b.2) else decide (a.1 ≤ b.1)

def Reduce.KeyLE (a b : RawBdd.RawPointer × RawBdd.RawPointer) : Prop

Equations

• Reduce.KeyLE a b = (Reduce.leKeyPair a b = true)

theorem Reduce.keyLE_refl (a : RawBdd.RawPointer × RawBdd.RawPointer) : KeyLE a a

theorem Reduce.keyLE_antisymm {a b : RawBdd.RawPointer × RawBdd.RawPointer} : KeyLE a b → KeyLE b a → a = b

theorem Reduce.keyLE_trans {a b c : RawBdd.RawPointer × RawBdd.RawPointer} : KeyLE a b → KeyLE b c → KeyLE a c

theorem Reduce.keyLE_sorted_mergeSort {m : ℕ} (l : List ((RawBdd.RawPointer × RawBdd.RawPointer) × Fin m)) : List.Pairwise (fun (a b : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) => KeyLE a.1 b.1) (l.mergeSort fun (a b : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) => leKeyPair a.1 b.1)

structure Reduce.State (n m : ℕ) : Type

• size : ℕ
• heap : Vector (RawBdd.RawNode n) self.size
• ids : Vector (Option RawBdd.RawPointer) m

structure Reduce.ProvedState (n m : ℕ) : Type

• state : State n m
• hh (k : Fin self.state.size) : RawBdd.RawNode.Bounded (↑k) self.state.heap[k]

def Reduce.provedStateInitial (n m : ℕ) : ProvedState n m

Equations

• Reduce.provedStateInitial n m = { state := { size := 0, heap := Vector.emptyWithCapacity 0, ids := Vector.replicate m none }, hh := ⋯ }

def Reduce.get_id {n m : ℕ} (ps : ProvedState n m) (p : Pointer m) (h : ∀ (j : Fin m), p = Pointer.node j → ps.state.ids[j].isSome = true) : RawBdd.RawPointer

Equations

• Reduce.get_id ps (Pointer.terminal b) h_2 = Sum.inl b
• Reduce.get_id ps (Pointer.node j) h_2 = ps.state.ids[j].get ⋯

def Reduce.set_id {n m : ℕ} (ps : ProvedState n m) (j : Fin m) (p : RawBdd.RawPointer) : ProvedState n m

Record that input node j maps to output pointer p.

Equations

• Reduce.set_id ps j p = { state := { size := ps.state.size, heap := ps.state.heap, ids := ps.state.ids.set (↑j) (some p) ⋯ }, hh := ⋯ }

theorem Reduce.set_id_self {n m : ℕ} (ps : ProvedState n m) (j : Fin m) (p : RawBdd.RawPointer) : (set_id ps j p).state.ids[j] = some p

theorem Reduce.set_id_ne {n m : ℕ} (ps : ProvedState n m) (j k : Fin m) (p : RawBdd.RawPointer) (h : k ≠ j) : (set_id ps j p).state.ids[k] = ps.state.ids[k]

def Reduce.push_node {n m : ℕ} (ps : ProvedState n m) (N : RawBdd.RawNode n) (hN : RawBdd.RawNode.Bounded ps.state.size N) : ProvedState n m × RawBdd.RawPointer

Equations

• Reduce.push_node ps N hN = ({ state := { size := ps.state.size + 1, heap := ps.state.heap.push N, ids := ps.state.ids }, hh := ⋯ }, Sum.inr ps.state.size)

theorem Reduce.structural_canonical_reduced {n s : ℕ} {v : Vector (RawBdd.RawNode n) s} {hh : ∀ (k : Fin s), RawBdd.RawNode.Bounded (↑k) v[k]} (hsc : ∀ (k1 k2 : Fin s), v[k1] = v[k2] → k1 = k2) {root : Pointer s} (hord : { heap := RawBdd.cook_heap v hh, root := root }.Ordered) (hnored : { heap := RawBdd.cook_heap v hh, root := root }.NoRedundancy) : OBdd.Reduced ⟨{ heap := RawBdd.cook_heap v hh, root := root }, ⋯⟩

In a structurally canonical heap (no two positions have the same raw node), any ordered BDD is reduced.

def Reduce.Invariant {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (i : ℕ) : Prop

Equations

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

theorem Reduce.inv_initial {n m : ℕ} {O : OBdd n m} {i : ℕ} (hi : ∀ (j : Fin m), ↑(↑O).heap[j].var ≤ i) : Invariant O (provedStateInitial n m) i

theorem Reduce.Invariant.ids_isSome {n m : ℕ} {O : OBdd n m} {ps : ProvedState n m} {i : ℕ} (inv : Invariant O ps i) {j : Fin m} (hvar : i < ↑(↑O).heap[j].var) (hreach : Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j)) : ps.state.ids[j].isSome = true

def Reduce.VarInvariant {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) : Prop

When ids[j] = some (.inr k), the output node's var ≥ the input node's var.

Equations

• Reduce.VarInvariant O ps = ∀ (j : Fin m) (k : Fin ps.state.size), ps.state.ids[j] = some (Sum.inr ↑k) → ↑(↑O).heap[j].var ≤ ↑ps.state.heap[k].va

def Reduce.AllAbove {n m : ℕ} (ps : ProvedState n m) (i : ℕ) : Prop

Equations

• Reduce.AllAbove ps i = ∀ (k : Fin ps.state.size), i < ↑ps.state.heap[k].va

def Reduce.HeapInjective {m n : ℕ} (ps : ProvedState n m) : Prop

The heap is injective: no two positions have the same raw node.

Equations

• Reduce.HeapInjective ps = ∀ (k1 k2 : Fin ps.state.size), ps.state.heap[k1] = ps.state.heap[k2] → k1 = k2

theorem Reduce.varInvariant_initial {n m : ℕ} {O : OBdd n m} : VarInvariant O (provedStateInitial n m)

theorem Reduce.allAbove_initial {n m i : ℕ} : AllAbove (provedStateInitial n m) i

theorem Reduce.heapInjective_initial {n m : ℕ} : HeapInjective (provedStateInitial n m)

def Reduce.EntryCorrect {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (i : ℕ) (entry : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : Prop

Equations

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

@[reducible, inline]

abbrev Reduce.NodePushedCorrectly {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (entry : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) (hbound : RawBdd.RawPointer.Bounded ps.state.size entry.1.1 ∧ RawBdd.RawPointer.Bounded ps.state.size entry.1.2) : Prop

The BDD obtained by pushing a fresh node for entry is ordered, reduced, and evaluates like the original sub-BDD at entry.2.

Equations

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

@[reducible, inline]

abbrev Reduce.CurptrSemantic {n m : ℕ} (O : OBdd n m) (ps : ProvedState n m) (curptr : RawBdd.RawPointer) (entry : (RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) : Prop

The current pointer curptr correctly represents the sub-BDD at entry.2.

Equations

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