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

State before:
aig : AIG BVBit
pred : BVPred
⊢ aig.decls.size ≤ (bitblast aig pred).aig.decls.size
Tactic:
cases pred with
| bin lhs op rhs =>
  cases op with
  | eq =>
    simp [bitblast]
    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
  | ult =>
    simp [bitblast]
    apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
| getLsb expr idx =>
  simp only [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
State after:
no goals

State before:
case bin
aig : AIG BVBit
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs op rhs)).aig.decls.size
Tactic:
cases op with
| eq =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
| ult =>
  simp [bitblast]
  apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
  apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
  apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
State after:
no goals

State before:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs BVBinPred.eq rhs)).aig.decls.size
Tactic:
simp [bitblast]
State after:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (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.size

State before:
case bin.eq
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (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.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkEq)
State after:
case bin.eq.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size

State before:
case bin.eq.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
State after:
case bin.eq.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size

State before:
case bin.eq.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
State after:
no goals

State before:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (bitblast aig (bin lhs BVBinPred.ult rhs)).aig.decls.size
Tactic:
simp [bitblast]
State after:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (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.size

State before:
case bin.ult
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤
    (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.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
State after:
case bin.ult.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size

State before:
case bin.ult.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
State after:
case bin.ult.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size

State before:
case bin.ult.h.h
aig : AIG BVBit
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ aig.decls.size ≤ (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
State after:
no goals

State before:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (bitblast aig (getLsb expr idx)).aig.decls.size
Tactic:
simp only [bitblast]
State after:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤
    (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls.size

State before:
case getLsb
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤
    (blastGetLsb (BVExpr.bitblast aig expr).aig (GetLsbTarget.mk (BVExpr.bitblast aig expr).stream idx)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
State after:
case getLsb.h
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (BVExpr.bitblast aig expr).aig.decls.size

State before:
case getLsb.h
aig : AIG BVBit
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ aig.decls.size ≤ (BVExpr.bitblast aig expr).aig.decls.size
Tactic:
apply AIG.LawfulStreamOperator.le_size (f := BVExpr.bitblast)
State after:
no goals