internlm/Lean-Github huggingface dataset:
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ let_fun this := ⋯;
  (bitblast aig (bin lhs op rhs)).aig.decls[idx] = aig.decls[idx]
Tactic:
cases op with
| eq =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    assumption
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    assumption
| ult =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    assumption
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ let_fun this := ⋯;
  (bitblast aig (bin lhs BVBinPred.eq rhs)).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [bitblast]
Proof state after:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
Proof state after:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
Proof state after:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast aig lhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast aig lhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
Proof state after:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
. apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  assumption
Proof state after:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
. apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.eq.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.eq.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.eq.h2.h.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx.succ ≤ aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.eq.h2.h.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx.succ ≤ aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ let_fun this := ⋯;
  (bitblast aig (bin lhs BVBinPred.ult rhs)).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [bitblast]
Proof state after:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
Proof state after:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls[idx] = aig.decls[idx]

case bin.ult.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls[idx] = aig.decls[idx]

case bin.ult.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
Proof state after:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast aig lhs).aig.decls[idx] = aig.decls[idx]

case bin.ult.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast aig lhs).aig.decls[idx] = aig.decls[idx]

case bin.ult.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
Proof state after:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
. apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  assumption
Proof state after:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
. apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.ult.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.ult.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
Proof state after:
case bin.ult.h2.h.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx.succ ≤ aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case bin.ult.h2.h.h
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx.succ ≤ aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ let_fun this := ⋯;
  (bitblast aig (getLsb expr idx)).aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
simp only [bitblast]
Proof state after:
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls[idx✝] =
    aig.decls[idx✝]
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls[idx✝] =
    aig.decls[idx✝]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
Proof state after:
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.bitblast aig expr).aig.decls[idx✝] = aig.decls[idx✝]

case getLsb.h1
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < (BVExpr.bitblast aig expr).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case getLsb
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.bitblast aig expr).aig.decls[idx✝] = aig.decls[idx✝]

case getLsb.h1
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < (BVExpr.bitblast aig expr).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
Proof state after:
case getLsb.h2
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < (BVExpr.bitblast aig expr).aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case getLsb.h2
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < (BVExpr.bitblast aig expr).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
Proof state after:
case getLsb.h2.h
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < aig.decls.size
Theorem: BVPred.bitblast_decl_eq
Proof state before:
case getLsb.h2.h
idx✝ : Nat
aig : AIG BVBit
h : idx✝ < aig.decls.size
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ idx✝ < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: bitvec_AddSub_1165
Proof state before:
⊢ ∀ (a b : BitVec 64), 0 - a + (0 - b) = 0 - (a + b)
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ 0 - a✝ + (0 - b✝) = 0 - (a✝ + b✝)
Theorem: bitvec_AddSub_1165
Proof state before:
a✝ b✝ : BitVec 64
⊢ 0 - a✝ + (0 - b✝) = 0 - (a✝ + b✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            if hdist : curr < distance then
              let res := aig.mkConstCached false;
              let aig_1 := res.aig;
              let zeroRef := res.ref;
              let_fun hfinal := ⋯;
              let s := s.cast hfinal;
              let input := input.cast hfinal;
              let s := s.pushRef zeroRef;
              go aig_1 input distance (curr + 1) ⋯ s
            else
              let s := s.pushRef (input.getRef (curr - distance) ⋯);
              go aig input distance (curr + 1) ⋯ s
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            if hdist : curr < distance then
              let res := aig.mkConstCached false;
              let aig_1 := res.aig;
              let zeroRef := res.ref;
              let_fun hfinal := ⋯;
              let s := s.cast hfinal;
              let input := input.cast hfinal;
              let s := s.pushRef zeroRef;
              go aig_1 input distance (curr + 1) ⋯ s
            else
              let s := s.pushRef (input.getRef (curr - distance) ⋯);
              go aig input distance (curr + 1) ⋯ s
          else
            let_fun hcurr := ⋯;
            { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : curr < w
⊢ aig.decls.size ≤
    (if hdist : curr < distance then
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hfinal := ⋯;
            let s := s.cast hfinal;
            let input := input.cast hfinal;
            let s := s.pushRef zeroRef;
            go aig_1 input distance (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (curr - distance) ⋯);
            go aig input distance (curr + 1) ⋯ s).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : curr < w
⊢ aig.decls.size ≤
    (if hdist : curr < distance then
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hfinal := ⋯;
            let s := s.cast hfinal;
            let input := input.cast hfinal;
            let s := s.pushRef zeroRef;
            go aig_1 input distance (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (curr - distance) ⋯);
            go aig input distance (curr + 1) ⋯ s).aig.decls.size

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
. dsimp
  split
  . refine Nat.le_trans ?_ (by apply go_le_size)
    apply AIG.LawfulOperator.le_size
  . refine Nat.le_trans ?_ (by apply go_le_size)
    omega
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_le_size
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : ¬curr < w
⊢ aig.decls.size ≤
    (let_fun hcurr := ⋯;
          { aig := aig, stream := hcurr ▸ s }).aig.decls.size
Tactic:
. simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_le_size
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : curr < w
⊢ aig.decls.size ≤
    (if hdist : curr < distance then
            let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let zeroRef := res.ref;
            let_fun hfinal := ⋯;
            let s := s.cast hfinal;
            let input := input.cast hfinal;
            let s := s.pushRef zeroRef;
            go aig_1 input distance (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (curr - distance) ⋯);
            go aig input distance (curr + 1) ⋯ s).aig.decls.size
Tactic:
dsimp
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
h✝ : curr < w
⊢ aig.decls.size ≤
    (if hdist : curr < distance then
            go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
              ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)
          else go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig.decls.size