Alphabet
pair
:
[nat → nat × nat] ⟶ nat
split
:
[nat] ⟶ nat
Variables
F
:
nat → nat
Y
:
nat
Rules
split
(
F
·
Y
)
⇒
pair
(
F
,
Y
)