internlm/Lean-Github huggingface dataset:
Theorem: incrementalLRATCheckerSound
Proof state before:
α : 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
Tactic:
by_cases h : (performRupAdd f empty rupHints).2
Proof state after:
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
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
h : (performRupAdd f empty rupHints).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
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
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
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
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
h : (performRupAdd f empty rupHints).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
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
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
. simp only [h, ite_true] at incrementalChecker_res
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
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
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
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
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
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
. simp only [Bool.not_eq_true] at h
  simp only [h, ite_false] at incrementalChecker_res
Proof state after:
no goals
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
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
h : (performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
simp only [h, ite_true] at incrementalChecker_res
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
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
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
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
simp only [Bool.not_eq_true] at h
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
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
h : (performRupAdd f empty rupHints).snd = false
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
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
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
h : (performRupAdd f empty rupHints).snd = false
⊢ unsatisfiable α f
Tactic:
simp only [h, ite_false] at incrementalChecker_res
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
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
Tactic:
next c rupHints =>
by_cases performRupAdd_success : (performRupAdd f c rupHints).2
. let f' := (performRupAdd f c rupHints).1
  have heq : performRupAdd f c rupHints = (f', true) := by rw [← performRupAdd_success]
  have f_liff_f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq
  unfold incrementalLRATChecker at incrementalChecker_res_unsat
  simp only [performRupAdd_success, ite_true] at incrementalChecker_res_unsat
  rw [liff_unsat f f' f_liff_f']
  exact incrementalChecker_res_unsat
. simp only [Bool.not_eq_true] at performRupAdd_success
  simp only [performRupAdd_success, ite_false] at incrementalChecker_res
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
α : 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
Tactic:
by_cases performRupAdd_success : (performRupAdd f c rupHints).2
Proof state after:
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).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 : β
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
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ unsatisfiable α f
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).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 : β
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
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
. let f' := (performRupAdd f c rupHints).1
  have heq : performRupAdd f c rupHints = (f', true) := by rw [← performRupAdd_success]
  have f_liff_f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq
  unfold incrementalLRATChecker at incrementalChecker_res_unsat
  simp only [performRupAdd_success, ite_true] at incrementalChecker_res_unsat
  rw [liff_unsat f f' f_liff_f']
  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 : β
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
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
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 : β
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
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
. simp only [Bool.not_eq_true] at performRupAdd_success
  simp only [performRupAdd_success, ite_false] at incrementalChecker_res
Proof state after:
no goals
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
let f' := (performRupAdd f c rupHints).1
Proof state after:
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f
Tactic:
have heq : performRupAdd f c rupHints = (f', true) := by rw [← performRupAdd_success]
Proof state after:
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
heq : performRupAdd f c rupHints = (f', true)
⊢ unsatisfiable α f
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
heq : performRupAdd f c rupHints = (f', true)
⊢ unsatisfiable α f
Tactic:
have f_liff_f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq
Proof state after:
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
heq : performRupAdd f c rupHints = (f', true)
f_liff_f' : liff α f f'
⊢ unsatisfiable α f
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 : β
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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
heq : performRupAdd f c rupHints = (f', true)
f_liff_f' : liff α f f'
⊢ unsatisfiable α f
Tactic:
unfold incrementalLRATChecker at incrementalChecker_res_unsat
Proof state after:
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 : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.addRup id✝ c rupHints with
      | Action.addEmpty id rupHints =>
        match performRupAdd f empty rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, success) else (f, rup_failure)
      | Action.addRup id c rupHints =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
heq : performRupAdd f c rupHints = (f', true)
f_liff_f' : liff α f f'
⊢ unsatisfiable α f