The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].
| mark#(U32(X)) | → | U32#(mark(X)) | U62#(X1, mark(X2), X3) | → | U62#(X1, X2, X3) | |
| mark#(U51(X1, X2)) | → | U51#(mark(X1), X2) | U15#(X1, active(X2)) | → | U15#(X1, X2) | |
| mark#(U11(X1, X2, X3)) | → | U11#(mark(X1), X2, X3) | active#(U15(tt, V2)) | → | U16#(isNat(V2)) | |
| U61#(X1, active(X2), X3) | → | U61#(X1, X2, X3) | mark#(U41(X)) | → | U41#(mark(X)) | |
| U61#(X1, X2, mark(X3)) | → | U61#(X1, X2, X3) | U52#(X1, active(X2)) | → | U52#(X1, X2) | |
| U51#(mark(X1), X2) | → | U51#(X1, X2) | mark#(U12(X1, X2, X3)) | → | active#(U12(mark(X1), X2, X3)) | |
| isNat#(active(X)) | → | isNat#(X) | U21#(X1, active(X2)) | → | U21#(X1, X2) | |
| mark#(s(X)) | → | mark#(X) | active#(U51(tt, N)) | → | mark#(U52(isNatKind(N), N)) | |
| mark#(U13(X1, X2, X3)) | → | mark#(X1) | mark#(plus(X1, X2)) | → | active#(plus(mark(X1), mark(X2))) | |
| active#(U31(tt, V2)) | → | U32#(isNatKind(V2)) | U62#(X1, X2, active(X3)) | → | U62#(X1, X2, X3) | |
| U14#(X1, mark(X2), X3) | → | U14#(X1, X2, X3) | active#(U21(tt, V1)) | → | isNatKind#(V1) | |
| U63#(X1, X2, active(X3)) | → | U63#(X1, X2, X3) | active#(U61(tt, M, N)) | → | mark#(U62(isNatKind(M), M, N)) | |
| U12#(X1, active(X2), X3) | → | U12#(X1, X2, X3) | U12#(X1, X2, mark(X3)) | → | U12#(X1, X2, X3) | |
| mark#(U41(X)) | → | mark#(X) | mark#(U11(X1, X2, X3)) | → | mark#(X1) | |
| active#(U15(tt, V2)) | → | mark#(U16(isNat(V2))) | active#(U15(tt, V2)) | → | isNat#(V2) | |
| U61#(active(X1), X2, X3) | → | U61#(X1, X2, X3) | active#(isNatKind(s(V1))) | → | U41#(isNatKind(V1)) | |
| mark#(U32(X)) | → | mark#(X) | U14#(X1, active(X2), X3) | → | U14#(X1, X2, X3) | |
| U32#(mark(X)) | → | U32#(X) | U15#(X1, mark(X2)) | → | U15#(X1, X2) | |
| U14#(mark(X1), X2, X3) | → | U14#(X1, X2, X3) | mark#(U16(X)) | → | mark#(X) | |
| U63#(X1, X2, mark(X3)) | → | U63#(X1, X2, X3) | active#(U12(tt, V1, V2)) | → | U13#(isNatKind(V2), V1, V2) | |
| U64#(X1, mark(X2), X3) | → | U64#(X1, X2, X3) | mark#(U22(X1, X2)) | → | mark#(X1) | |
| mark#(U21(X1, X2)) | → | active#(U21(mark(X1), X2)) | U11#(active(X1), X2, X3) | → | U11#(X1, X2, X3) | |
| mark#(U14(X1, X2, X3)) | → | active#(U14(mark(X1), X2, X3)) | U61#(mark(X1), X2, X3) | → | U61#(X1, X2, X3) | |
| mark#(isNatKind(X)) | → | isNatKind#(X) | active#(U31(tt, V2)) | → | mark#(U32(isNatKind(V2))) | |
| isNatKind#(mark(X)) | → | isNatKind#(X) | U52#(X1, mark(X2)) | → | U52#(X1, X2) | |
| U12#(X1, X2, active(X3)) | → | U12#(X1, X2, X3) | U15#(mark(X1), X2) | → | U15#(X1, X2) | |
| mark#(U61(X1, X2, X3)) | → | U61#(mark(X1), X2, X3) | U21#(active(X1), X2) | → | U21#(X1, X2) | |
| U64#(X1, X2, active(X3)) | → | U64#(X1, X2, X3) | mark#(U63(X1, X2, X3)) | → | U63#(mark(X1), X2, X3) | |
| U16#(active(X)) | → | U16#(X) | U51#(X1, mark(X2)) | → | U51#(X1, X2) | |
| active#(isNat(s(V1))) | → | U21#(isNatKind(V1), V1) | active#(plus(N, 0)) | → | mark#(U51(isNat(N), N)) | |
| U52#(mark(X1), X2) | → | U52#(X1, X2) | mark#(U64(X1, X2, X3)) | → | U64#(mark(X1), X2, X3) | |
| U63#(X1, active(X2), X3) | → | U63#(X1, X2, X3) | mark#(U52(X1, X2)) | → | U52#(mark(X1), X2) | |
| active#(isNat(plus(V1, V2))) | → | U11#(isNatKind(V1), V1, V2) | mark#(s(X)) | → | s#(mark(X)) | |
| active#(U21(tt, V1)) | → | U22#(isNatKind(V1), V1) | mark#(U11(X1, X2, X3)) | → | active#(U11(mark(X1), X2, X3)) | |
| active#(U12(tt, V1, V2)) | → | mark#(U13(isNatKind(V2), V1, V2)) | U41#(active(X)) | → | U41#(X) | |
| U16#(mark(X)) | → | U16#(X) | U64#(active(X1), X2, X3) | → | U64#(X1, X2, X3) | |
| U13#(X1, active(X2), X3) | → | U13#(X1, X2, X3) | active#(isNat(0)) | → | mark#(tt) | |
| U11#(mark(X1), X2, X3) | → | U11#(X1, X2, X3) | active#(U61(tt, M, N)) | → | U62#(isNatKind(M), M, N) | |
| mark#(U15(X1, X2)) | → | U15#(mark(X1), X2) | active#(U22(tt, V1)) | → | U23#(isNat(V1)) | |
| mark#(plus(X1, X2)) | → | mark#(X1) | isNatKind#(active(X)) | → | isNatKind#(X) | |
| active#(U64(tt, M, N)) | → | mark#(s(plus(N, M))) | U13#(X1, X2, mark(X3)) | → | U13#(X1, X2, X3) | |
| U12#(X1, mark(X2), X3) | → | U12#(X1, X2, X3) | mark#(U21(X1, X2)) | → | mark#(X1) | |
| mark#(U21(X1, X2)) | → | U21#(mark(X1), X2) | mark#(isNat(X)) | → | isNat#(X) | |
| isNat#(mark(X)) | → | isNat#(X) | active#(U12(tt, V1, V2)) | → | isNatKind#(V2) | |
| active#(isNat(plus(V1, V2))) | → | isNatKind#(V1) | U11#(X1, X2, mark(X3)) | → | U11#(X1, X2, X3) | |
| U14#(active(X1), X2, X3) | → | U14#(X1, X2, X3) | U23#(active(X)) | → | U23#(X) | |
| U64#(X1, active(X2), X3) | → | U64#(X1, X2, X3) | mark#(U12(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U22(X1, X2)) | → | active#(U22(mark(X1), X2)) | active#(U63(tt, M, N)) | → | isNatKind#(N) | |
| mark#(U62(X1, X2, X3)) | → | active#(U62(mark(X1), X2, X3)) | mark#(U64(X1, X2, X3)) | → | active#(U64(mark(X1), X2, X3)) | |
| active#(isNat(s(V1))) | → | mark#(U21(isNatKind(V1), V1)) | mark#(plus(X1, X2)) | → | plus#(mark(X1), mark(X2)) | |
| U64#(mark(X1), X2, X3) | → | U64#(X1, X2, X3) | mark#(U13(X1, X2, X3)) | → | U13#(mark(X1), X2, X3) | |
| s#(mark(X)) | → | s#(X) | mark#(U31(X1, X2)) | → | U31#(mark(X1), X2) | |
| mark#(U32(X)) | → | active#(U32(mark(X))) | active#(isNatKind(0)) | → | mark#(tt) | |
| U63#(mark(X1), X2, X3) | → | U63#(X1, X2, X3) | active#(isNatKind(plus(V1, V2))) | → | isNatKind#(V1) | |
| active#(U13(tt, V1, V2)) | → | U14#(isNatKind(V2), V1, V2) | active#(U62(tt, M, N)) | → | isNat#(N) | |
| mark#(U22(X1, X2)) | → | U22#(mark(X1), X2) | active#(U11(tt, V1, V2)) | → | mark#(U12(isNatKind(V1), V1, V2)) | |
| active#(plus(N, 0)) | → | isNat#(N) | active#(U22(tt, V1)) | → | isNat#(V1) | |
| active#(isNatKind(plus(V1, V2))) | → | mark#(U31(isNatKind(V1), V2)) | U22#(active(X1), X2) | → | U22#(X1, X2) | |
| U11#(X1, active(X2), X3) | → | U11#(X1, X2, X3) | U12#(mark(X1), X2, X3) | → | U12#(X1, X2, X3) | |
| active#(U41(tt)) | → | mark#(tt) | mark#(U13(X1, X2, X3)) | → | active#(U13(mark(X1), X2, X3)) | |
| mark#(U51(X1, X2)) | → | active#(U51(mark(X1), X2)) | active#(U51(tt, N)) | → | U52#(isNatKind(N), N) | |
| active#(U61(tt, M, N)) | → | isNatKind#(M) | active#(U22(tt, V1)) | → | mark#(U23(isNat(V1))) | |
| active#(isNatKind(s(V1))) | → | mark#(U41(isNatKind(V1))) | mark#(U15(X1, X2)) | → | mark#(X1) | |
| active#(isNat(s(V1))) | → | isNatKind#(V1) | active#(U11(tt, V1, V2)) | → | isNatKind#(V1) | |
| active#(U63(tt, M, N)) | → | U64#(isNatKind(N), M, N) | active#(U14(tt, V1, V2)) | → | U15#(isNat(V1), V2) | |
| U13#(X1, X2, active(X3)) | → | U13#(X1, X2, X3) | U63#(X1, mark(X2), X3) | → | U63#(X1, X2, X3) | |
| U64#(X1, X2, mark(X3)) | → | U64#(X1, X2, X3) | plus#(mark(X1), X2) | → | plus#(X1, X2) | |
| U13#(mark(X1), X2, X3) | → | U13#(X1, X2, X3) | plus#(active(X1), X2) | → | plus#(X1, X2) | |
| U51#(X1, active(X2)) | → | U51#(X1, X2) | U22#(mark(X1), X2) | → | U22#(X1, X2) | |
| mark#(tt) | → | active#(tt) | active#(U52(tt, N)) | → | mark#(N) | |
| U31#(X1, active(X2)) | → | U31#(X1, X2) | mark#(U23(X)) | → | active#(U23(mark(X))) | |
| U63#(active(X1), X2, X3) | → | U63#(X1, X2, X3) | mark#(U14(X1, X2, X3)) | → | mark#(X1) | |
| U22#(X1, active(X2)) | → | U22#(X1, X2) | U62#(X1, X2, mark(X3)) | → | U62#(X1, X2, X3) | |
| U21#(X1, mark(X2)) | → | U21#(X1, X2) | mark#(U23(X)) | → | mark#(X) | |
| active#(plus(N, 0)) | → | U51#(isNat(N), N) | U12#(active(X1), X2, X3) | → | U12#(X1, X2, X3) | |
| active#(U64(tt, M, N)) | → | s#(plus(N, M)) | U62#(mark(X1), X2, X3) | → | U62#(X1, X2, X3) | |
| mark#(U31(X1, X2)) | → | active#(U31(mark(X1), X2)) | active#(U21(tt, V1)) | → | mark#(U22(isNatKind(V1), V1)) | |
| U13#(X1, mark(X2), X3) | → | U13#(X1, X2, X3) | mark#(0) | → | active#(0) | |
| mark#(s(X)) | → | active#(s(mark(X))) | U52#(active(X1), X2) | → | U52#(X1, X2) | |
| mark#(U14(X1, X2, X3)) | → | U14#(mark(X1), X2, X3) | active#(U62(tt, M, N)) | → | U63#(isNat(N), M, N) | |
| mark#(U12(X1, X2, X3)) | → | U12#(mark(X1), X2, X3) | active#(plus(N, s(M))) | → | isNat#(M) | |
| active#(U16(tt)) | → | mark#(tt) | U11#(X1, X2, active(X3)) | → | U11#(X1, X2, X3) | |
| mark#(U15(X1, X2)) | → | active#(U15(mark(X1), X2)) | mark#(isNatKind(X)) | → | active#(isNatKind(X)) | |
| active#(isNatKind(plus(V1, V2))) | → | U31#(isNatKind(V1), V2) | active#(U63(tt, M, N)) | → | mark#(U64(isNatKind(N), M, N)) | |
| active#(isNat(plus(V1, V2))) | → | mark#(U11(isNatKind(V1), V1, V2)) | mark#(U63(X1, X2, X3)) | → | active#(U63(mark(X1), X2, X3)) | |
| U23#(mark(X)) | → | U23#(X) | U41#(mark(X)) | → | U41#(X) | |
| active#(U31(tt, V2)) | → | isNatKind#(V2) | active#(plus(N, s(M))) | → | U61#(isNat(M), M, N) | |
| active#(U13(tt, V1, V2)) | → | isNatKind#(V2) | plus#(X1, mark(X2)) | → | plus#(X1, X2) | |
| U31#(active(X1), X2) | → | U31#(X1, X2) | U62#(active(X1), X2, X3) | → | U62#(X1, X2, X3) | |
| mark#(U31(X1, X2)) | → | mark#(X1) | U62#(X1, active(X2), X3) | → | U62#(X1, X2, X3) | |
| mark#(U23(X)) | → | U23#(mark(X)) | active#(U32(tt)) | → | mark#(tt) | |
| U14#(X1, X2, active(X3)) | → | U14#(X1, X2, X3) | U61#(X1, mark(X2), X3) | → | U61#(X1, X2, X3) | |
| U15#(active(X1), X2) | → | U15#(X1, X2) | active#(U51(tt, N)) | → | isNatKind#(N) | |
| active#(U64(tt, M, N)) | → | plus#(N, M) | U13#(active(X1), X2, X3) | → | U13#(X1, X2, X3) | |
| plus#(X1, active(X2)) | → | plus#(X1, X2) | mark#(U63(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U52(X1, X2)) | → | active#(U52(mark(X1), X2)) | mark#(isNat(X)) | → | active#(isNat(X)) | |
| mark#(U16(X)) | → | U16#(mark(X)) | active#(U14(tt, V1, V2)) | → | mark#(U15(isNat(V1), V2)) | |
| mark#(U61(X1, X2, X3)) | → | active#(U61(mark(X1), X2, X3)) | mark#(U61(X1, X2, X3)) | → | mark#(X1) | |
| U22#(X1, mark(X2)) | → | U22#(X1, X2) | U51#(active(X1), X2) | → | U51#(X1, X2) | |
| mark#(U16(X)) | → | active#(U16(mark(X))) | mark#(U51(X1, X2)) | → | mark#(X1) | |
| U31#(X1, mark(X2)) | → | U31#(X1, X2) | mark#(U62(X1, X2, X3)) | → | mark#(X1) | |
| active#(U13(tt, V1, V2)) | → | mark#(U14(isNatKind(V2), V1, V2)) | mark#(plus(X1, X2)) | → | mark#(X2) | |
| active#(plus(N, s(M))) | → | mark#(U61(isNat(M), M, N)) | U14#(X1, X2, mark(X3)) | → | U14#(X1, X2, X3) | |
| active#(U14(tt, V1, V2)) | → | isNat#(V1) | active#(isNatKind(s(V1))) | → | isNatKind#(V1) | |
| U32#(active(X)) | → | U32#(X) | mark#(U52(X1, X2)) | → | mark#(X1) | |
| active#(U11(tt, V1, V2)) | → | U12#(isNatKind(V1), V1, V2) | active#(U62(tt, M, N)) | → | mark#(U63(isNat(N), M, N)) | |
| U31#(mark(X1), X2) | → | U31#(X1, X2) | active#(U23(tt)) | → | mark#(tt) | |
| U61#(X1, X2, active(X3)) | → | U61#(X1, X2, X3) | U21#(mark(X1), X2) | → | U21#(X1, X2) | |
| U11#(X1, mark(X2), X3) | → | U11#(X1, X2, X3) | s#(active(X)) | → | s#(X) | |
| mark#(U41(X)) | → | active#(U41(mark(X))) | mark#(U64(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U62(X1, X2, X3)) | → | U62#(mark(X1), X2, X3) |
| active(U11(tt, V1, V2)) | → | mark(U12(isNatKind(V1), V1, V2)) | active(U12(tt, V1, V2)) | → | mark(U13(isNatKind(V2), V1, V2)) | |
| active(U13(tt, V1, V2)) | → | mark(U14(isNatKind(V2), V1, V2)) | active(U14(tt, V1, V2)) | → | mark(U15(isNat(V1), V2)) | |
| active(U15(tt, V2)) | → | mark(U16(isNat(V2))) | active(U16(tt)) | → | mark(tt) | |
| active(U21(tt, V1)) | → | mark(U22(isNatKind(V1), V1)) | active(U22(tt, V1)) | → | mark(U23(isNat(V1))) | |
| active(U23(tt)) | → | mark(tt) | active(U31(tt, V2)) | → | mark(U32(isNatKind(V2))) | |
| active(U32(tt)) | → | mark(tt) | active(U41(tt)) | → | mark(tt) | |
| active(U51(tt, N)) | → | mark(U52(isNatKind(N), N)) | active(U52(tt, N)) | → | mark(N) | |
| active(U61(tt, M, N)) | → | mark(U62(isNatKind(M), M, N)) | active(U62(tt, M, N)) | → | mark(U63(isNat(N), M, N)) | |
| active(U63(tt, M, N)) | → | mark(U64(isNatKind(N), M, N)) | active(U64(tt, M, N)) | → | mark(s(plus(N, M))) | |
| active(isNat(0)) | → | mark(tt) | active(isNat(plus(V1, V2))) | → | mark(U11(isNatKind(V1), V1, V2)) | |
| active(isNat(s(V1))) | → | mark(U21(isNatKind(V1), V1)) | active(isNatKind(0)) | → | mark(tt) | |
| active(isNatKind(plus(V1, V2))) | → | mark(U31(isNatKind(V1), V2)) | active(isNatKind(s(V1))) | → | mark(U41(isNatKind(V1))) | |
| active(plus(N, 0)) | → | mark(U51(isNat(N), N)) | active(plus(N, s(M))) | → | mark(U61(isNat(M), M, N)) | |
| mark(U11(X1, X2, X3)) | → | active(U11(mark(X1), X2, X3)) | mark(tt) | → | active(tt) | |
| mark(U12(X1, X2, X3)) | → | active(U12(mark(X1), X2, X3)) | mark(isNatKind(X)) | → | active(isNatKind(X)) | |
| mark(U13(X1, X2, X3)) | → | active(U13(mark(X1), X2, X3)) | mark(U14(X1, X2, X3)) | → | active(U14(mark(X1), X2, X3)) | |
| mark(U15(X1, X2)) | → | active(U15(mark(X1), X2)) | mark(isNat(X)) | → | active(isNat(X)) | |
| mark(U16(X)) | → | active(U16(mark(X))) | mark(U21(X1, X2)) | → | active(U21(mark(X1), X2)) | |
| mark(U22(X1, X2)) | → | active(U22(mark(X1), X2)) | mark(U23(X)) | → | active(U23(mark(X))) | |
| mark(U31(X1, X2)) | → | active(U31(mark(X1), X2)) | mark(U32(X)) | → | active(U32(mark(X))) | |
| mark(U41(X)) | → | active(U41(mark(X))) | mark(U51(X1, X2)) | → | active(U51(mark(X1), X2)) | |
| mark(U52(X1, X2)) | → | active(U52(mark(X1), X2)) | mark(U61(X1, X2, X3)) | → | active(U61(mark(X1), X2, X3)) | |
| mark(U62(X1, X2, X3)) | → | active(U62(mark(X1), X2, X3)) | mark(U63(X1, X2, X3)) | → | active(U63(mark(X1), X2, X3)) | |
| mark(U64(X1, X2, X3)) | → | active(U64(mark(X1), X2, X3)) | mark(s(X)) | → | active(s(mark(X))) | |
| mark(plus(X1, X2)) | → | active(plus(mark(X1), mark(X2))) | mark(0) | → | active(0) | |
| U11(mark(X1), X2, X3) | → | U11(X1, X2, X3) | U11(X1, mark(X2), X3) | → | U11(X1, X2, X3) | |
| U11(X1, X2, mark(X3)) | → | U11(X1, X2, X3) | U11(active(X1), X2, X3) | → | U11(X1, X2, X3) | |
| U11(X1, active(X2), X3) | → | U11(X1, X2, X3) | U11(X1, X2, active(X3)) | → | U11(X1, X2, X3) | |
| U12(mark(X1), X2, X3) | → | U12(X1, X2, X3) | U12(X1, mark(X2), X3) | → | U12(X1, X2, X3) | |
| U12(X1, X2, mark(X3)) | → | U12(X1, X2, X3) | U12(active(X1), X2, X3) | → | U12(X1, X2, X3) | |
| U12(X1, active(X2), X3) | → | U12(X1, X2, X3) | U12(X1, X2, active(X3)) | → | U12(X1, X2, X3) | |
| isNatKind(mark(X)) | → | isNatKind(X) | isNatKind(active(X)) | → | isNatKind(X) | |
| U13(mark(X1), X2, X3) | → | U13(X1, X2, X3) | U13(X1, mark(X2), X3) | → | U13(X1, X2, X3) | |
| U13(X1, X2, mark(X3)) | → | U13(X1, X2, X3) | U13(active(X1), X2, X3) | → | U13(X1, X2, X3) | |
| U13(X1, active(X2), X3) | → | U13(X1, X2, X3) | U13(X1, X2, active(X3)) | → | U13(X1, X2, X3) | |
| U14(mark(X1), X2, X3) | → | U14(X1, X2, X3) | U14(X1, mark(X2), X3) | → | U14(X1, X2, X3) | |
| U14(X1, X2, mark(X3)) | → | U14(X1, X2, X3) | U14(active(X1), X2, X3) | → | U14(X1, X2, X3) | |
| U14(X1, active(X2), X3) | → | U14(X1, X2, X3) | U14(X1, X2, active(X3)) | → | U14(X1, X2, X3) | |
| U15(mark(X1), X2) | → | U15(X1, X2) | U15(X1, mark(X2)) | → | U15(X1, X2) | |
| U15(active(X1), X2) | → | U15(X1, X2) | U15(X1, active(X2)) | → | U15(X1, X2) | |
| isNat(mark(X)) | → | isNat(X) | isNat(active(X)) | → | isNat(X) | |
| U16(mark(X)) | → | U16(X) | U16(active(X)) | → | U16(X) | |
| U21(mark(X1), X2) | → | U21(X1, X2) | U21(X1, mark(X2)) | → | U21(X1, X2) | |
| U21(active(X1), X2) | → | U21(X1, X2) | U21(X1, active(X2)) | → | U21(X1, X2) | |
| U22(mark(X1), X2) | → | U22(X1, X2) | U22(X1, mark(X2)) | → | U22(X1, X2) | |
| U22(active(X1), X2) | → | U22(X1, X2) | U22(X1, active(X2)) | → | U22(X1, X2) | |
| U23(mark(X)) | → | U23(X) | U23(active(X)) | → | U23(X) | |
| U31(mark(X1), X2) | → | U31(X1, X2) | U31(X1, mark(X2)) | → | U31(X1, X2) | |
| U31(active(X1), X2) | → | U31(X1, X2) | U31(X1, active(X2)) | → | U31(X1, X2) | |
| U32(mark(X)) | → | U32(X) | U32(active(X)) | → | U32(X) | |
| U41(mark(X)) | → | U41(X) | U41(active(X)) | → | U41(X) | |
| U51(mark(X1), X2) | → | U51(X1, X2) | U51(X1, mark(X2)) | → | U51(X1, X2) | |
| U51(active(X1), X2) | → | U51(X1, X2) | U51(X1, active(X2)) | → | U51(X1, X2) | |
| U52(mark(X1), X2) | → | U52(X1, X2) | U52(X1, mark(X2)) | → | U52(X1, X2) | |
| U52(active(X1), X2) | → | U52(X1, X2) | U52(X1, active(X2)) | → | U52(X1, X2) | |
| U61(mark(X1), X2, X3) | → | U61(X1, X2, X3) | U61(X1, mark(X2), X3) | → | U61(X1, X2, X3) | |
| U61(X1, X2, mark(X3)) | → | U61(X1, X2, X3) | U61(active(X1), X2, X3) | → | U61(X1, X2, X3) | |
| U61(X1, active(X2), X3) | → | U61(X1, X2, X3) | U61(X1, X2, active(X3)) | → | U61(X1, X2, X3) | |
| U62(mark(X1), X2, X3) | → | U62(X1, X2, X3) | U62(X1, mark(X2), X3) | → | U62(X1, X2, X3) | |
| U62(X1, X2, mark(X3)) | → | U62(X1, X2, X3) | U62(active(X1), X2, X3) | → | U62(X1, X2, X3) | |
| U62(X1, active(X2), X3) | → | U62(X1, X2, X3) | U62(X1, X2, active(X3)) | → | U62(X1, X2, X3) | |
| U63(mark(X1), X2, X3) | → | U63(X1, X2, X3) | U63(X1, mark(X2), X3) | → | U63(X1, X2, X3) | |
| U63(X1, X2, mark(X3)) | → | U63(X1, X2, X3) | U63(active(X1), X2, X3) | → | U63(X1, X2, X3) | |
| U63(X1, active(X2), X3) | → | U63(X1, X2, X3) | U63(X1, X2, active(X3)) | → | U63(X1, X2, X3) | |
| U64(mark(X1), X2, X3) | → | U64(X1, X2, X3) | U64(X1, mark(X2), X3) | → | U64(X1, X2, X3) | |
| U64(X1, X2, mark(X3)) | → | U64(X1, X2, X3) | U64(active(X1), X2, X3) | → | U64(X1, X2, X3) | |
| U64(X1, active(X2), X3) | → | U64(X1, X2, X3) | U64(X1, X2, active(X3)) | → | U64(X1, X2, X3) | |
| s(mark(X)) | → | s(X) | s(active(X)) | → | s(X) | |
| plus(mark(X1), X2) | → | plus(X1, X2) | plus(X1, mark(X2)) | → | plus(X1, X2) | |
| plus(active(X1), X2) | → | plus(X1, X2) | plus(X1, active(X2)) | → | plus(X1, X2) |
Termination of terms over the following signature is verified: isNat, U64, U63, U62, U61, U41, U23, U21, U22, plus, isNatKind, mark, 0, U14, U51, s, U15, tt, U16, U52, U11, active, U12, U13, U31, U32