Theorem: BVLogicalExpr.bitblast_denote_eq_eval (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas.lean)

State before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
unfold bitblast
State after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧ = eval assign expr

State before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
unfold ofBoolExprCached
State after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr

State before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
rw [bitblast.go_eval_eq_eval]
State after:
no goals