The rewrite relation of the following TRS is considered.
U11(tt,V1,V2) |
→ |
U12(isNat(activate(V1)),activate(V2)) |
(1) |
U12(tt,V2) |
→ |
U13(isNat(activate(V2))) |
(2) |
U13(tt) |
→ |
tt |
(3) |
U21(tt,V1) |
→ |
U22(isNat(activate(V1))) |
(4) |
U22(tt) |
→ |
tt |
(5) |
U31(tt,V1,V2) |
→ |
U32(isNat(activate(V1)),activate(V2)) |
(6) |
U32(tt,V2) |
→ |
U33(isNat(activate(V2))) |
(7) |
U33(tt) |
→ |
tt |
(8) |
U41(tt,N) |
→ |
activate(N) |
(9) |
U51(tt,M,N) |
→ |
s(plus(activate(N),activate(M))) |
(10) |
U61(tt) |
→ |
0 |
(11) |
U71(tt,M,N) |
→ |
plus(x(activate(N),activate(M)),activate(N)) |
(12) |
and(tt,X) |
→ |
activate(X) |
(13) |
isNat(n__0) |
→ |
tt |
(14) |
isNat(n__plus(V1,V2)) |
→ |
U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(15) |
isNat(n__s(V1)) |
→ |
U21(isNatKind(activate(V1)),activate(V1)) |
(16) |
isNat(n__x(V1,V2)) |
→ |
U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(17) |
isNatKind(n__0) |
→ |
tt |
(18) |
isNatKind(n__plus(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(19) |
isNatKind(n__s(V1)) |
→ |
isNatKind(activate(V1)) |
(20) |
isNatKind(n__x(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(21) |
plus(N,0) |
→ |
U41(and(isNat(N),n__isNatKind(N)),N) |
(22) |
plus(N,s(M)) |
→ |
U51(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N) |
(23) |
x(N,0) |
→ |
U61(and(isNat(N),n__isNatKind(N))) |
(24) |
x(N,s(M)) |
→ |
U71(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N) |
(25) |
0 |
→ |
n__0 |
(26) |
plus(X1,X2) |
→ |
n__plus(X1,X2) |
(27) |
isNatKind(X) |
→ |
n__isNatKind(X) |
(28) |
s(X) |
→ |
n__s(X) |
(29) |
x(X1,X2) |
→ |
n__x(X1,X2) |
(30) |
and(X1,X2) |
→ |
n__and(X1,X2) |
(31) |
isNat(X) |
→ |
n__isNat(X) |
(32) |
activate(n__0) |
→ |
0 |
(33) |
activate(n__plus(X1,X2)) |
→ |
plus(activate(X1),activate(X2)) |
(34) |
activate(n__isNatKind(X)) |
→ |
isNatKind(X) |
(35) |
activate(n__s(X)) |
→ |
s(activate(X)) |
(36) |
activate(n__x(X1,X2)) |
→ |
x(activate(X1),activate(X2)) |
(37) |
activate(n__and(X1,X2)) |
→ |
and(activate(X1),X2) |
(38) |
activate(n__isNat(X)) |
→ |
isNat(X) |
(39) |
activate(X) |
→ |
X |
(40) |
U11(tt,V1,V2) |
→ |
U12(isNat(activate(V1)),activate(V2)) |
(1) |
U12(tt,V2) |
→ |
U13(isNat(activate(V2))) |
(2) |
U13(tt) |
→ |
tt |
(3) |
U21(tt,V1) |
→ |
U22(isNat(activate(V1))) |
(4) |
U31(tt,V1,V2) |
→ |
U32(isNat(activate(V1)),activate(V2)) |
(6) |
U32(tt,V2) |
→ |
U33(isNat(activate(V2))) |
(7) |
U33(tt) |
→ |
tt |
(8) |
U41(tt,N) |
→ |
activate(N) |
(9) |
U51(tt,M,N) |
→ |
s(plus(activate(N),activate(M))) |
(10) |
U61(tt) |
→ |
0 |
(11) |
U71(tt,M,N) |
→ |
plus(x(activate(N),activate(M)),activate(N)) |
(12) |
and(tt,X) |
→ |
activate(X) |
(13) |
isNat(n__0) |
→ |
tt |
(14) |
isNat(n__plus(V1,V2)) |
→ |
U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(15) |
isNat(n__s(V1)) |
→ |
U21(isNatKind(activate(V1)),activate(V1)) |
(16) |
isNat(n__x(V1,V2)) |
→ |
U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(17) |
isNatKind(n__0) |
→ |
tt |
(18) |
isNatKind(n__plus(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(19) |
isNatKind(n__s(V1)) |
→ |
isNatKind(activate(V1)) |
(20) |
isNatKind(n__x(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(21) |
plus(N,0) |
→ |
U41(and(isNat(N),n__isNatKind(N)),N) |
(22) |
plus(N,s(M)) |
→ |
U51(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N) |
(23) |
x(N,0) |
→ |
U61(and(isNat(N),n__isNatKind(N))) |
(24) |
x(N,s(M)) |
→ |
U71(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N) |
(25) |
There are no rules in the TRS. Hence, it is terminating.