Theorem: LRAT.DefaultFormula.rupAdd_sound (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd rupAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'
Tactic:
rw [performRupAdd] at rupAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess :
  (let negC := c.negate;
    match f.insertRupUnits negC with
    | (f, foundContradiction) =>
      if foundContradiction = true then
        let f := f.clearRupUnits;
        (f.insert c, true)
      else
        match f.performRupCheck rupHints with
        | (f, derivedLits, derivedEmpty, encounteredError) =>
          if encounteredError = true then (f, false)
          else
            if (!derivedEmpty) = 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)) =
    (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess :
  (let negC := c.negate;
    match f.insertRupUnits negC with
    | (f, foundContradiction) =>
      if foundContradiction = true then
        let f := f.clearRupUnits;
        (f.insert c, true)
      else
        match f.performRupCheck rupHints with
        | (f, derivedLits, derivedEmpty, encounteredError) =>
          if encounteredError = true then (f, false)
          else
            if (!derivedEmpty) = 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)) =
    (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'
Tactic:
simp only [Bool.not_eq_true'] at rupAddSuccess
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
rupAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true)
    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 = false then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          ({ 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)
⊢ liff (PosFin n) f f'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
rupAddSuccess :
  (if (f.insertRupUnits c.negate).snd = true then ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true)
    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 = false then
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
        else
          ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
split at rupAddSuccess
State after:
case isTrue
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
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse
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
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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)
⊢ liff (PosFin n) f f'

State before:
case isTrue
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
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse
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
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
. next insertRupContradiction =>
  intro p
  have f_limplies_fc := insertRup_entails_safe_insert f f_readyForRupAdd c insertRupContradiction p
  rw [f'_def]
  constructor
  . exact f_limplies_fc
  . exact limplies_of_insert f c p
State after:
case isFalse
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
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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)
⊢ liff (PosFin n) f f'

State before:
case isFalse
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
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
. split at rupAddSuccess
  . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
  . split at rupAddSuccess
    . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
    . next performRupCheck_success =>
      rw [Bool.not_eq_false] at performRupCheck_success
      have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
      rw [liff_iff_limplies_and_limplies f f', f'_def]
      constructor
      . exact f_limplies_fc
      . exact limplies_of_insert f c
State after:
no goals

State before:
case isTrue
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
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
next insertRupContradiction =>
intro p
have f_limplies_fc := insertRup_entails_safe_insert f f_readyForRupAdd c insertRupContradiction p
rw [f'_def]
constructor
. exact f_limplies_fc
. exact limplies_of_insert f c p
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
intro p
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
⊢ p ⊨ f ↔ p ⊨ f'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
⊢ p ⊨ f ↔ p ⊨ f'
Tactic:
have f_limplies_fc := insertRup_entails_safe_insert f f_readyForRupAdd c insertRupContradiction p
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f'
Tactic:
rw [f'_def]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f.insert c
Tactic:
constructor
State after:
case mp
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f → p ⊨ f.insert c

case mpr
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f.insert c → p ⊨ f

State before:
case mp
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f → p ⊨ f.insert c

case mpr
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f.insert c → p ⊨ f
Tactic:
. exact f_limplies_fc
State after:
case mpr
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f.insert c → p ⊨ f

State before:
case mpr
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f.insert c → p ⊨ f
Tactic:
. exact limplies_of_insert f c p
State after:
no goals

State before:
case mp
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f → p ⊨ f.insert c
Tactic:
exact f_limplies_fc
State after:
no goals

State before:
case mpr
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f.insert c → p ⊨ f
Tactic:
exact limplies_of_insert f c p
State after:
no goals

State before:
case isFalse
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
rupAddSuccess :
  (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 = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
split at rupAddSuccess
State after:
case isFalse.isTrue
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
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse.isFalse
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ 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)
⊢ liff (PosFin n) f f'

State before:
case isFalse.isTrue
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
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse.isFalse
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
. simp only [Prod.mk.injEq, and_false] at rupAddSuccess
State after:
case isFalse.isFalse
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ 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)
⊢ liff (PosFin n) f f'

State before:
case isFalse.isFalse
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
. split at rupAddSuccess
  . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
  . next performRupCheck_success =>
    rw [Bool.not_eq_false] at performRupCheck_success
    have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
    rw [liff_iff_limplies_and_limplies f f', f'_def]
    constructor
    . exact f_limplies_fc
    . exact limplies_of_insert f c
State after:
no goals

State before:
case isFalse.isTrue
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
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
simp only [Prod.mk.injEq, and_false] at rupAddSuccess
State after:
no goals

State before:
case isFalse.isFalse
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      ({ 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)
⊢ liff (PosFin n) f f'
Tactic:
split at rupAddSuccess
State after:
case isFalse.isFalse.isTrue
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
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse.isFalse.isFalse
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
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
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)
⊢ liff (PosFin n) f f'

State before:
case isFalse.isFalse.isTrue
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
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'

case isFalse.isFalse.isFalse
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
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
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)
⊢ liff (PosFin n) f f'
Tactic:
. simp only [Prod.mk.injEq, and_false] at rupAddSuccess
State after:
case isFalse.isFalse.isFalse
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
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
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)
⊢ liff (PosFin n) f f'

State before:
case isFalse.isFalse.isFalse
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
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
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)
⊢ liff (PosFin n) f f'
Tactic:
. next performRupCheck_success =>
  rw [Bool.not_eq_false] at performRupCheck_success
  have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
  rw [liff_iff_limplies_and_limplies f f', f'_def]
  constructor
  . exact f_limplies_fc
  . exact limplies_of_insert f c
State after:
no goals

State before:
case isFalse.isFalse.isTrue
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
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ liff (PosFin n) f f'
Tactic:
simp only [Prod.mk.injEq, and_false] at rupAddSuccess
State after:
no goals

State before:
case isFalse.isFalse.isFalse
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
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
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)
⊢ liff (PosFin n) f f'
Tactic:
next performRupCheck_success =>
rw [Bool.not_eq_false] at performRupCheck_success
have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
rw [liff_iff_limplies_and_limplies f f', f'_def]
constructor
. exact f_limplies_fc
. exact limplies_of_insert f c
State after:
no goals

State before:
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 = false
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)
⊢ liff (PosFin n) f f'
Tactic:
rw [Bool.not_eq_false] at performRupCheck_success
State after:
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)
⊢ liff (PosFin n) f f'

State before:
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)
⊢ liff (PosFin n) f f'
Tactic:
have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
State after:
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)
⊢ liff (PosFin n) f f'

State before:
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)
⊢ liff (PosFin n) f f'
Tactic:
rw [liff_iff_limplies_and_limplies f f', f'_def]
State after:
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) ∧ limplies (PosFin n) (f.insert c) f

State before:
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) ∧ limplies (PosFin n) (f.insert c) f
Tactic:
constructor
State after:
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

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
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

State before:
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 limplies_of_insert f c
State after:
no goals

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)
Tactic:
exact f_limplies_fc
State after:
no goals

State before:
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 limplies_of_insert f c
State after:
no goals