internlm/Lean-Github huggingface dataset:
Theorem: AIG.LawfulStreamOperator.lt_size_of_lt_aig_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < (f aig input).aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ Nat
Theorem: AIG.LawfulStreamOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ Nat
Tactic:
. exact h
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ x < ?m
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ (f aig input).aig.decls.size
Tactic:
apply Nat.le_trans
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ Nat
Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ Nat
Tactic:
. exact h
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.denote_input_entry
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }, assign⟧ = ⟦entry, assign⟧
Tactic:
apply denote.eq_of_aig_eq
Proof state after:
case hprefix
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls
Theorem: AIG.LawfulStreamOperator.denote_input_entry
Proof state before:
case hprefix
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls
Tactic:
apply IsPrefix_aig
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.denote_cast_entry
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).aig, ref := entry.ref.cast h }, assign⟧ = ⟦entry, assign⟧
Tactic:
simp [Ref.cast]
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.denote_mem_prefix
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size
Tactic:
apply lt_size_of_lt_aig_size
Proof state after:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < aig.decls.size
Theorem: AIG.LawfulStreamOperator.denote_mem_prefix
Proof state before:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.denote_mem_prefix
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ ⟦{ aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := h } }, assign⟧
Tactic:
rw [denote_input_entry ⟨aig, start, h⟩]
Proof state after:
no goals
Theorem: AIG.LawfulStreamOperator.denote_input_stream
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := (f s.aig input).aig, ref := (s.stream.getRef idx hidx).cast hcast }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧
Tactic:
rw [denote_mem_prefix]
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := s.aig, ref := { gate := ((s.stream.getRef idx hidx).cast hcast).gate, hgate := ?m.4622 } }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧

α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.stream.getRef idx hidx).cast hcast).gate < s.aig.decls.size
Theorem: AIG.LawfulStreamOperator.denote_input_stream
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦{ aig := s.aig, ref := { gate := ((s.stream.getRef idx hidx).cast hcast).gate, hgate := ?m.4622 } }, assign⟧ =
    ⟦{ aig := s.aig, ref := s.stream.getRef idx hidx }, assign⟧

α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len idx : Nat
hidx : idx < len
assign : α → Bool
s : RefStreamEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.stream.getRef idx hidx).cast hcast).gate < s.aig.decls.size
Tactic:
rfl
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2264
Proof state before:
⊢ ∀ (A B : BitVec 64), A ||| A ^^^ -1 ^^^ B = A ||| B ^^^ -1
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ ||| A✝ ^^^ -1 ^^^ B✝ = A✝ ||| B✝ ^^^ -1
Theorem: bitvec_AndOrXor_2264
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ ||| A✝ ^^^ -1 ^^^ B✝ = A✝ ||| B✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_1
Proof state before:
x y : BitVec 64
h : x ≠ y
⊢ y ≠ x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_2
Proof state before:
x y z : BitVec 32
h1 : x < y
h2 : y < z
⊢ x < z
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_2'
Proof state before:
x y z : BitVec 32
h1 : x.ult y = true
h2 : y < z
⊢ x.ult z = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_3
Proof state before:
x y z : BitVec 32
h1 : x ≤ y
h2 : y ≤ z
⊢ x ≤ z
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_3'
Proof state before:
x y z : BitVec 32
h1 : x.ule y = true
h2 : y ≤ z
⊢ x.ule z = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_4
Proof state before:
x y z : BitVec 32
h1 : x > y
h2 : y > z
⊢ x > z
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_5
Proof state before:
x y z : BitVec 32
h1 : x ≥ y
h2 : y ≥ z
⊢ x ≥ z
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_6
Proof state before:
x y z : BitVec 32
h1 : x.slt y = true
h2 : y.slt z = true
⊢ x.slt z = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: ineq_unit_7
Proof state before:
x y z : BitVec 32
h1 : x.sle y = true
h2 : y.sle z = true
⊢ x.sle z = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_1
Proof state before:
x y z : BitVec 8
⊢ x = y ∧ y = z ↔ ¬(¬x = y ∨ ¬y = z)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_1'
Proof state before:
x y z : BitVec 8
⊢ (decide (x = y) && decide (y = z)) = true ↔ ¬(decide ¬x = y || !decide (y = z)) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_1''
Proof state before:
x y z : BitVec 8
⊢ (decide (x = y)).and (decide (y = z)) = true ↔ ¬(!decide (x = y)).or (decide (y = z)).not = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_2
Proof state before:
x y : BitVec 8
⊢ x = y → y = x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_3
Proof state before:
x y : BitVec 8
⊢ xor (decide (x = y)) (decide (y ≠ x)) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_3'
Proof state before:
x y : BitVec 8
⊢ (decide (x = y)).xor (decide (y ≠ x)) = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_4
Proof state before:
a b : Bool
⊢ (a && b) = (b && a)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: substructure_unit_5
Proof state before:
a : Bool
b c : BitVec 32
h1 : b < c ↔ a = true
h2 : a = true
⊢ b < c
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2263
Proof state before:
⊢ ∀ (B op0 : BitVec 64), op0 ||| op0 ^^^ B = op0 ||| B
Tactic:
intros
Proof state after:
B✝ op0✝ : BitVec 64
⊢ op0✝ ||| op0✝ ^^^ B✝ = op0✝ ||| B✝
Theorem: bitvec_AndOrXor_2263
Proof state before:
B✝ op0✝ : BitVec 64
⊢ op0✝ ||| op0✝ ^^^ B✝ = op0✝ ||| B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2417
Proof state before:
⊢ ∀ (nx y : BitVec 64), (nx ^^^ -1 ||| y) ^^^ -1 = nx &&& (y ^^^ -1)
Tactic:
intros
Proof state after:
nx✝ y✝ : BitVec 64
⊢ (nx✝ ^^^ -1 ||| y✝) ^^^ -1 = nx✝ &&& (y✝ ^^^ -1)
Theorem: bitvec_AndOrXor_2417
Proof state before:
nx✝ y✝ : BitVec 64
⊢ (nx✝ ^^^ -1 ||| y✝) ^^^ -1 = nx✝ &&& (y✝ ^^^ -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1043
Proof state before:
⊢ ∀ (C1 Z RHS : BitVec 64), (Z &&& C1 ^^^ C1) + 1 + RHS = RHS - (Z ||| ~~~C1)
Tactic:
intros
Proof state after:
C1✝ Z✝ RHS✝ : BitVec 64
⊢ (Z✝ &&& C1✝ ^^^ C1✝) + 1 + RHS✝ = RHS✝ - (Z✝ ||| ~~~C1✝)
Theorem: bitvec_AddSub_1043
Proof state before:
C1✝ Z✝ RHS✝ : BitVec 64
⊢ (Z✝ &&& C1✝ ^^^ C1✝) + 1 + RHS✝ = RHS✝ - (Z✝ ||| ~~~C1✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderOut
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦mkFullAdderOut aig input, assign⟧ =
    xor (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧)
      ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
simp only [mkFullAdderOut, Ref_cast', denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
  Bool.bne_left_inj]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.cin }, assign⟧
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderOut
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦mkFullAdderCarry aig input, assign⟧ =
    (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := input.cin }, assign⟧ ||
      ⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
Tactic:
simp only [mkFullAdderCarry, Ref_cast', Int.reduceNeg, denote_mkOrCached,
  LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry',
  denote_mkXorCached, denote_projected_entry]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.cin.gate, hgate := ⋯ } },
          assign⟧ ||
      ⟦{
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.lhs.gate, hgate := ⋯ } },
          assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := input.cin }, assign⟧ ||
      ⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)