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

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

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

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