Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case intro.inl
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_rw : p' = fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negateLiteral ratHints[i]).snd =
    true
performRupCheck_res_satisfies_assignments_invariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
c'' : DefaultClause n
hc'' : c'' ∈ (f.insertRupUnits c.negate).fst.toList
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
c''_in_negc :
  ∃ a, (a, false) ∈ c.clause ∧ Clause.unit (a, true) = c'' ∨ (a, true) ∈ c.clause ∧ Clause.unit (a, false) = c''
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
rcases c''_in_negc with ⟨l, ⟨l_in_negc, l_def⟩ | ⟨l_in_negc, l_def⟩⟩
Proof state after:
case intro.inl.intro.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_rw : p' = fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negateLiteral ratHints[i]).snd =
    true
performRupCheck_res_satisfies_assignments_invariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
c'' : DefaultClause n
hc'' : c'' ∈ (f.insertRupUnits c.negate).fst.toList
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
l : PosFin n
l_in_negc : (l, false) ∈ c.clause
l_def : Clause.unit (l, true) = c''
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

case intro.inl.intro.inr.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_rw : p' = fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negateLiteral ratHints[i]).snd =
    true
performRupCheck_res_satisfies_assignments_invariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
c'' : DefaultClause n
hc'' : c'' ∈ (f.insertRupUnits c.negate).fst.toList
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
l : PosFin n
l_in_negc : (l, true) ∈ c.clause
l_def : Clause.unit (l, false) = c''
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true