Alphabet

0:nat
s:[nat] ⟶ nat
+:[nat × nat] ⟶ nat
*:[nat × nat] ⟶ nat
rec:[nat × nat × nat → nat → nat] ⟶ nat

Variables

x:nat
y:nat
U:nat
F:nat → nat → nat

Rules

+(x, 0)⇒x
+(x, s(y))⇒s(+(x, y))
rec(0, U, F)⇒U
rec(s(x), U, F)⇒F · x · rec(x, U, F)
*(x, y)⇒rec(y, 0, λz1:nat.λz2:nat.+(x, z2))