Proposition 2.1.13
(Rosser)
.
Define the following
λ
-term
:
A
+
:
=
λ
x
.
λ
y
.
λ
s
.
λ
z
.
x
s
(
y
s
(
z
)
)
,
A
∗
:
=
λ
x
.
λ
y
.
λ
s
.
x
(
y
s
)
,
A
e
:
=
λ
x
.
λ
y
.
y
x
.
Then for all
n
,
m
∈
ℕ
:
A
+
c
n
c
m
≡
β
c
n
+
m
;
A
∗
c
n
c
m
≡
β
c
n
m
;
A
e
c
n
c
m
≡
β
c
n
m
if
m
>
0
.