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,N) |
→ |
activate(N) |
(6) |
U41(tt,M,N) |
→ |
s(plus(activate(N),activate(M))) |
(7) |
and(tt,X) |
→ |
activate(X) |
(8) |
isNat(n__0) |
→ |
tt |
(9) |
isNat(n__plus(V1,V2)) |
→ |
U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(10) |
isNat(n__s(V1)) |
→ |
U21(isNatKind(activate(V1)),activate(V1)) |
(11) |
isNatKind(n__0) |
→ |
tt |
(12) |
isNatKind(n__plus(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(13) |
isNatKind(n__s(V1)) |
→ |
isNatKind(activate(V1)) |
(14) |
plus(N,0) |
→ |
U31(and(isNat(N),n__isNatKind(N)),N) |
(15) |
plus(N,s(M)) |
→ |
U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N) |
(16) |
0 |
→ |
n__0 |
(17) |
plus(X1,X2) |
→ |
n__plus(X1,X2) |
(18) |
isNatKind(X) |
→ |
n__isNatKind(X) |
(19) |
s(X) |
→ |
n__s(X) |
(20) |
and(X1,X2) |
→ |
n__and(X1,X2) |
(21) |
activate(n__0) |
→ |
0 |
(22) |
activate(n__plus(X1,X2)) |
→ |
plus(X1,X2) |
(23) |
activate(n__isNatKind(X)) |
→ |
isNatKind(X) |
(24) |
activate(n__s(X)) |
→ |
s(X) |
(25) |
activate(n__and(X1,X2)) |
→ |
and(X1,X2) |
(26) |
activate(X) |
→ |
X |
(27) |
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,N) |
→ |
activate(N) |
(6) |
U41(tt,M,N) |
→ |
s(plus(activate(N),activate(M))) |
(7) |
and(tt,X) |
→ |
activate(X) |
(8) |
isNat(n__0) |
→ |
tt |
(9) |
isNat(n__plus(V1,V2)) |
→ |
U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2)) |
(10) |
isNat(n__s(V1)) |
→ |
U21(isNatKind(activate(V1)),activate(V1)) |
(11) |
isNatKind(n__0) |
→ |
tt |
(12) |
isNatKind(n__plus(V1,V2)) |
→ |
and(isNatKind(activate(V1)),n__isNatKind(activate(V2))) |
(13) |
isNatKind(n__s(V1)) |
→ |
isNatKind(activate(V1)) |
(14) |
plus(N,0) |
→ |
U31(and(isNat(N),n__isNatKind(N)),N) |
(15) |
plus(N,s(M)) |
→ |
U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N) |
(16) |
There are no rules in the TRS. Hence, it is terminating.