0 :: nat
apply :: nat → nat → nat
avg :: nat → nat → nat
check :: nat → nat
fun :: (nat → nat) → nat
s :: nat → nat
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