Alphabet
branch
:
[a × b × b] ⟶ b
leaf
:
[a] ⟶ b
mapbt
:
[a → a × b] ⟶ b
Variables
F
:
a → a
Y
:
a
G
:
a → a
V
:
b
W
:
b
P
:
a
Rules
mapbt
(
F
,
leaf
(
Y
))
⇒
leaf
(
F
·
Y
)
mapbt
(
G
,
branch
(
P
,
V
,
W
))
⇒
branch
(
G
·
P
,
mapbt
(
G
,
V
),
mapbt
(
G
,
W
))