(VAR x y) (RULES double(x) -> permute(x, x, a) permute(x,y,a) -> permute(isZero(x),x,b) permute(false,x,b) -> permute(ack(x,x),p(x),c) permute(true,x,b) -> 0 permute(y,x,c) -> s(s(permute(x,y,a))) p(0) -> 0 p(s(x)) -> x ack(0,x) -> plus(x,s(0)) ack(s(x),0) -> ack(x, s(0)) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) plus(0,y) -> y plus(s(x),y) -> plus(x,s(y)) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(x,s(0)) -> s(x) plus(x,0) -> x isZero(0) -> true isZero(s(x)) -> false )