Theorem: lratCheckerSound (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
prf : List (Action β α)
prfWellFormed : ∀ (a : Action β α), a ∈ prf → wellFormedAction a
⊢ lratChecker f prf = success → unsatisfiable α f
Tactic:
induction prf generalizing f
State after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ lratChecker f [] = success → unsatisfiable α f

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f

State before:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ lratChecker f [] = success → unsatisfiable α f

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f
Tactic:
. unfold lratChecker
  simp only [false_implies]
State after:
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f

State before:
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f
Tactic:
. next action restPrf ih =>
  simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
  rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
  unfold lratChecker
  split
  . intro h
    exfalso
    simp only at h
  . next id rupHints restPrf' _ =>
    simp only [ite_eq_left_iff, Bool.not_eq_true]
    intro rupAddSuccess
    rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
    exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
  . 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]
  . next id c pivot rupHints ratHints 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
      simp only [wellFormedAction, hprf.1] at actionWellFormed
      exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
        restPrfWellFormed ih f'_success
    . simp only [false_implies]
  . next ids restPrf' hprf =>
    intro h
    simp only [List.cons.injEq] at hprf
    rw [← hprf.2] at h
    exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
State after:
no goals

State before:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ lratChecker f [] = success → unsatisfiable α f
Tactic:
unfold lratChecker
State after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ out_of_proof = success → unsatisfiable α f

State before:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ [] → wellFormedAction a
⊢ out_of_proof = success → unsatisfiable α f
Tactic:
simp only [false_implies]
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
head✝ : Action β α
tail✝ : List (Action β α)
tail_ih✝ :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ tail✝ → wellFormedAction a) → lratChecker f tail✝ = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
prfWellFormed : ∀ (a : Action β α), a ∈ head✝ :: tail✝ → wellFormedAction a
⊢ lratChecker f (head✝ :: tail✝) = success → unsatisfiable α f
Tactic:
next action restPrf ih =>
simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
unfold lratChecker
split
. intro h
  exfalso
  simp only at h
. next id rupHints restPrf' _ =>
  simp only [ite_eq_left_iff, Bool.not_eq_true]
  intro rupAddSuccess
  rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
  exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
. 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]
. next id c pivot rupHints ratHints 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
    simp only [wellFormedAction, hprf.1] at actionWellFormed
    exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
      restPrfWellFormed ih f'_success
  . simp only [false_implies]
. next ids restPrf' hprf =>
  intro h
  simp only [List.cons.injEq] at hprf
  rw [← hprf.2] at h
  exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
State after:
no goals

State before:
α : 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
prfWellFormed : ∀ (a : Action β α), a ∈ action :: restPrf → wellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → unsatisfiable α f
Tactic:
simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
State after:
α : 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
prfWellFormed : wellFormedAction action ∧ ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → unsatisfiable α f

State before:
α : 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
prfWellFormed : wellFormedAction action ∧ ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → unsatisfiable α f
Tactic:
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
State after:
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

State before:
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
Tactic:
unfold lratChecker
State after:
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

State before:
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
Tactic:
split
State after:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
⊢ out_of_proof = success → unsatisfiable α f

case intro.h_2
α : 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
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f

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

State before:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
⊢ out_of_proof = success → unsatisfiable α f

case intro.h_2
α : 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
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f

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:
. intro h
  exfalso
  simp only at h
State after:
case intro.h_2
α : 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
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f

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

State before:
case intro.h_2
α : 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
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f

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 rupHints restPrf' _ =>
  simp only [ite_eq_left_iff, Bool.not_eq_true]
  intro rupAddSuccess
  rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
  exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
State after:
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

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

State before:
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 pivot rupHints ratHints 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
    simp only [wellFormedAction, hprf.1] at actionWellFormed
    exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
      restPrfWellFormed ih f'_success
  . simp only [false_implies]
State after:
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

State before:
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 ids restPrf' hprf =>
  intro h
  simp only [List.cons.injEq] at hprf
  rw [← hprf.2] at h
  exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
State after:
no goals

State before:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
⊢ out_of_proof = success → unsatisfiable α f
Tactic:
intro h
State after:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
h : out_of_proof = success
⊢ unsatisfiable α f

State before:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
h : out_of_proof = success
⊢ unsatisfiable α f
Tactic:
exfalso
State after:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
h : out_of_proof = success
⊢ False

State before:
case intro.h_1
α : 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 β α)
heq✝ : action :: restPrf = []
h : out_of_proof = success
⊢ False
Tactic:
simp only at h
State after:
no goals

State before:
case intro.h_2
α : 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
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f
Tactic:
next id rupHints restPrf' _ =>
simp only [ite_eq_left_iff, Bool.not_eq_true]
intro rupAddSuccess
rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
State after:
no goals

State before:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
⊢ (match performRupAdd f empty rupHints with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f
Tactic:
simp only [ite_eq_left_iff, Bool.not_eq_true]
State after:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
⊢ ((performRupAdd f empty rupHints).snd = false → False) → unsatisfiable α f

State before:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
⊢ ((performRupAdd f empty rupHints).snd = false → False) → unsatisfiable α f
Tactic:
intro rupAddSuccess
State after:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
rupAddSuccess : (performRupAdd f empty rupHints).snd = false → False
⊢ unsatisfiable α f

State before:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
rupAddSuccess : (performRupAdd f empty rupHints).snd = false → False
⊢ unsatisfiable α f
Tactic:
rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
State after:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f

State before:
α : 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
rupHints : Array Nat
restPrf' : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id rupHints :: restPrf'
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f
Tactic:
exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
State after:
no goals

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

State before:
α : 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 β α)
hprf : 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
Tactic:
split
State after:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f✝ : σ
checkSuccess✝ : Bool
heq✝ : performRupAdd f c rupHints = (f✝, checkSuccess✝)
⊢ (if checkSuccess✝ = true then lratChecker f✝ restPrf' else rup_failure) = success → unsatisfiable α f

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f✝ : σ
checkSuccess✝ : Bool
heq✝ : performRupAdd f c rupHints = (f✝, checkSuccess✝)
⊢ (if checkSuccess✝ = true then lratChecker f✝ restPrf' else rup_failure) = success → unsatisfiable α f
Tactic:
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]
State after:
no goals

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
⊢ (if checkSuccess = true then lratChecker f' restPrf' else rup_failure) = success → unsatisfiable α f
Tactic:
split
State after:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f

case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f

State before:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f

case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
. 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
State after:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f

State before:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
. simp only [false_implies]
State after:
no goals

State before:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f
Tactic:
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
State after:
no goals

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f
Tactic:
intro f'_success
State after:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
⊢ unsatisfiable α f

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
⊢ unsatisfiable α f
Tactic:
simp only [List.cons.injEq] at hprf
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
rw [← hprf.2] at f'_success
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
rw [hCheckSuccess] at heq
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRup id c rupHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success
State after:
no goals

State before:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRup id c rupHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRupAdd f c rupHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
simp only [false_implies]
State after:
no goals

State before:
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
Tactic:
next id c pivot rupHints ratHints 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
  simp only [wellFormedAction, hprf.1] at actionWellFormed
  exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
    restPrfWellFormed ih f'_success
. simp only [false_implies]
State after:
no goals

State before:
α : 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 β α)
hprf : 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
Tactic:
split
State after:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f✝ : σ
checkSuccess✝ : Bool
heq✝ : performRatAdd f c pivot rupHints ratHints = (f✝, checkSuccess✝)
⊢ (if checkSuccess✝ = true then lratChecker f✝ restPrf' else rup_failure) = success → unsatisfiable α f

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f✝ : σ
checkSuccess✝ : Bool
heq✝ : performRatAdd f c pivot rupHints ratHints = (f✝, checkSuccess✝)
⊢ (if checkSuccess✝ = true then lratChecker f✝ restPrf' else rup_failure) = success → unsatisfiable α f
Tactic:
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
  simp only [wellFormedAction, hprf.1] at actionWellFormed
  exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
    restPrfWellFormed ih f'_success
. simp only [false_implies]
State after:
no goals

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
⊢ (if checkSuccess = true then lratChecker f' restPrf' else rup_failure) = success → unsatisfiable α f
Tactic:
split
State after:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f

case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f

State before:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f

case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
. next hCheckSuccess =>
  intro f'_success
  simp only [List.cons.injEq] at hprf
  rw [← hprf.2] at f'_success
  rw [hCheckSuccess] at heq
  simp only [wellFormedAction, hprf.1] at actionWellFormed
  exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
    restPrfWellFormed ih f'_success
State after:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f

State before:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
. simp only [false_implies]
State after:
no goals

State before:
case isTrue
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f
Tactic:
next hCheckSuccess =>
intro f'_success
simp only [List.cons.injEq] at hprf
rw [← hprf.2] at f'_success
rw [hCheckSuccess] at heq
simp only [wellFormedAction, hprf.1] at actionWellFormed
exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
  restPrfWellFormed ih f'_success
State after:
no goals

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
⊢ lratChecker f' restPrf' = success → unsatisfiable α f
Tactic:
intro f'_success
State after:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
⊢ unsatisfiable α f

State before:
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
⊢ unsatisfiable α f
Tactic:
simp only [List.cons.injEq] at hprf
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
rw [← hprf.2] at f'_success
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
rw [hCheckSuccess] at heq
State after:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
simp only [wellFormedAction, hprf.1] at actionWellFormed
State after:
α : 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
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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
actionWellFormed : limplies α pivot c
⊢ unsatisfiable α f

State before:
α : 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
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 β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
actionWellFormed : limplies α pivot c
⊢ unsatisfiable α f
Tactic:
exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
  restPrfWellFormed ih f'_success
State after:
no goals

State before:
case isFalse
α : 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 β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
h✝ : ¬checkSuccess = true
⊢ False → unsatisfiable α f
Tactic:
simp only [false_implies]
State after:
no goals

State before:
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 ids restPrf' hprf =>
intro h
simp only [List.cons.injEq] at hprf
rw [← hprf.2] at h
exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
State after:
no goals

State before:
α : 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 β α)
hprf : action :: restPrf = Action.del ids :: restPrf'
⊢ lratChecker (Formula.delete f ids) restPrf' = success → unsatisfiable α f
Tactic:
intro h
State after:
α : 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 β α)
hprf : action :: restPrf = Action.del ids :: restPrf'
h : lratChecker (Formula.delete f ids) restPrf' = success
⊢ unsatisfiable α f

State before:
α : 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 β α)
hprf : action :: restPrf = Action.del ids :: restPrf'
h : lratChecker (Formula.delete f ids) restPrf' = success
⊢ unsatisfiable α f
Tactic:
simp only [List.cons.injEq] at hprf
State after:
α : 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 β α)
h : lratChecker (Formula.delete f ids) restPrf' = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
h : lratChecker (Formula.delete f ids) restPrf' = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
rw [← hprf.2] at h
State after:
α : 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 β α)
h : lratChecker (Formula.delete f ids) restPrf = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ unsatisfiable α f

State before:
α : 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 β α)
h : lratChecker (Formula.delete f ids) restPrf = success
hprf : action = Action.del ids ∧ restPrf = restPrf'
⊢ unsatisfiable α f
Tactic:
exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
State after:
no goals