internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof 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'
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof 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'
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof 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'
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof 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'
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof state before:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : limplies (PosFin n) f (f.insert c)
⊢ limplies (PosFin n) f (f.insert c)
Tactic:
exact f_limplies_fc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.rupAdd_sound
Proof 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
Proof state after:
no goals
Theorem: bitvec_AndOrXor_698
Proof state before:
⊢ ∀ (a b d : BitVec 64), (a &&& b == 0 && a &&& d == 0) = (a &&& (b ||| d) == 0)
Tactic:
intros
Proof state after:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == 0 && a✝ &&& d✝ == 0) = (a✝ &&& (b✝ ||| d✝) == 0)
Theorem: bitvec_AndOrXor_698
Proof state before:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == 0 && a✝ &&& d✝ == 0) = (a✝ &&& (b✝ ||| d✝) == 0)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVBinOp.eval_and
Proof state before:
w : Nat
⊢ and.eval = fun x x_1 => x &&& x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: BVBinOp.eval_or
Proof state before:
w : Nat
⊢ or.eval = fun x x_1 => x ||| x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: BVBinOp.eval_xor
Proof state before:
w : Nat
⊢ xor.eval = fun x x_1 => x ^^^ x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: BVBinOp.eval_add
Proof state before:
w : Nat
⊢ add.eval = fun x x_1 => x + x_1
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_not
Proof state before:
w : Nat
⊢ not.eval = fun x => ~~~x
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_shiftLeftConst
Proof state before:
n w : Nat
⊢ (shiftLeftConst n).eval = fun x => x <<< n
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_shiftRightConst
Proof state before:
n w : Nat
⊢ (shiftRightConst n).eval = fun x => x >>> n
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_rotateLeft
Proof state before:
n w : Nat
⊢ (rotateLeft n).eval = fun x => x.rotateLeft n
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_rotateRight
Proof state before:
n w : Nat
⊢ (rotateRight n).eval = fun x => x.rotateRight n
Tactic:
rfl
Proof state after:
no goals
Theorem: BVUnOp.eval_arithShiftRightConst
Proof state before:
n w : Nat
⊢ (arithShiftRightConst n).eval = fun x => x.sshiftRight n
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_var
Proof state before:
assign : Assignment
w idx : Nat
⊢ eval assign (var idx) = BitVec.truncate w (assign.getD idx).bv
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_const
Proof state before:
assign : Assignment
w✝ : Nat
val : BitVec w✝
⊢ eval assign (const val) = val
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_zeroExtend
Proof state before:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_extract
Proof state before:
assign : Assignment
hi lo a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (extract hi lo expr) = BitVec.extractLsb hi lo (eval assign expr)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_bin
Proof state before:
assign : Assignment
a✝ : Nat
lhs : BVExpr a✝
op : BVBinOp
rhs : BVExpr a✝
⊢ eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_un
Proof state before:
assign : Assignment
op : BVUnOp
a✝ : Nat
operand : BVExpr a✝
⊢ eval assign (un op operand) = op.eval (eval assign operand)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.eval_append
Proof state before:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs
Tactic:
rfl
Proof state after:
no goals