rw [performRatAdd] at ratAddSuccess
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
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'
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
ratAddSuccess :
  (if f.ratHintsExhaustive pivot ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck pivot.negateLiteral ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints 0 with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'