diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean
index 583daf3..d4e630d 100644
--- a/lean/Spa/Analysis/Forward/Adapters.lean
+++ b/lean/Spa/Analysis/Forward/Adapters.lean
@@ -14,20 +14,20 @@ theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
     Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
   FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
 
-def evalB (_ : prog.State) (bs : BasicStmt)
+def evalBasicStmt (_ : prog.State) (bs : BasicStmt)
     (vs : VariableValues L prog) : VariableValues L prog :=
   match bs with
   | .assign k e => updateVariablesFromExpression k e vs
   | .noop => vs
 
-theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
-    Monotone (evalB (L := L) (prog := prog) s bs) := by
+theorem evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) :
+    Monotone (evalBasicStmt (L := L) (prog := prog) s bs) := by
   cases bs with
   | assign k e => exact updateVariablesFromExpression_mono k e
   | noop => exact monotone_id
 
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
-  ⟨evalB, evalB_mono⟩
+  ⟨evalBasicStmt, evalBasicStmt_mono⟩
 
 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
     [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by