def Relabel.orelabel {n m : ℕ} (O : OBdd n m) {f : ℕ → ℕ} (hf : ∀ (i : Fin n), f ↑i < f n) (hu : ∀ (i i' : Fin n), i < i' → (↑O).usesVar i → (↑O).usesVar i' → f ↑i < f ↑i') : OBdd (f n) m

Equations

• Relabel.orelabel O hf hu = ⟨Relabel.relabel✝ hf ↑O, ⋯⟩

@[simp, irreducible]

theorem Relabel.orelabel_evaluate {n m : ℕ} (O : OBdd n m) {f : ℕ → ℕ} {hf : ∀ (i : Fin n), f ↑i < f n} {hu : ∀ (i i' : Fin n), i < i' → (↑O).usesVar i → (↑O).usesVar i' → f ↑i < f ↑i'} {I : Vector Bool (f n)} : (orelabel O hf hu).evaluate I = O.evaluate (Vector.ofFn fun (i : Fin n) => I[f ↑i])

theorem Relabel.orelabel_reduced {n m : ℕ} {O : OBdd n m} {f : ℕ → ℕ} {hf : ∀ (i : Fin n), f ↑i < f n} {hu : ∀ (i i' : Fin n), i < i' → (↑O).usesVar i → (↑O).usesVar i' → f ↑i < f ↑i'} : O.Reduced → (orelabel O hf hu).Reduced

@[simp]

theorem Relabel.orelabel_id {n m : ℕ} {O : OBdd n m} : orelabel O ⋯ ⋯ = O