(COMMENT mapping of an Ackermann like function) (VAR k l x y z) (RULES app(nil, k) -> k app(l, nil) -> l app(cons(x,l), k) -> cons(x, app(l, k)) sum(cons(x,nil)) -> cons(x,nil) sum(cons(x,cons(y,l))) -> sum(cons(a(x,y,h),l)) a(h,h,x) -> s(x) a(x,s(y),h) -> a(x,y,s(h)) a(x,s(y),s(z)) -> a(x,y,a(x,s(y),z)) a(s(x),h,z) -> a(x,z,z) )