Alphabet
f
:
[o × o → o] ⟶ o
g
:
[o × o × o → o] ⟶ o
b
:
o
a
:
o
Variables
x
:
o
y
:
o
F
:
o → o
Rules
g
(
x
,
y
,
F
)
⇒
f
(
f
(
x
,
F
),
F
)
f
(
x
,
F
)
⇒
b
b
⇒
a
f
(
b
, λ
z
:o.
g
(
z
,
z
,
F
))
⇒
g
(
f
(
a
, λ
z
:o.
g
(
z
,
z
,
F
)),
f
(
b
, λ
z
:o.
b
),
F
)