internlm/Lean-Github huggingface dataset:
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
next hcase =>
exfalso
rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
simp[hcase] at hn
Proof state after:
no goals
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
exfalso
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ False
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ False
Tactic:
rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
Proof state after:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? x = some n
⊢ False
Theorem: AIG.relabelNat_unsat_iff
Proof state before:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? x = some n
⊢ False
Tactic:
simp[hcase] at hn
Proof state after:
no goals
Theorem: AIG.Entrypoint.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.relabelNat.unsat ↔ entry.unsat
Tactic:
simp [relabelNat, unsat]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
Theorem: AIG.Entrypoint.relabelNat_unsat_iff
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
Tactic:
rw [AIG.relabelNat_unsat_iff]
Proof state after:
no goals
Theorem: bitvec_AddSub_1614
Proof state before:
⊢ ∀ (Y X : BitVec 64), X - (X + Y) = 0 - Y
Tactic:
intros
Proof state after:
Y✝ X✝ : BitVec 64
⊢ X✝ - (X✝ + Y✝) = 0 - Y✝
Theorem: bitvec_AddSub_1614
Proof state before:
Y✝ X✝ : BitVec 64
⊢ X✝ - (X✝ + Y✝) = 0 - Y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ aig.decls.size ≤ (go aig curr hcurr cin lhs rhs).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ aig.decls.size ≤
    (if hidx : curr < a✝ then
            let lin := lhs.getRef curr hidx;
            let rin := rhs.getRef curr hidx;
            let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
            let_fun this := ⋯;
            let aig_1 := res.aig;
            let carryRef := res.ref;
            let lhs_1 := lhs.cast this;
            let rhs_1 := rhs.cast this;
            go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
          else { aig := aig, ref := cin }).aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ aig.decls.size ≤
    (if hidx : curr < a✝ then
            let lin := lhs.getRef curr hidx;
            let rin := rhs.getRef curr hidx;
            let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
            let_fun this := ⋯;
            let aig_1 := res.aig;
            let carryRef := res.ref;
            let lhs_1 := lhs.cast this;
            let rhs_1 := rhs.cast this;
            go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
          else { aig := aig, ref := cin }).aig.decls.size
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ aig.decls.size ≤
    (if hidx : curr < a✝ then
            go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
              (curr + 1) ⋯
              (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
              (lhs.cast ⋯) (rhs.cast ⋯)
          else { aig := aig, ref := cin }).aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ aig.decls.size ≤
    (if hidx : curr < a✝ then
            go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
              (curr + 1) ⋯
              (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
              (lhs.cast ⋯) (rhs.cast ⋯)
          else { aig := aig, ref := cin }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ aig.decls.size ≤
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ { aig := aig, ref := cin }.aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ aig.decls.size ≤
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ { aig := aig, ref := cin }.aig.decls.size
Tactic:
. refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size (f := mkFullAdderCarry)
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ { aig := aig, ref := cin }.aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ { aig := aig, ref := cin }.aig.decls.size
Tactic:
. dsimp
  omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ aig.decls.size ≤
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ aig.decls.size ≤
    (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ aig.decls.size ≤
    (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size (f := mkFullAdderCarry)
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : curr < a✝
⊢ ?m.8987 ≤
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ { aig := aig, ref := cin }.aig.decls.size
Tactic:
dsimp
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
h✝ : ¬curr < a✝
⊢ aig.decls.size ≤ aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr hcurr cin lhs rhs).aig.decls.size),
    (go aig curr hcurr cin lhs rhs).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go aig curr hcurr cin lhs rhs = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo : go aig curr hcurr cin lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo : go aig curr hcurr cin lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo :
  (if hidx : curr < a✝ then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
      let_fun this := ⋯;
      let aig_1 := res.aig;
      let carryRef := res.ref;
      let lhs_1 := lhs.cast this;
      let rhs_1 := rhs.cast this;
      go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
    else { aig := aig, ref := cin }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo :
  (if hidx : curr < a✝ then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
      let_fun this := ⋯;
      let aig_1 := res.aig;
      let carryRef := res.ref;
      let lhs_1 := lhs.cast this;
      let rhs_1 := rhs.cast this;
      go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
    else { aig := aig, ref := cin }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo :
  (if hidx : curr < a✝ then
      go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1)
        ⋯ (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, ref := cin }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
hgo :
  (if hidx : curr < a✝ then
      go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1)
        ⋯ (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, ref := cin }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (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 α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : ¬curr < a✝
hgo : { aig := aig, ref := cin } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (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 α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : ¬curr < a✝
hgo : { aig := aig, ref := cin } = 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]
  rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
  assumption
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : ¬curr < a✝
hgo : { aig := aig, ref := cin } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : ¬curr < a✝
hgo : { aig := aig, ref := cin } = 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.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (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 α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
      (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
      (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intros
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
      (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls.size
⊢ (go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
            (rhs.cast ⋯)).aig.decls[idx✝] =
    aig.decls[idx✝]