As of version 1.5.1 ProB supports common subexpression elimination (CSE).
To enable it you need to set the advanced preference CSE to true (this can be done using the switch -p CSE TRUE when using the command-line version probcli or using the Advanced Preferences command in ProB Tcl/Tk). With CSE enabled, ProB will translate the predicate
x:dom(f(a)) & r=f(a)(x)
into
(LET @0==(f(a)) IN x ∈ dom(@0) ∧ r = @0(x))
before evaluating it. As you can see, the common sub-expression f(a) has been lifted into a LET statement. This has the advantage that the expression f(a) will only get evaluated once (rather than twice, in case x:dom(f(a))). Identifiers introduced by the CSE always start with the @-sign. As another example, the predicate
x*x+2*x > y*y*y & y*y*y > x*x+2*x
gets translated into
LET @2==(x*x+2*x) IN (LET @4==((y*y)*y) IN @2 > @4 & @4 > @2))
You may observe that the B-language does not have a let-construct for expression nor predicates (only for substitutions). There are various ways one can overcome this (e.g., using an existential quantifier for a predicate), but ProB adds its own LET-construct to the language in the interpreter. Moreover, to avoid issues with well-definedness and ensuring that ProB only evaluates the LET expressions when really needed, this LET has a different behaviour than the ``standard constructs. Indeed, ProB's LET is lazy, i.e., it will only evaluate the expression when required by the computation of the body of the LET. For example, in LET @1==f(a) IN 2>3 & @1+@1>10, the expression f(a) will never be evaluated. This is important for well-definedness and for performance.
To enable CSE also inside substitutions (aka B statements) you need to set the preference CSE_SUBST to true.