Alphabet

0:nat
a:[nat] ⟶ nat
f:[nat → nat × nat × nat] ⟶ nat
g:[nat × nat × nat → nat × nat] ⟶ nat
h:[nat] ⟶ nat
i:[nat] ⟶ nat
s:[nat] ⟶ nat

Variables

F:nat → nat
Y:nat
U:nat
V:nat

Rules

f(F, Y, U)⇒g(Y, U, F, Y)
g(s(Y), s(U), F, V)⇒g(Y, U, F, V)
g(0, 0, F, V)⇒f(F, s(V), F · h(V))
h(0)⇒a(0)
h(s(Y))⇒a(h(Y))
i(0)⇒0
i(a(Y))⇒s(i(Y))