Alphabet

0:nat
cons:[nat × list] ⟶ list
map:[nat → nat × list] ⟶ list
nil:list
op:[nat → nat × nat → nat] ⟶ nat → nat
pow:[nat → nat × nat] ⟶ nat → nat
s:[nat] ⟶ nat

Variables

F:nat → nat
Z:nat → nat
U:nat
V:nat
W:list

Rules

map(F, nil)⇒nil
map(F, cons(U, W))⇒cons(F · U, map(F, W))
pow(F, 0)⇒λ%X:nat.%X
pow(F, s(V))⇒op(F, pow(F, V))
op(F, Z) · V⇒F · (Z · V)
λ%Y:nat.F · %Y⇒F