Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert (LeanSAT/LRAT/Formula/RatAddSound.lean)

State before:
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 : pivot ∈ Clause.toList 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
⊢ equisat (PosFin n) f (f.insert c)
Tactic:
constructor
State after:
case mp
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 : pivot ∈ Clause.toList 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
⊢ unsatisfiable (PosFin n) f → unsatisfiable (PosFin n) (f.insert c)

case mpr
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 : pivot ∈ Clause.toList 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
⊢ unsatisfiable (PosFin n) (f.insert c) → unsatisfiable (PosFin n) f

State before:
case mp
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 : pivot ∈ Clause.toList 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
⊢ unsatisfiable (PosFin n) f → unsatisfiable (PosFin n) (f.insert c)
Tactic:
intro h p pfc
State after:
case mp
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 : pivot ∈ Clause.toList 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
h : unsatisfiable (PosFin n) f
p : PosFin n → Bool
pfc : p ⊨ f.insert c
⊢ False

State before:
case mp
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 : pivot ∈ Clause.toList 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
h : unsatisfiable (PosFin n) f
p : PosFin n → Bool
pfc : p ⊨ f.insert c
⊢ False
Tactic:
specialize h p
State after:
case mp
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 : pivot ∈ Clause.toList 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
pfc : p ⊨ f.insert c
h : ¬(p ⊨ f)
⊢ False

State before:
case mp
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 : pivot ∈ Clause.toList 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
h : ∃ x, x ∈ f.toList ∧ ¬((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
⊢ False
Tactic:
rcases h with ⟨c', c'_in_f, pc'⟩
State after:
case mp.intro.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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ False

State before:
case mp.intro.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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ False
Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by rw [insert_iff]; exact Or.inr c'_in_f
State after:
case mp.intro.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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
c'_in_fc : c' ∈ (f.insert c).toList
⊢ False

State before:
case mp.intro.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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
c'_in_fc : c' ∈ (f.insert c).toList
⊢ False
Tactic:
exact pc' $ pfc c' c'_in_fc
State after:
no goals

State before:
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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' ∈ (f.insert c).toList
Tactic:
rw [insert_iff]
State after:
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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' = c ∨ c' ∈ f.toList

State before:
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 : pivot ∈ Clause.toList 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
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ c' = c ∨ c' ∈ f.toList
Tactic:
exact Or.inr c'_in_f
State after:
no goals

State before:
case mpr
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 : pivot ∈ Clause.toList 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
⊢ unsatisfiable (PosFin n) (f.insert c) → unsatisfiable (PosFin n) f
Tactic:
intro fc_unsat p pf
State after:
case mpr
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
⊢ False

State before:
case mpr
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
⊢ False
Tactic:
by_cases pc : p ⊨ c
State after:
case pos
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
⊢ False

case neg
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
⊢ False

State before:
case pos
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
⊢ False
Tactic:
specialize fc_unsat p
State after:
case pos
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
fc_unsat : ¬(p ⊨ f.insert c)
⊢ False

State before:
case pos
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
fc_unsat : ∃ x, x ∈ (f.insert c).toList ∧ ¬decide (Clause.instHSat.1 p x) = true
⊢ False
Tactic:
rcases fc_unsat with ⟨c', c'_in_fc, pc'⟩
State after:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False

State before:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Tactic:
rw [insert_iff] at c'_in_fc
State after:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False

State before:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
pc' : ¬decide (Clause.instHSat.1 p c') = true
⊢ False
Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f
State after:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False

case pos.intro.intro.inr
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False

State before:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False

case pos.intro.intro.inr
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False
Tactic:
. simp only [c'_eq_c, decide_eq_true_eq] at pc'
  exact pc' pc
State after:
case pos.intro.intro.inr
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
⊢ False

State before:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_eq_c : c' = c
⊢ False
Tactic:
simp only [c'_eq_c, decide_eq_true_eq] at pc'
State after:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_eq_c : c' = c
pc' : ¬Clause.instHSat.1 p c
⊢ False

State before:
case pos.intro.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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
c'_eq_c : c' = c
pc' : ¬Clause.instHSat.1 p c
⊢ False
Tactic:
exact pc' pc
State after:
no goals

State before:
case pos.intro.intro.inr
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 : pivot ∈ Clause.toList 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
pc : p ⊨ c
c' : DefaultClause n
pc' : ¬decide (Clause.instHSat.1 p c') = true
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → decide (Clause.instHSat.1 p x) = true
⊢ False
Tactic:
exact pc' $ pf c' c'_in_f
State after:
no goals

State before:
case neg
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 : pivot ∈ Clause.toList 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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
⊢ False
Tactic:
rw [← Clause.limplies_iff_mem] at pivot_in_c
State after:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
⊢ False

State before:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
⊢ False
Tactic:
let p' : (PosFin n) → Bool := fun a => if a = pivot.1 then pivot.2 else p a
State after:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
⊢ False

State before:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
⊢ False
Tactic:
have p'_rw : p' = (fun a => if a = pivot.1 then pivot.2 else p a) := rfl
State after:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
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
⊢ False

State before:
case neg
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
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
⊢ False
Tactic:
specialize fc_unsat p'
State after:
case neg
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
pc : ¬(p ⊨ c)
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
fc_unsat : ¬(p' ⊨ f.insert c)
⊢ False

State before:
case neg
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
pc : ¬(p ⊨ c)
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
fc_unsat : ¬(p' ⊨ f.insert c)
⊢ False
Tactic:
simp only [← p'_rw, formulaHSat_def, List.all_eq_true, decide_eq_true_eq, Misc.not_forall, exists_prop] at fc_unsat
State after:
case neg
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
pc : ¬(p ⊨ c)
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
fc_unsat : ∃ x, x ∈ (f.insert c).toList ∧ ¬(p' ⊨ x)
⊢ False

State before:
case neg
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
pc : ¬(p ⊨ c)
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
fc_unsat : ∃ x, x ∈ (f.insert c).toList ∧ ¬(p' ⊨ x)
⊢ False
Tactic:
rcases fc_unsat with ⟨c', c'_in_fc, p'_not_entails_c'⟩
State after:
case neg.intro.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
pc : ¬(p ⊨ c)
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
c'_in_fc : c' ∈ (f.insert c).toList
p'_not_entails_c' : ¬(p' ⊨ c')
⊢ False

State before:
case neg.intro.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
pc : ¬(p ⊨ c)
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
c'_in_fc : c' ∈ (f.insert c).toList
p'_not_entails_c' : ¬(p' ⊨ c')
⊢ False
Tactic:
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton] at c'_in_fc
State after:
case neg.intro.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
pc : ¬(p ⊨ c)
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_fc : c' = c ∨ c' ∈ f.toList
⊢ False

State before:
case neg.intro.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
pc : ¬(p ⊨ c)
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_fc : c' = c ∨ c' ∈ f.toList
⊢ False
Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f
State after:
case neg.intro.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
pc : ¬(p ⊨ c)
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'_eq_c : c' = c
⊢ False

case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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
⊢ False

State before:
case neg.intro.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
pc : ¬(p ⊨ c)
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'_eq_c : c' = c
⊢ False

case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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
⊢ False
Tactic:
. rw [← c'_eq_c] at p'_entails_c
  exact p'_not_entails_c' p'_entails_c
State after:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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
⊢ False

State before:
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
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' ⊨ c
Tactic:
specialize pivot_in_c p'
State after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
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
pivot_in_c : p' ⊨ pivot → p' ⊨ c
⊢ p' ⊨ c

State before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
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
fc_unsat : unsatisfiable (PosFin n) (f.insert c)
p : PosFin n → Bool
pf : p ⊨ f
pc : ¬(p ⊨ c)
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
pivot_in_c : ((Clause.toList c).any fun l => decide ((if l.fst = pivot.fst then pivot.snd else p l.fst) = l.snd)) = true
⊢ p' ⊨ c
Tactic:
exact pivot_in_c
State after:
no goals

State before:
case neg.intro.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
pc : ¬(p ⊨ c)
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'_eq_c : c' = c
⊢ False
Tactic:
rw [← c'_eq_c] at p'_entails_c
State after:
case neg.intro.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
pc : ¬(p ⊨ c)
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
c' : DefaultClause n
p'_entails_c : p' ⊨ c'
p'_not_entails_c' : ¬(p' ⊨ c')
c'_eq_c : c' = c
⊢ False

State before:
case neg.intro.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
pc : ¬(p ⊨ c)
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
c' : DefaultClause n
p'_entails_c : p' ⊨ c'
p'_not_entails_c' : ¬(p' ⊨ c')
c'_eq_c : c' = c
⊢ False
Tactic:
exact p'_not_entails_c' p'_entails_c
State after:
no goals

State before:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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'
⊢ False
Tactic:
have negPivot_in_c' : negateLiteral pivot ∈ Clause.toList c' := mem_of_necessary_assignment pc' p'_not_entails_c'
State after:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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'
⊢ False

State before:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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'
h : p ⊨ c'.delete pivot.negateLiteral
⊢ False
Tactic:
have p'_entails_c'_del_negPivot : p' ⊨ c'.delete (negateLiteral pivot) := entails_of_irrelevant_assignment h
State after:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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'
h : p ⊨ c'.delete pivot.negateLiteral
p'_entails_c'_del_negPivot : p' ⊨ c'.delete pivot.negateLiteral
⊢ False

State before:
case neg.intro.intro.inr
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
pc : ¬(p ⊨ c)
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'
h : p ⊨ c'.delete pivot.negateLiteral
p'_entails_c'_del_negPivot : p' ⊨ c'.delete pivot.negateLiteral
⊢ False
Tactic:
exact p'_not_entails_c' $ Clause.entails_of_entails_delete p'_entails_c'_del_negPivot
State after:
no goals

State before:
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
pc : ¬(p ⊨ c)
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
pf : ∀ (x : DefaultClause n), x ∈ f.toList → decide (Clause.instHSat.1 p x) = true
⊢ p ⊨ c'
Tactic:
exact of_decide_eq_true $ pf c' c'_in_f
State after:
no goals

State before:
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
pc : ¬(p ⊨ c)
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'
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
rcases existsRatHint_of_ratHintsExhaustive f f_readyForRatAdd pivot ratHints
  ratHintsExhaustive_eq_true c' c'_in_f negPivot_in_c' with ⟨i, hc'⟩
State after:
case 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
pc : ¬(p ⊨ c)
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'
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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'
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
have h_performRupCheck_res :
  (performRupCheck (insertRupUnits f (negate c)).fst rupHints).fst.ratUnits = #[] ∧
  (performRupCheck (insertRupUnits f (negate c)).fst rupHints).fst.assignments.size = n := by
  simp only [performRupCheck_preserves_ratUnits, insertRupUnits_preserves_ratUnits, f_readyForRatAdd.1,
    performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1, and_self]
State after:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
have performRatCheck_success :=
  performRatCheck_success_of_performRatCheck_fold_success (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
    h_performRupCheck_res (negateLiteral pivot) ratHints i performRatCheck_fold_success
State after:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
have performRupCheck_res_satisfies_assignments_invariant :
  assignments_invariant (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1 := by
  apply performRupCheck_preserves_assignments_invariant (insertRupUnits f (negate c)).1
  apply insertRupUnits_preserves_assignments_invariant f f_readyForRatAdd.2
State after:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
have h :=
  performRatCheck_success_entails_c_without_negPivot (performRupCheck (insertRupUnits f (negate c)).fst rupHints).1
    ⟨h_performRupCheck_res.1, performRupCheck_res_satisfies_assignments_invariant⟩ (negateLiteral pivot) ratHints[i]
    performRatCheck_success
State after:
case 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
pc : ¬(p ⊨ c)
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.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.clauses[ratHints[i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.clauses[ratHints[i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
simp only [performRupCheck_preserves_clauses, insertRupUnits_preserves_clauses, Fin.getElem_fin] at h
State after:
case 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
pc : ¬(p ⊨ c)
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)
⊢ p ⊨ c'.delete pivot.negateLiteral

State before:
case 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
pc : ¬(p ⊨ c)
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)
⊢ p ⊨ c'.delete pivot.negateLiteral
Tactic:
apply h c' hc' p
State after:
case 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
pc : ¬(p ⊨ c)
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)
⊢ p ⊨ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst

State before:
case 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
pc : ¬(p ⊨ c)
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)
⊢ (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.toList.all fun s =>
      decide (((Clause.toList s).any fun l => decide (p l.fst = l.snd)) = true)) =
    true
Tactic:
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool,
  Bool.decide_coe, List.all_eq_true, decide_eq_true_eq]
State after:
case 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
pc : ¬(p ⊨ c)
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)
⊢ ∀ (x : DefaultClause n),
    x ∈ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.toList →
      ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true

State before:
case 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
pc : ¬(p ⊨ c)
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)
⊢ ∀ (x : DefaultClause n),
    x ∈ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.toList →
      ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
Tactic:
intro c'' hc''
State after:
case 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
pc : ¬(p ⊨ c)
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.performRupCheck rupHints).fst.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case 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
pc : ¬(p ⊨ c)
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.performRupCheck rupHints).fst.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
simp only [toList, performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits,
  performRupCheck_preserves_ratUnits] at hc''
State after:
case 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
pc : ¬(p ⊨ c)
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'' ∈
    List.filterMap id (f.insertRupUnits c.negate).fst.clauses.toList ++
        List.map unit (f.insertRupUnits c.negate).fst.rupUnits.toList ++
      List.map unit (f.insertRupUnits c.negate).fst.ratUnits.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case 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
pc : ¬(p ⊨ c)
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'' ∈
    List.filterMap id (f.insertRupUnits c.negate).fst.clauses.toList ++
        List.map unit (f.insertRupUnits c.negate).fst.rupUnits.toList ++
      List.map unit (f.insertRupUnits c.negate).fst.ratUnits.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
rw [← toList] at hc''
State after:
case 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
pc : ¬(p ⊨ c)
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
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case 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
pc : ¬(p ⊨ c)
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
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
have hc'' := mem_of_insertRupUnits f (negate c) c'' hc''
State after:
case 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
pc : ¬(p ⊨ c)
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
hc'' : c'' ∈ List.map Clause.unit c.negate ∨ c'' ∈ f.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case 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
pc : ¬(p ⊨ c)
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
hc'' : c'' ∈ List.map Clause.unit c.negate ∨ c'' ∈ f.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
rcases hc'' with c''_in_negc | c''_in_f
State after:
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
pc : ¬(p ⊨ c)
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
c''_in_negc : c'' ∈ List.map Clause.unit c.negate
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

case intro.inr
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
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
pc : ¬(p ⊨ c)
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'
⊢ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
Tactic:
simp only [performRupCheck_preserves_ratUnits, insertRupUnits_preserves_ratUnits, f_readyForRatAdd.1,
  performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1, and_self]
State after:
no goals

State before:
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
pc : ¬(p ⊨ c)
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
⊢ ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
Tactic:
apply performRupCheck_preserves_assignments_invariant (insertRupUnits f (negate c)).1
State after:
case f_assignments_invariant
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
pc : ¬(p ⊨ c)
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
⊢ (f.insertRupUnits c.negate).fst.assignments_invariant

State before:
case f_assignments_invariant
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
pc : ¬(p ⊨ c)
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
⊢ (f.insertRupUnits c.negate).fst.assignments_invariant
Tactic:
apply insertRupUnits_preserves_assignments_invariant f f_readyForRatAdd.2
State after:
no goals

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
pc : ¬((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true
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
c''_in_negc : c'' ∈ List.map Clause.unit c.negate
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool, not_exists,
  not_or, not_and, Clause.toList, DefaultClause.toList] at pc
State after:
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
c''_in_negc : c'' ∈ List.map Clause.unit c.negate
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

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
c''_in_negc : c'' ∈ List.map Clause.unit c.negate
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
simp only [negate, negateLiteral, List.map_map, List.mem_map, Function.comp_apply, Prod.exists,
  Bool.exists_bool, Bool.not_false, Bool.not_true] at c''_in_negc
State after:
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

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

State before:
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
Tactic:
apply Exists.intro l ∘ Or.inr
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''
⊢ (l, true) ∈ Clause.toList c'' ∧ p l = true

State before:
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''
⊢ p l = true
Tactic:
have h := (pc l).1 l_in_negc
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''
h : ¬p l = false
⊢ p l = true

State before:
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''
h : p l = true
⊢ p l = true
Tactic:
assumption
State after:
no goals

State before:
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
Tactic:
apply Exists.intro l ∘ Or.inl
State after:
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''
⊢ (l, false) ∈ Clause.toList c'' ∧ p l = false

State before:
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''
⊢ p l = false
Tactic:
have h := (pc l).2 l_in_negc
State after:
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''
h : ¬p l = true
⊢ p l = false

State before:
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''
h : p l = false
⊢ p l = false
Tactic:
assumption
State after:
no goals

State before:
case intro.inr
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 : (f.toList.all fun s => decide (((Clause.toList s).any fun l => decide (p l.fst = l.snd)) = true)) = true
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, List.all_eq_true] at pf
State after:
case intro.inr
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case intro.inr
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
simp only [Bool.decide_eq_false, Bool.not_eq_true'] at pf
State after:
case intro.inr
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true

State before:
case intro.inr
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c'' ∧ p a = false ∨ (a, true) ∈ Clause.toList c'' ∧ p a = true
Tactic:
apply pf
State after:
case intro.inr.a
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ c'' ∈ f.toList

State before:
case intro.inr.a
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
pc : ¬(p ⊨ c)
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
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ c'' ∈ f.toList
Tactic:
assumption
State after:
no goals