A rewrite system has the Z property if there is a function ' such that a → b implies b ↠ a' and a' ↠ b'.

 a  ———>  b
       /
      /
     v
    v
 a' -->>  b'

Intuitively, it's a monotone function which contracts all redexes in the term (and possibly more).

This property is equivalent to confluence: b ↞ a ↠ c implies there is some d such that b ↠ d ↞ c.

(↠ is the reflexive-transitive closure of →)

A call-by-value calculus with let.

v ∷= x | λx. e
e ∷= v | v v | let x = e in e

(λx. e) v       →  e[x:=v]   (β.λ)
let x = v in e  →  e[x:=v]   (β.let)

Here, reductions are defined in the specification logic (λProlog), while the "superdevelopment" is defined in the reasoning logic. For applications, the subexpressions are reduced first and then we reduce the possible (β.λ) redex, while for lets we try to reduce the (β.let) first and then reduce subexpressions. It's a choice, and the second one seems to have turned out a bit simpler (?).