(VAR x y z u)

(DATATYPES b = µX. < s(X), 0 >
 )

(SIGNATURES
   q :: b x b -> b
   p :: b x b x b x b -> b
   add :: b x b -> b
 )

(RULES
 q(s(x),y) -> p(s(x),0,s(0),y)
 p(s(x),y,z,u) -> p(x,s(y),s(s(z)),u)
 p(0,s(x),y,z) -> q(x,add(x,z))
 add(0,x) -> x
 add(s(x),y) -> s(add(x,y))
)