A right-hand side, when supplied with a valuation that gives meaning to its free variables, evaluates to a property. More precisely, a right-hand side is a monotone function of valuations to properties.

When lfp is applied to a system of equations eqs, it performs no actual computation. It produces a valuation, get, which represents the least solution of the system of equations. The actual fixed point computation takes place, on demand, when get is applied.