Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  (if
        (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 =
          false then
      ((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).fst,
        false)
    else
      ({
                clauses :=
                  (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).1.clauses,
                rupUnits :=
                  (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).1.rupUnits,
                ratUnits :=
                  (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).1.ratUnits,
                assignments :=
                  restoreAssignments
                    (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).1.assignments
                    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
          c,
        true)) =
    (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
. split at ratAddSuccess
  . simp at ratAddSuccess
  . next performRatCheck_fold_success =>
    simp only [Bool.not_eq_false] at performRatCheck_fold_success
    rw [f'_def]
    exact performRatCheck_fold_success_entails_safe_insert f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
      ratHintsExhaustive_eq_true performRatCheck_fold_success
Proof state after:
no goals