Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof state before:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : limplies (PosFin n) f (f.insert c)
⊢ limplies (PosFin n) f (f.insert c)

case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : limplies (PosFin n) f (f.insert c)
⊢ limplies (PosFin n) (f.insert c) f
Tactic:
. exact f_limplies_fc
Proof state after:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : limplies (PosFin n) f (f.insert c)
⊢ limplies (PosFin n) (f.insert c) f