module M : sig ... endmodule P : sig ... endtype variable = M.keytype property = P.propertyA 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.
A system of equations is a mapping of variables to right-hand sides.
lfp eqs produces the least solution of the system of monotone equations eqs.
It is guaranteed that, for each variable v, the application eqs v is performed at most once (whereas the right-hand side produced by this application is, in general, evaluated multiple times). This guarantee can be used to perform costly pre-computation, or memory allocation, when eqs is applied to its first argument.