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

Equations

• Lift.olift h O = ⟨Lift.lift✝ h ↑O, ⋯⟩

@[simp]

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

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