Theorem: lratCheckerSound
Proof state before:
case intro.h_3
α : 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
prf✝ : List (Action β α)
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addRup id✝ c✝ rupHints✝ :: restPrf✝
⊢ (match performRupAdd f c✝ rupHints✝ with
      | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf✝ else rup_failure) =
      success →
    unsatisfiable α f

case intro.h_4
α : 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
prf✝ : List (Action β α)
id✝ : Nat
c✝ : β
pivot✝ : Literal α
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = 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) =
      success →
    unsatisfiable α f

case intro.h_5
α : 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
prf✝ : List (Action β α)
ids✝ : Array Nat
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.del ids✝ :: restPrf✝
⊢ lratChecker (Formula.delete f ids✝) restPrf✝ = success → unsatisfiable α f
Tactic:
. next id c rupHints restPrf' hprf =>
  split
  next f' checkSuccess heq =>
  split
  . next hCheckSuccess =>
    intro f'_success
    simp only [List.cons.injEq] at hprf
    rw [← hprf.2] at f'_success
    rw [hCheckSuccess] at heq
    exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success
  . simp only [false_implies]
Proof state after:
case intro.h_4
α : 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
prf✝ : List (Action β α)
id✝ : Nat
c✝ : β
pivot✝ : Literal α
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = 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) =
      success →
    unsatisfiable α f

case intro.h_5
α : 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
prf✝ : List (Action β α)
ids✝ : Array Nat
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.del ids✝ :: restPrf✝
⊢ lratChecker (Formula.delete f ids✝) restPrf✝ = success → unsatisfiable α f