(VAR V2 N M V1 X1 X2 X)
(RULES 
U11(tt,V2) -> U12(isNat(activate(V2)))
U12(tt) -> tt
U21(tt) -> tt
U31(tt,V2) -> U32(isNat(activate(V2)))
U32(tt) -> tt
U41(tt,N) -> activate(N)
U51(tt,M,N) -> U52(isNat(activate(N)),activate(M),activate(N))
U52(tt,M,N) -> s(plus(activate(N),activate(M)))
U61(tt) -> 0
U71(tt,M,N) -> U72(isNat(activate(N)),activate(M),activate(N))
U72(tt,M,N) -> plus(x(activate(N),activate(M)),activate(N))
isNat(n__0) -> tt
isNat(n__plus(V1,V2)) -> U11(isNat(activate(V1)),activate(V2))
isNat(n__s(V1)) -> U21(isNat(activate(V1)))
isNat(n__x(V1,V2)) -> U31(isNat(activate(V1)),activate(V2))
plus(N,0) -> U41(isNat(N),N)
plus(N,s(M)) -> U51(isNat(M),M,N)
x(N,0) -> U61(isNat(N))
x(N,s(M)) -> U71(isNat(M),M,N)
0 -> n__0
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
x(X1,X2) -> n__x(X1,X2)
activate(n__0) -> 0
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
activate(n__x(X1,X2)) -> x(X1,X2)
activate(X) -> X
)