Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : 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
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
⊢ unsatisfiable α f

case neg
α : 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
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ unsatisfiable α f
Tactic:
. let f' := (performRatAdd f c pivot rupHints ratHints).1
  have heq : performRatAdd f c pivot rupHints ratHints = (f', true) := by rw [← performRatAdd_success]
  simp only [wellFormedAction, limplies_iff_mem] at aWellFormed
  unfold incrementalLRATChecker at incrementalChecker_res_unsat
  simp only [performRatAdd_success, ite_true] at incrementalChecker_res_unsat
  have h := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd aWellFormed heq
  rw [equisat] at h
  rw [h]
  exact incrementalChecker_res_unsat
Proof state after:
case neg
α : 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
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ unsatisfiable α f