Alphabet

0:nat
apply:[nat × nat] ⟶ nat
avg:[nat × nat] ⟶ nat
check:[nat] ⟶ nat
fun:[nat → nat] ⟶ nat
s:[nat] ⟶ nat

Variables

X:nat
Y:nat
U:nat
V:nat
I:nat → nat
P:nat
X1:nat

Rules

avg(s(X), Y)⇒avg(X, s(Y))
avg(U, s(s(s(V))))⇒s(avg(s(U), V))
avg(0, 0)⇒0
avg(0, s(0))⇒0
avg(0, s(s(0)))⇒s(0)
apply(fun(I), P)⇒I · check(P)
check(s(X1))⇒s(check(X1))
check(0)⇒0