Theorem: AIG.unsat_relabel (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
⊢ idx < (relabel f aig).decls.size
Tactic:
simp[hidx]
State after:
no goals

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
⊢ aig.unsatAt idx hidx → (relabel f aig).unsatAt idx ⋯
Tactic:
intro h assign
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
h : aig.unsatAt idx hidx
assign : β → Bool
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
h : aig.unsatAt idx hidx
assign : β → Bool
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Tactic:
specialize h (assign ∘ f)
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign ∘ f⟧ = false
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign ∘ f⟧ = false
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Tactic:
simp [h]
State after:
no goals