YES
The TRS could be proven terminating. The proof took 21104 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (253ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (8781ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (7078ms).
| | | – Problem 4 was processed with processor DependencyGraph (31ms).
| | | | – Problem 5 was processed with processor PolynomialLinearRange4iUR (2617ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (0ms).
| | | | – Problem 6 was processed with processor PolynomialLinearRange4iUR (948ms).
| | | | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (917ms).
| | | | | | – Problem 10 was processed with processor DependencyGraph (1ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (10ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(U11(X1, X2)) | → | mark#(X1) | | mark#(isNat(X)) | → | a__isNat#(X) |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | mark#(zeros) | → | a__zeros# |
| a__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) | | a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) |
| a__isNat#(s(V1)) | → | a__isNat#(V1) | | mark#(length(X)) | → | a__length#(mark(X)) |
| a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) | | a__isNatIList#(V) | → | a__isNatList#(V) |
| a__U11#(tt, L) | → | mark#(L) | | a__and#(tt, X) | → | mark#(X) |
| mark#(length(X)) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| a__length#(cons(N, L)) | → | a__isNatList#(L) | | a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) |
| a__U11#(tt, L) | → | a__length#(mark(L)) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__length#(cons(N, L)) | → | a__and#(a__isNatList(L), isNat(N)) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
| mark#(isNatList(X)) | → | a__isNatList#(X) | | mark#(and(X1, X2)) | → | mark#(X1) |
| a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
The following SCCs where found
| a__isNatList#(cons(V1, V2)) → a__isNat#(V1) | mark#(U11(X1, X2)) → mark#(X1) |
| a__U11#(tt, L) → a__length#(mark(L)) | mark#(isNat(X)) → a__isNat#(X) |
| mark#(isNatIList(X)) → a__isNatIList#(X) | mark#(cons(X1, X2)) → mark#(X1) |
| a__length#(cons(N, L)) → a__U11#(a__and(a__isNatList(L), isNat(N)), L) | a__length#(cons(N, L)) → a__and#(a__isNatList(L), isNat(N)) |
| a__isNatIList#(cons(V1, V2)) → a__and#(a__isNat(V1), isNatIList(V2)) | a__isNat#(s(V1)) → a__isNat#(V1) |
| a__isNatList#(cons(V1, V2)) → a__and#(a__isNat(V1), isNatList(V2)) | a__isNat#(length(V1)) → a__isNatList#(V1) |
| mark#(length(X)) → a__length#(mark(X)) | mark#(isNatList(X)) → a__isNatList#(X) |
| mark#(and(X1, X2)) → mark#(X1) | a__isNatIList#(cons(V1, V2)) → a__isNat#(V1) |
| a__isNatIList#(V) → a__isNatList#(V) | mark#(and(X1, X2)) → a__and#(mark(X1), X2) |
| a__U11#(tt, L) → mark#(L) | a__and#(tt, X) → mark#(X) |
| mark#(length(X)) → mark#(X) | mark#(U11(X1, X2)) → a__U11#(mark(X1), X2) |
| mark#(s(X)) → mark#(X) | a__length#(cons(N, L)) → a__isNatList#(L) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(U11(X1, X2)) | → | mark#(X1) |
| a__U11#(tt, L) | → | a__length#(mark(L)) | | mark#(isNat(X)) | → | a__isNat#(X) |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) | | a__length#(cons(N, L)) | → | a__and#(a__isNatList(L), isNat(N)) |
| a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) | | a__isNat#(s(V1)) | → | a__isNat#(V1) |
| a__isNat#(length(V1)) | → | a__isNatList#(V1) | | mark#(isNatList(X)) | → | a__isNatList#(X) |
| mark#(length(X)) | → | a__length#(mark(X)) | | a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) |
| mark#(and(X1, X2)) | → | mark#(X1) | | a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) |
| a__isNatIList#(V) | → | a__isNatList#(V) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__U11#(tt, L) | → | mark#(L) | | a__and#(tt, X) | → | mark#(X) |
| mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) | | mark#(length(X)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | a__length#(cons(N, L)) | → | a__isNatList#(L) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): 2y + x
- a__U11(x,y): 2y + x
- a__U11#(x,y): 3y
- a__and(x,y): y + 2x
- a__and#(x,y): 2y
- a__isNat(x): 0
- a__isNat#(x): 0
- a__isNatIList(x): x + 1
- a__isNatIList#(x): 2x + 2
- a__isNatList(x): 0
- a__isNatList#(x): 0
- a__length(x): x
- a__length#(x): 2x
- a__zeros: 0
- and(x,y): y + 2x
- cons(x,y): 2y + x
- isNat(x): 0
- isNatIList(x): x + 1
- isNatList(x): 0
- length(x): x
- mark(x): x
- mark#(x): 2x
- nil: 3
- s(x): 2x
- tt: 0
- zeros: 0
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | a__length(X) | → | length(X) |
| a__isNat(0) | → | tt | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(X) | → | isNat(X) | | a__isNatList(nil) | → | tt |
| a__isNat(s(V1)) | → | a__isNat(V1) | | mark(nil) | → | nil |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | mark(tt) | → | tt |
| a__U11(X1, X2) | → | U11(X1, X2) | | mark(0) | → | 0 |
| a__and(X1, X2) | → | and(X1, X2) | | mark(length(X)) | → | a__length(mark(X)) |
| a__and(tt, X) | → | mark(X) | | a__zeros | → | zeros |
| mark(isNat(X)) | → | a__isNat(X) | | a__isNatIList(X) | → | isNatIList(X) |
| mark(zeros) | → | a__zeros | | a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) |
| a__isNatIList(V) | → | a__isNatList(V) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__zeros | → | cons(0, zeros) |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | 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__isNatIList#(V) | → | a__isNatList#(V) | | a__isNatIList#(cons(V1, V2)) | → | a__isNat#(V1) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | mark#(U11(X1, X2)) | → | mark#(X1) |
| a__U11#(tt, L) | → | a__length#(mark(L)) | | mark#(isNat(X)) | → | a__isNat#(X) |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) | | a__length#(cons(N, L)) | → | a__and#(a__isNatList(L), isNat(N)) |
| a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) | | a__isNat#(s(V1)) | → | a__isNat#(V1) |
| a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
| mark#(isNatList(X)) | → | a__isNatList#(X) | | mark#(length(X)) | → | a__length#(mark(X)) |
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__U11#(tt, L) | → | mark#(L) | | a__and#(tt, X) | → | mark#(X) |
| mark#(length(X)) | → | mark#(X) | | mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) |
| mark#(s(X)) | → | mark#(X) | | a__length#(cons(N, L)) | → | a__isNatList#(L) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, zeros, tt, a__isNat, length, U11, a__U11, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): 3y + x + 2
- a__U11(x,y): 3y + x + 2
- a__U11#(x,y): 2y
- a__and(x,y): y + x
- a__and#(x,y): y + x
- a__isNat(x): x
- a__isNat#(x): x
- a__isNatIList(x): 2x
- a__isNatIList#(x): x
- a__isNatList(x): 2x
- a__isNatList#(x): 2x
- a__length(x): 3x + 2
- a__length#(x): 2x
- a__zeros: 0
- and(x,y): y + x
- cons(x,y): 2y + 2x
- isNat(x): x
- isNatIList(x): 2x
- isNatList(x): 2x
- length(x): 3x + 2
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): x
- tt: 0
- zeros: 0
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | a__length(X) | → | length(X) |
| a__isNat(0) | → | tt | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(X) | → | isNat(X) | | a__isNatList(nil) | → | tt |
| a__isNat(s(V1)) | → | a__isNat(V1) | | mark(nil) | → | nil |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | mark(tt) | → | tt |
| a__U11(X1, X2) | → | U11(X1, X2) | | mark(0) | → | 0 |
| a__and(X1, X2) | → | and(X1, X2) | | mark(length(X)) | → | a__length(mark(X)) |
| a__and(tt, X) | → | mark(X) | | a__zeros | → | zeros |
| mark(isNat(X)) | → | a__isNat(X) | | a__isNatIList(X) | → | isNatIList(X) |
| mark(zeros) | → | a__zeros | | a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) |
| a__isNatIList(V) | → | a__isNatList(V) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__zeros | → | cons(0, zeros) |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | 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#(U11(X1, X2)) | → | mark#(X1) | | a__isNat#(length(V1)) | → | a__isNatList#(V1) |
| mark#(length(X)) | → | a__length#(mark(X)) | | mark#(U11(X1, X2)) | → | a__U11#(mark(X1), X2) |
| mark#(length(X)) | → | mark#(X) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__isNatList#(cons(V1, V2)) | → | a__isNat#(V1) | | a__U11#(tt, L) | → | a__length#(mark(L)) |
| mark#(isNat(X)) | → | a__isNat#(X) | | mark#(isNatIList(X)) | → | a__isNatIList#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) |
| a__length#(cons(N, L)) | → | a__and#(a__isNatList(L), isNat(N)) | | a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) |
| a__isNat#(s(V1)) | → | a__isNat#(V1) | | a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) |
| mark#(isNatList(X)) | → | a__isNatList#(X) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | | a__U11#(tt, L) | → | mark#(L) |
| a__and#(tt, X) | → | mark#(X) | | mark#(s(X)) | → | mark#(X) |
| a__length#(cons(N, L)) | → | a__isNatList#(L) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
The following SCCs where found
| a__U11#(tt, L) → a__length#(mark(L)) | a__length#(cons(N, L)) → a__U11#(a__and(a__isNatList(L), isNat(N)), L) |
| a__isNat#(s(V1)) → a__isNat#(V1) |
| mark#(and(X1, X2)) → mark#(X1) | mark#(and(X1, X2)) → a__and#(mark(X1), X2) |
| mark#(isNatIList(X)) → a__isNatIList#(X) | a__and#(tt, X) → mark#(X) |
| mark#(cons(X1, X2)) → mark#(X1) | mark#(s(X)) → mark#(X) |
| a__isNatIList#(cons(V1, V2)) → a__and#(a__isNat(V1), isNatIList(V2)) | mark#(isNatList(X)) → a__isNatList#(X) |
| a__isNatList#(cons(V1, V2)) → a__and#(a__isNat(V1), isNatList(V2)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__U11#(tt, L) | → | a__length#(mark(L)) | | a__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): y + 1
- a__U11(x,y): 2y + 3
- a__U11#(x,y): 2y + x
- a__and(x,y): 2y + x
- a__isNat(x): x + 1
- a__isNatIList(x): x + 1
- a__isNatList(x): x
- a__length(x): x + 2
- a__length#(x): x
- a__zeros: 1
- and(x,y): y + x
- cons(x,y): 3y + 2x + 1
- isNat(x): x
- isNatIList(x): x
- isNatList(x): x
- length(x): x + 1
- mark(x): 2x + 1
- nil: 1
- s(x): x
- tt: 1
- zeros: 0
Improved Usable rules
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | a__length(X) | → | length(X) |
| a__isNat(0) | → | tt | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__isNat(X) | → | isNat(X) | | a__isNatList(nil) | → | tt |
| a__isNat(s(V1)) | → | a__isNat(V1) | | mark(nil) | → | nil |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | mark(tt) | → | tt |
| a__U11(X1, X2) | → | U11(X1, X2) | | mark(0) | → | 0 |
| a__and(X1, X2) | → | and(X1, X2) | | mark(length(X)) | → | a__length(mark(X)) |
| a__and(tt, X) | → | mark(X) | | a__zeros | → | zeros |
| mark(isNat(X)) | → | a__isNat(X) | | a__isNatIList(X) | → | isNatIList(X) |
| mark(zeros) | → | a__zeros | | a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) |
| a__isNatIList(V) | → | a__isNatList(V) | | mark(and(X1, X2)) | → | a__and(mark(X1), X2) |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | mark(s(X)) | → | s(mark(X)) |
| mark(isNatList(X)) | → | a__isNatList(X) | | a__zeros | → | cons(0, zeros) |
| a__isNatIList(zeros) | → | tt | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | 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__length#(cons(N, L)) | → | a__U11#(a__and(a__isNatList(L), isNat(N)), L) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U11#(tt, L) | → | a__length#(mark(L)) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, zeros, tt, a__isNat, length, U11, a__U11, nil, cons
Strategy
There are no SCCs!
Problem 6: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | a__and#(tt, X) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | mark#(s(X)) | → | mark#(X) |
| a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) | | mark#(isNatList(X)) | → | a__isNatList#(X) |
| a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
Polynomial Interpretation
- 0: 2
- U11(x,y): 3
- a__U11(x,y): 0
- a__and(x,y): 2
- a__and#(x,y): y
- a__isNat(x): x
- a__isNatIList(x): 0
- a__isNatIList#(x): 2
- a__isNatList(x): 3
- a__isNatList#(x): 2
- a__length(x): 0
- a__zeros: 3
- and(x,y): 2y + 2x
- cons(x,y): x
- isNat(x): 2
- isNatIList(x): 2
- isNatList(x): 2
- length(x): 0
- mark(x): x
- mark#(x): x
- nil: 3
- s(x): x + 2
- tt: 2
- zeros: 2
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(isNatIList(X)) | → | a__isNatIList#(X) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | | a__and#(tt, X) | → | mark#(X) |
| mark#(cons(X1, X2)) | → | mark#(X1) | | a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) |
| a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) | | mark#(isNatList(X)) | → | a__isNatList#(X) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, zeros, tt, a__isNat, length, U11, a__U11, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): 3y + 3x + 3
- a__U11(x,y): x
- a__and(x,y): x
- a__and#(x,y): y + 1
- a__isNat(x): 0
- a__isNatIList(x): 0
- a__isNatIList#(x): x
- a__isNatList(x): 2
- a__isNatList#(x): 2x
- a__length(x): 0
- a__zeros: 3
- and(x,y): 2y + x + 2
- cons(x,y): 2y + x + 1
- isNat(x): 0
- isNatIList(x): 2x
- isNatList(x): 2x
- length(x): 0
- mark(x): 0
- mark#(x): x
- nil: 3
- s(x): 2x
- tt: 0
- zeros: 1
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__and#(tt, X) | → | mark#(X) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| a__isNatList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatList(V2)) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(isNatIList(X)) | → | a__isNatIList#(X) | | a__isNatIList#(cons(V1, V2)) | → | a__and#(a__isNat(V1), isNatIList(V2)) |
| mark#(isNatList(X)) | → | a__isNatList#(X) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
There are no SCCs!
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__isNat#(s(V1)) | → | a__isNat#(V1) |
Rewrite Rules
| a__zeros | → | cons(0, zeros) | | a__U11(tt, L) | → | s(a__length(mark(L))) |
| a__and(tt, X) | → | mark(X) | | a__isNat(0) | → | tt |
| a__isNat(length(V1)) | → | a__isNatList(V1) | | a__isNat(s(V1)) | → | a__isNat(V1) |
| a__isNatIList(V) | → | a__isNatList(V) | | a__isNatIList(zeros) | → | tt |
| a__isNatIList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatIList(V2)) | | a__isNatList(nil) | → | tt |
| a__isNatList(cons(V1, V2)) | → | a__and(a__isNat(V1), isNatList(V2)) | | a__length(nil) | → | 0 |
| a__length(cons(N, L)) | → | a__U11(a__and(a__isNatList(L), isNat(N)), L) | | mark(zeros) | → | a__zeros |
| mark(U11(X1, X2)) | → | a__U11(mark(X1), X2) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isNat(X)) | → | a__isNat(X) |
| mark(isNatList(X)) | → | a__isNatList(X) | | mark(isNatIList(X)) | → | a__isNatIList(X) |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | | mark(0) | → | 0 |
| mark(tt) | → | tt | | mark(s(X)) | → | s(mark(X)) |
| mark(nil) | → | nil | | a__zeros | → | zeros |
| a__U11(X1, X2) | → | U11(X1, X2) | | a__length(X) | → | length(X) |
| a__and(X1, X2) | → | and(X1, X2) | | a__isNat(X) | → | isNat(X) |
| a__isNatList(X) | → | isNatList(X) | | a__isNatIList(X) | → | isNatIList(X) |
Original Signature
Termination of terms over the following signature is verified: a__zeros, isNatIList, a__length, mark, and, a__and, isNat, a__isNatList, 0, isNatList, a__isNatIList, s, tt, zeros, a__isNat, length, U11, a__U11, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- U11(x,y): 0
- a__U11(x,y): 0
- a__and(x,y): 0
- a__isNat(x): 0
- a__isNat#(x): x + 1
- a__isNatIList(x): 0
- a__isNatList(x): 0
- a__length(x): 0
- a__zeros: 0
- and(x,y): 0
- cons(x,y): 0
- isNat(x): 0
- isNatIList(x): 0
- isNatList(x): 0
- length(x): 0
- mark(x): 0
- nil: 0
- s(x): x + 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:
| a__isNat#(s(V1)) | → | a__isNat#(V1) |