Theorem: incrementalLRATCheckerSound
Proof state before:
case right.h_1
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addEmpty id✝ rupHints✝)).fst
incrementalChecker_res :
  (if (performRupAdd f empty rupHints✝).snd = true then ((performRupAdd f empty rupHints✝).fst, success)
      else ((performRupAdd f empty rupHints✝).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f

case right.h_2
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addRup id✝ c✝ rupHints✝)).fst
incrementalChecker_res :
  (if (performRupAdd f c✝ rupHints✝).snd = true then ((performRupAdd f c✝ rupHints✝).fst, out_of_proof)
      else ((performRupAdd f c✝ rupHints✝).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f

case right.h_3
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c✝ : β
pivot✝ : Literal α
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)).fst
incrementalChecker_res :
  (if (performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).snd = true then
        ((performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).fst, out_of_proof)
      else ((performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f

case right.h_4
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.del ids✝)).fst
incrementalChecker_res : (Formula.delete f ids✝, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
. next rupHints =>
  by_cases h : (performRupAdd f empty rupHints).2
  . simp only [h, ite_true] at incrementalChecker_res
  . simp only [Bool.not_eq_true] at h
    simp only [h, ite_false] at incrementalChecker_res
Proof state after:
case right.h_2
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addRup id✝ c✝ rupHints✝)).fst
incrementalChecker_res :
  (if (performRupAdd f c✝ rupHints✝).snd = true then ((performRupAdd f c✝ rupHints✝).fst, out_of_proof)
      else ((performRupAdd f c✝ rupHints✝).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f

case right.h_3
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c✝ : β
pivot✝ : Literal α
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)).fst
incrementalChecker_res :
  (if (performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).snd = true then
        ((performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).fst, out_of_proof)
      else ((performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f

case right.h_4
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.del ids✝)).fst
incrementalChecker_res : (Formula.delete f ids✝, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f