Proposition 2.1.13 (Rosser). Define the following λ-term:

  • A+:=λx.λy.λs.λz.xs(ys(z)),

  • A:=λx.λy.λs.x(ys),

  • Ae:=λx.λy.yx.

Then for all n,m:

  • A+cncmβcn+m;

  • Acncmβcnm;

  • Aecncmβcnm if m>0.