0 :: a
comp :: (b → b) → (b → b) → b → b
plus :: a → a → a
s :: a → a
times :: a → a → a
twice :: (b → b) → b → b
plus(0, X) → X
plus(s(Y), U) → s(plus(Y, U))
times(0, V) → 0
times(s(W), P) → plus(times(W, P), P)
comp(F1, Z1, U1) → F1(Z1(U1))
twice(H1) → comp(H1, H1)