Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p 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
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
ratAddSuccess :
  {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.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 p.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 p.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 p.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 =
    f'
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.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 p.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 p.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 p.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 =
    f.insert c
Tactic:
clear f' ratAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p 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
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ {
            clauses :=
              (Array.foldl
                    (fun x ratHint =>
                      if x.snd = true then x.fst.performRatCheck p.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 p.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 p.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 p.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 =
    f.insert c