TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1638ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (3ms), ReductionPairSAT (7246ms), DependencyGraph (44ms), ReductionPairSAT (7075ms), DependencyGraph (3ms), ReductionPairSAT (7109ms), DependencyGraph (3ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor ReductionPairSAT (210ms).
| | – Problem 13 was processed with processor ReductionPairSAT (69ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| | – Problem 12 was processed with processor ReductionPairSAT (83ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (3ms).
| – Problem 10 was processed with processor SubtermCriterion (0ms).
| – Problem 11 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, top, eq, cons, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(length(X)) | → | length#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) | | active#(eq(s(X), s(Y))) | → | eq#(X, Y) |
| proper#(cons(any(X1), X2)) | → | any#(proper(X2)) | | active#(take(X1, X2)) | → | take#(active(X1), X2) |
| any#(proper(X)) | → | any#(any(X)) | | active#(inf(X)) | → | active#(X) |
| active#(take(s(X), cons(Y, L))) | → | take#(X, L) | | length#(ok(X)) | → | length#(X) |
| top#(mark(X)) | → | proper#(X) | | proper#(cons(any(X1), X2)) | → | any#(proper(X1)) |
| any#(proper(X)) | → | any#(any(any(X))) | | length#(mark(X)) | → | length#(X) |
| top#(mark(X)) | → | top#(proper(X)) | | active#(take(X1, X2)) | → | active#(X2) |
| any#(X) | → | s#(X) | | active#(length(X)) | → | active#(X) |
| active#(length(cons(X, L))) | → | length#(L) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
| active#(take(s(X), cons(Y, L))) | → | cons#(Y, take(X, L)) | | proper#(s(X)) | → | proper#(X) |
| proper#(cons(any(X1), X2)) | → | proper#(X1) | | proper#(eq(X1, X2)) | → | proper#(X1) |
| proper#(take(X1, X2)) | → | take#(proper(X1), proper(X2)) | | active#(inf(X)) | → | cons#(X, inf(s(X))) |
| proper#(inf(X)) | → | inf#(proper(X)) | | proper#(cons(any(X1), X2)) | → | any#(any(proper(X1))) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | proper#(inf(X)) | → | proper#(X) |
| top#(ok(X)) | → | active#(X) | | active#(inf(X)) | → | s#(X) |
| inf#(ok(X)) | → | inf#(X) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(cons(any(X1), X2)) | → | cons#(any(any(proper(X1))), any(proper(X2))) | | take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
| active#(length(X)) | → | length#(active(X)) | | active#(inf(X)) | → | inf#(s(X)) |
| active#(length(cons(X, L))) | → | s#(length(L)) | | active#(take(X1, X2)) | → | active#(X1) |
| proper#(take(X1, X2)) | → | proper#(X2) | | proper#(eq(X1, X2)) | → | eq#(proper(X1), proper(X2)) |
| proper#(eq(X1, X2)) | → | proper#(X2) | | s#(ok(X)) | → | s#(X) |
| proper#(length(X)) | → | proper#(X) | | active#(inf(X)) | → | inf#(active(X)) |
| active#(take(X1, X2)) | → | take#(X1, active(X2)) | | proper#(cons(any(X1), X2)) | → | proper#(X2) |
| any#(proper(X)) | → | any#(X) | | proper#(s(X)) | → | s#(proper(X)) |
| eq#(ok(X1), ok(X2)) | → | eq#(X1, X2) | | inf#(mark(X)) | → | inf#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
The following SCCs where found
| length#(mark(X)) → length#(X) | length#(ok(X)) → length#(X) |
| proper#(s(X)) → proper#(X) | proper#(length(X)) → proper#(X) |
| proper#(take(X1, X2)) → proper#(X1) | proper#(cons(any(X1), X2)) → proper#(X1) |
| proper#(cons(any(X1), X2)) → proper#(X2) | proper#(eq(X1, X2)) → proper#(X1) |
| proper#(take(X1, X2)) → proper#(X2) | proper#(inf(X)) → proper#(X) |
| proper#(eq(X1, X2)) → proper#(X2) |
| inf#(ok(X)) → inf#(X) | inf#(mark(X)) → inf#(X) |
| any#(proper(X)) → any#(any(any(X))) | any#(proper(X)) → any#(any(X)) |
| any#(proper(X)) → any#(X) |
| cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| eq#(ok(X1), ok(X2)) → eq#(X1, X2) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, mark(X2)) → take#(X1, X2) |
| take#(ok(X1), ok(X2)) → take#(X1, X2) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| active#(inf(X)) → active#(X) | active#(take(X1, X2)) → active#(X2) |
| active#(take(X1, X2)) → active#(X1) | active#(length(X)) → active#(X) |
Problem 3: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| any#(proper(X)) | → | any#(any(any(X))) | | any#(proper(X)) | → | any#(any(X)) |
| any#(proper(X)) | → | any#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Function Precedence
any# < s < any < proper < inf = true = mark = 0 = take = length = active = false = ok = top = cons = nil = eq
Argument Filtering
inf: collapses to 1
true: all arguments are removed from true
mark: 1
0: all arguments are removed from 0
s: collapses to 1
take: 1 2
any: collapses to 1
length: all arguments are removed from length
active: all arguments are removed from active
false: all arguments are removed from false
ok: all arguments are removed from ok
proper: 1
any#: collapses to 1
top: all arguments are removed from top
cons: all arguments are removed from cons
nil: all arguments are removed from nil
eq: 1 2
Status
true: multiset
mark: lexicographic with permutation 1 → 1
0: multiset
take: lexicographic with permutation 1 → 1 2 → 2
length: multiset
active: multiset
false: multiset
ok: multiset
proper: multiset
top: multiset
cons: multiset
nil: multiset
eq: lexicographic with permutation 1 → 1 2 → 2
Usable Rules
| any(X) → s(X) | any(proper(X)) → any(any(any(X))) |
| s(ok(X)) → ok(s(X)) |
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| any#(proper(X)) → any#(any(any(X))) | any#(proper(X)) → any#(any(X)) |
Problem 13: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| any#(proper(X)) | → | any#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, top, eq, cons, nil
Strategy
Function Precedence
inf = true = mark = 0 = s = take = any = length = active = false = ok = proper = any# = top = cons = nil = eq
Argument Filtering
inf: all arguments are removed from inf
true: all arguments are removed from true
mark: all arguments are removed from mark
0: all arguments are removed from 0
s: all arguments are removed from s
take: all arguments are removed from take
any: 1
length: all arguments are removed from length
active: all arguments are removed from active
false: all arguments are removed from false
ok: all arguments are removed from ok
proper: 1
any#: 1
top: all arguments are removed from top
cons: 1 2
nil: all arguments are removed from nil
eq: all arguments are removed from eq
Status
inf: multiset
true: multiset
mark: multiset
0: multiset
s: multiset
take: multiset
any: lexicographic with permutation 1 → 1
length: multiset
active: multiset
false: multiset
ok: multiset
proper: multiset
any#: lexicographic with permutation 1 → 1
top: multiset
cons: lexicographic with permutation 1 → 1 2 → 2
nil: multiset
eq: multiset
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| any#(proper(X)) → any#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(inf(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X2) |
| active#(take(X1, X2)) | → | active#(X1) | | active#(length(X)) | → | active#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(inf(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X2) |
| active#(length(X)) | → | active#(X) | | active#(take(X1, X2)) | → | active#(X1) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(mark(X)) | → | length#(X) | | length#(ok(X)) | → | length#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(ok(X1), ok(X2)) | → | eq#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(ok(X1), ok(X2)) | → | eq#(X1, X2) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
| take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(ok(X1), ok(X2)) | → | take#(X1, X2) |
Problem 12: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, top, eq, cons, nil
Strategy
Function Precedence
inf = true = mark = take# = 0 = s = take = any = length = active = false = ok = proper = top = cons = nil = eq
Argument Filtering
inf: collapses to 1
true: all arguments are removed from true
mark: 1
take#: collapses to 2
0: all arguments are removed from 0
s: collapses to 1
take: all arguments are removed from take
any: collapses to 1
length: all arguments are removed from length
active: collapses to 1
false: all arguments are removed from false
ok: all arguments are removed from ok
proper: collapses to 1
top: all arguments are removed from top
cons: collapses to 1
nil: all arguments are removed from nil
eq: 1 2
Status
true: multiset
mark: lexicographic with permutation 1 → 1
0: multiset
take: multiset
length: multiset
false: multiset
ok: multiset
top: multiset
nil: multiset
eq: lexicographic with permutation 1 → 2 2 → 1
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| take#(X1, mark(X2)) → take#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| inf#(ok(X)) | → | inf#(X) | | inf#(mark(X)) | → | inf#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| inf#(ok(X)) | → | inf#(X) | | inf#(mark(X)) | → | inf#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(s(X)) | → | proper#(X) | | proper#(length(X)) | → | proper#(X) |
| proper#(take(X1, X2)) | → | proper#(X1) | | proper#(cons(any(X1), X2)) | → | proper#(X1) |
| proper#(cons(any(X1), X2)) | → | proper#(X2) | | proper#(eq(X1, X2)) | → | proper#(X1) |
| proper#(take(X1, X2)) | → | proper#(X2) | | proper#(inf(X)) | → | proper#(X) |
| proper#(eq(X1, X2)) | → | proper#(X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| active(inf(X)) | → | inf(active(X)) | | active(take(X1, X2)) | → | take(active(X1), X2) |
| active(take(X1, X2)) | → | take(X1, active(X2)) | | active(length(X)) | → | length(active(X)) |
| inf(mark(X)) | → | mark(inf(X)) | | take(mark(X1), X2) | → | mark(take(X1, X2)) |
| take(X1, mark(X2)) | → | mark(take(X1, X2)) | | length(mark(X)) | → | mark(length(X)) |
| proper(eq(X1, X2)) | → | eq(proper(X1), proper(X2)) | | proper(0) | → | ok(0) |
| proper(true) | → | ok(true) | | proper(s(X)) | → | s(proper(X)) |
| proper(false) | → | ok(false) | | proper(inf(X)) | → | inf(proper(X)) |
| proper(cons(any(X1), X2)) | → | cons(any(any(proper(X1))), any(proper(X2))) | | proper(take(X1, X2)) | → | take(proper(X1), proper(X2)) |
| proper(nil) | → | ok(nil) | | proper(length(X)) | → | length(proper(X)) |
| eq(ok(X1), ok(X2)) | → | ok(eq(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| inf(ok(X)) | → | ok(inf(X)) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| take(ok(X1), ok(X2)) | → | ok(take(X1, X2)) | | length(ok(X)) | → | ok(length(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
| any(X) | → | s(X) | | any(proper(X)) | → | any(any(any(X))) |
Original Signature
Termination of terms over the following signature is verified: inf, true, mark, 0, s, take, any, length, active, false, ok, proper, nil, cons, eq, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(length(X)) | → | proper#(X) | | proper#(s(X)) | → | proper#(X) |
| proper#(cons(any(X1), X2)) | → | proper#(X2) | | proper#(take(X1, X2)) | → | proper#(X1) |
| proper#(cons(any(X1), X2)) | → | proper#(X1) | | proper#(eq(X1, X2)) | → | proper#(X1) |
| proper#(take(X1, X2)) | → | proper#(X2) | | proper#(inf(X)) | → | proper#(X) |
| proper#(eq(X1, X2)) | → | proper#(X2) |