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)].
| active#(U51(X1, X2)) | → | active#(X1) | proper#(U11(X1, X2, X3)) | → | proper#(X3) | |
| proper#(U15(X1, X2)) | → | proper#(X1) | active#(U15(tt, V2)) | → | U16#(isNat(V2)) | |
| U51#(mark(X1), X2) | → | U51#(X1, X2) | proper#(U11(X1, X2, X3)) | → | proper#(X2) | |
| top#(mark(X)) | → | proper#(X) | active#(U13(X1, X2, X3)) | → | active#(X1) | |
| active#(U62(X1, X2, X3)) | → | U62#(active(X1), X2, X3) | isNatKind#(ok(X)) | → | isNatKind#(X) | |
| active#(U31(tt, V2)) | → | U32#(isNatKind(V2)) | active#(U32(X)) | → | active#(X) | |
| active#(U21(tt, V1)) | → | isNatKind#(V1) | active#(U12(X1, X2, X3)) | → | active#(X1) | |
| active#(plus(X1, X2)) | → | active#(X2) | proper#(U23(X)) | → | U23#(proper(X)) | |
| proper#(U12(X1, X2, X3)) | → | proper#(X1) | proper#(U52(X1, X2)) | → | proper#(X1) | |
| proper#(isNatKind(X)) | → | isNatKind#(proper(X)) | active#(U15(tt, V2)) | → | isNat#(V2) | |
| active#(isNatKind(s(V1))) | → | U41#(isNatKind(V1)) | U15#(ok(X1), ok(X2)) | → | U15#(X1, X2) | |
| U32#(mark(X)) | → | U32#(X) | U14#(mark(X1), X2, X3) | → | U14#(X1, X2, X3) | |
| proper#(U16(X)) | → | U16#(proper(X)) | active#(U52(X1, X2)) | → | active#(X1) | |
| active#(U12(X1, X2, X3)) | → | U12#(active(X1), X2, X3) | active#(U12(tt, V1, V2)) | → | U13#(isNatKind(V2), V1, V2) | |
| U64#(ok(X1), ok(X2), ok(X3)) | → | U64#(X1, X2, X3) | U52#(ok(X1), ok(X2)) | → | U52#(X1, X2) | |
| active#(U31(X1, X2)) | → | active#(X1) | active#(U22(X1, X2)) | → | active#(X1) | |
| U61#(mark(X1), X2, X3) | → | U61#(X1, X2, X3) | proper#(U51(X1, X2)) | → | proper#(X2) | |
| proper#(U22(X1, X2)) | → | U22#(proper(X1), proper(X2)) | active#(U21(X1, X2)) | → | U21#(active(X1), X2) | |
| plus#(ok(X1), ok(X2)) | → | plus#(X1, X2) | proper#(isNat(X)) | → | proper#(X) | |
| U15#(mark(X1), X2) | → | U15#(X1, X2) | proper#(U63(X1, X2, X3)) | → | U63#(proper(X1), proper(X2), proper(X3)) | |
| U22#(ok(X1), ok(X2)) | → | U22#(X1, X2) | active#(isNat(s(V1))) | → | U21#(isNatKind(V1), V1) | |
| proper#(U13(X1, X2, X3)) | → | proper#(X1) | proper#(U31(X1, X2)) | → | U31#(proper(X1), proper(X2)) | |
| active#(U41(X)) | → | U41#(active(X)) | proper#(U21(X1, X2)) | → | proper#(X1) | |
| U31#(ok(X1), ok(X2)) | → | U31#(X1, X2) | proper#(U13(X1, X2, X3)) | → | U13#(proper(X1), proper(X2), proper(X3)) | |
| U52#(mark(X1), X2) | → | U52#(X1, X2) | active#(U22(X1, X2)) | → | U22#(active(X1), X2) | |
| active#(isNat(plus(V1, V2))) | → | U11#(isNatKind(V1), V1, V2) | active#(U21(tt, V1)) | → | U22#(isNatKind(V1), V1) | |
| proper#(U51(X1, X2)) | → | U51#(proper(X1), proper(X2)) | U16#(mark(X)) | → | U16#(X) | |
| active#(U51(X1, X2)) | → | U51#(active(X1), X2) | proper#(U14(X1, X2, X3)) | → | proper#(X1) | |
| proper#(plus(X1, X2)) | → | proper#(X1) | proper#(U16(X)) | → | proper#(X) | |
| U11#(mark(X1), X2, X3) | → | U11#(X1, X2, X3) | active#(U61(tt, M, N)) | → | U62#(isNatKind(M), M, N) | |
| proper#(U63(X1, X2, X3)) | → | proper#(X1) | active#(U22(tt, V1)) | → | U23#(isNat(V1)) | |
| proper#(U12(X1, X2, X3)) | → | proper#(X3) | proper#(s(X)) | → | proper#(X) | |
| active#(plus(X1, X2)) | → | active#(X1) | active#(U14(X1, X2, X3)) | → | active#(X1) | |
| active#(U13(X1, X2, X3)) | → | U13#(active(X1), X2, X3) | active#(U62(X1, X2, X3)) | → | active#(X1) | |
| active#(U63(X1, X2, X3)) | → | U63#(active(X1), X2, X3) | proper#(U31(X1, X2)) | → | proper#(X2) | |
| active#(U11(X1, X2, X3)) | → | U11#(active(X1), X2, X3) | active#(U16(X)) | → | U16#(active(X)) | |
| active#(U12(tt, V1, V2)) | → | isNatKind#(V2) | proper#(U51(X1, X2)) | → | proper#(X1) | |
| active#(isNat(plus(V1, V2))) | → | isNatKind#(V1) | proper#(U15(X1, X2)) | → | proper#(X2) | |
| proper#(U32(X)) | → | proper#(X) | proper#(plus(X1, X2)) | → | proper#(X2) | |
| active#(U63(tt, M, N)) | → | isNatKind#(N) | proper#(U63(X1, X2, X3)) | → | proper#(X2) | |
| proper#(U63(X1, X2, X3)) | → | proper#(X3) | U61#(ok(X1), ok(X2), ok(X3)) | → | U61#(X1, X2, X3) | |
| U64#(mark(X1), X2, X3) | → | U64#(X1, X2, X3) | proper#(U11(X1, X2, X3)) | → | U11#(proper(X1), proper(X2), proper(X3)) | |
| s#(mark(X)) | → | s#(X) | active#(s(X)) | → | active#(X) | |
| proper#(U41(X)) | → | proper#(X) | U14#(ok(X1), ok(X2), ok(X3)) | → | U14#(X1, X2, X3) | |
| U21#(ok(X1), ok(X2)) | → | U21#(X1, X2) | U63#(mark(X1), X2, X3) | → | U63#(X1, X2, X3) | |
| active#(U64(X1, X2, X3)) | → | active#(X1) | proper#(U62(X1, X2, X3)) | → | proper#(X3) | |
| active#(isNatKind(plus(V1, V2))) | → | isNatKind#(V1) | active#(U15(X1, X2)) | → | active#(X1) | |
| active#(U13(tt, V1, V2)) | → | U14#(isNatKind(V2), V1, V2) | proper#(isNatKind(X)) | → | proper#(X) | |
| active#(U62(tt, M, N)) | → | isNat#(N) | active#(plus(N, 0)) | → | isNat#(N) | |
| proper#(U23(X)) | → | proper#(X) | active#(U22(tt, V1)) | → | isNat#(V1) | |
| proper#(U13(X1, X2, X3)) | → | proper#(X2) | proper#(U64(X1, X2, X3)) | → | proper#(X3) | |
| U12#(mark(X1), X2, X3) | → | U12#(X1, X2, X3) | proper#(U61(X1, X2, X3)) | → | U61#(proper(X1), proper(X2), proper(X3)) | |
| isNat#(ok(X)) | → | isNat#(X) | active#(U61(tt, M, N)) | → | isNatKind#(M) | |
| active#(U51(tt, N)) | → | U52#(isNatKind(N), N) | active#(U11(tt, V1, V2)) | → | isNatKind#(V1) | |
| active#(isNat(s(V1))) | → | isNatKind#(V1) | U41#(ok(X)) | → | U41#(X) | |
| active#(U63(tt, M, N)) | → | U64#(isNatKind(N), M, N) | active#(U14(tt, V1, V2)) | → | U15#(isNat(V1), V2) | |
| proper#(U32(X)) | → | U32#(proper(X)) | proper#(U61(X1, X2, X3)) | → | proper#(X1) | |
| U11#(ok(X1), ok(X2), ok(X3)) | → | U11#(X1, X2, X3) | plus#(mark(X1), X2) | → | plus#(X1, X2) | |
| U13#(mark(X1), X2, X3) | → | U13#(X1, X2, X3) | proper#(U15(X1, X2)) | → | U15#(proper(X1), proper(X2)) | |
| active#(U61(X1, X2, X3)) | → | active#(X1) | active#(U15(X1, X2)) | → | U15#(active(X1), X2) | |
| U22#(mark(X1), X2) | → | U22#(X1, X2) | active#(U41(X)) | → | active#(X) | |
| active#(U52(X1, X2)) | → | U52#(active(X1), X2) | U13#(ok(X1), ok(X2), ok(X3)) | → | U13#(X1, X2, X3) | |
| top#(ok(X)) | → | active#(X) | proper#(U62(X1, X2, X3)) | → | U62#(proper(X1), proper(X2), proper(X3)) | |
| active#(plus(N, 0)) | → | U51#(isNat(N), N) | active#(U64(tt, M, N)) | → | s#(plus(N, M)) | |
| proper#(U13(X1, X2, X3)) | → | proper#(X3) | proper#(isNat(X)) | → | isNat#(proper(X)) | |
| U62#(mark(X1), X2, X3) | → | U62#(X1, X2, X3) | proper#(U64(X1, X2, X3)) | → | U64#(proper(X1), proper(X2), proper(X3)) | |
| U51#(ok(X1), ok(X2)) | → | U51#(X1, X2) | active#(U14(X1, X2, X3)) | → | U14#(active(X1), X2, X3) | |
| active#(U61(X1, X2, X3)) | → | U61#(active(X1), X2, X3) | proper#(U12(X1, X2, X3)) | → | proper#(X2) | |
| proper#(U12(X1, X2, X3)) | → | U12#(proper(X1), proper(X2), proper(X3)) | active#(s(X)) | → | s#(active(X)) | |
| active#(U62(tt, M, N)) | → | U63#(isNat(N), M, N) | s#(ok(X)) | → | s#(X) | |
| proper#(U11(X1, X2, X3)) | → | proper#(X1) | proper#(U14(X1, X2, X3)) | → | proper#(X3) | |
| proper#(U14(X1, X2, X3)) | → | proper#(X2) | active#(plus(N, s(M))) | → | isNat#(M) | |
| active#(U23(X)) | → | active#(X) | proper#(s(X)) | → | s#(proper(X)) | |
| active#(isNatKind(plus(V1, V2))) | → | U31#(isNatKind(V1), V2) | top#(ok(X)) | → | top#(active(X)) | |
| proper#(U31(X1, X2)) | → | proper#(X1) | U23#(mark(X)) | → | U23#(X) | |
| U32#(ok(X)) | → | U32#(X) | U41#(mark(X)) | → | U41#(X) | |
| proper#(U52(X1, X2)) | → | U52#(proper(X1), proper(X2)) | active#(U31(tt, V2)) | → | isNatKind#(V2) | |
| active#(plus(N, s(M))) | → | U61#(isNat(M), M, N) | active#(U13(tt, V1, V2)) | → | isNatKind#(V2) | |
| proper#(U62(X1, X2, X3)) | → | proper#(X2) | plus#(X1, mark(X2)) | → | plus#(X1, X2) | |
| active#(U23(X)) | → | U23#(active(X)) | proper#(plus(X1, X2)) | → | plus#(proper(X1), proper(X2)) | |
| top#(mark(X)) | → | top#(proper(X)) | proper#(U41(X)) | → | U41#(proper(X)) | |
| proper#(U14(X1, X2, X3)) | → | U14#(proper(X1), proper(X2), proper(X3)) | active#(U51(tt, N)) | → | isNatKind#(N) | |
| proper#(U22(X1, X2)) | → | proper#(X2) | proper#(U61(X1, X2, X3)) | → | proper#(X2) | |
| active#(U16(X)) | → | active#(X) | active#(U64(tt, M, N)) | → | plus#(N, M) | |
| active#(U11(X1, X2, X3)) | → | active#(X1) | U12#(ok(X1), ok(X2), ok(X3)) | → | U12#(X1, X2, X3) | |
| U63#(ok(X1), ok(X2), ok(X3)) | → | U63#(X1, X2, X3) | U62#(ok(X1), ok(X2), ok(X3)) | → | U62#(X1, X2, X3) | |
| proper#(U61(X1, X2, X3)) | → | proper#(X3) | proper#(U62(X1, X2, X3)) | → | proper#(X1) | |
| proper#(U21(X1, X2)) | → | proper#(X2) | proper#(U22(X1, X2)) | → | proper#(X1) | |
| proper#(U64(X1, X2, X3)) | → | proper#(X1) | active#(U31(X1, X2)) | → | U31#(active(X1), X2) | |
| active#(U63(X1, X2, X3)) | → | active#(X1) | active#(U14(tt, V1, V2)) | → | isNat#(V1) | |
| U23#(ok(X)) | → | U23#(X) | active#(isNatKind(s(V1))) | → | isNatKind#(V1) | |
| proper#(U21(X1, X2)) | → | U21#(proper(X1), proper(X2)) | active#(U32(X)) | → | U32#(active(X)) | |
| active#(U64(X1, X2, X3)) | → | U64#(active(X1), X2, X3) | active#(U11(tt, V1, V2)) | → | U12#(isNatKind(V1), V1, V2) | |
| proper#(U64(X1, X2, X3)) | → | proper#(X2) | U31#(mark(X1), X2) | → | U31#(X1, X2) | |
| proper#(U52(X1, X2)) | → | proper#(X2) | active#(plus(X1, X2)) | → | plus#(X1, active(X2)) | |
| active#(U21(X1, X2)) | → | active#(X1) | U16#(ok(X)) | → | U16#(X) | |
| U21#(mark(X1), X2) | → | U21#(X1, X2) | active#(plus(X1, X2)) | → | plus#(active(X1), X2) |
| 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)) | |
| active(U11(X1, X2, X3)) | → | U11(active(X1), X2, X3) | active(U12(X1, X2, X3)) | → | U12(active(X1), X2, X3) | |
| active(U13(X1, X2, X3)) | → | U13(active(X1), X2, X3) | active(U14(X1, X2, X3)) | → | U14(active(X1), X2, X3) | |
| active(U15(X1, X2)) | → | U15(active(X1), X2) | active(U16(X)) | → | U16(active(X)) | |
| active(U21(X1, X2)) | → | U21(active(X1), X2) | active(U22(X1, X2)) | → | U22(active(X1), X2) | |
| active(U23(X)) | → | U23(active(X)) | active(U31(X1, X2)) | → | U31(active(X1), X2) | |
| active(U32(X)) | → | U32(active(X)) | active(U41(X)) | → | U41(active(X)) | |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | active(U52(X1, X2)) | → | U52(active(X1), X2) | |
| active(U61(X1, X2, X3)) | → | U61(active(X1), X2, X3) | active(U62(X1, X2, X3)) | → | U62(active(X1), X2, X3) | |
| active(U63(X1, X2, X3)) | → | U63(active(X1), X2, X3) | active(U64(X1, X2, X3)) | → | U64(active(X1), X2, X3) | |
| active(s(X)) | → | s(active(X)) | active(plus(X1, X2)) | → | plus(active(X1), X2) | |
| active(plus(X1, X2)) | → | plus(X1, active(X2)) | U11(mark(X1), X2, X3) | → | mark(U11(X1, X2, X3)) | |
| U12(mark(X1), X2, X3) | → | mark(U12(X1, X2, X3)) | U13(mark(X1), X2, X3) | → | mark(U13(X1, X2, X3)) | |
| U14(mark(X1), X2, X3) | → | mark(U14(X1, X2, X3)) | U15(mark(X1), X2) | → | mark(U15(X1, X2)) | |
| U16(mark(X)) | → | mark(U16(X)) | U21(mark(X1), X2) | → | mark(U21(X1, X2)) | |
| U22(mark(X1), X2) | → | mark(U22(X1, X2)) | U23(mark(X)) | → | mark(U23(X)) | |
| U31(mark(X1), X2) | → | mark(U31(X1, X2)) | U32(mark(X)) | → | mark(U32(X)) | |
| U41(mark(X)) | → | mark(U41(X)) | U51(mark(X1), X2) | → | mark(U51(X1, X2)) | |
| U52(mark(X1), X2) | → | mark(U52(X1, X2)) | U61(mark(X1), X2, X3) | → | mark(U61(X1, X2, X3)) | |
| U62(mark(X1), X2, X3) | → | mark(U62(X1, X2, X3)) | U63(mark(X1), X2, X3) | → | mark(U63(X1, X2, X3)) | |
| U64(mark(X1), X2, X3) | → | mark(U64(X1, X2, X3)) | s(mark(X)) | → | mark(s(X)) | |
| plus(mark(X1), X2) | → | mark(plus(X1, X2)) | plus(X1, mark(X2)) | → | mark(plus(X1, X2)) | |
| proper(U11(X1, X2, X3)) | → | U11(proper(X1), proper(X2), proper(X3)) | proper(tt) | → | ok(tt) | |
| proper(U12(X1, X2, X3)) | → | U12(proper(X1), proper(X2), proper(X3)) | proper(isNatKind(X)) | → | isNatKind(proper(X)) | |
| proper(U13(X1, X2, X3)) | → | U13(proper(X1), proper(X2), proper(X3)) | proper(U14(X1, X2, X3)) | → | U14(proper(X1), proper(X2), proper(X3)) | |
| proper(U15(X1, X2)) | → | U15(proper(X1), proper(X2)) | proper(isNat(X)) | → | isNat(proper(X)) | |
| proper(U16(X)) | → | U16(proper(X)) | proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | |
| proper(U22(X1, X2)) | → | U22(proper(X1), proper(X2)) | proper(U23(X)) | → | U23(proper(X)) | |
| proper(U31(X1, X2)) | → | U31(proper(X1), proper(X2)) | proper(U32(X)) | → | U32(proper(X)) | |
| proper(U41(X)) | → | U41(proper(X)) | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) | |
| proper(U52(X1, X2)) | → | U52(proper(X1), proper(X2)) | proper(U61(X1, X2, X3)) | → | U61(proper(X1), proper(X2), proper(X3)) | |
| proper(U62(X1, X2, X3)) | → | U62(proper(X1), proper(X2), proper(X3)) | proper(U63(X1, X2, X3)) | → | U63(proper(X1), proper(X2), proper(X3)) | |
| proper(U64(X1, X2, X3)) | → | U64(proper(X1), proper(X2), proper(X3)) | proper(s(X)) | → | s(proper(X)) | |
| proper(plus(X1, X2)) | → | plus(proper(X1), proper(X2)) | proper(0) | → | ok(0) | |
| U11(ok(X1), ok(X2), ok(X3)) | → | ok(U11(X1, X2, X3)) | U12(ok(X1), ok(X2), ok(X3)) | → | ok(U12(X1, X2, X3)) | |
| isNatKind(ok(X)) | → | ok(isNatKind(X)) | U13(ok(X1), ok(X2), ok(X3)) | → | ok(U13(X1, X2, X3)) | |
| U14(ok(X1), ok(X2), ok(X3)) | → | ok(U14(X1, X2, X3)) | U15(ok(X1), ok(X2)) | → | ok(U15(X1, X2)) | |
| isNat(ok(X)) | → | ok(isNat(X)) | U16(ok(X)) | → | ok(U16(X)) | |
| U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) | U22(ok(X1), ok(X2)) | → | ok(U22(X1, X2)) | |
| U23(ok(X)) | → | ok(U23(X)) | U31(ok(X1), ok(X2)) | → | ok(U31(X1, X2)) | |
| U32(ok(X)) | → | ok(U32(X)) | U41(ok(X)) | → | ok(U41(X)) | |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | U52(ok(X1), ok(X2)) | → | ok(U52(X1, X2)) | |
| U61(ok(X1), ok(X2), ok(X3)) | → | ok(U61(X1, X2, X3)) | U62(ok(X1), ok(X2), ok(X3)) | → | ok(U62(X1, X2, X3)) | |
| U63(ok(X1), ok(X2), ok(X3)) | → | ok(U63(X1, X2, X3)) | U64(ok(X1), ok(X2), ok(X3)) | → | ok(U64(X1, X2, X3)) | |
| s(ok(X)) | → | ok(s(X)) | plus(ok(X1), ok(X2)) | → | ok(plus(X1, X2)) | |
| top(mark(X)) | → | top(proper(X)) | top(ok(X)) | → | top(active(X)) |
Termination of terms over the following signature is verified: isNat, U64, U63, U62, U61, U41, ok, proper, U23, U21, top, U22, plus, isNatKind, mark, 0, U14, U51, s, U15, tt, U16, U52, U11, active, U12, U13, U31, U32