internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. rw [← hgo]
  intros
  rw [go_decl_eq]
  unfold mkFullAdder
  rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
  rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)]
  . apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
    assumption
  . apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
    apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
    assumption
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. simp [← hgo]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
rw [← hgo]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
                ((s.cast ⋯).pushRef
                  (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
                ((s.cast ⋯).pushRef
                  (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intros
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx✝] =
    aig.decls[idx✝]
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
. apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
  assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
Proof state after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
Proof state after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
Proof state after:
case isTrue.h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isTrue.h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
simp [← hgo]
Proof state after:
no goals
Theorem: cast_unit_1
Proof state before:
x : BitVec 64
⊢ ↑0 &&& x = 0
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_2
Proof state before:
x : BitVec 64
⊢ zeroExtend 32 x = zeroExtend 32 (zeroExtend 64 x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_3
Proof state before:
x : BitVec 64
⊢ zeroExtend 128 x = zeroExtend 128 (zeroExtend 64 x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_3'
Proof state before:
x : BitVec 64
⊢ truncate 128 x = zeroExtend 128 (truncate 64 x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_4
Proof state before:
x y : BitVec 32
⊢ extractLsb 32 0 (zeroExtend 64 x) = extractLsb 32 0 (zeroExtend 64 y) → x = y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_5
Proof state before:
x y : BitVec 64
⊢ extractLsb 63 0 (x ++ y) = extractLsb 127 64 (y ++ x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_5'
Proof state before:
x y : BitVec 64
⊢ extractLsb 63 0 (x.append y) = extractLsb 127 64 (y ++ x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_6
Proof state before:
x : BitVec 64
⊢ signExtend 32 x = signExtend 32 (signExtend 64 x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_7
Proof state before:
x : BitVec 64
⊢ signExtend 128 x = signExtend 128 (signExtend 64 x)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: cast_unit_8
Proof state before:
x : BitVec 64
⊢ signExtend 128 x = zeroExtend 128 x ↔ x.msb = false
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1574
Proof state before:
⊢ ∀ (X C C2 : BitVec 64), C - (X + C2) = C - C2 - X
Tactic:
intros
Proof state after:
X✝ C✝ C2✝ : BitVec 64
⊢ C✝ - (X✝ + C2✝) = C✝ - C2✝ - X✝
Theorem: bitvec_AddSub_1574
Proof state before:
X✝ C✝ C2✝ : BitVec 64
⊢ C✝ - (X✝ + C2✝) = C✝ - C2✝ - X✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: SatStress.t1
Proof state before:
x : Bool
x✝¹ : x = true
x1 x0 : Bool
x✝ : (x0 && x1) = x
⊢ x0 = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: SatStress.t2
Proof state before:
x : Bool
x✝³ : x = true
x1 x0 : Bool
x✝² : (x0 && x1) = x
x11 x10 : Bool
x✝¹ : (x10 && x11) = x1
x01 x00 : Bool
x✝ : (x00 && x01) = x0
⊢ x00 = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: SatStress.t3
Proof state before:
x : Bool
x✝⁷ : x = true
x1 x0 : Bool
x✝⁶ : (x0 && x1) = x
x11 x10 : Bool
x✝⁵ : (x10 && x11) = x1
x111 x110 : Bool
x✝⁴ : (x110 && x111) = x11
x101 x100 : Bool
x✝³ : (x100 && x101) = x10
x01 x00 : Bool
x✝² : (x00 && x01) = x0
x011 x010 : Bool
x✝¹ : (x010 && x011) = x01
x001 x000 : Bool
x✝ : (x000 && x001) = x00
⊢ x000 = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: SatStress.t4
Proof state before:
x : Bool
x✝¹⁵ : x = true
x1 x0 : Bool
x✝¹⁴ : (x0 && x1) = x
x11 x10 : Bool
x✝¹³ : (x10 && x11) = x1
x111 x110 : Bool
x✝¹² : (x110 && x111) = x11
x1111 x1110 : Bool
x✝¹¹ : (x1110 && x1111) = x111
x1101 x1100 : Bool
x✝¹⁰ : (x1100 && x1101) = x110
x101 x100 : Bool
x✝⁹ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝⁸ : (x1010 && x1011) = x101
x1001 x1000 : Bool
x✝⁷ : (x1000 && x1001) = x100
x01 x00 : Bool
x✝⁶ : (x00 && x01) = x0
x011 x010 : Bool
x✝⁵ : (x010 && x011) = x01
x0111 x0110 : Bool
x✝⁴ : (x0110 && x0111) = x011
x0101 x0100 : Bool
x✝³ : (x0100 && x0101) = x010
x001 x000 : Bool
x✝² : (x000 && x001) = x00
x0011 x0010 : Bool
x✝¹ : (x0010 && x0011) = x001
x0001 x0000 : Bool
x✝ : (x0000 && x0001) = x000
⊢ x0000 = true
Tactic:
bv_decide
Proof state after:
no goals