Theorem: incrementalLRATCheckerSound (LeanSAT/LRAT/LRATCheckerSound.lean)

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
a : Action β α
aWellFormed : wellFormedAction a
⊢ ((incrementalLRATChecker f a).snd = success → unsatisfiable α f) ∧
    ((incrementalLRATChecker f a).snd = out_of_proof →
      unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f)
Tactic:
constructor
State after:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = success → unsatisfiable α f

case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f

State before:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = success → unsatisfiable α f

case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f
Tactic:
. intro incrementalChecker_success p pf
  unfold incrementalLRATChecker at incrementalChecker_success
  simp only at incrementalChecker_success
  split at incrementalChecker_success
  . next rupHints =>
    by_cases performRupAdd_success : (performRupAdd f empty rupHints).2
    . exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
    . simp only [performRupAdd_success, ite_false] at incrementalChecker_success
  . next c rupHints =>
    by_cases performRupAdd_success : (performRupAdd f c rupHints).2
    . simp only [performRupAdd_success, ite_true] at incrementalChecker_success
    . simp only [performRupAdd_success, ite_false] at incrementalChecker_success
  . next c pivot rupHints ratHints =>
    by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
    . simp only [performRatAdd_success, ite_true] at incrementalChecker_success
    . simp only [performRatAdd_success, ite_false] at incrementalChecker_success
  . simp only at incrementalChecker_success
State after:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f

State before:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f
Tactic:
. intro incrementalChecker_res incrementalChecker_res_unsat
  unfold incrementalLRATChecker at incrementalChecker_res
  simp only at incrementalChecker_res
  split at incrementalChecker_res
  . 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
  . 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
  . next c pivot rupHints ratHints =>
    by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
    . 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
    . simp only [Bool.not_eq_true] at performRatAdd_success
      simp only [performRatAdd_success, ite_false] at incrementalChecker_res
  . next ids =>
    unfold incrementalLRATChecker at incrementalChecker_res_unsat
    simp only at incrementalChecker_res_unsat
    intro p pf
    exact incrementalChecker_res_unsat p (limplies_delete p pf)
State after:
no goals

State before:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = success → unsatisfiable α f
Tactic:
intro incrementalChecker_success p pf
State after:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success : (incrementalLRATChecker f a).snd = success
p : α → Bool
pf : p ⊨ f
⊢ False

State before:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success : (incrementalLRATChecker f a).snd = success
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
unfold incrementalLRATChecker at incrementalChecker_success
State after:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success :
  (match a 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)).snd =
    success
p : α → Bool
pf : p ⊨ f
⊢ False

State before:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success :
  (match a 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)).snd =
    success
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
simp only at incrementalChecker_success
State after:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success :
  (match a with
      | Action.addEmpty id rupHints =>
        if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
        else ((performRupAdd f empty rupHints).fst, rup_failure)
      | Action.addRup id c rupHints =>
        if (performRupAdd f c rupHints).snd = true then ((performRupAdd f c rupHints).fst, out_of_proof)
        else ((performRupAdd f c rupHints).fst, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        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)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).snd =
    success
p : α → Bool
pf : p ⊨ f
⊢ False

State before:
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_success :
  (match a with
      | Action.addEmpty id rupHints =>
        if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
        else ((performRupAdd f empty rupHints).fst, rup_failure)
      | Action.addRup id c rupHints =>
        if (performRupAdd f c rupHints).snd = true then ((performRupAdd f c rupHints).fst, out_of_proof)
        else ((performRupAdd f c rupHints).fst, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        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)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).snd =
    success
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
split at incrementalChecker_success
State after:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints✝)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints✝).snd = true then ((performRupAdd f empty rupHints✝).fst, success)
      else ((performRupAdd f empty rupHints✝).fst, rup_failure)).snd =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints✝)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints✝).snd = true then ((performRupAdd f empty rupHints✝).fst, success)
      else ((performRupAdd f empty rupHints✝).fst, rup_failure)).snd =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False
Tactic:
. next rupHints =>
  by_cases performRupAdd_success : (performRupAdd f empty rupHints).2
  . exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
  . simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False
Tactic:
. next c rupHints =>
  by_cases performRupAdd_success : (performRupAdd f c rupHints).2
  . simp only [performRupAdd_success, ite_true] at incrementalChecker_success
  . simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False

State before:
case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False

case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False
Tactic:
. next c pivot rupHints ratHints =>
  by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
  . simp only [performRatAdd_success, ite_true] at incrementalChecker_success
  . simp only [performRatAdd_success, ite_false] at incrementalChecker_success
State after:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False
Tactic:
. simp only at incrementalChecker_success
State after:
no goals

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints✝)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints✝).snd = true then ((performRupAdd f empty rupHints✝).fst, success)
      else ((performRupAdd f empty rupHints✝).fst, rup_failure)).snd =
    success
⊢ False
Tactic:
next rupHints =>
by_cases performRupAdd_success : (performRupAdd f empty rupHints).2
. exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
. simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
⊢ False
Tactic:
by_cases performRupAdd_success : (performRupAdd f empty rupHints).2
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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : (performRupAdd f empty rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : ¬(performRupAdd f empty rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : (performRupAdd f empty rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : ¬(performRupAdd f empty rupHints).snd = true
⊢ False
Tactic:
. exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : ¬(performRupAdd f empty rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : ¬(performRupAdd f empty rupHints).snd = true
⊢ False
Tactic:
. simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : (performRupAdd f empty rupHints).snd = true
⊢ False
Tactic:
exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_success :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    success
performRupAdd_success : ¬(performRupAdd f empty rupHints).snd = true
⊢ False
Tactic:
simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (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 =
    success
⊢ False
Tactic:
next c rupHints =>
by_cases performRupAdd_success : (performRupAdd f c rupHints).2
. simp only [performRupAdd_success, ite_true] at incrementalChecker_success
. simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
⊢ False
Tactic:
by_cases performRupAdd_success : (performRupAdd f c rupHints).2
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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : (performRupAdd f c rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : (performRupAdd f c rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ False
Tactic:
. simp only [performRupAdd_success, ite_true] at incrementalChecker_success
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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ False
Tactic:
. simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : (performRupAdd f c rupHints).snd = true
⊢ False
Tactic:
simp only [performRupAdd_success, ite_true] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c : β
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c rupHints)
incrementalChecker_success :
  (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 =
    success
performRupAdd_success : ¬(performRupAdd f c rupHints).snd = true
⊢ False
Tactic:
simp only [performRupAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

State before:
case left.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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False
Tactic:
next c pivot rupHints ratHints =>
by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
. simp only [performRatAdd_success, ite_true] at incrementalChecker_success
. simp only [performRatAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
⊢ False
Tactic:
by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False
Tactic:
. simp only [performRatAdd_success, ite_true] at incrementalChecker_success
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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False
Tactic:
. simp only [performRatAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False
Tactic:
simp only [performRatAdd_success, ite_true] at incrementalChecker_success
State after:
no goals

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
p : α → Bool
pf : p ⊨ 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_success :
  (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 =
    success
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ False
Tactic:
simp only [performRatAdd_success, ite_false] at incrementalChecker_success
State after:
no goals

State before:
case left.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
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_success : (Formula.delete f ids✝, out_of_proof).snd = success
⊢ False
Tactic:
simp only at incrementalChecker_success
State after:
no goals

State before:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f
Tactic:
intro incrementalChecker_res incrementalChecker_res_unsat
State after:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res : (incrementalLRATChecker f a).snd = out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f

State before:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res : (incrementalLRATChecker f a).snd = out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f
Tactic:
unfold incrementalLRATChecker at incrementalChecker_res
State after:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res :
  (match a 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)).snd =
    out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f

State before:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res :
  (match a 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)).snd =
    out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f
Tactic:
simp only at incrementalChecker_res
State after:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res :
  (match a with
      | Action.addEmpty id rupHints =>
        if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
        else ((performRupAdd f empty rupHints).fst, rup_failure)
      | Action.addRup id c rupHints =>
        if (performRupAdd f c rupHints).snd = true then ((performRupAdd f c rupHints).fst, out_of_proof)
        else ((performRupAdd f c rupHints).fst, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        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)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).snd =
    out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f

State before:
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
incrementalChecker_res :
  (match a with
      | Action.addEmpty id rupHints =>
        if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
        else ((performRupAdd f empty rupHints).fst, rup_failure)
      | Action.addRup id c rupHints =>
        if (performRupAdd f c rupHints).snd = true then ((performRupAdd f c rupHints).fst, out_of_proof)
        else ((performRupAdd f c rupHints).fst, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        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)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).snd =
    out_of_proof
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f a).fst
⊢ unsatisfiable α f
Tactic:
split at incrementalChecker_res
State after:
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

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
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

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

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 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
State after:
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

State before:
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 c pivot rupHints ratHints =>
  by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
  . 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
  . simp only [Bool.not_eq_true] at performRatAdd_success
    simp only [performRatAdd_success, ite_false] at incrementalChecker_res
State after:
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

State before:
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 ids =>
  unfold incrementalLRATChecker at incrementalChecker_res_unsat
  simp only at incrementalChecker_res_unsat
  intro p pf
  exact incrementalChecker_res_unsat p (limplies_delete p pf)
State after:
no goals

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
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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
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

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
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

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 α
    (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
Tactic:
simp only [performRupAdd_success, ite_true] at incrementalChecker_res_unsat
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 :
  (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'
incrementalChecker_res_unsat : unsatisfiable α (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f

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 :
  (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'
incrementalChecker_res_unsat : unsatisfiable α (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f
Tactic:
rw [liff_unsat f f' f_liff_f']
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 :
  (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'
incrementalChecker_res_unsat : unsatisfiable α (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f'

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 :
  (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'
incrementalChecker_res_unsat : unsatisfiable α (performRupAdd f c rupHints).fst
⊢ unsatisfiable α f'
Tactic:
exact incrementalChecker_res_unsat
State after:
no goals

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
performRupAdd_success : (performRupAdd f c rupHints).snd = true
f' : σ := (performRupAdd f c rupHints).fst
⊢ performRupAdd f c rupHints = (f', true)
Tactic:
rw [← performRupAdd_success]
State after:
no goals

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
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 = false
⊢ unsatisfiable α f

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 = false
⊢ unsatisfiable α f
Tactic:
simp only [performRupAdd_success, ite_false] at incrementalChecker_res
State after:
no goals

State before:
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
Tactic:
next c pivot rupHints ratHints =>
by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
. 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
. simp only [Bool.not_eq_true] at performRatAdd_success
  simp only [performRatAdd_success, ite_false] at incrementalChecker_res
State after:
no goals

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 : β
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
Tactic:
by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
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 : β
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

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
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

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 : β
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:
. simp only [Bool.not_eq_true] at performRatAdd_success
  simp only [performRatAdd_success, ite_false] at incrementalChecker_res
State after:
no goals

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
Tactic:
let f' := (performRatAdd f c pivot rupHints ratHints).1
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 : β
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f

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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f
Tactic:
have heq : performRatAdd f c pivot rupHints ratHints = (f', true) := by rw [← performRatAdd_success]
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 : β
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
⊢ unsatisfiable α f

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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
⊢ unsatisfiable α f
Tactic:
simp only [wellFormedAction, limplies_iff_mem] at aWellFormed
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
⊢ unsatisfiable α f

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)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
⊢ unsatisfiable α f
Tactic:
unfold incrementalLRATChecker at incrementalChecker_res_unsat
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.addRat id✝ c pivot rupHints ratHints 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 (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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
⊢ unsatisfiable α f

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)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.addRat id✝ c pivot rupHints ratHints 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 (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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
⊢ unsatisfiable α f
Tactic:
simp only [performRatAdd_success, ite_true] at incrementalChecker_res_unsat
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f

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)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f
Tactic:
have h := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd aWellFormed heq
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : equisat α f f'
⊢ unsatisfiable α f

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)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : equisat α f f'
⊢ unsatisfiable α f
Tactic:
rw [equisat] at h
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f

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)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f
Tactic:
rw [h]
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 : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f'

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)
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f'
Tactic:
exact incrementalChecker_res_unsat
State after:
no goals

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 : β
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
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
⊢ performRatAdd f c pivot rupHints ratHints = (f', true)
Tactic:
rw [← performRatAdd_success]
State after:
no goals

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 : β
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:
simp only [Bool.not_eq_true] at performRatAdd_success
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 = false
⊢ unsatisfiable α f

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 : β
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 = false
⊢ unsatisfiable α f
Tactic:
simp only [performRatAdd_success, ite_false] at incrementalChecker_res
State after:
no goals

State before:
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 ids =>
unfold incrementalLRATChecker at incrementalChecker_res_unsat
simp only at incrementalChecker_res_unsat
intro p pf
exact incrementalChecker_res_unsat p (limplies_delete p pf)
State after:
no goals

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 β α
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:
unfold incrementalLRATChecker at incrementalChecker_res_unsat
State after:
α : 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 α
    (match Action.del ids 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 : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f

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 β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.del ids 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 : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
simp only at incrementalChecker_res_unsat
State after:
α : 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 α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f

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 β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
intro p pf
State after:
α : 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 α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
p : α → Bool
pf : p ⊨ f
⊢ False

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 β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
exact incrementalChecker_res_unsat p (limplies_delete p pf)
State after:
no goals