YES
The TRS could be proven terminating. The proof took 44616 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1447ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (907ms).
| | – Problem 5 was processed with processor DependencyGraph (162ms).
| | | – Problem 6 was processed with processor PolynomialLinearRange4 (267ms).
| | | | – Problem 8 was processed with processor DependencyGraph (1ms).
| | | – Problem 7 was processed with processor PolynomialLinearRange4 (340ms).
| | | | – Problem 9 was processed with processor DependencyGraph (85ms).
| | | | | – Problem 10 was processed with processor PolynomialLinearRange4 (197ms).
| | | | | | – Problem 11 was processed with processor DependencyGraph (45ms).
| | | | | | | – Problem 12 was processed with processor PolynomialLinearRange4 (39ms).
| | | | | | | | – Problem 13 was processed with processor PolynomialLinearRange4 (9ms).
| – Problem 3 was processed with processor SubtermCriterion (4ms).
| | – Problem 4 was processed with processor DependencyGraph (10ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U91#(tt, IL, M, N) | → | a__U92#(a__isNat(M), IL, M, N) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(U62(X)) | → | a__U62#(mark(X)) | | mark#(isNatIList(X)) | → | a__isNatIList#(X) |
| mark#(U31(X)) | → | a__U31#(mark(X)) | | a__length#(cons(N, L)) | → | a__U71#(a__isNatList(L), L, N) |
| a__isNatList#(cons(V1, V2)) | → | a__U51#(a__isNat(V1), V2) | | a__U51#(tt, V2) | → | a__isNatList#(V2) |
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) | | a__isNatIList#(V) | → | a__isNatList#(V) |
| mark#(U81(X)) | → | mark#(X) | | mark#(U21(X)) | → | a__U21#(mark(X)) |
| mark#(U41(X1, X2)) | → | a__U41#(mark(X1), X2) | | a__U71#(tt, L, N) | → | a__U72#(a__isNat(N), L) |
| mark#(U92(X1, X2, X3, X4)) | → | a__U92#(mark(X1), X2, X3, X4) | | a__take#(s(M), cons(N, IL)) | → | a__U91#(a__isNatIList(IL), IL, M, N) |
| mark#(s(X)) | → | mark#(X) | | a__take#(0, IL) | → | a__isNatIList#(IL) |
| a__U92#(tt, IL, M, N) | → | a__U93#(a__isNat(N), IL, M, N) | | a__isNatList#(take(V1, V2)) | → | a__U61#(a__isNat(V1), V2) |
| mark#(U71(X1, X2, X3)) | → | mark#(X1) | | mark#(U72(X1, X2)) | → | mark#(X1) |
| a__U41#(tt, V2) | → | a__isNatIList#(V2) | | a__isNatList#(take(V1, V2)) | → | a__isNat#(V1) |
| a__U91#(tt, IL, M, N) | → | a__isNat#(M) | | a__take#(0, IL) | → | a__U81#(a__isNatIList(IL)) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) |
| a__U71#(tt, L, N) | → | a__isNat#(N) | | mark#(U52(X)) | → | mark#(X) |
| mark#(isNatList(X)) | → | a__isNatList#(X) | | mark#(U61(X1, X2)) | → | a__U61#(mark(X1), X2) |
| mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | a__U71#(mark(X1), X2, X3) |
| mark#(U62(X)) | → | mark#(X) | | a__U51#(tt, V2) | → | a__U52#(a__isNatList(V2)) |
| mark#(U42(X)) | → | a__U42#(mark(X)) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) | | a__isNatIList#(V) | → | a__U31#(a__isNatList(V)) |
| mark#(U61(X1, X2)) | → | mark#(X1) | | mark#(isNat(X)) | → | a__isNat#(X) |
| mark#(zeros) | → | a__zeros# | | a__U41#(tt, V2) | → | a__U42#(a__isNatIList(V2)) |
| a__U61#(tt, V2) | → | a__U62#(a__isNatIList(V2)) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | a__U72#(tt, L) | → | a__length#(mark(L)) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U93#(tt, IL, M, N) | → | mark#(N) |
| a__isNat#(s(V1)) | → | a__isNat#(V1) | | mark#(U21(X)) | → | mark#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | a__take#(s(M), cons(N, IL)) | → | a__isNatIList#(IL) |
| a__U72#(tt, L) | → | mark#(L) | | a__isNat#(s(V1)) | → | a__U21#(a__isNat(V1)) |
| a__U61#(tt, V2) | → | a__isNatIList#(V2) | | mark#(length(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | a__length#(cons(N, L)) | → | a__isNatList#(L) |
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(U51(X1, X2)) | → | a__U51#(mark(X1), X2) |
| a__U92#(tt, IL, M, N) | → | a__isNat#(N) | | mark#(U72(X1, X2)) | → | a__U72#(mark(X1), X2) |
| a__isNat#(length(V1)) | → | a__isNatList#(V1) | | mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) |
| a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(U11(X)) | → | a__U11#(mark(X)) |
| mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | | mark#(take(X1, X2)) | → | mark#(X2) |
| mark#(U91(X1, X2, X3, X4)) | → | a__U91#(mark(X1), X2, X3, X4) | | mark#(U52(X)) | → | a__U52#(mark(X)) |
| mark#(U81(X)) | → | a__U81#(mark(X)) | | a__isNat#(length(V1)) | → | a__U11#(a__isNatList(V1)) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
The following SCCs where found
| a__isNatList#(cons(V1, V2)) → a__isNat#(V1) | a__isNatIList#(cons(V1, V2)) → a__U41#(a__isNat(V1), V2) |
| a__isNatList#(take(V1, V2)) → a__U61#(a__isNat(V1), V2) | a__U41#(tt, V2) → a__isNatIList#(V2) |
| a__isNatIList#(V) → a__isNatList#(V) | a__isNatIList#(cons(V1, V2)) → a__isNat#(V1) |
| a__isNatList#(take(V1, V2)) → a__isNat#(V1) | a__U61#(tt, V2) → a__isNatIList#(V2) |
| a__isNat#(s(V1)) → a__isNat#(V1) | a__isNatList#(cons(V1, V2)) → a__U51#(a__isNat(V1), V2) |
| a__U51#(tt, V2) → a__isNatList#(V2) | a__isNat#(length(V1)) → a__isNatList#(V1) |
| a__U91#(tt, IL, M, N) → a__U92#(a__isNat(M), IL, M, N) | mark#(take(X1, X2)) → mark#(X1) |
| mark#(U11(X)) → mark#(X) | mark#(U42(X)) → mark#(X) |
| a__length#(cons(N, L)) → a__U71#(a__isNatList(L), L, N) | a__U72#(tt, L) → a__length#(mark(L)) |
| a__U93#(tt, IL, M, N) → mark#(N) | mark#(U51(X1, X2)) → mark#(X1) |
| mark#(U21(X)) → mark#(X) | mark#(length(X)) → a__length#(mark(X)) |
| a__U72#(tt, L) → mark#(L) | mark#(U81(X)) → mark#(X) |
| a__U71#(tt, L, N) → a__U72#(a__isNat(N), L) | mark#(U92(X1, X2, X3, X4)) → a__U92#(mark(X1), X2, X3, X4) |
| mark#(length(X)) → mark#(X) | a__take#(s(M), cons(N, IL)) → a__U91#(a__isNatIList(IL), IL, M, N) |
| mark#(s(X)) → mark#(X) | mark#(U41(X1, X2)) → mark#(X1) |
| a__U92#(tt, IL, M, N) → a__U93#(a__isNat(N), IL, M, N) | mark#(U72(X1, X2)) → mark#(X1) |
| mark#(U71(X1, X2, X3)) → mark#(X1) | mark#(U72(X1, X2)) → a__U72#(mark(X1), X2) |
| mark#(U93(X1, X2, X3, X4)) → a__U93#(mark(X1), X2, X3, X4) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(U52(X)) → mark#(X) | mark#(U91(X1, X2, X3, X4)) → mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) → mark#(X1) | mark#(U71(X1, X2, X3)) → a__U71#(mark(X1), X2, X3) |
| mark#(take(X1, X2)) → a__take#(mark(X1), mark(X2)) | mark#(U62(X)) → mark#(X) |
| mark#(U31(X)) → mark#(X) | mark#(take(X1, X2)) → mark#(X2) |
| mark#(U92(X1, X2, X3, X4)) → mark#(X1) | mark#(U91(X1, X2, X3, X4)) → a__U91#(mark(X1), X2, X3, X4) |
| mark#(U61(X1, X2)) → mark#(X1) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U91#(tt, IL, M, N) | → | a__U92#(a__isNat(M), IL, M, N) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| a__length#(cons(N, L)) | → | a__U71#(a__isNatList(L), L, N) | | a__U72#(tt, L) | → | a__length#(mark(L)) |
| a__U93#(tt, IL, M, N) | → | mark#(N) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U21(X)) | → | mark#(X) | | mark#(length(X)) | → | a__length#(mark(X)) |
| a__U72#(tt, L) | → | mark#(L) | | mark#(U81(X)) | → | mark#(X) |
| mark#(U92(X1, X2, X3, X4)) | → | a__U92#(mark(X1), X2, X3, X4) | | a__U71#(tt, L, N) | → | a__U72#(a__isNat(N), L) |
| mark#(length(X)) | → | mark#(X) | | a__take#(s(M), cons(N, IL)) | → | a__U91#(a__isNatIList(IL), IL, M, N) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
| a__U92#(tt, IL, M, N) | → | a__U93#(a__isNat(N), IL, M, N) | | mark#(U71(X1, X2, X3)) | → | mark#(X1) |
| mark#(U72(X1, X2)) | → | mark#(X1) | | mark#(U72(X1, X2)) | → | a__U72#(mark(X1), X2) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | a__U71#(mark(X1), X2, X3) |
| mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | | mark#(U62(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X2) |
| mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U91(X1, X2, X3, X4)) | → | a__U91#(mark(X1), X2, X3, X4) |
| mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x
- U21(x): x
- U31(x): x
- U41(x,y): x
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y): x
- U62(x): x
- U71(x,y,z): 2y + x
- U72(x,y): 2y + x
- U81(x): x
- U91(x1,x2,x3,x4): 3x4 + x3 + 2x2 + x1
- U92(x1,x2,x3,x4): 3x4 + x3 + 2x2 + x1
- U93(x1,x2,x3,x4): 2x4 + x3 + 2x2 + x1
- a__U11(x): x
- a__U21(x): x
- a__U31(x): x
- a__U41(x,y): x
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y): x
- a__U62(x): x
- a__U71(x,y,z): 2y + x
- a__U71#(x,y,z): y + x
- a__U72(x,y): 2y + x
- a__U72#(x,y): y + x
- a__U81(x): x
- a__U91(x1,x2,x3,x4): 3x4 + x3 + 2x2 + x1
- a__U91#(x1,x2,x3,x4): x4 + x3 + 2x2
- a__U92(x1,x2,x3,x4): 3x4 + x3 + 2x2 + x1
- a__U92#(x1,x2,x3,x4): x4 + x3 + x2
- a__U93(x1,x2,x3,x4): 2x4 + x3 + 2x2 + x1
- a__U93#(x1,x2,x3,x4): x4 + x3
- a__isNat(x): 2
- a__isNatIList(x): 2
- a__isNatList(x): 2
- a__length(x): 2x + 2
- a__length#(x): x + 2
- a__take(x,y): 2y + x + 2
- a__take#(x,y): 2y + x
- a__zeros: 0
- cons(x,y): y + 2x
- isNat(x): 2
- isNatIList(x): 2
- isNatList(x): 2
- length(x): 2x + 2
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): x
- take(x,y): 2y + x + 2
- tt: 2
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__length(X) | → | length(X) | | a__U81(tt) | → | nil |
| a__isNat(0) | → | tt | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(X) | → | isNat(X) | | a__U81(X) | → | U81(X) |
| a__U62(X) | → | U62(X) | | mark(U62(X)) | → | a__U62(mark(X)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__U71(X1, X2, X3) | → | U71(X1, X2, X3) | | mark(tt) | → | tt |
| mark(U42(X)) | → | a__U42(mark(X)) | | a__U21(X) | → | U21(X) |
| a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__zeros | → | zeros |
| mark(zeros) | → | a__zeros | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) | | a__U31(X) | → | U31(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(s(X)) | → | s(mark(X)) |
| a__U11(tt) | → | tt | | a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) |
| a__length(nil) | → | 0 | | a__isNatIList(zeros) | → | tt |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| a__U11(X) | → | U11(X) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) | | a__U31(tt) | → | tt |
| mark(U81(X)) | → | a__U81(mark(X)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) |
| mark(nil) | → | nil | | a__U51(X1, X2) | → | U51(X1, X2) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__take(X1, X2) | → | take(X1, X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt) | → | tt |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) |
| a__U42(X) | → | U42(X) | | a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) |
| mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | | a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) |
| a__zeros | → | cons(0, zeros) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) |
| a__U52(X) | → | U52(X) | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__U52(tt) | → | tt | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| a__U42(tt) | → | tt | | a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__isNatList(X) | → | isNatList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(take(X1, X2)) | → | mark#(X1) | | a__U72#(tt, L) | → | mark#(L) |
| mark#(length(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) |
| mark#(take(X1, X2)) | → | mark#(X2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U91#(tt, IL, M, N) | → | a__U92#(a__isNat(M), IL, M, N) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | a__length#(cons(N, L)) | → | a__U71#(a__isNatList(L), L, N) |
| a__U72#(tt, L) | → | a__length#(mark(L)) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a__U93#(tt, IL, M, N) | → | mark#(N) | | mark#(U21(X)) | → | mark#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | mark#(U81(X)) | → | mark#(X) |
| a__U71#(tt, L, N) | → | a__U72#(a__isNat(N), L) | | mark#(U92(X1, X2, X3, X4)) | → | a__U92#(mark(X1), X2, X3, X4) |
| a__take#(s(M), cons(N, IL)) | → | a__U91#(a__isNatIList(IL), IL, M, N) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | a__U92#(tt, IL, M, N) | → | a__U93#(a__isNat(N), IL, M, N) |
| mark#(U71(X1, X2, X3)) | → | mark#(X1) | | mark#(U72(X1, X2)) | → | mark#(X1) |
| mark#(U72(X1, X2)) | → | a__U72#(mark(X1), X2) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U71(X1, X2, X3)) | → | a__U71#(mark(X1), X2, X3) | | mark#(U62(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U91(X1, X2, X3, X4)) | → | a__U91#(mark(X1), X2, X3, X4) |
| mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
The following SCCs where found
| a__U91#(tt, IL, M, N) → a__U92#(a__isNat(M), IL, M, N) | mark#(U71(X1, X2, X3)) → mark#(X1) |
| mark#(U72(X1, X2)) → mark#(X1) | mark#(U93(X1, X2, X3, X4)) → a__U93#(mark(X1), X2, X3, X4) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(U11(X)) → mark#(X) |
| mark#(U42(X)) → mark#(X) | mark#(U52(X)) → mark#(X) |
| a__U93#(tt, IL, M, N) → mark#(N) | mark#(U51(X1, X2)) → mark#(X1) |
| mark#(U21(X)) → mark#(X) | mark#(U91(X1, X2, X3, X4)) → mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) → mark#(X1) | mark#(U81(X)) → mark#(X) |
| mark#(U62(X)) → mark#(X) | mark#(U92(X1, X2, X3, X4)) → a__U92#(mark(X1), X2, X3, X4) |
| mark#(U31(X)) → mark#(X) | mark#(U92(X1, X2, X3, X4)) → mark#(X1) |
| mark#(U91(X1, X2, X3, X4)) → a__U91#(mark(X1), X2, X3, X4) | mark#(U41(X1, X2)) → mark#(X1) |
| mark#(s(X)) → mark#(X) | a__U92#(tt, IL, M, N) → a__U93#(a__isNat(N), IL, M, N) |
| mark#(U61(X1, X2)) → mark#(X1) |
| a__U71#(tt, L, N) → a__U72#(a__isNat(N), L) | a__length#(cons(N, L)) → a__U71#(a__isNatList(L), L, N) |
| a__U72#(tt, L) → a__length#(mark(L)) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U71#(tt, L, N) | → | a__U72#(a__isNat(N), L) | | a__length#(cons(N, L)) | → | a__U71#(a__isNatList(L), L, N) |
| a__U72#(tt, L) | → | a__length#(mark(L)) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 2
- U11(x): x
- U21(x): x
- U31(x): 2
- U41(x,y): 2
- U42(x): x
- U51(x,y): y
- U52(x): x
- U61(x,y): x
- U62(x): 2
- U71(x,y,z): 2y
- U72(x,y): 2y
- U81(x): x
- U91(x1,x2,x3,x4): 2x3
- U92(x1,x2,x3,x4): 2x3
- U93(x1,x2,x3,x4): 2x3
- a__U11(x): x
- a__U21(x): x
- a__U31(x): 2
- a__U41(x,y): 2
- a__U42(x): x
- a__U51(x,y): y
- a__U52(x): x
- a__U61(x,y): x
- a__U62(x): 2
- a__U71(x,y,z): 2y
- a__U71#(x,y,z): 3y + x
- a__U72(x,y): 2y
- a__U72#(x,y): 2y
- a__U81(x): x
- a__U91(x1,x2,x3,x4): 2x3
- a__U92(x1,x2,x3,x4): 2x3
- a__U93(x1,x2,x3,x4): 2x3
- a__isNat(x): x
- a__isNatIList(x): 2
- a__isNatList(x): x
- a__length(x): x
- a__length#(x): 2x
- a__take(x,y): x
- a__zeros: 0
- cons(x,y): 2y
- isNat(x): x
- isNatIList(x): 2
- isNatList(x): x
- length(x): x
- mark(x): x
- nil: 2
- s(x): 2x
- take(x,y): x
- tt: 2
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__length(X) | → | length(X) | | a__U81(tt) | → | nil |
| a__isNat(0) | → | tt | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(X) | → | isNat(X) | | a__U81(X) | → | U81(X) |
| a__U62(X) | → | U62(X) | | mark(U62(X)) | → | a__U62(mark(X)) |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__U71(X1, X2, X3) | → | U71(X1, X2, X3) | | mark(tt) | → | tt |
| mark(U42(X)) | → | a__U42(mark(X)) | | a__U21(X) | → | U21(X) |
| a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__zeros | → | zeros |
| mark(zeros) | → | a__zeros | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) | | a__U31(X) | → | U31(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(s(X)) | → | s(mark(X)) |
| a__U11(tt) | → | tt | | a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) |
| a__length(nil) | → | 0 | | a__isNatIList(zeros) | → | tt |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| a__U11(X) | → | U11(X) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) | | a__U31(tt) | → | tt |
| mark(U81(X)) | → | a__U81(mark(X)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) |
| mark(nil) | → | nil | | a__U51(X1, X2) | → | U51(X1, X2) |
| a__take(X1, X2) | → | take(X1, X2) | | a__U72(X1, X2) | → | U72(X1, X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt) | → | tt |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) |
| mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | | a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) |
| a__zeros | → | cons(0, zeros) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) |
| a__U52(X) | → | U52(X) | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__U52(tt) | → | tt | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__U42(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__isNatList(X) | → | isNatList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a__U71#(tt, L, N) | → | a__U72#(a__isNat(N), L) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__length#(cons(N, L)) | → | a__U71#(a__isNatList(L), L, N) | | a__U72#(tt, L) | → | a__length#(mark(L)) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
There are no SCCs!
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U72(X1, X2)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | mark#(X1) |
| a__U91#(tt, IL, M, N) | → | a__U92#(a__isNat(M), IL, M, N) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U93#(tt, IL, M, N) | → | mark#(N) |
| mark#(U21(X)) | → | mark#(X) | | mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U81(X)) | → | mark#(X) |
| mark#(U62(X)) | → | mark#(X) | | mark#(U92(X1, X2, X3, X4)) | → | a__U92#(mark(X1), X2, X3, X4) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U91(X1, X2, X3, X4)) | → | a__U91#(mark(X1), X2, X3, X4) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | a__U92#(tt, IL, M, N) | → | a__U93#(a__isNat(N), IL, M, N) |
| mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x
- U21(x): x
- U31(x): x
- U41(x,y): x
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y): x
- U62(x): x
- U71(x,y,z): 2x
- U72(x,y): 2x
- U81(x): x
- U91(x1,x2,x3,x4): x4 + 3x3 + 2x1
- U92(x1,x2,x3,x4): 2x4 + 2x1
- U93(x1,x2,x3,x4): x4 + x1
- a__U11(x): x
- a__U21(x): x
- a__U31(x): x
- a__U41(x,y): x
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y): x
- a__U62(x): x
- a__U71(x,y,z): 2x
- a__U72(x,y): 2x
- a__U81(x): x
- a__U91(x1,x2,x3,x4): 2x4 + 3x3 + 2x1
- a__U91#(x1,x2,x3,x4): 2x4 + 2x3 + 2x1
- a__U92(x1,x2,x3,x4): 2x4 + 2x1
- a__U92#(x1,x2,x3,x4): 2x4 + 2x1
- a__U93(x1,x2,x3,x4): 2x4 + x1
- a__U93#(x1,x2,x3,x4): 2x4
- a__isNat(x): 1
- a__isNatIList(x): 1
- a__isNatList(x): 1
- a__length(x): 2
- a__take(x,y): 2y + 3x + 2
- a__zeros: 0
- cons(x,y): x
- isNat(x): 1
- isNatIList(x): 1
- isNatList(x): 1
- length(x): 1
- mark(x): 2x
- mark#(x): 2x
- nil: 0
- s(x): x
- take(x,y): 2y + 3x + 1
- tt: 1
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__length(X) | → | length(X) | | a__U81(tt) | → | nil |
| a__isNat(0) | → | tt | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(X) | → | isNat(X) | | a__U81(X) | → | U81(X) |
| a__U62(X) | → | U62(X) | | mark(U62(X)) | → | a__U62(mark(X)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__take(0, IL) | → | a__U81(a__isNatIList(IL)) | | mark(tt) | → | tt |
| mark(U42(X)) | → | a__U42(mark(X)) | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__U21(X) | → | U21(X) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__zeros | → | zeros |
| mark(zeros) | → | a__zeros | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) | | a__U31(X) | → | U31(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(s(X)) | → | s(mark(X)) |
| a__U11(tt) | → | tt | | a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) |
| a__length(nil) | → | 0 | | a__isNatIList(zeros) | → | tt |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__U11(X) | → | U11(X) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) | | a__U31(tt) | → | tt |
| mark(U81(X)) | → | a__U81(mark(X)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) |
| mark(nil) | → | nil | | a__U51(X1, X2) | → | U51(X1, X2) |
| a__take(X1, X2) | → | take(X1, X2) | | a__U72(X1, X2) | → | U72(X1, X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) |
| a__U62(tt) | → | tt | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) |
| mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | | a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) |
| a__zeros | → | cons(0, zeros) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) |
| a__U52(X) | → | U52(X) | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__U52(tt) | → | tt | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__U42(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__isNatList(X) | → | isNatList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a__U92#(tt, IL, M, N) | → | a__U93#(a__isNat(N), IL, M, N) |
Problem 9: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(U72(X1, X2)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | mark#(X1) |
| a__U91#(tt, IL, M, N) | → | a__U92#(a__isNat(M), IL, M, N) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U93#(tt, IL, M, N) | → | mark#(N) |
| mark#(U21(X)) | → | mark#(X) | | mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U81(X)) | → | mark#(X) |
| mark#(U62(X)) | → | mark#(X) | | mark#(U92(X1, X2, X3, X4)) | → | a__U92#(mark(X1), X2, X3, X4) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U91(X1, X2, X3, X4)) | → | a__U91#(mark(X1), X2, X3, X4) |
| mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
The following SCCs where found
| mark#(U72(X1, X2)) → mark#(X1) | mark#(U71(X1, X2, X3)) → mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) → a__U93#(mark(X1), X2, X3, X4) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(U11(X)) → mark#(X) | mark#(U42(X)) → mark#(X) |
| mark#(U52(X)) → mark#(X) | a__U93#(tt, IL, M, N) → mark#(N) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U21(X)) → mark#(X) |
| mark#(U91(X1, X2, X3, X4)) → mark#(X1) | mark#(U93(X1, X2, X3, X4)) → mark#(X1) |
| mark#(U81(X)) → mark#(X) | mark#(U62(X)) → mark#(X) |
| mark#(U31(X)) → mark#(X) | mark#(U92(X1, X2, X3, X4)) → mark#(X1) |
| mark#(s(X)) → mark#(X) | mark#(U41(X1, X2)) → mark#(X1) |
| mark#(U61(X1, X2)) → mark#(X1) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U71(X1, X2, X3)) | → | mark#(X1) | | mark#(U72(X1, X2)) | → | mark#(X1) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a__U93#(tt, IL, M, N) | → | mark#(N) | | mark#(U21(X)) | → | mark#(X) |
| mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U81(X)) | → | mark#(X) | | mark#(U62(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 1
- U11(x): x
- U21(x): x
- U31(x): x
- U41(x,y): x
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y): x
- U62(x): x
- U71(x,y,z): x
- U72(x,y): x
- U81(x): x
- U91(x1,x2,x3,x4): 3x4 + x1 + 1
- U92(x1,x2,x3,x4): 3x4 + x1 + 1
- U93(x1,x2,x3,x4): 2x4 + x1 + 1
- a__U11(x): x
- a__U21(x): x
- a__U31(x): x
- a__U41(x,y): x
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y): x
- a__U62(x): x
- a__U71(x,y,z): x
- a__U72(x,y): x
- a__U81(x): x
- a__U91(x1,x2,x3,x4): 3x4 + x1 + 1
- a__U92(x1,x2,x3,x4): 3x4 + x1 + 1
- a__U93(x1,x2,x3,x4): 2x4 + x1 + 1
- a__U93#(x1,x2,x3,x4): 3x4
- a__isNat(x): 2
- a__isNatIList(x): 2
- a__isNatList(x): 2
- a__length(x): 2
- a__take(x,y): 3y + 3
- a__zeros: 2
- cons(x,y): x
- isNat(x): 2
- isNatIList(x): 2
- isNatList(x): 2
- length(x): 2
- mark(x): x
- mark#(x): 2x
- nil: 1
- s(x): x
- take(x,y): 3y + 3
- tt: 2
- zeros: 2
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__U61(X1, X2) | → | U61(X1, X2) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__length(X) | → | length(X) | | a__U81(tt) | → | nil |
| a__isNat(0) | → | tt | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(X) | → | isNat(X) | | a__U81(X) | → | U81(X) |
| a__U62(X) | → | U62(X) | | mark(U62(X)) | → | a__U62(mark(X)) |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__U71(X1, X2, X3) | → | U71(X1, X2, X3) | | mark(tt) | → | tt |
| mark(U42(X)) | → | a__U42(mark(X)) | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__U21(X) | → | U21(X) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__zeros | → | zeros |
| mark(zeros) | → | a__zeros | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) | | a__U31(X) | → | U31(X) |
| mark(s(X)) | → | s(mark(X)) | | mark(isNatList(X)) | → | a__isNatList(X) |
| a__U11(tt) | → | tt | | a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__U11(X) | → | U11(X) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) | | a__U31(tt) | → | tt |
| mark(U81(X)) | → | a__U81(mark(X)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__isNatList(nil) | → | tt |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(nil) | → | nil |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__take(X1, X2) | → | take(X1, X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt) | → | tt |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | a__U42(X) | → | U42(X) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) |
| mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | | a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) |
| a__U72(tt, L) | → | s(a__length(mark(L))) | | a__zeros | → | cons(0, zeros) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(X) | → | U52(X) |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__U52(tt) | → | tt | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__isNatList(X) | → | isNatList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(U93(X1, X2, X3, X4)) | → | a__U93#(mark(X1), X2, X3, X4) | | mark#(U91(X1, X2, X3, X4)) | → | mark#(X1) |
| mark#(U93(X1, X2, X3, X4)) | → | mark#(X1) | | mark#(U92(X1, X2, X3, X4)) | → | mark#(X1) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(U71(X1, X2, X3)) | → | mark#(X1) | | mark#(U72(X1, X2)) | → | mark#(X1) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U93#(tt, IL, M, N) | → | mark#(N) |
| mark#(U21(X)) | → | mark#(X) | | mark#(U81(X)) | → | mark#(X) |
| mark#(U62(X)) | → | mark#(X) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
| mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
The following SCCs where found
| mark#(U71(X1, X2, X3)) → mark#(X1) | mark#(U72(X1, X2)) → mark#(X1) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(U11(X)) → mark#(X) |
| mark#(U42(X)) → mark#(X) | mark#(U52(X)) → mark#(X) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U21(X)) → mark#(X) |
| mark#(U81(X)) → mark#(X) | mark#(U62(X)) → mark#(X) |
| mark#(U31(X)) → mark#(X) | mark#(U41(X1, X2)) → mark#(X1) |
| mark#(s(X)) → mark#(X) | mark#(U61(X1, X2)) → mark#(X1) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U72(X1, X2)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | mark#(X1) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U21(X)) | → | mark#(X) |
| mark#(U81(X)) | → | mark#(X) | | mark#(U62(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): 2x + 2
- U21(x): 2x + 2
- U31(x): 2x + 2
- U41(x,y): 2x + 2
- U42(x): 2x + 2
- U51(x,y): 2y + 2x + 2
- U52(x): x + 2
- U61(x,y): 2y + 2x
- U62(x): 2x + 2
- U71(x,y,z): 2z + 2x + 2
- U72(x,y): 2x + 2
- U81(x): x + 2
- U91(x1,x2,x3,x4): 0
- U92(x1,x2,x3,x4): 0
- U93(x1,x2,x3,x4): 0
- a__U11(x): 0
- a__U21(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x,y): 0
- a__U62(x): 0
- a__U71(x,y,z): 0
- a__U72(x,y): 0
- a__U81(x): 0
- a__U91(x1,x2,x3,x4): 0
- a__U92(x1,x2,x3,x4): 0
- a__U93(x1,x2,x3,x4): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 0
- a__take(x,y): 0
- a__zeros: 0
- cons(x,y): 3y + x + 2
- isNat(x): 0
- isNatIList(x): 0
- isNatList(x): 0
- length(x): 0
- mark(x): 0
- mark#(x): x
- nil: 0
- s(x): 2x + 2
- take(x,y): 0
- tt: 0
- zeros: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(U72(X1, X2)) | → | mark#(X1) | | mark#(U71(X1, X2, X3)) | → | mark#(X1) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U21(X)) | → | mark#(X) |
| mark#(U81(X)) | → | mark#(X) | | mark#(U62(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U61(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): 0
- U21(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x,y): x + 2
- U62(x): 0
- U71(x,y,z): 0
- U72(x,y): 0
- U81(x): 0
- U91(x1,x2,x3,x4): 0
- U92(x1,x2,x3,x4): 0
- U93(x1,x2,x3,x4): 0
- a__U11(x): 0
- a__U21(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x,y): 0
- a__U62(x): 0
- a__U71(x,y,z): 0
- a__U72(x,y): 0
- a__U81(x): 0
- a__U91(x1,x2,x3,x4): 0
- a__U92(x1,x2,x3,x4): 0
- a__U93(x1,x2,x3,x4): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 0
- a__take(x,y): 0
- a__zeros: 0
- cons(x,y): 0
- isNat(x): 0
- isNatIList(x): 0
- isNatList(x): 0
- length(x): 0
- mark(x): 0
- mark#(x): x
- nil: 0
- s(x): 0
- take(x,y): 0
- tt: 0
- zeros: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(U61(X1, X2)) | → | mark#(X1) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) | | a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) |
| a__isNatList#(take(V1, V2)) | → | a__U61#(a__isNat(V1), V2) | | a__isNatIList#(V) | → | a__isNatList#(V) |
| a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) | | a__U41#(tt, V2) | → | a__isNatIList#(V2) |
| a__isNatList#(take(V1, V2)) | → | a__isNat#(V1) | | a__U61#(tt, V2) | → | a__isNatIList#(V2) |
| a__isNat#(s(V1)) | → | a__isNat#(V1) | | a__isNatList#(cons(V1, V2)) | → | a__U51#(a__isNat(V1), V2) |
| a__U51#(tt, V2) | → | a__isNatList#(V2) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, a__U91, U42, U93, a__U92, U41, U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, s, a__isNatIList, U51, isNatList, zeros, tt, a__isNat, take, U52, U81, a__U31, U11, a__U81, a__U11, U31, a__U61, nil
Strategy
Projection
The following projection was used:
- π (a__U51#): 2
- π (a__U41#): 2
- π (a__isNatIList#): 1
- π (a__isNat#): 1
- π (a__isNatList#): 1
- π (a__U61#): 2
Thus, the following dependency pairs are removed:
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) |
| a__isNatList#(take(V1, V2)) | → | a__U61#(a__isNat(V1), V2) | | a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) |
| a__isNatList#(take(V1, V2)) | → | a__isNat#(V1) | | a__isNat#(s(V1)) | → | a__isNat#(V1) |
| a__isNatList#(cons(V1, V2)) | → | a__U51#(a__isNat(V1), V2) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U41#(tt, V2) | → | a__isNatIList#(V2) | | a__isNatIList#(V) | → | a__isNatList#(V) |
| a__U61#(tt, V2) | → | a__isNatIList#(V2) | | a__U51#(tt, V2) | → | a__isNatList#(V2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt) | → | tt |
| a__U21(tt) | → | tt | | a__U31(tt) | → | tt |
| a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) | | a__U42(tt) | → | tt |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(tt) | → | tt |
| a__U61(tt, V2) | → | a__U62(a__isNatIList(V2)) | | a__U62(tt) | → | tt |
| a__U71(tt, L, N) | → | a__U72(a__isNat(N), L) | | a__U72(tt, L) | → | s(a__length(mark(L))) |
| a__U81(tt) | → | nil | | a__U91(tt, IL, M, N) | → | a__U92(a__isNat(M), IL, M, N) |
| a__U92(tt, IL, M, N) | → | a__U93(a__isNat(N), IL, M, N) | | a__U93(tt, IL, M, N) | → | cons(mark(N), take(M, IL)) |
| a__isNat(0) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__isNatIList(V) | → | a__U31(a__isNatList(V)) |
| a__isNatIList(zeros) | → | tt | | a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) |
| a__isNatList(nil) | → | tt | | a__isNatList(cons(V1, V2)) | → | a__U51(a__isNat(V1), V2) |
| a__isNatList(take(V1, V2)) | → | a__U61(a__isNat(V1), V2) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U71(a__isNatList(L), L, N) | | a__take(0, IL) | → | a__U81(a__isNatIList(IL)) |
| a__take(s(M), cons(N, IL)) | → | a__U91(a__isNatIList(IL), IL, M, N) | | mark(zeros) | → | a__zeros |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(U21(X)) | → | a__U21(mark(X)) |
| mark(U31(X)) | → | a__U31(mark(X)) | | mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) |
| mark(U42(X)) | → | a__U42(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(isNatList(X)) | → | a__isNatList(X) | | mark(U61(X1, X2)) | → | a__U61(mark(X1), X2) |
| mark(U62(X)) | → | a__U62(mark(X)) | | mark(U71(X1, X2, X3)) | → | a__U71(mark(X1), X2, X3) |
| mark(U72(X1, X2)) | → | a__U72(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(length(X)) | → | a__length(mark(X)) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U91(X1, X2, X3, X4)) | → | a__U91(mark(X1), X2, X3, X4) | | mark(U92(X1, X2, X3, X4)) | → | a__U92(mark(X1), X2, X3, X4) |
| mark(U93(X1, X2, X3, X4)) | → | a__U93(mark(X1), X2, X3, X4) | | mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) |
| 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(X) | → | U11(X) | | a__U21(X) | → | U21(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNatIList(X) | → | isNatIList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__isNatList(X) | → | isNatList(X) | | a__U61(X1, X2) | → | U61(X1, X2) |
| a__U62(X) | → | U62(X) | | a__U71(X1, X2, X3) | → | U71(X1, X2, X3) |
| a__U72(X1, X2) | → | U72(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) | | a__U81(X) | → | U81(X) |
| a__U91(X1, X2, X3, X4) | → | U91(X1, X2, X3, X4) | | a__U92(X1, X2, X3, X4) | → | U92(X1, X2, X3, X4) |
| a__U93(X1, X2, X3, X4) | → | U93(X1, X2, X3, X4) | | a__take(X1, X2) | → | take(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a__take, isNat, a__isNatList, U62, U61, U93, U42, a__U91, U92, U41, a__U92, U91, a__U93, length, a__U41, a__U72, a__U42, a__U71, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, U71, U72, 0, isNatList, U51, a__isNatIList, s, tt, zeros, take, a__isNat, U81, U52, U11, a__U31, a__U81, U31, a__U11, a__U61, nil
Strategy
There are no SCCs!