Alphabet

0:a → b
cons:(a → b) → c → c
hd:c → a → b
map:((a → b) → a → b) → c → c
nil:c

Variables

F:(a → b) → a → b
Y:a
G:(a → b) → a → b
H:(a → b) → a → b
I:a → b
P:c

Rules

F · 0 · Y⇒hd · (map · F · (cons · 0 · nil)) · Y
map · G · nil⇒nil
map · H · (cons · I · P)⇒cons · (H · I) · (map · H · P)