Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
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
ratAddSuccess :
  (if f.ratHintsExhaustive pivot ratHints = true then
      if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
            (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
          else
            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)
    else (f, false)) =
    (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
split at ratAddSuccess
Proof state after:
case isTrue
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
h✝ : f.ratHintsExhaustive pivot ratHints = true
ratAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          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'

case 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
h✝ : ¬f.ratHintsExhaustive pivot ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ equisat (PosFin n) f f'