Alphabet
cons
:
[a × b] ⟶ b
map
:
[a → a × b] ⟶ b
nil
:
b
Variables
F
:
a → a
Z
:
a → a
U
:
a
V
:
b
Rules
map
(
F
,
nil
)
⇒
nil
map
(
Z
,
cons
(
U
,
V
))
⇒
cons
(
Z
·
U
,
map
(
Z
,
V
))