unfold lratChecker
case intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
actionWellFormed : wellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → unsatisfiable α f
case intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
actionWellFormed : wellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
⊢ (match action :: restPrf with
      | [] => out_of_proof
      | Action.addEmpty id rupHints :: tail =>
        match performRupAdd f empty rupHints with
        | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure
      | Action.addRup id c rupHints :: restPrf =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf else rup_failure
      | Action.addRat id c pivot rupHints ratHints :: restPrf =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf else rup_failure
      | Action.del ids :: restPrf => lratChecker (Formula.delete f ids) restPrf) =
      success →
    unsatisfiable α f