Theorem: LRAT.DefaultFormula.rupAdd_result (LeanSAT/LRAT/Formula/RupAddResult.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)
⊢ f' = f.insert c
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' = f.insert c

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' = f.insert c
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
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)
⊢ f' = f.insert c

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
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
h✝ : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ f' = f.insert c

case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

State before:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
h✝ : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ f' = f.insert c

case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
Tactic:
. simp only [clear_insertRup f f_readyForRupAdd (negate c), Prod.mk.injEq, and_true] at rupAddSuccess
  exact rupAddSuccess.symm
State after:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

State before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
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
    . let fc := (insertRupUnits f (negate c)).1
      have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
        rw [insertRupUnits_preserves_assignments_size f (negate c)]
        exact f_readyForRupAdd.2.1
      simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
        restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
      have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
        rw [rupAddSuccess]
      rw [clear_insertRup f f_readyForRupAdd (negate c)] at rupAddSuccess
      exact rupAddSuccess.symm
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
h✝ : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
⊢ f' = f.insert c
Tactic:
simp only [clear_insertRup f f_readyForRupAdd (negate c), Prod.mk.injEq, and_true] at rupAddSuccess
State after:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
h✝ : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : f.insert c = f'
⊢ f' = f.insert c

State before:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
h✝ : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : f.insert c = f'
⊢ f' = f.insert c
Tactic:
exact rupAddSuccess.symm
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
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c

case isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

State before:
case isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

case isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c

State before:
case isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
Tactic:
. split at rupAddSuccess
  . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
  . let fc := (insertRupUnits f (negate c)).1
    have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
      rw [insertRupUnits_preserves_assignments_size f (negate c)]
      exact f_readyForRupAdd.2.1
    simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
      restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
    have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
      rw [rupAddSuccess]
    rw [clear_insertRup f f_readyForRupAdd (negate c)] at rupAddSuccess
    exact rupAddSuccess.symm
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
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c

case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c

case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
⊢ f' = f.insert c
Tactic:
. let fc := (insertRupUnits f (negate c)).1
  have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
    rw [insertRupUnits_preserves_assignments_size f (negate c)]
    exact f_readyForRupAdd.2.1
  simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
    restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
  have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
    rw [rupAddSuccess]
  rw [clear_insertRup f f_readyForRupAdd (negate c)] at rupAddSuccess
  exact rupAddSuccess.symm
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
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)
⊢ f' = f.insert c
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
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)
⊢ f' = f.insert c
Tactic:
let fc := (insertRupUnits f (negate c)).1
State after:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f' = f.insert c
Tactic:
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
  rw [insertRupUnits_preserves_assignments_size f (negate c)]
  exact f_readyForRupAdd.2.1
State after:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ f' = f.insert c
Tactic:
simp only [performRupCheck_preserves_clauses, performRupCheck_preserves_rupUnits, performRupCheck_preserves_ratUnits,
  restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] 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
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c
Tactic:
have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
  rw [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
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'
⊢ f' = f.insert c
Tactic:
rw [clear_insertRup f f_readyForRupAdd (negate c)] 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
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : f.insert c = f'
⊢ f' = f.insert c

State before:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : f.insert c = f'
⊢ f' = f.insert c
Tactic:
exact rupAddSuccess.symm
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ (f.insertRupUnits c.negate).fst.assignments.size = n
Tactic:
rw [insertRupUnits_preserves_assignments_size f (negate c)]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n
Tactic:
exact f_readyForRupAdd.2.1
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
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
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
⊢ (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'
Tactic:
rw [rupAddSuccess]
State after:
no goals