(VAR x y z)
(RULES
sqr(0) -> 0
sqr(s(x)) -> +(sqr(x),s(double(x)))
double(0) -> 0
double(s(x)) -> s(s(double(x)))
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
sqr(s(x)) -> s(+(sqr(x),double(x)))
)
(COMMENT Example 2.19 (Square Numbers) in \cite{SK90})