def Lift.lift {n n' m : ℕ} (h : n ≤ n') (B : Bdd n m) : Bdd n' m

Equations

• Lift.lift h B = { heap := Vector.map (fun (N : Node n m) => { var := ⟨↑N.var, ⋯⟩, low := N.low, high := N.high }) B.heap, root := B.root }

theorem Lift.lift_ordered {n n' m : ℕ} {h : n ≤ n'} {B : Bdd n m} : B.Ordered → (lift h B).Ordered

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_SimilarRP {n n' m : ℕ} {h : n ≤ n'} {O : OBdd n m} {p q : Pointer m} {hp : Pointer.Reachable (↑(olift h O)).heap (↑(olift h O)).root p} {hq : Pointer.Reachable (↑(olift h O)).heap (↑(olift h O)).root q} : (olift h O).SimilarRP ⟨p, hp⟩ ⟨q, hq⟩ → O.SimilarRP ⟨p, ⋯⟩ ⟨q, ⋯⟩

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