internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : 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⟧)
Tactic:
conv =>
  lhs
  lhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.cin.hgate)]
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, 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⟧)
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : 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, 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⟧)
Tactic:
conv =>
  lhs
  rhs
  lhs
  rw [
    LawfulOperator.denote_mem_prefix
      (f := mkAndCached)
      (h := by
        apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
        apply Ref.hgate
      )
  ]
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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧)
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : 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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧)
Tactic:
conv =>
  lhs
  rhs
  lhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.lhs.hgate)]
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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := 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⟧)
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : 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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := 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⟧)
Tactic:
conv =>
  lhs
  rhs
  rhs
  rw [
    LawfulOperator.denote_mem_prefix
      (f := mkAndCached)
      (h := by
        apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
        apply Ref.hgate
      )
  ]
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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧)
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
α : 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, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧)
Tactic:
conv =>
  lhs
  rhs
  rhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.rhs.hgate)]
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
⊢ input.lhs.gate < (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
Proof state after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size
Tactic:
apply Ref.hgate
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
⊢ input.rhs.gate < (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.decls.size
Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
Proof state after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry
Proof state before:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size
Tactic:
apply Ref.hgate
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdder 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 α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (mkFullAdder aig input).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (mkFullAdder aig input).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Tactic:
exact hstart
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (mkFullAdder aig input).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (mkFullAdder aig input).aig.decls.size
Tactic:
apply FullAdderOutput.hle
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdder aig input).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
unfold mkFullAdder
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.7385 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.7385 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ start < (go aig curr hcurr cin s lhs rhs).aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.blastAdd.go_denote_mem_prefix
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Tactic:
exact hstart
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size
Theorem: BVExpr.bitblast.blastAdd.go_denote_mem_prefix
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size
Tactic:
apply go_le_size
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd.go_denote_mem_prefix
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (go aig curr hcurr cin s lhs rhs).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
apply denote.eq_of_aig_eq (entry := ⟨aig, start,hstart⟩)
Proof state after:
case hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls
    (go aig curr hcurr cin s lhs rhs).aig.decls