@[reducible, inline]

abbrev Apply.p2t : ℕ → ℕ → ℕ

Equations

• Apply.p2t l r = (l + 2) * (r + 2)

def Apply.apply {n m m' : ℕ} : (Bool → Bool → Bool) → OBdd n.succ m → OBdd n.succ m' → Bdd n.succ (p2t m m')

Equations

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

def Apply.apply' {n n' m m' p : ℕ} : max n n' = p.succ → (Bool → Bool → Bool) → OBdd n m → OBdd n' m' → OBdd (max n n') (p2t m m')

Equations

• Apply.apply' h op O U = ⟨⋯ ▸ Apply.apply op (h ▸ Lift.olift ⋯ O) (h ▸ Lift.olift ⋯ U), ⋯⟩

theorem Apply.apply_spec {n m m' : ℕ} {op : Bool → Bool → Bool} {O : OBdd n.succ m} {U : OBdd n.succ m'} : ∃ (o : (apply op O U).Ordered), ∀ (I : Vector Bool n.succ), op (O.evaluate I) (U.evaluate I) = OBdd.evaluate ⟨apply op O U, ⋯⟩ I

theorem Apply.apply'_spec {n n' m m' p : ℕ} {h : max n n' = p.succ} {op : Bool → Bool → Bool} {O : OBdd n m} {U : OBdd n' m'} (I : Vector Bool (max n n')) : op ((Lift.olift ⋯ O).evaluate I) ((Lift.olift ⋯ U).evaluate I) = (apply' h op O U).evaluate I