Alphabet

0:nat
h:[nat → bool × nat → nat × nat] ⟶ nat
if:[bool × nat × nat] ⟶ nat
true:bool
false:bool
s:[nat] ⟶ nat

Variables

X:nat
Y:nat
F:nat → bool
G:nat → nat

Rules

if(true, X, Y)⇒X
if(false, X, Y)⇒Y
h(F, G, 0)⇒0
h(F, G, s(Y))⇒G · h(F, G, if(F · Y, Y, 0))