Alphabet
0
:
a
rec
:
(a → b → b) → b → a → b
s
:
a → a
Variables
F
:
a → b → b
Y
:
b
G
:
a → b → b
V
:
b
W
:
a
Rules
rec
· (λ
%Y
:a.λ
%X
:b.
F
·
%Y
·
%X
) ·
Y
·
0
⇒
Y
rec
· (λ
%U
:a.λ
%Z
:b.
G
·
%U
·
%Z
) ·
V
· (
s
·
W
)
⇒
G
· (
s
·
W
) · (
rec
· (λ
%W
:a.λ
%V
:b.
G
·
%W
·
%V
) ·
V
·
W
)