Alphabet

cons:[nat × list] ⟶ list
emap:[nat → nat × list] ⟶ list
nil:list
twice:[nat → nat] ⟶ nat → nat

Variables

F:nat → nat
Z:nat → nat
U:nat
V:list
I:nat → nat
P:nat

Rules

emap(F, nil)⇒nil
emap(Z, cons(U, V))⇒cons(Z · U, emap(λ%X:nat.twice(Z) · %X, V))
twice(I) · P⇒I · (I · P)