def Lift.olift {n n' m : ℕ} (h : n ≤ n') (O : OBdd n m) : OBdd n' m

Equations

• Lift.olift h O = { bdd := Lift.lift✝ h O.bdd, ordered := ⋯ }

@[simp]

theorem Lift.olift_trivial_eq {n n' m : ℕ} {h : n = n'} {O : OBdd n m} : olift ⋯ O = h ▸ O

@[simp]

theorem Lift.olift_preserves_root {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} : (olift h O).bdd.root = O.bdd.root

theorem Lift.olift_low {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} {j : Fin m} (hr : O.bdd.root = Pointer.node j) : (olift h O).low ⋯ = olift h (O.low hr)

theorem Lift.olift_high {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} {j : Fin m} (hr : O.bdd.root = Pointer.node j) : (olift h O).high ⋯ = olift h (O.high hr)

@[simp]

theorem Lift.olift_evaluate {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} {I : Vector Bool n'} : (olift h O).evaluate I = O.evaluate (Vector.cast ⋯ (I.take n))

theorem Lift.olift_reduced {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} : O.Reduced → (olift h O).Reduced

@[simp]

theorem Lift.olift_olift {n n' n'' m : ℕ} {h1 : n ≤ n'} {h2 : n' ≤ n''} {O : OBdd n m} : olift h2 (olift h1 O) = olift ⋯ O