internlm/Lean-Github huggingface dataset:
Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.addRat id✝ c pivot rupHints ratHints with
      | Action.addEmpty id rupHints =>
        match performRupAdd f empty rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, success) else (f, rup_failure)
      | Action.addRup id c rupHints =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).fst
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
⊢ unsatisfiable α f
Tactic:
simp only [performRatAdd_success, ite_true] at incrementalChecker_res_unsat
Proof state after:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
⊢ unsatisfiable α f
Tactic:
have h := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd aWellFormed heq
Proof state after:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : equisat α f f'
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : equisat α f f'
⊢ unsatisfiable α f
Tactic:
rw [equisat] at h
Proof state after:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f
Tactic:
rw [h]
Proof state after:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f'
Theorem: incrementalLRATCheckerSound
Proof state before:
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
aWellFormed : pivot ∈ Clause.toList c
incrementalChecker_res_unsat : unsatisfiable α (performRatAdd f c pivot rupHints ratHints).fst
h : unsatisfiable α f ↔ unsatisfiable α f'
⊢ unsatisfiable α f'
Tactic:
exact incrementalChecker_res_unsat
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c pivot rupHints ratHints)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c pivot rupHints ratHints)).fst
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = true
f' : σ := (performRatAdd f c pivot rupHints ratHints).fst
⊢ performRatAdd f c pivot rupHints ratHints = (f', true)
Tactic:
rw [← performRatAdd_success]
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
case neg
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c pivot rupHints ratHints)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c pivot rupHints ratHints)).fst
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : ¬(performRatAdd f c pivot rupHints ratHints).snd = true
⊢ unsatisfiable α f
Tactic:
simp only [Bool.not_eq_true] at performRatAdd_success
Proof state after:
case neg
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c pivot rupHints ratHints)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c pivot rupHints ratHints)).fst
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = false
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
case neg
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
aWellFormed : wellFormedAction (Action.addRat id✝ c pivot rupHints ratHints)
incrementalChecker_res_unsat :
  unsatisfiable α (incrementalLRATChecker f (Action.addRat id✝ c pivot rupHints ratHints)).fst
incrementalChecker_res :
  (if (performRatAdd f c pivot rupHints ratHints).snd = true then
        ((performRatAdd f c pivot rupHints ratHints).fst, out_of_proof)
      else ((performRatAdd f c pivot rupHints ratHints).fst, rup_failure)).snd =
    out_of_proof
performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).snd = false
⊢ unsatisfiable α f
Tactic:
simp only [performRatAdd_success, ite_false] at incrementalChecker_res
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
case right.h_4
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids✝ : Array Nat
aWellFormed : wellFormedAction (Action.del ids✝)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.del ids✝)).fst
incrementalChecker_res : (Formula.delete f ids✝, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
next ids =>
unfold incrementalLRATChecker at incrementalChecker_res_unsat
simp only at incrementalChecker_res_unsat
intro p pf
exact incrementalChecker_res_unsat p (limplies_delete p pf)
Proof state after:
no goals
Theorem: incrementalLRATCheckerSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.del ids)).fst
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
unfold incrementalLRATChecker at incrementalChecker_res_unsat
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.del ids with
      | Action.addEmpty id rupHints =>
        match performRupAdd f empty rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, success) else (f, rup_failure)
      | Action.addRup id c rupHints =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).fst
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat :
  unsatisfiable α
    (match Action.del ids with
      | Action.addEmpty id rupHints =>
        match performRupAdd f empty rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, success) else (f, rup_failure)
      | Action.addRup id c rupHints =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.addRat id c pivot rupHints ratHints =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then (f, out_of_proof) else (f, rup_failure)
      | Action.del ids => (Formula.delete f ids, out_of_proof)).fst
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
simp only at incrementalChecker_res_unsat
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Theorem: incrementalLRATCheckerSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
⊢ unsatisfiable α f
Tactic:
intro p pf
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
p : α → Bool
pf : p ⊨ f
⊢ False
Theorem: incrementalLRATCheckerSound
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
ids : Array Nat
aWellFormed : wellFormedAction (Action.del ids)
incrementalChecker_res_unsat : unsatisfiable α (Formula.delete f ids)
incrementalChecker_res : (Formula.delete f ids, out_of_proof).snd = out_of_proof
p : α → Bool
pf : p ⊨ f
⊢ False
Tactic:
exact incrementalChecker_res_unsat p (limplies_delete p pf)
Proof state after:
no goals
Theorem: bitvec_AddSub_1564
Proof state before:
⊢ ∀ (x C : BitVec 64), C - (x ^^^ -1) = x + (C + 1)
Tactic:
intros
Proof state after:
x✝ C✝ : BitVec 64
⊢ C✝ - (x✝ ^^^ -1) = x✝ + (C✝ + 1)
Theorem: bitvec_AddSub_1564
Proof state before:
x✝ C✝ : BitVec 64
⊢ C✝ - (x✝ ^^^ -1) = x✝ + (C✝ + 1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1294_A__B__A__B___A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), (A ||| B) &&& (A ^^^ -1 ^^^ B) = A &&& B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ ||| B✝) &&& (A✝ ^^^ -1 ^^^ B✝) = A✝ &&& B✝
Theorem: bitvec_AndOrXor_1294_A__B__A__B___A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ||| B✝) &&& (A✝ ^^^ -1 ^^^ B✝) = A✝ &&& B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_887_2
Proof state before:
⊢ ∀ (a C1 : BitVec 64), (a == C1 && a != C1) = false
Tactic:
intros
Proof state after:
a✝ C1✝ : BitVec 64
⊢ (a✝ == C1✝ && a✝ != C1✝) = false
Theorem: bitvec_AndOrXor_887_2
Proof state before:
a✝ C1✝ : BitVec 64
⊢ (a✝ == C1✝ && a✝ != C1✝) = false
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2118___A__B__A___A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 = A ^^^ -1 ||| B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ -1 = A✝ ^^^ -1 ||| B✝
Theorem: bitvec_AndOrXor_2118___A__B__A___A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ -1 = A✝ ^^^ -1 ||| B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1152
Proof state before:
⊢ ∀ (y x : BitVec 1), x + y = x ^^^ y
Tactic:
intros
Proof state after:
y✝ x✝ : BitVec 1
⊢ x✝ + y✝ = x✝ ^^^ y✝
Theorem: bitvec_AddSub_1152
Proof state before:
y✝ x✝ : BitVec 1
⊢ x✝ + y✝ = x✝ ^^^ y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_val_eq_bitblast
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ (go aig expr).val = bitblast aig expr
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ start < (go aig expr).val.aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig expr).val.aig.decls.size

case m
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig expr).val.aig.decls.size

case m
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Tactic:
exact hstart
Proof state after:
case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case a
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
apply (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (go aig expr).val.aig, ref := { gate := start, hgate := ⋯ } }, assign.toAIGAssignment⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign.toAIGAssignment⟧
Tactic:
apply denote.eq_of_aig_eq (entry := ⟨aig, start,hstart⟩)
Proof state after:
case hprefix
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig expr).val.aig.decls