TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60008 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (26219ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 6 was processed with processor DependencyGraph (4ms).
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (199ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (192ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (205ms), ReductionPairSAT (timeout)].
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (3430ms), PolynomialLinearRange4iUR (18ms), DependencyGraph (3470ms), PolynomialLinearRange8NegiUR (71ms), DependencyGraph (3439ms)].
| – Problem 5 was processed with processor SubtermCriterion (6ms).
| | – Problem 7 was processed with processor DependencyGraph (29ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| a__U83#(tt, V1, V2) | → | a__U84#(a__isNatIListKind(V2), V1, V2) | | a__U22#(tt, V1) | → | a__isNat#(V1) |
| a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1), V1) | | a__U82#(tt, V1, V2) | → | a__U83#(a__isNatIListKind(V2), V1, V2) |
| a__U11#(tt, V1) | → | a__U12#(a__isNatIListKind(V1), V1) | | a__U84#(tt, V1, V2) | → | a__isNat#(V1) |
| a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1), V1) | | a__U84#(tt, V1, V2) | → | a__U85#(a__isNat(V1), V2) |
| a__isNatList#(cons(V1, V2)) | → | a__U81#(a__isNatKind(V1), V1, V2) | | a__U81#(tt, V1, V2) | → | a__U82#(a__isNatKind(V1), V1, V2) |
| a__U21#(tt, V1) | → | a__U22#(a__isNatKind(V1), V1) | | a__U12#(tt, V1) | → | a__isNatList#(V1) |
| a__U85#(tt, V2) | → | a__isNatList#(V2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, isNatKind, a__U84, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U83, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, a__U94, a__U23, length, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, U51, s, isNatList, tt, U82, U81, U52, a__U13, U11, a__U12, U12, a__U11, U13, a__U61, a__isNatKind, nil
Open Dependency Pair Problem 4
Dependency Pairs
| mark#(U11(X1, X2)) | → | mark#(X1) | | mark#(U91(X1, X2, X3)) | → | mark#(X1) |
| mark#(U84(X1, X2, X3)) | → | mark#(X1) | | mark#(U43(X1, X2, X3)) | → | mark#(X1) |
| mark#(U92(X1, X2, X3)) | → | a__U92#(mark(X1), X2, X3) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U33(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U85(X1, X2)) | → | mark#(X1) | | mark#(U81(X1, X2, X3)) | → | mark#(X1) |
| mark#(U44(X1, X2, X3)) | → | mark#(X1) | | mark#(U94(X1, X2)) | → | mark#(X1) |
| a__U93#(tt, L, N) | → | a__U94#(a__isNatKind(N), L) | | mark#(U86(X)) | → | mark#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | mark#(U94(X1, X2)) | → | a__U94#(mark(X1), X2) |
| mark#(U23(X)) | → | mark#(X) | | mark#(U83(X1, X2, X3)) | → | mark#(X1) |
| mark#(U22(X1, X2)) | → | mark#(X1) | | a__length#(cons(N, L)) | → | a__U91#(a__isNatList(L), L, N) |
| mark#(length(X)) | → | mark#(X) | | mark#(U31(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | mark#(U61(X)) | → | mark#(X) |
| mark#(U12(X1, X2)) | → | mark#(X1) | | mark#(U92(X1, X2, X3)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3)) | → | a__U93#(mark(X1), X2, X3) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U42(X1, X2, X3)) | → | mark#(X1) | | mark#(U82(X1, X2, X3)) | → | mark#(X1) |
| mark#(U52(X)) | → | mark#(X) | | a__U94#(tt, L) | → | mark#(L) |
| a__U92#(tt, L, N) | → | a__U93#(a__isNat(N), L, N) | | a__U91#(tt, L, N) | → | a__U92#(a__isNatIListKind(L), L, N) |
| mark#(U41(X1, X2, X3)) | → | mark#(X1) | | mark#(U91(X1, X2, X3)) | → | a__U91#(mark(X1), X2, X3) |
| mark#(U32(X1, X2)) | → | mark#(X1) | | mark#(U93(X1, X2, X3)) | → | mark#(X1) |
| a__U94#(tt, L) | → | a__length#(mark(L)) | | mark#(U46(X)) | → | mark#(X) |
| mark#(U71(X)) | → | mark#(X) | | mark#(U13(X)) | → | mark#(X) |
| mark#(U45(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, isNatKind, a__U84, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U83, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, a__U94, a__U23, length, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, U51, s, isNatList, tt, U82, U81, U52, a__U13, U11, a__U12, U12, a__U11, U13, a__U61, a__isNatKind, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(U11(X1, X2)) | → | mark#(X1) | | mark#(isNatIList(X)) | → | a__isNatIList#(X) |
| mark#(U84(X1, X2, X3)) | → | mark#(X1) | | mark#(U92(X1, X2, X3)) | → | a__U92#(mark(X1), X2, X3) |
| mark#(U46(X)) | → | a__U46#(mark(X)) | | mark#(U85(X1, X2)) | → | mark#(X1) |
| a__isNatKind#(s(V1)) | → | a__U71#(a__isNatKind(V1)) | | a__U93#(tt, L, N) | → | a__U94#(a__isNatKind(N), L) |
| mark#(U94(X1, X2)) | → | mark#(X1) | | mark#(U23(X)) | → | a__U23#(mark(X)) |
| mark#(U13(X)) | → | a__U13#(mark(X)) | | a__length#(cons(N, L)) | → | a__U91#(a__isNatList(L), L, N) |
| a__U82#(tt, V1, V2) | → | a__isNatIListKind#(V2) | | a__U41#(tt, V1, V2) | → | a__U42#(a__isNatKind(V1), V1, V2) |
| mark#(s(X)) | → | mark#(X) | | a__U81#(tt, V1, V2) | → | a__U82#(a__isNatKind(V1), V1, V2) |
| mark#(U12(X1, X2)) | → | mark#(X1) | | a__U12#(tt, V1) | → | a__U13#(a__isNatList(V1)) |
| a__U51#(tt, V2) | → | a__U52#(a__isNatIListKind(V2)) | | a__U44#(tt, V1, V2) | → | a__U45#(a__isNat(V1), V2) |
| mark#(U93(X1, X2, X3)) | → | a__U93#(mark(X1), X2, X3) | | a__U22#(tt, V1) | → | a__isNat#(V1) |
| a__U43#(tt, V1, V2) | → | a__isNatIListKind#(V2) | | a__isNatIList#(V) | → | a__U31#(a__isNatIListKind(V), V) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U42(X1, X2, X3)) | → | mark#(X1) |
| a__U31#(tt, V) | → | a__U32#(a__isNatIListKind(V), V) | | mark#(U82(X1, X2, X3)) | → | mark#(X1) |
| mark#(U52(X)) | → | mark#(X) | | a__U84#(tt, V1, V2) | → | a__isNat#(V1) |
| mark#(U41(X1, X2, X3)) | → | mark#(X1) | | mark#(U32(X1, X2)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3)) | → | mark#(X1) | | a__U85#(tt, V2) | → | a__isNatList#(V2) |
| mark#(U45(X1, X2)) | → | mark#(X1) | | a__U41#(tt, V1, V2) | → | a__isNatKind#(V1) |
| mark#(isNat(X)) | → | a__isNat#(X) | | a__U81#(tt, V1, V2) | → | a__isNatKind#(V1) |
| a__U83#(tt, V1, V2) | → | a__U84#(a__isNatIListKind(V2), V1, V2) | | a__isNat#(length(V1)) | → | a__isNatIListKind#(V1) |
| mark#(U91(X1, X2, X3)) | → | mark#(X1) | | mark#(U43(X1, X2, X3)) | → | mark#(X1) |
| mark#(zeros) | → | a__zeros# | | mark#(U86(X)) | → | a__U86#(mark(X)) |
| a__isNatIListKind#(cons(V1, V2)) | → | a__isNatKind#(V1) | | a__U82#(tt, V1, V2) | → | a__U83#(a__isNatIListKind(V2), V1, V2) |
| mark#(U41(X1, X2, X3)) | → | a__U41#(mark(X1), X2, X3) | | mark#(U33(X)) | → | mark#(X) |
| a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | | mark#(U81(X1, X2, X3)) | → | mark#(X1) |
| mark#(length(X)) | → | a__length#(mark(X)) | | a__U11#(tt, V1) | → | a__isNatIListKind#(V1) |
| mark#(U94(X1, X2)) | → | a__U94#(mark(X1), X2) | | a__U51#(tt, V2) | → | a__isNatIListKind#(V2) |
| mark#(U22(X1, X2)) | → | mark#(X1) | | mark#(U23(X)) | → | mark#(X) |
| a__U83#(tt, V1, V2) | → | a__isNatIListKind#(V2) | | a__U21#(tt, V1) | → | a__isNatKind#(V1) |
| a__U84#(tt, V1, V2) | → | a__U85#(a__isNat(V1), V2) | | mark#(length(X)) | → | mark#(X) |
| mark#(U61(X)) | → | mark#(X) | | mark#(U61(X)) | → | a__U61#(mark(X)) |
| a__U12#(tt, V1) | → | a__isNatList#(V1) | | a__U32#(tt, V) | → | a__U33#(a__isNatList(V)) |
| a__length#(cons(N, L)) | → | a__isNatList#(L) | | mark#(U45(X1, X2)) | → | a__U45#(mark(X1), X2) |
| mark#(U51(X1, X2)) | → | a__U51#(mark(X1), X2) | | a__isNatKind#(length(V1)) | → | a__U61#(a__isNatIListKind(V1)) |
| mark#(U92(X1, X2, X3)) | → | mark#(X1) | | a__isNat#(length(V1)) | → | a__U11#(a__isNatIListKind(V1), V1) |
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNatKind(V1), V1, V2) | | a__U94#(tt, L) | → | mark#(L) |
| a__isNat#(s(V1)) | → | a__U21#(a__isNatKind(V1), V1) | | mark#(U52(X)) | → | a__U52#(mark(X)) |
| mark#(U44(X1, X2, X3)) | → | a__U44#(mark(X1), X2, X3) | | mark#(U71(X)) | → | mark#(X) |
| mark#(U71(X)) | → | a__U71#(mark(X)) | | a__U32#(tt, V) | → | a__isNatList#(V) |
| a__U45#(tt, V2) | → | a__isNatIList#(V2) | | mark#(isNatIListKind(X)) | → | a__isNatIListKind#(X) |
| mark#(U22(X1, X2)) | → | a__U22#(mark(X1), X2) | | a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) |
| a__isNatList#(cons(V1, V2)) | → | a__U81#(a__isNatKind(V1), V1, V2) | | mark#(U85(X1, X2)) | → | a__U85#(mark(X1), X2) |
| mark#(U31(X1, X2)) | → | mark#(X1) | | mark#(U32(X1, X2)) | → | a__U32#(mark(X1), X2) |
| mark#(U84(X1, X2, X3)) | → | a__U84#(mark(X1), X2, X3) | | a__U92#(tt, L, N) | → | a__isNat#(N) |
| a__U22#(tt, V1) | → | a__U23#(a__isNat(V1)) | | a__isNatList#(cons(V1, V2)) | → | a__isNatKind#(V1) |
| mark#(U33(X)) | → | a__U33#(mark(X)) | | a__isNat#(s(V1)) | → | a__isNatKind#(V1) |
| a__U11#(tt, V1) | → | a__U12#(a__isNatIListKind(V1), V1) | | mark#(isNatList(X)) | → | a__isNatList#(X) |
| a__U42#(tt, V1, V2) | → | a__isNatIListKind#(V2) | | mark#(U12(X1, X2)) | → | a__U12#(mark(X1), X2) |
| mark#(U42(X1, X2, X3)) | → | a__U42#(mark(X1), X2, X3) | | a__U94#(tt, L) | → | a__length#(mark(L)) |
| mark#(U46(X)) | → | mark#(X) | | a__U21#(tt, V1) | → | a__U22#(a__isNatKind(V1), V1) |
| a__U85#(tt, V2) | → | a__U86#(a__isNatList(V2)) | | a__U43#(tt, V1, V2) | → | a__U44#(a__isNatIListKind(V2), V1, V2) |
| mark#(U83(X1, X2, X3)) | → | a__U83#(mark(X1), X2, X3) | | a__isNatIList#(V) | → | a__isNatIListKind#(V) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | mark#(U31(X1, X2)) | → | a__U31#(mark(X1), X2) |
| a__U93#(tt, L, N) | → | a__isNatKind#(N) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U44(X1, X2, X3)) | → | mark#(X1) | | mark#(U86(X)) | → | mark#(X) |
| mark#(U83(X1, X2, X3)) | → | mark#(X1) | | mark#(U82(X1, X2, X3)) | → | a__U82#(mark(X1), X2, X3) |
| a__isNatIList#(cons(V1, V2)) | → | a__isNatKind#(V1) | | a__U44#(tt, V1, V2) | → | a__isNat#(V1) |
| a__isNatIListKind#(cons(V1, V2)) | → | a__U51#(a__isNatKind(V1), V2) | | a__U45#(tt, V2) | → | a__U46#(a__isNatIList(V2)) |
| a__U31#(tt, V) | → | a__isNatIListKind#(V) | | a__U42#(tt, V1, V2) | → | a__U43#(a__isNatIListKind(V2), V1, V2) |
| a__U91#(tt, L, N) | → | a__isNatIListKind#(L) | | a__U92#(tt, L, N) | → | a__U93#(a__isNat(N), L, N) |
| a__U91#(tt, L, N) | → | a__U92#(a__isNatIListKind(L), L, N) | | mark#(U21(X1, X2)) | → | a__U21#(mark(X1), X2) |
| mark#(U91(X1, X2, X3)) | → | a__U91#(mark(X1), X2, X3) | | mark#(U43(X1, X2, X3)) | → | a__U43#(mark(X1), X2, X3) |
| mark#(isNatKind(X)) | → | a__isNatKind#(X) | | mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) |
| mark#(U81(X1, X2, X3)) | → | a__U81#(mark(X1), X2, X3) | | mark#(U13(X)) | → | mark#(X) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, a__U84, isNatKind, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U83, a__U32, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, a__U93, U91, a__U94, length, a__U23, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, isNatList, s, U51, tt, U82, U52, U81, U11, a__U13, U12, a__U12, U13, a__U11, a__U61, nil, a__isNatKind
Strategy
The following SCCs where found
| a__U45#(tt, V2) → a__isNatIList#(V2) | a__U42#(tt, V1, V2) → a__U43#(a__isNatIListKind(V2), V1, V2) |
| a__U43#(tt, V1, V2) → a__U44#(a__isNatIListKind(V2), V1, V2) | a__U44#(tt, V1, V2) → a__U45#(a__isNat(V1), V2) |
| a__U41#(tt, V1, V2) → a__U42#(a__isNatKind(V1), V1, V2) | a__isNatIList#(cons(V1, V2)) → a__U41#(a__isNatKind(V1), V1, V2) |
| mark#(U11(X1, X2)) → mark#(X1) | mark#(U91(X1, X2, X3)) → mark#(X1) |
| mark#(U84(X1, X2, X3)) → mark#(X1) | mark#(U92(X1, X2, X3)) → a__U92#(mark(X1), X2, X3) |
| mark#(U43(X1, X2, X3)) → mark#(X1) | mark#(U21(X1, X2)) → mark#(X1) |
| mark#(U33(X)) → mark#(X) | mark#(U51(X1, X2)) → mark#(X1) |
| mark#(U44(X1, X2, X3)) → mark#(X1) | mark#(U81(X1, X2, X3)) → mark#(X1) |
| mark#(U85(X1, X2)) → mark#(X1) | a__U93#(tt, L, N) → a__U94#(a__isNatKind(N), L) |
| mark#(U94(X1, X2)) → mark#(X1) | mark#(length(X)) → a__length#(mark(X)) |
| mark#(U86(X)) → mark#(X) | mark#(U94(X1, X2)) → a__U94#(mark(X1), X2) |
| mark#(U22(X1, X2)) → mark#(X1) | mark#(U83(X1, X2, X3)) → mark#(X1) |
| mark#(U23(X)) → mark#(X) | a__length#(cons(N, L)) → a__U91#(a__isNatList(L), L, N) |
| mark#(length(X)) → mark#(X) | mark#(U31(X1, X2)) → mark#(X1) |
| mark#(s(X)) → mark#(X) | mark#(U61(X)) → mark#(X) |
| mark#(U12(X1, X2)) → mark#(X1) | mark#(U92(X1, X2, X3)) → mark#(X1) |
| mark#(U93(X1, X2, X3)) → a__U93#(mark(X1), X2, X3) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(U42(X1, X2, X3)) → mark#(X1) | mark#(U82(X1, X2, X3)) → mark#(X1) |
| mark#(U52(X)) → mark#(X) | a__U94#(tt, L) → mark#(L) |
| a__U92#(tt, L, N) → a__U93#(a__isNat(N), L, N) | a__U91#(tt, L, N) → a__U92#(a__isNatIListKind(L), L, N) |
| mark#(U41(X1, X2, X3)) → mark#(X1) | mark#(U91(X1, X2, X3)) → a__U91#(mark(X1), X2, X3) |
| mark#(U93(X1, X2, X3)) → mark#(X1) | mark#(U32(X1, X2)) → mark#(X1) |
| a__U94#(tt, L) → a__length#(mark(L)) | mark#(U46(X)) → mark#(X) |
| mark#(U71(X)) → mark#(X) | mark#(U45(X1, X2)) → mark#(X1) |
| mark#(U13(X)) → mark#(X) |
| a__U51#(tt, V2) → a__isNatIListKind#(V2) | a__isNatIListKind#(cons(V1, V2)) → a__isNatKind#(V1) |
| a__isNatIListKind#(cons(V1, V2)) → a__U51#(a__isNatKind(V1), V2) | a__isNatKind#(s(V1)) → a__isNatKind#(V1) |
| a__isNatKind#(length(V1)) → a__isNatIListKind#(V1) |
| a__U83#(tt, V1, V2) → a__U84#(a__isNatIListKind(V2), V1, V2) | a__isNat#(length(V1)) → a__U11#(a__isNatIListKind(V1), V1) |
| a__U22#(tt, V1) → a__isNat#(V1) | a__U82#(tt, V1, V2) → a__U83#(a__isNatIListKind(V2), V1, V2) |
| a__U11#(tt, V1) → a__U12#(a__isNatIListKind(V1), V1) | a__U84#(tt, V1, V2) → a__isNat#(V1) |
| a__isNat#(s(V1)) → a__U21#(a__isNatKind(V1), V1) | a__U84#(tt, V1, V2) → a__U85#(a__isNat(V1), V2) |
| a__isNatList#(cons(V1, V2)) → a__U81#(a__isNatKind(V1), V1, V2) | a__U81#(tt, V1, V2) → a__U82#(a__isNatKind(V1), V1, V2) |
| a__U12#(tt, V1) → a__isNatList#(V1) | a__U21#(tt, V1) → a__U22#(a__isNatKind(V1), V1) |
| a__U85#(tt, V2) → a__isNatList#(V2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__U51#(tt, V2) | → | a__isNatIListKind#(V2) | | a__isNatIListKind#(cons(V1, V2)) | → | a__isNatKind#(V1) |
| a__isNatIListKind#(cons(V1, V2)) | → | a__U51#(a__isNatKind(V1), V2) | | a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) |
| a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, a__U84, isNatKind, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U83, a__U32, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, a__U93, U91, a__U94, length, a__U23, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, isNatList, s, U51, tt, U82, U52, U81, U11, a__U13, U12, a__U12, U13, a__U11, a__U61, nil, a__isNatKind
Strategy
Projection
The following projection was used:
- π (a__U51#): 2
- π (a__isNatIListKind#): 1
- π (a__isNatKind#): 1
Thus, the following dependency pairs are removed:
| a__isNatIListKind#(cons(V1, V2)) | → | a__isNatKind#(V1) | | a__isNatIListKind#(cons(V1, V2)) | → | a__U51#(a__isNatKind(V1), V2) |
| a__isNatKind#(s(V1)) | → | a__isNatKind#(V1) | | a__isNatKind#(length(V1)) | → | a__isNatIListKind#(V1) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U51#(tt, V2) | → | a__isNatIListKind#(V2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, isNatKind, a__U84, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U83, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, a__U94, a__U23, length, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, U51, s, isNatList, tt, U82, U81, U52, a__U13, U11, a__U12, U12, a__U11, U13, a__U61, a__isNatKind, nil
Strategy
There are no SCCs!
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__U45#(tt, V2) | → | a__isNatIList#(V2) | | a__U42#(tt, V1, V2) | → | a__U43#(a__isNatIListKind(V2), V1, V2) |
| a__U43#(tt, V1, V2) | → | a__U44#(a__isNatIListKind(V2), V1, V2) | | a__U44#(tt, V1, V2) | → | a__U45#(a__isNat(V1), V2) |
| a__U41#(tt, V1, V2) | → | a__U42#(a__isNatKind(V1), V1, V2) | | a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNatKind(V1), V1, V2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, a__U84, isNatKind, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U83, a__U32, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, a__U93, U91, a__U94, length, a__U23, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, isNatList, s, U51, tt, U82, U52, U81, U11, a__U13, U12, a__U12, U13, a__U11, a__U61, nil, a__isNatKind
Strategy
Projection
The following projection was used:
- π (a__U44#): 3
- π (a__U41#): 3
- π (a__U42#): 3
- π (a__U45#): 2
- π (a__isNatIList#): 1
- π (a__U43#): 3
Thus, the following dependency pairs are removed:
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNatKind(V1), V1, V2) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U45#(tt, V2) | → | a__isNatIList#(V2) | | a__U42#(tt, V1, V2) | → | a__U43#(a__isNatIListKind(V2), V1, V2) |
| a__U43#(tt, V1, V2) | → | a__U44#(a__isNatIListKind(V2), V1, V2) | | a__U44#(tt, V1, V2) | → | a__U45#(a__isNat(V1), V2) |
| a__U41#(tt, V1, V2) | → | a__U42#(a__isNatKind(V1), V1, V2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, V1) | → | a__U12(a__isNatIListKind(V1), V1) |
| a__U12(tt, V1) | → | a__U13(a__isNatList(V1)) | | a__U13(tt) | → | tt |
| a__U21(tt, V1) | → | a__U22(a__isNatKind(V1), V1) | | a__U22(tt, V1) | → | a__U23(a__isNat(V1)) |
| a__U23(tt) | → | tt | | a__U31(tt, V) | → | a__U32(a__isNatIListKind(V), V) |
| a__U32(tt, V) | → | a__U33(a__isNatList(V)) | | a__U33(tt) | → | tt |
| a__U41(tt, V1, V2) | → | a__U42(a__isNatKind(V1), V1, V2) | | a__U42(tt, V1, V2) | → | a__U43(a__isNatIListKind(V2), V1, V2) |
| a__U43(tt, V1, V2) | → | a__U44(a__isNatIListKind(V2), V1, V2) | | a__U44(tt, V1, V2) | → | a__U45(a__isNat(V1), V2) |
| a__U45(tt, V2) | → | a__U46(a__isNatIList(V2)) | | a__U46(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatIListKind(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt) | → | tt | | a__U71(tt) | → | tt |
| a__U81(tt, V1, V2) | → | a__U82(a__isNatKind(V1), V1, V2) | | a__U82(tt, V1, V2) | → | a__U83(a__isNatIListKind(V2), V1, V2) |
| a__U83(tt, V1, V2) | → | a__U84(a__isNatIListKind(V2), V1, V2) | | a__U84(tt, V1, V2) | → | a__U85(a__isNat(V1), V2) |
| a__U85(tt, V2) | → | a__U86(a__isNatList(V2)) | | a__U86(tt) | → | tt |
| a__U91(tt, L, N) | → | a__U92(a__isNatIListKind(L), L, N) | | a__U92(tt, L, N) | → | a__U93(a__isNat(N), L, N) |
| a__U93(tt, L, N) | → | a__U94(a__isNatKind(N), L) | | a__U94(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatIListKind(V1), V1) |
| a__isNat(s(V1)) | → | a__U21(a__isNatKind(V1), V1) | | a__isNatIList(V) | → | a__U31(a__isNatIListKind(V), V) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNatKind(V1), V1, V2) |
| a__isNatIListKind(nil) | → | tt | | a__isNatIListKind(zeros) | → | tt |
| a__isNatIListKind(cons(V1, V2)) | → | a__U51(a__isNatKind(V1), V2) | | a__isNatKind(0) | → | tt |
| a__isNatKind(length(V1)) | → | a__U61(a__isNatIListKind(V1)) | | a__isNatKind(s(V1)) | → | a__U71(a__isNatKind(V1)) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U81(a__isNatKind(V1), V1, V2) |
| a__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U91(a__isNatList(L), L, N) |
| mark(zeros) | → | a__zeros | | mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) |
| mark(U12(X1, X2)) | → | a__U12(mark(X1), X2) | | mark(isNatIListKind(X)) | → | a__isNatIListKind(X) |
| mark(U13(X)) | → | a__U13(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) |
| mark(isNatKind(X)) | → | a__isNatKind(X) | | mark(U23(X)) | → | a__U23(mark(X)) |
| mark(isNat(X)) | → | a__isNat(X) | | mark(U31(X1, X2)) | → | a__U31(mark(X1), X2) |
| mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | | mark(U33(X)) | → | a__U33(mark(X)) |
| mark(U41(X1, X2, X3)) | → | a__U41(mark(X1), X2, X3) | | mark(U42(X1, X2, X3)) | → | a__U42(mark(X1), X2, X3) |
| mark(U43(X1, X2, X3)) | → | a__U43(mark(X1), X2, X3) | | mark(U44(X1, X2, X3)) | → | a__U44(mark(X1), X2, X3) |
| mark(U45(X1, X2)) | → | a__U45(mark(X1), X2) | | mark(U46(X)) | → | a__U46(mark(X)) |
| mark(isNatIList(X)) | → | a__isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X)) | → | a__U71(mark(X)) | | mark(U81(X1, X2, X3)) | → | a__U81(mark(X1), X2, X3) |
| mark(U82(X1, X2, X3)) | → | a__U82(mark(X1), X2, X3) | | mark(U83(X1, X2, X3)) | → | a__U83(mark(X1), X2, X3) |
| mark(U84(X1, X2, X3)) | → | a__U84(mark(X1), X2, X3) | | mark(U85(X1, X2)) | → | a__U85(mark(X1), X2) |
| mark(U86(X)) | → | a__U86(mark(X)) | | mark(U91(X1, X2, X3)) | → | a__U91(mark(X1), X2, X3) |
| mark(U92(X1, X2, X3)) | → | a__U92(mark(X1), X2, X3) | | mark(U93(X1, X2, X3)) | → | a__U93(mark(X1), X2, X3) |
| mark(U94(X1, X2)) | → | a__U94(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__U12(X1, X2) | → | U12(X1, X2) |
| a__isNatIListKind(X) | → | isNatIListKind(X) | | a__U13(X) | → | U13(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X1, X2) | → | U22(X1, X2) | | a__isNatKind(X) | → | isNatKind(X) |
| a__U23(X) | → | U23(X) | | a__isNat(X) | → | isNat(X) |
| a__U31(X1, X2) | → | U31(X1, X2) | | a__U32(X1, X2) | → | U32(X1, X2) |
| a__U33(X) | → | U33(X) | | a__U41(X1, X2, X3) | → | U41(X1, X2, X3) |
| a__U42(X1, X2, X3) | → | U42(X1, X2, X3) | | a__U43(X1, X2, X3) | → | U43(X1, X2, X3) |
| a__U44(X1, X2, X3) | → | U44(X1, X2, X3) | | a__U45(X1, X2) | → | U45(X1, X2) |
| a__U46(X) | → | U46(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X) | → | U71(X) |
| a__U81(X1, X2, X3) | → | U81(X1, X2, X3) | | a__U82(X1, X2, X3) | → | U82(X1, X2, X3) |
| a__U83(X1, X2, X3) | → | U83(X1, X2, X3) | | a__U84(X1, X2, X3) | → | U84(X1, X2, X3) |
| a__U85(X1, X2) | → | U85(X1, X2) | | a__U86(X) | → | U86(X) |
| a__U91(X1, X2, X3) | → | U91(X1, X2, X3) | | a__U92(X1, X2, X3) | → | U92(X1, X2, X3) |
| a__U93(X1, X2, X3) | → | U93(X1, X2, X3) | | a__U94(X1, X2) | → | U94(X1, X2) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: U61, a__U41, a__U43, a__U42, a__U71, U23, a__U45, a__U44, U21, U22, a__U46, isNatIList, a__U86, isNatKind, a__U84, a__U85, mark, U71, 0, a__isNatIList, zeros, a__isNat, a__U32, a__U83, a__U31, a__U82, a__U81, U31, U32, U33, a__U33, a__U51, a__U52, isNatIListKind, U94, a__isNatIListKind, U46, isNat, U45, a__isNatList, U44, U43, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, a__U94, a__U23, length, a__U22, a__U21, cons, a__zeros, a__length, U83, U84, U85, U86, U51, s, isNatList, tt, U82, U81, U52, a__U13, U11, a__U12, U12, a__U11, U13, a__U61, a__isNatKind, nil
Strategy
There are no SCCs!