unfold incrementalLRATChecker at incrementalChecker_res_unsat
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
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