Theorem: BVPred.bitblast_decl_eq (LeanSAT/Reflect/BVExpr/BitBlast/Impl/Pred.lean)

State before:
idx : Nat
aig : AIG BVBit
pred : BVPred
h : idx < aig.decls.size
this : aig.decls.size ≤ (bitblast aig pred).aig.decls.size
⊢ idx < (bitblast aig pred).aig.decls.size
Tactic:
omega
State after:
no goals

State before:
idx : Nat
aig : AIG BVBit
pred : BVPred
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (bitblast aig pred).aig.decls[idx] = aig.decls[idx]
Tactic:
cases pred with
| bin lhs op rhs =>
  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
| getLsb expr idx =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  assumption
State after:
no goals

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
State after:
no goals

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]
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]

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)]
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

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)]
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

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)]
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

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
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

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
State after:
no goals

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)
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

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
State after:
no goals

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)
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

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)
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

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
State after:
no goals

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]
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]

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)]
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

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)]
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

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)]
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

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
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

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
State after:
no goals

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)
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

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
State after:
no goals

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)
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

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)
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

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
State after:
no goals

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]
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✝]

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)]
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

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)]
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

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)
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

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
State after:
no goals