YES
The TRS could be proven terminating. The proof took 60003 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (669ms).
| – Problem 2 was processed with processor SubtermCriterion (34ms).
| | – Problem 5 was processed with processor DependencyGraph (0ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (216ms).
| | – Problem 7 was processed with processor DependencyGraph (55ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (165ms).
| | | | – Problem 9 was processed with processor PolynomialLinearRange4 (260ms).
| | | | | – Problem 10 was processed with processor PolynomialLinearRange4 (135ms).
| | | | | | – Problem 11 was processed with processor DependencyGraph (13ms).
| | | | | | | – Problem 12 was processed with processor PolynomialLinearRange4 (37ms).
| | | | | | | | – Problem 13 was processed with processor PolynomialLinearRange4 (17ms).
| | | | | | | | | – Problem 14 was processed with processor PolynomialLinearRange4 (15ms).
| | | | | | | | | | – Problem 15 was processed with processor PolynomialLinearRange4 (7ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| | – Problem 6 was processed with processor DependencyGraph (33ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(isNat(X)) | → | a__isNat#(X) |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | mark#(U31(X)) | → | a__U31#(mark(X)) |
| mark#(zeros) | → | a__zeros# | | a__U41#(tt, V2) | → | a__U42#(a__isNatIList(V2)) |
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) |
| mark#(U62(X1, X2)) | → | mark#(X1) | | a__isNat#(s(V1)) | → | a__isNat#(V1) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U51#(tt, V2) | → | a__isNatList#(V2) |
| a__isNatList#(cons(V1, V2)) | → | a__U51#(a__isNat(V1), V2) | | mark#(U21(X)) | → | mark#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) |
| a__isNatIList#(V) | → | a__isNatList#(V) | | a__isNat#(s(V1)) | → | a__U21#(a__isNat(V1)) |
| mark#(U41(X1, X2)) | → | a__U41#(mark(X1), X2) | | mark#(U21(X)) | → | a__U21#(mark(X)) |
| mark#(length(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(s(X)) | → | mark#(X) | | mark#(U61(X1, X2, X3)) | → | a__U61#(mark(X1), X2, X3) |
| 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__U41#(tt, V2) | → | a__isNatIList#(V2) |
| a__U61#(tt, L, N) | → | a__U62#(a__isNat(N), L) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U52(X)) | → | mark#(X) | | a__U62#(tt, L) | → | a__length#(mark(L)) |
| a__U61#(tt, L, N) | → | a__isNat#(N) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
| mark#(isNatList(X)) | → | a__isNatList#(X) | | a__length#(cons(N, L)) | → | a__U61#(a__isNatList(L), L, N) |
| a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(U11(X)) | → | a__U11#(mark(X)) |
| a__U51#(tt, V2) | → | a__U52#(a__isNatList(V2)) | | mark#(U42(X)) | → | a__U42#(mark(X)) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U52(X)) | → | a__U52#(mark(X)) |
| a__isNatIList#(V) | → | a__U31#(a__isNatList(V)) | | 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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
The following SCCs where found
| a__isNatIList#(cons(V1, V2)) → a__U41#(a__isNat(V1), V2) | a__U41#(tt, V2) → a__isNatIList#(V2) |
| a__isNatList#(cons(V1, V2)) → a__isNat#(V1) | 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__U62#(tt, L) → mark#(L) | a__U61#(tt, L, N) → a__U62#(a__isNat(N), L) |
| mark#(U61(X1, X2, X3)) → mark#(X1) | mark#(cons(X1, X2)) → mark#(X1) |
| mark#(U11(X)) → mark#(X) | mark#(U62(X1, X2)) → a__U62#(mark(X1), X2) |
| mark#(U42(X)) → mark#(X) | mark#(U62(X1, X2)) → mark#(X1) |
| mark#(U52(X)) → mark#(X) | a__U62#(tt, L) → a__length#(mark(L)) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U21(X)) → mark#(X) |
| mark#(length(X)) → a__length#(mark(X)) | a__length#(cons(N, L)) → a__U61#(a__isNatList(L), L, N) |
| mark#(U31(X)) → mark#(X) | mark#(length(X)) → mark#(X) |
| mark#(s(X)) → mark#(X) | mark#(U41(X1, X2)) → mark#(X1) |
| mark#(U61(X1, X2, X3)) → a__U61#(mark(X1), X2, X3) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) | | a__U41#(tt, V2) | → | a__isNatIList#(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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Projection
The following projection was used:
- π (a__U41#): 2
- π (a__isNatIList#): 1
Thus, the following dependency pairs are removed:
| a__isNatIList#(cons(V1, V2)) | → | a__U41#(a__isNat(V1), V2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U41#(tt, V2) | → | a__isNatIList#(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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
There are no SCCs!
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | a__U61#(tt, L, N) | → | a__U62#(a__isNat(N), L) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(U61(X1, X2, X3)) | → | mark#(X1) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U62(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a__U62#(tt, L) | → | a__length#(mark(L)) | | mark#(U21(X)) | → | mark#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | a__length#(cons(N, L)) | → | a__U61#(a__isNatList(L), L, N) |
| mark#(U31(X)) | → | mark#(X) | | mark#(length(X)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U61(X1, X2, X3)) | → | a__U61#(mark(X1), X2, X3) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 1
- U11(x): x
- U21(x): x
- U31(x): x
- U41(x,y): y + x
- U42(x): x
- U51(x,y): y + x
- U52(x): x
- U61(x,y,z): z + y + x
- U62(x,y): y + x
- a__U11(x): x
- a__U21(x): x
- a__U31(x): x
- a__U41(x,y): y + x
- a__U42(x): x
- a__U51(x,y): y + x
- a__U52(x): x
- a__U61(x,y,z): z + y + x
- a__U61#(x,y,z): 2z + 2y + 2x
- a__U62(x,y): y + x
- a__U62#(x,y): 2y + 2x
- a__isNat(x): x
- a__isNatIList(x): x + 1
- a__isNatList(x): x
- a__length(x): x
- a__length#(x): 2x
- a__zeros: 1
- cons(x,y): 2y + x
- isNat(x): x
- isNatIList(x): x
- isNatList(x): x
- length(x): x
- mark(x): x + 1
- mark#(x): 2x + 2
- nil: 2
- s(x): x
- tt: 1
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__length(X) | → | length(X) | | a__isNat(0) | → | tt |
| a__isNat(X) | → | isNat(X) | | a__U62(X1, X2) | → | U62(X1, X2) |
| a__U61(X1, X2, X3) | → | U61(X1, X2, X3) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | 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__U31(X) | → | U31(X) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__U11(tt) | → | tt |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| mark(U31(X)) | → | a__U31(mark(X)) | | a__U11(X) | → | U11(X) |
| a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, N) | | a__U61(tt, L, N) | → | a__U62(a__isNat(N), L) |
| a__U31(tt) | → | tt | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| mark(U21(X)) | → | a__U21(mark(X)) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U61(X1, X2, X3)) | → | a__U61(mark(X1), X2, X3) | | a__U42(X) | → | U42(X) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__zeros | → | cons(0, zeros) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(X) | → | U52(X) |
| a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) | | a__U52(tt) | → | tt |
| 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:
| a__U61#(tt, L, N) | → | a__U62#(a__isNat(N), L) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U62(X1, X2)) | → | mark#(X1) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a__U62#(tt, L) | → | a__length#(mark(L)) |
| mark#(U21(X)) | → | mark#(X) | | mark#(length(X)) | → | a__length#(mark(X)) |
| a__length#(cons(N, L)) | → | a__U61#(a__isNatList(L), L, N) | | mark#(length(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U61(X1, X2, X3)) | → | a__U61#(mark(X1), X2, X3) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
The following SCCs where found
| a__U62#(tt, L) → mark#(L) | mark#(U61(X1, X2, X3)) → mark#(X1) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(U11(X)) → mark#(X) |
| mark#(U62(X1, X2)) → a__U62#(mark(X1), X2) | mark#(U62(X1, X2)) → mark#(X1) |
| mark#(U42(X)) → mark#(X) | mark#(U52(X)) → mark#(X) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U21(X)) → mark#(X) |
| mark#(length(X)) → mark#(X) | mark#(U31(X)) → mark#(X) |
| mark#(U41(X1, X2)) → mark#(X1) | mark#(s(X)) → mark#(X) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U62(X1, X2)) | → | mark#(X1) |
| mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U21(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(length(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x
- U21(x): x
- U31(x): 2x + 1
- U41(x,y): 2x + 1
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y,z): y + x
- U62(x,y): y + x
- a__U11(x): x
- a__U21(x): x
- a__U31(x): 2x + 1
- a__U41(x,y): 2x + 1
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y,z): 2y + x
- a__U62(x,y): 2y + x
- a__U62#(x,y): y
- a__isNat(x): 1
- a__isNatIList(x): 3
- a__isNatList(x): 1
- a__length(x): x
- a__zeros: 1
- cons(x,y): 2y + x + 1
- isNat(x): 0
- isNatIList(x): 1
- isNatList(x): 1
- length(x): x
- mark(x): 2x + 1
- mark#(x): x
- nil: 1
- s(x): x
- tt: 1
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__length(X) | → | length(X) | | a__isNat(0) | → | tt |
| a__isNat(X) | → | isNat(X) | | a__U62(X1, X2) | → | U62(X1, X2) |
| a__U61(X1, X2, X3) | → | U61(X1, X2, X3) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | 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__U31(X) | → | U31(X) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__U11(tt) | → | tt |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| mark(U31(X)) | → | a__U31(mark(X)) | | a__U11(X) | → | U11(X) |
| a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, N) | | a__U61(tt, L, N) | → | a__U62(a__isNat(N), L) |
| a__U31(tt) | → | tt | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| mark(U21(X)) | → | a__U21(mark(X)) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U61(X1, X2, X3)) | → | a__U61(mark(X1), X2, X3) | | a__U42(X) | → | U42(X) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__zeros | → | cons(0, zeros) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(X) | → | U52(X) |
| a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) | | a__U52(tt) | → | tt |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__U42(tt) | → | tt |
| 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#(cons(X1, X2)) | → | mark#(X1) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(U61(X1, X2, X3)) | → | mark#(X1) |
| mark#(length(X)) | → | mark#(X) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) | | mark#(U62(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U21(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x
- U21(x): x
- U31(x): 2x
- U41(x,y): 2x
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y,z): y + 2x
- U62(x,y): y + 2x
- a__U11(x): x
- a__U21(x): x
- a__U31(x): 2x
- a__U41(x,y): 2x
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y,z): 2y + 2x
- a__U62(x,y): 2y + 2x
- a__U62#(x,y): 2y
- a__isNat(x): 1
- a__isNatIList(x): 2
- a__isNatList(x): 1
- a__length(x): x + 2
- a__zeros: 0
- cons(x,y): 2y
- isNat(x): 1
- isNatIList(x): 1
- isNatList(x): 1
- length(x): x + 1
- mark(x): 2x
- mark#(x): 2x
- nil: 0
- s(x): x
- tt: 1
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__length(X) | → | length(X) | | a__isNat(0) | → | tt |
| a__isNat(X) | → | isNat(X) | | a__U62(X1, X2) | → | U62(X1, X2) |
| a__U61(X1, X2, X3) | → | U61(X1, X2, X3) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | 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__U31(X) | → | U31(X) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__U11(tt) | → | tt |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| mark(U31(X)) | → | a__U31(mark(X)) | | a__U11(X) | → | U11(X) |
| a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, N) | | a__U61(tt, L, N) | → | a__U62(a__isNat(N), L) |
| a__U31(tt) | → | tt | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| mark(U21(X)) | → | a__U21(mark(X)) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U61(X1, X2, X3)) | → | a__U61(mark(X1), X2, X3) | | a__U42(X) | → | U42(X) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__zeros | → | cons(0, zeros) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(X) | → | U52(X) |
| a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) | | a__U52(tt) | → | tt |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__U42(tt) | → | tt |
| 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#(length(X)) | → | mark#(X) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(U61(X1, X2, X3)) | → | mark#(X1) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U62(X1, X2)) | → | mark#(X1) | | mark#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) |
| mark#(U52(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U21(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x
- U21(x): x
- U31(x): 1
- U41(x,y): x + 1
- U42(x): x
- U51(x,y): x
- U52(x): x
- U61(x,y,z): y + 2x
- U62(x,y): y + 2x
- a__U11(x): x
- a__U21(x): x
- a__U31(x): 1
- a__U41(x,y): x + 1
- a__U42(x): x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x,y,z): 2y + 2x
- a__U62(x,y): 2y + 2x
- a__U62#(x,y): y + x + 1
- a__isNat(x): 1
- a__isNatIList(x): 2
- a__isNatList(x): 1
- a__length(x): x + 2
- a__zeros: 0
- cons(x,y): 3y
- isNat(x): 1
- isNatIList(x): 1
- isNatList(x): 1
- length(x): x + 1
- mark(x): 2x
- mark#(x): x + 2
- nil: 0
- s(x): x
- tt: 1
- zeros: 0
Standard Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| a__length(X) | → | length(X) | | a__isNat(0) | → | tt |
| a__isNat(X) | → | isNat(X) | | a__U62(X1, X2) | → | U62(X1, X2) |
| a__U61(X1, X2, X3) | → | U61(X1, X2, X3) | | a__U41(tt, V2) | → | a__U42(a__isNatIList(V2)) |
| a__U41(X1, X2) | → | U41(X1, X2) | | 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__U31(X) | → | U31(X) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__U11(tt) | → | tt |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| mark(U31(X)) | → | a__U31(mark(X)) | | a__U11(X) | → | U11(X) |
| a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, N) | | a__U61(tt, L, N) | → | a__U62(a__isNat(N), L) |
| a__U31(tt) | → | tt | | mark(U11(X)) | → | a__U11(mark(X)) |
| a__isNatList(nil) | → | tt | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| a__U21(tt) | → | tt | | a__isNat(length(V1)) | → | a__U11(a__isNatList(V1)) |
| mark(0) | → | 0 | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| mark(U21(X)) | → | a__U21(mark(X)) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(U61(X1, X2, X3)) | → | a__U61(mark(X1), X2, X3) | | a__U42(X) | → | U42(X) |
| a__isNatIList(X) | → | isNatIList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__isNat(s(V1)) | → | a__U21(a__isNat(V1)) | | a__zeros | → | cons(0, zeros) |
| a__U51(tt, V2) | → | a__U52(a__isNatList(V2)) | | a__U52(X) | → | U52(X) |
| a__isNatIList(cons(V1, V2)) | → | a__U41(a__isNat(V1), V2) | | a__U52(tt) | → | tt |
| a__isNatIList(V) | → | a__U31(a__isNatList(V)) | | a__U42(tt) | → | tt |
| 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#(U62(X1, X2)) | → | a__U62#(mark(X1), X2) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U62#(tt, L) | → | mark#(L) | | mark#(U61(X1, X2, X3)) | → | mark#(X1) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U62(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U21(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
The following SCCs where found
| mark#(U61(X1, X2, X3)) → mark#(X1) | mark#(U11(X)) → mark#(X) |
| mark#(U62(X1, X2)) → mark#(X1) | mark#(U42(X)) → mark#(X) |
| mark#(s(X)) → mark#(X) | mark#(U52(X)) → mark#(X) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U21(X)) → mark#(X) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U62(X1, X2)) | → | mark#(X1) | | mark#(U42(X)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U21(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): 2x
- U21(x): x + 2
- U31(x): 0
- U41(x,y): 0
- U42(x): 2x
- U51(x,y): x + 2
- U52(x): x + 2
- U61(x,y,z): 2x
- U62(x,y): x + 1
- 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,z): 0
- a__U62(x,y): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 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 + 1
- nil: 0
- s(x): 2x + 2
- 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#(U62(X1, X2)) | → | mark#(X1) | | mark#(U52(X)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U21(X)) | → | mark#(X) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): 2x
- U21(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): x + 1
- U51(x,y): 0
- U52(x): 0
- U61(x,y,z): 3z + 3x
- U62(x,y): 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,z): 0
- a__U62(x,y): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 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): 2x
- nil: 0
- s(x): 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:
Problem 14: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U61(X1, X2, X3)) | → | mark#(X1) | | mark#(U11(X)) | → | mark#(X) |
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): 3x
- U21(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x,y,z): x + 1
- U62(x,y): 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,z): 0
- a__U62(x,y): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 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): 3x
- nil: 0
- s(x): 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, X3)) | → | mark#(X1) |
Problem 15: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x): x + 1
- U21(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x,y,z): 0
- U62(x,y): 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,z): 0
- a__U62(x,y): 0
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 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 + 1
- nil: 0
- s(x): 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:
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | 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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, length, a__U41, a__U42, U21, a__U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, zeros, tt, a__isNat, U52, U11, a__U31, U31, a__U11, a__U61, nil
Strategy
Projection
The following projection was used:
- π (a__U51#): 2
- π (a__isNat#): 1
- π (a__isNatList#): 1
Thus, the following dependency pairs are removed:
| a__isNatList#(cons(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 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| 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, L, N) | → | a__U62(a__isNat(N), L) | | a__U62(tt, L) | → | s(a__length(mark(L))) |
| 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__length(nil) | → | 0 | | a__length(cons(N, L)) | → | a__U61(a__isNatList(L), L, 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, X3)) | → | a__U61(mark(X1), X2, X3) | | mark(U62(X1, X2)) | → | a__U62(mark(X1), X2) |
| mark(isNat(X)) | → | a__isNat(X) | | 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(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, X3) | → | U61(X1, X2, X3) |
| a__U62(X1, X2) | → | U62(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isNat, a__isNatList, U62, U61, U42, U41, a__U41, length, a__U42, a__U21, U21, cons, a__zeros, a__U62, isNatIList, a__length, mark, 0, isNatList, U51, a__isNatIList, s, tt, zeros, a__isNat, U52, a__U31, U11, a__U11, U31, a__U61, nil
Strategy
There are no SCCs!