dom :: N → N → N → N
eval :: N → N → N
fun :: (N → N) → N → N → N
o :: N
s :: N → N
eval(fun(F, X, Y), Z) → F(dom(X, Y, Z))
dom(s(X), s(Y), s(Z)) → s(dom(X, Y, Z))
dom(o, s(Y), s(Z)) → s(dom(o, Y, Z))
dom(X, Y, o) → X
dom(o, o, Z) → o