TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60000 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (491ms).
 | – Problem 2 was processed with processor ForwardNarrowing (6ms).
 |    | – Problem 10 was processed with processor ForwardNarrowing (4ms).
 |    |    | – Problem 11 was processed with processor ForwardNarrowing (2ms).
 |    |    |    | – Problem 12 was processed with processor ForwardNarrowing (6ms).
 |    |    |    |    | – Problem 13 was processed with processor ForwardNarrowing (3ms).
 |    |    |    |    |    | – Problem 14 was processed with processor ForwardNarrowing (2ms).
 |    |    |    |    |    |    | – Problem 15 was processed with processor ForwardNarrowing (7ms).
 |    |    |    |    |    |    |    | – Problem 16 was processed with processor ForwardNarrowing (5ms).
 |    |    |    |    |    |    |    |    | – Problem 17 was processed with processor ForwardNarrowing (8ms).
 |    |    |    |    |    |    |    |    |    | – Problem 18 was processed with processor ForwardNarrowing (6ms).
 |    |    |    |    |    |    |    |    |    |    | – Problem 19 was processed with processor ForwardNarrowing (6ms).
 |    |    |    |    |    |    |    |    |    |    |    | – Problem 20 was processed with processor ForwardNarrowing (5ms).
 |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 21 was processed with processor ForwardNarrowing (7ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 22 was processed with processor ForwardNarrowing (5ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 23 was processed with processor ForwardNarrowing (6ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 24 was processed with processor ForwardNarrowing (6ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 25 was processed with processor ForwardNarrowing (9ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 26 was processed with processor ForwardNarrowing (11ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 27 was processed with processor ForwardNarrowing (4ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 28 was processed with processor ForwardNarrowing (7ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 29 was processed with processor ForwardNarrowing (16ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 30 was processed with processor ForwardNarrowing (57ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 31 was processed with processor ForwardNarrowing (124ms).
 |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    |    | – Problem 32 remains open; application of the following processors failed [ForwardNarrowing (30ms), ForwardNarrowing (63ms), ForwardNarrowing (34ms), ForwardNarrowing (81ms), ForwardNarrowing (48ms), ForwardNarrowing (26ms), ForwardNarrowing (49ms), ForwardNarrowing (77ms), ForwardNarrowing (50ms), ForwardNarrowing (53ms), ForwardNarrowing (111ms), ForwardNarrowing (115ms), ForwardNarrowing (40ms), ForwardNarrowing (134ms), ForwardNarrowing (125ms), ForwardNarrowing (112ms), ForwardNarrowing (104ms), ForwardNarrowing (119ms), ForwardNarrowing (128ms), ForwardNarrowing (timeout)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 | – Problem 4 was processed with processor SubtermCriterion (3ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (3ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (0ms).

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(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2)) → proper#(X1)proper#(length(X)) → length#(proper(X))
top#(ok(X)) → top#(active(X))cons#(mark(X1), X2) → cons#(X1, X2)
active#(from(X)) → from#(active(X))proper#(length1(X)) → length1#(proper(X))
cons#(ok(X1), ok(X2)) → cons#(X1, X2)from#(mark(X)) → from#(X)
from#(ok(X)) → from#(X)top#(ok(X)) → active#(X)
active#(cons(X1, X2)) → cons#(active(X1), X2)active#(from(X)) → cons#(X, from(s(X)))
proper#(from(X)) → from#(proper(X))length#(ok(X)) → length#(X)
top#(mark(X)) → proper#(X)proper#(from(X)) → proper#(X)
proper#(length1(X)) → proper#(X)top#(mark(X)) → top#(proper(X))
proper#(cons(X1, X2)) → proper#(X2)active#(from(X)) → active#(X)
active#(length(cons(X, Y))) → length1#(Y)active#(s(X)) → s#(active(X))
s#(ok(X)) → s#(X)active#(from(X)) → s#(X)
s#(mark(X)) → s#(X)proper#(length(X)) → proper#(X)
proper#(s(X)) → proper#(X)active#(length(cons(X, Y))) → s#(length1(Y))
proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))active#(s(X)) → active#(X)
proper#(s(X)) → s#(proper(X))active#(length1(X)) → length#(X)
length1#(ok(X)) → length1#(X)active#(from(X)) → from#(s(X))
active#(cons(X1, X2)) → active#(X1)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The following SCCs where found

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)
active#(from(X)) → active#(X)active#(s(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)
length#(ok(X)) → length#(X)
from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)
length1#(ok(X)) → length1#(X)
top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))
s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)
proper#(length1(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(length(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(from(X)) → proper#(X)

Problem 2: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(mark(X)) → top#(proper(X)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(proper(_x21))) 
top#(ok(0)) 
top#(cons(proper(_x21), proper(_x22))) 
top#(s(proper(_x21))) 
top#(length(proper(_x21))) 
top#(length1(proper(_x21))) 
top#(ok(nil)) 
Thus, the rule top#(mark(X)) → top#(proper(X)) is replaced by the following rules:
top#(mark(0)) → top#(ok(0))top#(mark(nil)) → top#(ok(nil))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))

Problem 10: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(mark(0)) → top#(ok(0))top#(ok(X)) → top#(active(X))
top#(mark(nil)) → top#(ok(nil))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(length(_x21))) → top#(length(proper(_x21)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(X)) → top#(active(X)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(mark(0)) 
top#(s(active(_x21))) 
top#(mark(s(length1(_x21)))) 
top#(mark(length(_x21))) 
top#(cons(active(_x21), _x22)) 
top#(from(active(_x21))) 
top#(mark(cons(_x21, from(s(_x21))))) 
Thus, the rule top#(ok(X)) → top#(active(X)) is replaced by the following rules:
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(_x21))) → top#(from(active(_x21)))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Problem 11: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(mark(0)) → top#(ok(0))
top#(ok(from(_x21))) → top#(from(active(_x21)))top#(mark(nil)) → top#(ok(nil))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(mark(0)) → top#(ok(0)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
Thus, the rule top#(mark(0)) → top#(ok(0)) is deleted.

Problem 12: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(_x21))) → top#(from(active(_x21)))
top#(mark(nil)) → top#(ok(nil))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(_x21))) → top#(from(active(_x21))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(0))) 
top#(from(mark(cons(_x41, from(s(_x41)))))) 
top#(from(s(active(_x41)))) 
top#(from(from(active(_x41)))) 
top#(from(mark(length(_x41)))) 
top#(from(mark(s(length1(_x41))))) 
top#(from(cons(active(_x41), _x42))) 
Thus, the rule top#(ok(from(_x21))) → top#(from(active(_x21))) is replaced by the following rules:
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(length1(_x41)))) → top#(from(mark(length(_x41))))
top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))

Problem 13: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(length1(_x41)))) → top#(from(mark(length(_x41))))
top#(mark(nil)) → top#(ok(nil))top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))
top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(length1(_x41)))) → top#(from(mark(length(_x41)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(mark(from(length(_x41)))) 
top#(from(mark(ok(length(_x51))))) 
Thus, the rule top#(ok(from(length1(_x41)))) → top#(from(mark(length(_x41)))) is replaced by the following rules:
top#(ok(from(length1(ok(_x51))))) → top#(from(mark(ok(length(_x51)))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))

Problem 14: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(mark(nil)) → top#(ok(nil))
top#(ok(from(length1(ok(_x51))))) → top#(from(mark(ok(length(_x51)))))top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))
top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(mark(nil)) → top#(ok(nil)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
Thus, the rule top#(mark(nil)) → top#(ok(nil)) is deleted.

Problem 15: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(length1(ok(_x51))))) → top#(from(mark(ok(length(_x51)))))
top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(length1(ok(_x51))))) → top#(from(mark(ok(length(_x51))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(ok(ok(length(_x61)))))) 
top#(mark(from(ok(length(_x51))))) 
Thus, the rule top#(ok(from(length1(ok(_x51))))) → top#(from(mark(ok(length(_x51))))) is replaced by the following rules:
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(from(length1(ok(ok(_x61)))))) → top#(from(mark(ok(ok(length(_x61))))))

Problem 16: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(_x61)))))) → top#(from(mark(ok(ok(length(_x61))))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))
top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(length1(ok(ok(_x61)))))) → top#(from(mark(ok(ok(length(_x61)))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(mark(from(ok(ok(length(_x61)))))) 
top#(from(mark(ok(ok(ok(length(_x71))))))) 
Thus, the rule top#(ok(from(length1(ok(ok(_x61)))))) → top#(from(mark(ok(ok(length(_x61)))))) is replaced by the following rules:
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(from(mark(ok(ok(ok(length(_x71)))))))

Problem 17: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(from(mark(ok(ok(ok(length(_x71)))))))
top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(from(mark(ok(ok(ok(length(_x71))))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(mark(from(ok(ok(ok(length(_x71))))))) 
top#(from(mark(ok(ok(ok(ok(length(_x81)))))))) 
Thus, the rule top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(from(mark(ok(ok(ok(length(_x71))))))) is replaced by the following rules:
top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))

Problem 18: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))
top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42)))top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(cons(s(active(_x51)), _x42))) 
top#(from(cons(mark(length(_x51)), _x42))) 
top#(from(cons(cons(active(_x51), _x52), _x42))) 
top#(from(cons(from(active(_x51)), _x42))) 
top#(from(cons(mark(s(length1(_x51))), _x42))) 
top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42))) 
top#(from(cons(mark(0), _x42))) 
Thus, the rule top#(ok(from(cons(_x41, _x42)))) → top#(from(cons(active(_x41), _x42))) is replaced by the following rules:
top#(ok(from(cons(length1(_x51), _x42)))) → top#(from(cons(mark(length(_x51)), _x42)))top#(ok(from(cons(length(cons(_x52, _x51)), _x42)))) → top#(from(cons(mark(s(length1(_x51))), _x42)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))

Problem 19: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(cons(length1(_x51), _x42)))) → top#(from(cons(mark(length(_x51)), _x42)))top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))
top#(ok(from(cons(length(cons(_x52, _x51)), _x42)))) → top#(from(cons(mark(s(length1(_x51))), _x42)))top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(cons(length1(_x51), _x42)))) → top#(from(cons(mark(length(_x51)), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(cons(mark(ok(length(_x61))), _x42))) 
top#(from(mark(cons(length(_x51), _x32)))) 
Thus, the rule top#(ok(from(cons(length1(_x51), _x42)))) → top#(from(cons(mark(length(_x51)), _x42))) is replaced by the following rules:
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))

Problem 20: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(cons(length(cons(_x52, _x51)), _x42)))) → top#(from(cons(mark(s(length1(_x51))), _x42)))
top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))
top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(cons(length(cons(_x52, _x51)), _x42)))) → top#(from(cons(mark(s(length1(_x51))), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(cons(s(length1(_x51)), _x32)))) 
top#(from(cons(mark(s(ok(length1(_x71)))), _x42))) 
Thus, the rule top#(ok(from(cons(length(cons(_x52, _x51)), _x42)))) → top#(from(cons(mark(s(length1(_x51))), _x42))) is replaced by the following rules:
top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))

Problem 21: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(_x41)))) → top#(from(from(active(_x41))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(from(_x41)))) → top#(from(from(active(_x41)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(from(cons(active(_x51), _x52)))) 
top#(from(from(from(active(_x51))))) 
top#(from(from(mark(length(_x51))))) 
top#(from(from(mark(s(length1(_x51)))))) 
top#(from(from(s(active(_x51))))) 
top#(from(from(mark(cons(_x51, from(s(_x51))))))) 
top#(from(from(mark(0)))) 
Thus, the rule top#(ok(from(from(_x41)))) → top#(from(from(active(_x41)))) is replaced by the following rules:
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))top#(ok(from(from(length(nil))))) → top#(from(from(mark(0))))
top#(ok(from(from(length1(_x51))))) → top#(from(from(mark(length(_x51)))))top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))
top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))

Problem 22: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(from(length(nil))))) → top#(from(from(mark(0))))top#(ok(from(from(length1(_x51))))) → top#(from(from(mark(length(_x51)))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(from(length(nil))))) → top#(from(from(mark(0)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(from(0)))) 
Thus, the rule top#(ok(from(from(length(nil))))) → top#(from(from(mark(0)))) is replaced by the following rules:
top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))

Problem 23: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(from(length1(_x51))))) → top#(from(from(mark(length(_x51)))))top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(from(length1(_x51))))) → top#(from(from(mark(length(_x51))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(from(mark(ok(length(_x61)))))) 
top#(from(mark(from(length(_x51))))) 
Thus, the rule top#(ok(from(from(length1(_x51))))) → top#(from(from(mark(length(_x51))))) is replaced by the following rules:
top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))

Problem 24: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41)))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))
top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(s(ok(length1(_x61)))))) 
top#(mark(from(s(length1(_x41))))) 
Thus, the rule top#(ok(from(length(cons(_x42, _x41))))) → top#(from(mark(s(length1(_x41))))) is replaced by the following rules:
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))

Problem 25: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(mark(from(_x21))) → top#(from(proper(_x21)))top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))
top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))
top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))
top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(s(_x21))) → top#(s(active(_x21)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(cons(from(mark(length(_x61))), _x42))) 
top#(from(cons(from(mark(s(length1(_x61)))), _x42))) 
top#(from(cons(from(s(active(_x61))), _x42))) 
top#(from(cons(from(from(active(_x61))), _x42))) 
top#(from(cons(from(cons(active(_x61), _x62)), _x42))) 
top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42))) 
top#(from(cons(from(mark(0)), _x42))) 
Thus, the rule top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(from(active(_x51)), _x42))) is replaced by the following rules:
top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(from(mark(0)), _x42)))top#(ok(from(cons(from(cons(_x61, _x62)), _x42)))) → top#(from(cons(from(cons(active(_x61), _x62)), _x42)))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))
top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(from(mark(length(_x61))), _x42)))

Problem 26: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(cons(from(cons(_x61, _x62)), _x42)))) → top#(from(cons(from(cons(active(_x61), _x62)), _x42)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(length(nil)))) → top#(from(mark(0)))top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))
top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(from(mark(0)), _x42)))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))
top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(from(mark(length(_x61))), _x42)))
top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))
top#(ok(length1(_x21))) → top#(mark(length(_x21)))top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))
top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(cons(from(cons(_x61, _x62)), _x42)))) → top#(from(cons(from(cons(active(_x61), _x62)), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(cons(from(cons(s(active(_x71)), _x62)), _x42))) 
top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42))) 
top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42))) 
top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42))) 
top#(from(cons(from(cons(mark(0), _x62)), _x42))) 
top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42))) 
top#(from(cons(from(cons(mark(s(length1(_x71))), _x62)), _x42))) 
Thus, the rule top#(ok(from(cons(from(cons(_x61, _x62)), _x42)))) → top#(from(cons(from(cons(active(_x61), _x62)), _x42))) is replaced by the following rules:
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))top#(ok(from(cons(from(cons(s(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(s(active(_x71)), _x62)), _x42)))
top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(length1(_x71))), _x62)), _x42)))top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))
top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))

Problem 27: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(from(mark(0)), _x42)))
top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))
top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))
top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))
top#(ok(from(cons(from(cons(s(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(s(active(_x71)), _x62)), _x42)))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))
top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(length1(_x71))), _x62)), _x42)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))
top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))
top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))
top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(from(mark(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))
top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(from(mark(0)), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(cons(mark(from(0)), _x42))) 
Thus, the rule top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(from(mark(0)), _x42))) is replaced by the following rules:
top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(mark(from(0)), _x42)))

Problem 28: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42)))
top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(from(from(mark(s(length1(_x51))))))top#(ok(from(cons(cons(_x51, _x52), _x42)))) → top#(from(cons(cons(active(_x51), _x52), _x42)))
top#(ok(cons(_x21, _x22))) → top#(cons(active(_x21), _x22))top#(ok(from(from(length1(ok(_x61)))))) → top#(from(from(mark(ok(length(_x61))))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(from(from(from(_x51))))) → top#(from(from(from(active(_x51)))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(from(cons(s(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(s(active(_x71)), _x62)), _x42)))
top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(s(ok(length1(_x71)))), _x42)))top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(length1(_x71))), _x62)), _x42)))
top#(mark(s(_x21))) → top#(s(proper(_x21)))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(mark(from(0)), _x42)))
top#(ok(s(_x21))) → top#(s(active(_x21)))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))
top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))
top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))
top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(from(mark(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))
top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(length(nil))) → top#(mark(0))
top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, ok, mark, proper, length1, from, top, nil, cons

Strategy

The right-hand side of the rule top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(from(mark(cons(0, _x32)))) 
Thus, the rule top#(ok(from(cons(length(nil), _x42)))) → top#(from(cons(mark(0), _x42))) is replaced by the following rules:
top#(ok(from(cons(length(nil), _x32)))) → top#(from(mark(cons(0, _x32))))

Problem 29: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(cons(_x81, from(s(_x81))))), _x62)), _x42)))top#(ok(s(s(from(_x51))))) → top#(s(s(from(active(_x51)))))
top#(ok(s(s(length1(ok(_x61)))))) → top#(s(s(mark(ok(length(_x61))))))top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(mark(cons(_x61, from(s(_x61))))))))
top#(ok(s(s(length(nil))))) → top#(s(s(mark(0))))top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(mark(cons(_x61, from(s(_x61))))), _x22))
top#(ok(s(length1(_x41)))) → top#(s(mark(length(_x41))))top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))
top#(ok(from(cons(length(nil), _x32)))) → top#(mark(from(cons(0, _x32))))top#(ok(s(s(cons(_x51, _x52))))) → top#(s(s(cons(active(_x51), _x52))))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))top#(ok(s(length(cons(_x42, _x41))))) → top#(mark(s(s(length1(_x41)))))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(cons(_x81, from(s(_x81)))), _x72))))))top#(ok(s(cons(_x41, _x42)))) → top#(s(cons(active(_x41), _x42)))
top#(ok(from(cons(from(cons(length(cons(_x72, ok(_x91))), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(ok(length1(_x91)))), _x62)), _x42)))top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(mark(from(from(s(length1(_x51))))))
top#(ok(cons(cons(_x41, _x42), _x22))) → top#(cons(cons(active(_x41), _x42), _x22))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(ok(ok(s(length1(_x81))))))))
top#(ok(from(from(from(s(cons(cons(_x81, _x82), _x72))))))) → top#(from(from(from(s(cons(cons(active(_x81), _x82), _x72))))))top#(ok(from(from(length1(ok(_x61)))))) → top#(from(mark(from(ok(length(_x61))))))
top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(from(cons(mark(s(ok(ok(length1(_x81))))), _x42)))top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))
top#(ok(from(cons(cons(length1(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(length(_x61)), _x52), _x42)))top#(ok(cons(length(cons(_x42, _x41)), _x32))) → top#(mark(cons(s(length1(_x41)), _x32)))
top#(ok(from(cons(cons(from(_x61), _x52), _x42)))) → top#(from(cons(cons(from(active(_x61)), _x52), _x42)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(from(from(mark(ok(s(length1(_x71)))))))
top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(from(mark(ok(from(s(length1(_x71)))))))top#(ok(s(length(nil)))) → top#(s(mark(0)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(_x101))))), _x52), _x42)))) → top#(from(cons(cons(s(mark(s(ok(ok(length1(_x101)))))), _x52), _x42)))top#(ok(from(from(length1(ok(ok(_x71))))))) → top#(from(from(mark(ok(ok(length(_x71)))))))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(mark(from(_x21))) → top#(from(proper(_x21)))
top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(from(mark(length(_x61))), _x42)))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(s(ok(length1(_x61))))))
top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))
top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))top#(ok(from(from(from(s(s(_x71))))))) → top#(from(from(from(s(s(active(_x71)))))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(cons(s(cons(_x61, _x62)), _x22))) → top#(cons(s(cons(active(_x61), _x62)), _x22))
top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))top#(ok(s(s(from(_x51))))) → top#(s(s(mark(cons(_x51, from(s(_x51)))))))
top#(ok(from(from(from(s(from(_x71))))))) → top#(from(from(from(s(from(active(_x71)))))))top#(ok(from(from(from(s(cons(length(nil), _x72))))))) → top#(from(from(from(s(cons(mark(0), _x72))))))
top#(ok(s(from(_x41)))) → top#(s(mark(cons(_x41, from(s(_x41))))))top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))
top#(ok(length(nil))) → top#(mark(0))top#(ok(from(from(from(s(cons(length(cons(_x82, _x81)), _x62))))))) → top#(from(from(from(s(mark(cons(s(length1(_x81)), _x62)))))))
top#(ok(s(s(length(cons(_x52, _x51)))))) → top#(s(s(mark(s(length1(_x51))))))top#(ok(from(cons(from(cons(s(length(cons(_x82, _x81))), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(s(length1(_x81)))), _x62)), _x42)))
top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))top#(ok(s(s(length1(_x51))))) → top#(s(mark(s(length(_x51)))))
top#(ok(from(from(from(s(cons(length1(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(length(_x81)), _x72))))))top#(ok(cons(from(_x41), _x22))) → top#(cons(mark(cons(_x41, from(s(_x41)))), _x22))
top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(s(ok(length1(_x71)))))))top#(ok(s(s(s(_x51))))) → top#(s(s(s(active(_x51)))))
top#(ok(from(from(from(s(cons(length(cons(_x82, ok(_x101))), _x72))))))) → top#(from(from(from(s(cons(mark(s(ok(length1(_x101)))), _x72))))))top#(ok(from(from(from(length1(_x61)))))) → top#(from(from(mark(from(length(_x61))))))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(from(active(_x81)), _x72))))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(s(length(cons(_x42, ok(_x61)))))) → top#(s(mark(s(ok(length1(_x61))))))top#(ok(cons(length1(_x41), _x22))) → top#(cons(mark(length(_x41)), _x22))
top#(ok(from(from(from(s(cons(s(_x81), _x72))))))) → top#(from(from(from(s(cons(s(active(_x81)), _x72))))))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(from(mark(s(ok(ok(length1(_x81))))))))top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(mark(from(0)), _x42)))top#(ok(cons(length(cons(_x42, ok(_x71))), _x22))) → top#(cons(mark(s(ok(length1(_x71)))), _x22))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(from(active(_x71))), _x52), _x42)))top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))
top#(ok(cons(s(length1(_x61)), _x22))) → top#(cons(s(mark(length(_x61))), _x22))top#(ok(cons(length(nil), _x32))) → top#(mark(cons(0, _x32)))
top#(ok(from(cons(cons(length(cons(_x62, _x61)), _x52), _x42)))) → top#(from(cons(cons(mark(s(length1(_x61))), _x52), _x42)))top#(ok(from(cons(cons(s(length1(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(length(_x71))), _x52), _x42)))
top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x52)), _x42)))) → top#(from(cons(from(mark(cons(s(length1(_x71)), _x52))), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(s(mark(ok(s(length1(_x91))))), _x52), _x42)))top#(ok(from(from(from(s(from(_x71))))))) → top#(from(from(from(s(mark(cons(_x71, from(s(_x71)))))))))
top#(ok(cons(s(length(nil)), _x22))) → top#(cons(s(mark(0)), _x22))top#(ok(from(from(from(s(length1(_x71))))))) → top#(from(from(from(s(mark(length(_x71)))))))
top#(ok(from(cons(cons(s(cons(_x71, _x72)), _x52), _x42)))) → top#(from(cons(cons(s(cons(active(_x71), _x72)), _x52), _x42)))top#(ok(from(cons(from(cons(s(s(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(s(active(_x81))), _x62)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(ok(_x91))))))))) → top#(from(mark(from(ok(s(ok(ok(length1(_x91)))))))))top#(ok(from(cons(cons(s(length(cons(_x72, _x71))), _x42), _x42)))) → top#(from(cons(mark(cons(s(s(length1(_x71))), _x42)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(ok(s(length1(_x71)))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(s(ok(ok(length1(_x81))))))))
top#(ok(from(cons(from(cons(s(length(nil)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(0)), _x62)), _x42)))top#(ok(from(cons(cons(s(length(nil)), _x52), _x42)))) → top#(from(cons(cons(s(mark(0)), _x52), _x42)))
top#(ok(from(from(from(length1(ok(_x71))))))) → top#(from(from(from(mark(ok(length(_x71)))))))top#(ok(from(cons(cons(cons(_x61, _x62), _x52), _x42)))) → top#(from(cons(cons(cons(active(_x61), _x62), _x52), _x42)))
top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))
top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(ok(s(length1(_x71)))), _x42)))top#(ok(from(cons(cons(s(s(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(s(active(_x71))), _x52), _x42)))
top#(ok(s(from(_x41)))) → top#(s(from(active(_x41))))top#(ok(from(from(from(length(nil)))))) → top#(from(from(from(mark(0)))))
top#(ok(from(from(from(cons(_x61, _x62)))))) → top#(from(from(from(cons(active(_x61), _x62)))))top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))
top#(ok(cons(s(length(cons(_x62, _x61))), _x22))) → top#(cons(s(mark(s(length1(_x61)))), _x22))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(ok(from(from(from(length(cons(_x62, _x61))))))) → top#(from(from(from(mark(s(length1(_x61)))))))top#(ok(from(cons(from(cons(s(length1(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(length(_x81))), _x62)), _x42)))
top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(from(active(_x81))), _x62)), _x42)))top#(ok(from(cons(cons(length(nil), _x52), _x42)))) → top#(from(cons(cons(mark(0), _x52), _x42)))
top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(from(active(_x61))), _x22))
top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))top#(ok(from(cons(cons(from(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(cons(_x61, from(s(_x61)))), _x52), _x42)))
top#(ok(from(from(from(s(length(cons(_x72, _x71)))))))) → top#(from(from(from(s(mark(s(length1(_x71))))))))top#(ok(from(cons(from(cons(s(cons(_x81, _x82)), _x62)), _x42)))) → top#(from(cons(from(cons(s(cons(active(_x81), _x82)), _x62)), _x42)))
top#(ok(cons(from(_x41), _x22))) → top#(cons(from(active(_x41)), _x22))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(ok(from(s(ok(length1(_x81))))))))
top#(ok(from(from(from(s(length(nil))))))) → top#(from(from(from(s(mark(0))))))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(from(mark(cons(s(ok(length1(_x71))), _x32))))
top#(ok(cons(s(s(_x61)), _x22))) → top#(cons(s(s(active(_x61))), _x22))top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(from(active(_x61))))))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(mark(s(s(ok(length1(_x91))))), _x52), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(mark(from(from(ok(s(ok(length1(_x81))))))))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(s(s(from(_x51))))) → top#(s(s(from(active(_x51))))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(s(s(from(from(active(_x61)))))) 
top#(s(s(from(mark(0))))) 
top#(s(s(from(mark(s(length1(_x61))))))) 
top#(s(s(from(mark(cons(_x61, from(s(_x61)))))))) 
top#(s(s(from(s(active(_x61)))))) 
top#(s(s(from(cons(active(_x61), _x62))))) 
top#(s(s(from(mark(length(_x61)))))) 
Thus, the rule top#(ok(s(s(from(_x51))))) → top#(s(s(from(active(_x51))))) is replaced by the following rules:
top#(ok(s(s(from(length(nil)))))) → top#(s(s(from(mark(0)))))top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(from(active(_x61))))))
top#(ok(s(s(from(length(cons(_x62, _x61))))))) → top#(s(s(from(mark(s(length1(_x61)))))))top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(mark(cons(_x61, from(s(_x61))))))))
top#(ok(s(s(from(length1(_x61)))))) → top#(s(s(from(mark(length(_x61))))))top#(ok(s(s(from(s(_x61)))))) → top#(s(s(from(s(active(_x61))))))
top#(ok(s(s(from(cons(_x61, _x62)))))) → top#(s(s(from(cons(active(_x61), _x62)))))

Problem 30: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(mark(cons(_x61, from(s(_x61))))))))top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(mark(cons(_x61, from(s(_x61))))), _x22))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))top#(ok(s(cons(from(_x51), _x42)))) → top#(s(cons(mark(cons(_x51, from(s(_x51)))), _x42)))
top#(ok(s(s(from(s(from(cons(from(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(mark(cons(_x91, from(s(_x91)))), _x82)))))))top#(ok(s(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))
top#(ok(s(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))top#(ok(s(length1(_x41)))) → top#(mark(s(length(_x41))))
top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(mark(cons(_x61, from(s(_x61))))))))top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))
top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(s(cons(cons(from(s(from(length1(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(from(length(_x91))))), _x52), _x42)))top#(ok(from(from(length(nil))))) → top#(from(mark(from(0))))
top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x32)))) → top#(from(mark(cons(s(ok(ok(length1(_x81)))), _x32))))top#(ok(s(cons(cons(from(length(nil)), _x42), _x42)))) → top#(s(cons(mark(cons(from(0), _x42)), _x42)))
top#(ok(from(from(from(s(cons(length(nil), _x72))))))) → top#(from(from(from(s(cons(mark(0), _x72))))))top#(ok(from(from(from(s(from(_x71))))))) → top#(from(from(from(s(from(active(_x71)))))))
top#(ok(s(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(mark(s(cons(s(ok(length1(_x71))), _x32))))top#(ok(s(from(_x41)))) → top#(s(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(cons(cons(cons(_x61, _x62), _x52), _x42)))) → top#(s(cons(cons(cons(active(_x61), _x62), _x52), _x42)))top#(ok(s(s(from(s(from(s(_x81)))))))) → top#(s(s(from(s(from(s(active(_x81))))))))
top#(ok(s(s(from(cons(length(cons(_x72, ok(_x91))), _x62)))))) → top#(s(s(from(cons(mark(ok(s(length1(_x91)))), _x62)))))top#(ok(length(nil))) → top#(mark(0))
top#(mark(from(0))) → top#(from(ok(0)))top#(ok(s(s(from(cons(from(_x71), _x62)))))) → top#(s(s(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)))))
top#(ok(s(s(length1(ok(_x61)))))) → top#(mark(s(s(ok(length(_x61))))))top#(ok(s(s(from(s(from(length(nil)))))))) → top#(s(s(from(s(from(mark(0)))))))
top#(ok(from(cons(cons(from(s(from(_x81))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(active(_x81)))), _x52), _x42)))top#(ok(from(from(from(s(cons(length(cons(_x82, _x81)), _x62))))))) → top#(from(from(from(s(mark(cons(s(length1(_x81)), _x62)))))))
top#(ok(from(cons(from(cons(s(length(cons(_x82, _x81))), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(s(length1(_x81)))), _x62)), _x42)))top#(ok(from(length(cons(_x42, ok(ok(_x71))))))) → top#(from(mark(s(ok(ok(length1(_x71)))))))
top#(ok(from(cons(cons(from(s(s(_x81))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(active(_x81)))), _x52), _x42)))top#(ok(s(s(cons(from(_x61), _x52))))) → top#(s(s(cons(mark(cons(_x61, from(s(_x61)))), _x52))))
top#(ok(s(cons(length1(_x51), _x42)))) → top#(s(cons(mark(length(_x51)), _x42)))top#(ok(s(cons(cons(length1(_x61), _x52), _x42)))) → top#(s(cons(cons(mark(length(_x61)), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(active(_x91))))), _x52), _x42)))top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(s(ok(length1(_x71)))))))
top#(ok(from(cons(cons(from(length1(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(mark(length(_x71))), _x52), _x42)))top#(ok(s(s(from(cons(length1(_x71), _x62)))))) → top#(s(s(from(cons(mark(length(_x71)), _x62)))))
top#(ok(s(s(cons(cons(_x61, _x62), _x52))))) → top#(s(s(cons(cons(active(_x61), _x62), _x52))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(mark(from(ok(from(s(ok(length1(_x81))))))))
top#(ok(s(cons(cons(from(s(s(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(s(length1(_x91)))))), _x52), _x42)))top#(ok(s(s(s(_x51))))) → top#(s(s(s(active(_x51)))))
top#(mark(from(nil))) → top#(from(ok(nil)))top#(ok(s(cons(cons(from(s(s(length1(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(length(_x91))))), _x52), _x42)))
top#(ok(s(cons(cons(from(length1(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(mark(length(_x71))), _x52), _x42)))top#(ok(s(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(from(active(_x71))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(length(nil)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(0)))), _x52), _x42)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(from(from(s(cons(s(_x81), _x72))))))) → top#(from(from(from(s(cons(s(active(_x81)), _x72))))))top#(ok(from(cons(cons(from(s(cons(_x81, _x82))), _x52), _x42)))) → top#(from(cons(cons(from(s(cons(active(_x81), _x82))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(length(nil))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(0))), _x52), _x42)))top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))
top#(ok(s(s(from(s(length(nil))))))) → top#(s(s(from(s(mark(0))))))top#(ok(s(s(cons(length(cons(_x62, _x61)), _x52))))) → top#(s(s(cons(mark(s(length1(_x61))), _x52))))
top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))top#(mark(from(s(_x41)))) → top#(from(s(proper(_x41))))
top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(mark(from(0)), _x42)))top#(ok(from(cons(length(cons(_x52, ok(ok(ok(ok(_x101)))))), _x42)))) → top#(from(cons(mark(s(ok(ok(ok(ok(length1(_x101))))))), _x42)))
top#(ok(s(cons(cons(length(cons(_x62, _x61)), _x52), _x42)))) → top#(s(cons(cons(mark(s(length1(_x61))), _x52), _x42)))top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(_x101)))), _x52)))))) → top#(s(s(from(mark(cons(s(ok(ok(length1(_x101)))), _x52))))))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(from(active(_x71))), _x52), _x42)))top#(ok(cons(s(length1(_x61)), _x22))) → top#(cons(s(mark(length(_x61))), _x22))
top#(ok(s(s(from(cons(cons(_x71, _x72), _x62)))))) → top#(s(s(from(cons(cons(active(_x71), _x72), _x62)))))top#(ok(s(s(from(s(length(cons(_x72, _x71)))))))) → top#(s(s(from(s(mark(s(length1(_x71))))))))
top#(ok(cons(length(nil), _x32))) → top#(mark(cons(0, _x32)))top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(mark(from(length(_x61))), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(s(mark(ok(s(length1(_x91))))), _x52), _x42)))top#(ok(from(from(from(s(length1(_x71))))))) → top#(from(from(from(s(mark(length(_x71)))))))
top#(ok(cons(s(length(nil)), _x22))) → top#(cons(s(mark(0)), _x22))top#(ok(from(cons(cons(from(length(nil)), _x52), _x42)))) → top#(from(cons(cons(from(mark(0)), _x52), _x42)))
top#(ok(s(s(cons(from(_x61), _x52))))) → top#(s(s(cons(from(active(_x61)), _x52))))top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(from(active(_x61))))))
top#(ok(from(cons(cons(s(length(cons(_x72, _x71))), _x42), _x42)))) → top#(from(cons(mark(cons(s(s(length1(_x71))), _x42)), _x42)))top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(ok(s(length1(_x71)))))))
top#(ok(from(cons(cons(s(length(nil)), _x52), _x42)))) → top#(from(cons(cons(s(mark(0)), _x52), _x42)))top#(ok(from(cons(from(cons(s(length(nil)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(0)), _x62)), _x42)))
top#(ok(s(s(from(length(cons(_x62, _x61))))))) → top#(s(mark(s(from(s(length1(_x61)))))))top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))
top#(ok(from(cons(cons(cons(_x61, _x62), _x52), _x42)))) → top#(from(cons(cons(cons(active(_x61), _x62), _x52), _x42)))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(ok(s(length1(_x71)))), _x42)))
top#(ok(from(cons(cons(s(s(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(s(active(_x71))), _x52), _x42)))top#(ok(from(from(from(length(nil)))))) → top#(from(from(from(mark(0)))))
top#(ok(s(from(_x41)))) → top#(s(from(active(_x41))))top#(ok(s(s(from(length(nil)))))) → top#(s(s(from(mark(0)))))
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(from(from(cons(_x61, _x62)))))) → top#(from(from(from(cons(active(_x61), _x62)))))
top#(ok(cons(s(length(cons(_x62, _x61))), _x22))) → top#(cons(s(mark(s(length1(_x61)))), _x22))top#(ok(s(length(nil)))) → top#(mark(s(0)))
top#(ok(from(from(length1(ok(_x61)))))) → top#(from(mark(ok(from(length(_x61))))))top#(ok(s(s(from(length1(_x61)))))) → top#(s(s(from(mark(length(_x61))))))
top#(ok(s(s(from(cons(length(nil), _x52)))))) → top#(s(s(mark(from(cons(0, _x52))))))top#(ok(from(cons(cons(from(length(cons(_x72, _x71))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(length1(_x71)))), _x52), _x42)))
top#(ok(from(from(from(length(cons(_x62, _x61))))))) → top#(from(from(from(mark(s(length1(_x61)))))))top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))
top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(from(active(_x81))), _x62)), _x42)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(from(active(_x61))), _x22))top#(ok(s(s(from(s(from(cons(from(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(from(active(_x91)), _x82)))))))
top#(ok(from(cons(cons(from(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(cons(_x61, from(s(_x61)))), _x52), _x42)))top#(ok(s(length1(ok(_x51))))) → top#(s(mark(ok(length(_x51)))))
top#(ok(cons(from(_x41), _x22))) → top#(cons(from(active(_x41)), _x22))top#(mark(from(length(_x41)))) → top#(from(length(proper(_x41))))
top#(ok(s(s(from(s(length1(_x71))))))) → top#(s(s(from(s(mark(length(_x71)))))))top#(ok(s(s(from(s(cons(_x71, _x72))))))) → top#(s(s(from(s(cons(active(_x71), _x72))))))
top#(ok(cons(s(s(_x61)), _x22))) → top#(cons(s(s(active(_x61))), _x22))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(from(mark(cons(s(ok(length1(_x71))), _x32))))
top#(ok(from(from(from(s(length(nil))))))) → top#(from(from(from(s(mark(0))))))top#(ok(s(s(from(length(cons(_x62, ok(_x81)))))))) → top#(s(s(from(mark(s(ok(length1(_x81))))))))
top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(from(active(_x61))))))top#(ok(s(cons(cons(length(nil), _x52), _x42)))) → top#(s(cons(cons(mark(0), _x52), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(mark(s(s(ok(length1(_x91))))), _x52), _x42)))top#(mark(from(length1(_x41)))) → top#(from(length1(proper(_x41))))
top#(ok(s(s(from(s(from(cons(s(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(s(active(_x91)), _x82)))))))top#(ok(s(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(s(mark(cons(ok(s(length1(_x71))), _x32))))
top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(cons(_x81, from(s(_x81))))), _x62)), _x42)))top#(ok(from(cons(cons(from(s(from(_x81))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(cons(_x81, from(s(_x81)))))), _x52), _x42)))
top#(ok(s(s(length1(ok(ok(_x71))))))) → top#(s(mark(s(ok(ok(length(_x71)))))))top#(ok(s(s(from(s(from(_x71))))))) → top#(s(s(from(s(mark(cons(_x71, from(s(_x71)))))))))
top#(ok(from(cons(cons(from(s(length(nil))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(0))), _x52), _x42)))top#(ok(from(cons(from(length1(ok(_x71))), _x42)))) → top#(from(cons(from(mark(ok(length(_x71)))), _x42)))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(nil), _x32)))) → top#(mark(from(cons(0, _x32))))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(ok(s(ok(length1(_x81))))))))top#(ok(s(length(cons(_x42, _x41))))) → top#(mark(s(s(length1(_x41)))))
top#(ok(s(s(from(s(from(cons(length(cons(_x92, _x91)), _x82)))))))) → top#(s(s(from(s(from(cons(mark(s(length1(_x91))), _x82)))))))top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(_x101))))), _x52), _x42)))) → top#(from(cons(cons(mark(s(s(ok(ok(length1(_x101)))))), _x52), _x42)))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(cons(_x81, from(s(_x81)))), _x72))))))top#(ok(s(s(cons(length(nil), _x52))))) → top#(s(s(cons(mark(0), _x52))))
top#(ok(s(s(from(cons(length(cons(_x72, _x71)), _x52)))))) → top#(s(s(from(mark(cons(s(length1(_x71)), _x52))))))top#(ok(s(cons(cons(from(s(length(cons(_x82, _x81)))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(s(length1(_x81))))), _x52), _x42)))
top#(ok(from(from(length1(ok(ok(_x71))))))) → top#(from(mark(from(ok(ok(length(_x71)))))))top#(ok(from(cons(from(cons(length(cons(_x72, ok(_x91))), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(ok(length1(_x91)))), _x62)), _x42)))
top#(ok(s(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(s(cons(mark(s(ok(ok(length1(_x81))))), _x42)))top#(mark(from(cons(_x41, _x42)))) → top#(from(cons(proper(_x41), proper(_x42))))
top#(ok(from(from(length1(ok(ok(ok(_x81)))))))) → top#(from(from(mark(ok(ok(ok(length(_x81))))))))top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(mark(from(from(s(length1(_x51))))))
top#(ok(cons(cons(_x41, _x42), _x22))) → top#(cons(cons(active(_x41), _x42), _x22))top#(ok(s(cons(cons(from(s(s(length(nil)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(0)))), _x52), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(ok(ok(s(length1(_x81))))))))top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(ok(from(from(s(length1(_x71)))))))
top#(ok(from(from(from(s(cons(cons(_x81, _x82), _x72))))))) → top#(from(from(from(s(cons(cons(active(_x81), _x82), _x72))))))top#(mark(from(from(_x41)))) → top#(from(from(proper(_x41))))
top#(ok(s(s(cons(s(_x61), _x52))))) → top#(s(s(cons(s(active(_x61)), _x52))))top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))
top#(ok(from(cons(cons(length1(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(length(_x61)), _x52), _x42)))top#(ok(cons(length(cons(_x42, _x41)), _x32))) → top#(mark(cons(s(length1(_x41)), _x32)))
top#(ok(s(cons(cons(s(_x61), _x52), _x42)))) → top#(s(cons(cons(s(active(_x61)), _x52), _x42)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(length1(_x81))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(length(_x81)))), _x52), _x42)))
top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(_x101)))), _x62)))))) → top#(s(s(from(cons(mark(ok(s(ok(length1(_x101))))), _x62)))))top#(mark(length1(_x21))) → top#(length1(proper(_x21)))
top#(ok(s(cons(cons(from(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(mark(s(ok(length1(_x91))))), _x52), _x42)))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(from(from(s(s(_x71))))))) → top#(from(from(from(s(s(active(_x71)))))))top#(ok(s(cons(length(cons(_x52, _x51)), _x32)))) → top#(s(mark(cons(s(length1(_x51)), _x32))))
top#(ok(s(s(cons(length1(_x61), _x52))))) → top#(s(s(cons(mark(length(_x61)), _x52))))top#(ok(cons(s(cons(_x61, _x62)), _x22))) → top#(cons(s(cons(active(_x61), _x62)), _x22))
top#(ok(s(s(from(_x51))))) → top#(s(s(mark(cons(_x51, from(s(_x51)))))))top#(ok(s(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(s(cons(mark(ok(s(ok(length1(_x81))))), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(_x101))))), _x52), _x42)))) → top#(from(cons(cons(s(mark(ok(s(ok(length1(_x101)))))), _x52), _x42)))top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))
top#(ok(s(cons(cons(from(s(from(s(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(s(active(_x91))))), _x52), _x42)))top#(ok(s(s(from(length(cons(_x62, ok(_x81)))))))) → top#(s(s(mark(from(s(ok(length1(_x81))))))))
top#(ok(s(s(length1(ok(ok(_x71))))))) → top#(s(s(mark(ok(ok(length(_x71)))))))top#(ok(s(s(length(cons(_x52, _x51)))))) → top#(s(s(mark(s(length1(_x51))))))
top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))top#(ok(s(cons(cons(from(s(from(_x81))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(cons(_x81, from(s(_x81)))))), _x52), _x42)))
top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(ok(s(length1(_x61))))))top#(ok(s(s(length1(_x51))))) → top#(s(mark(s(length(_x51)))))
top#(ok(from(cons(cons(from(s(length1(ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(ok(length(_x91))))), _x52), _x42)))top#(ok(cons(from(_x41), _x22))) → top#(cons(mark(cons(_x41, from(s(_x41)))), _x22))
top#(ok(from(from(from(s(cons(length1(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(length(_x81)), _x72))))))top#(ok(s(s(from(s(from(cons(length(nil), _x82)))))))) → top#(s(s(from(s(from(cons(mark(0), _x82)))))))
top#(ok(s(cons(cons(from(s(s(s(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(s(active(_x91))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(s(length1(_x91)))))), _x52), _x42)))
top#(ok(s(s(from(cons(length(cons(_x72, ok(_x91))), _x52)))))) → top#(s(s(from(mark(cons(s(ok(length1(_x91))), _x52))))))top#(ok(from(cons(length(cons(_x52, ok(ok(ok(_x91))))), _x32)))) → top#(from(mark(cons(s(ok(ok(ok(length1(_x91))))), _x32))))
top#(ok(from(from(from(s(cons(length(cons(_x82, ok(_x101))), _x72))))))) → top#(from(from(from(s(cons(mark(s(ok(length1(_x101)))), _x72))))))top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(from(cons(mark(ok(s(ok(length1(_x81))))), _x42)))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(from(active(_x81)), _x72))))))top#(ok(from(from(from(length1(_x61)))))) → top#(from(from(mark(from(length(_x61))))))
top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))top#(ok(s(s(from(s(from(from(_x81)))))))) → top#(s(s(from(s(from(mark(cons(_x81, from(s(_x81))))))))))
top#(ok(from(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(from(active(_x71))), _x52), _x42)))top#(ok(s(s(from(s(from(length1(_x81)))))))) → top#(s(s(from(s(from(mark(length(_x81))))))))
top#(ok(s(length(cons(_x42, ok(_x61)))))) → top#(s(mark(s(ok(length1(_x61))))))top#(ok(cons(length1(_x41), _x22))) → top#(cons(mark(length(_x41)), _x22))
top#(ok(from(from(length1(ok(_x61)))))) → top#(mark(from(from(ok(length(_x61))))))top#(ok(s(s(length(nil))))) → top#(s(mark(s(0))))
top#(ok(s(s(from(s(from(from(_x81)))))))) → top#(s(s(from(s(from(from(active(_x81))))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(from(mark(s(ok(ok(length1(_x81))))))))
top#(ok(s(s(from(s(from(cons(cons(_x91, _x92), _x82)))))))) → top#(s(s(from(s(from(cons(cons(active(_x91), _x92), _x82)))))))top#(ok(s(s(from(s(from(length(cons(_x82, ok(_x101)))))))))) → top#(s(s(from(s(from(mark(s(ok(length1(_x101))))))))))
top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(ok(_x111))))), _x62)))))) → top#(s(s(from(cons(mark(s(ok(ok(ok(length1(_x111)))))), _x62)))))
top#(ok(cons(length(cons(_x42, ok(_x71))), _x22))) → top#(cons(mark(s(ok(length1(_x71)))), _x22))top#(ok(s(cons(cons(from(length(cons(_x72, _x71))), _x52), _x42)))) → top#(s(cons(cons(mark(from(s(length1(_x71)))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(length1(ok(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(ok(length(_x101)))))), _x52), _x42)))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))
top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))
top#(ok(s(cons(length(cons(_x52, ok(ok(_x91)))), _x32)))) → top#(s(mark(cons(s(ok(ok(length1(_x91)))), _x32))))top#(ok(from(cons(cons(length(cons(_x62, _x61)), _x52), _x42)))) → top#(from(cons(cons(mark(s(length1(_x61))), _x52), _x42)))
top#(ok(from(cons(cons(s(length1(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(length(_x71))), _x52), _x42)))top#(ok(from(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))
top#(ok(s(s(from(cons(s(_x71), _x62)))))) → top#(s(s(from(cons(s(active(_x71)), _x62)))))top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))
top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x52)), _x42)))) → top#(from(cons(from(mark(cons(s(length1(_x71)), _x52))), _x42)))top#(ok(from(from(from(s(from(_x71))))))) → top#(from(from(from(s(mark(cons(_x71, from(s(_x71)))))))))
top#(ok(s(s(from(cons(from(_x71), _x62)))))) → top#(s(s(from(cons(from(active(_x71)), _x62)))))top#(ok(s(cons(s(_x51), _x42)))) → top#(s(cons(s(active(_x51)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(from(mark(ok(s(ok(length1(_x81))))))))top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(ok(_x111)))))), _x52), _x42)))) → top#(from(cons(cons(s(mark(s(ok(ok(ok(length1(_x111))))))), _x52), _x42)))
top#(ok(s(s(from(s(from(length(cons(_x82, _x81))))))))) → top#(s(s(from(s(mark(from(s(length1(_x81)))))))))top#(ok(from(cons(cons(s(cons(_x71, _x72)), _x52), _x42)))) → top#(from(cons(cons(s(cons(active(_x71), _x72)), _x52), _x42)))
top#(ok(from(cons(from(cons(s(s(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(s(active(_x81))), _x62)), _x42)))top#(mark(length(_x21))) → top#(length(proper(_x21)))
top#(ok(from(cons(cons(from(cons(_x71, _x72)), _x52), _x42)))) → top#(from(cons(cons(from(cons(active(_x71), _x72)), _x52), _x42)))top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))
top#(ok(s(cons(length(nil), _x42)))) → top#(s(cons(mark(0), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(ok(_x91))))))))) → top#(from(mark(from(ok(s(ok(ok(length1(_x91)))))))))
top#(ok(s(s(from(s(s(_x71))))))) → top#(s(s(from(s(s(active(_x71)))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(s(ok(ok(length1(_x81))))))))
top#(ok(from(from(from(length1(ok(_x71))))))) → top#(from(from(from(mark(ok(length(_x71)))))))top#(ok(s(s(from(s(from(cons(length1(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(mark(length(_x91)), _x82)))))))
top#(ok(from(cons(cons(from(s(length1(_x81))), _x52), _x42)))) → top#(from(cons(cons(mark(from(s(length(_x81)))), _x52), _x42)))top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))
top#(ok(from(cons(cons(from(s(length1(ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(ok(length(_x91))))), _x52), _x42)))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(mark(from(s(ok(length1(_x61))))))
top#(ok(s(s(length1(ok(_x61)))))) → top#(s(mark(ok(s(length(_x61))))))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(ok(from(cons(from(cons(s(length1(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(length(_x81))), _x62)), _x42)))top#(ok(from(cons(cons(length(nil), _x52), _x42)))) → top#(from(cons(cons(mark(0), _x52), _x42)))
top#(ok(from(cons(length(cons(_x52, ok(ok(ok(_x91))))), _x42)))) → top#(from(cons(mark(ok(s(ok(ok(length1(_x91)))))), _x42)))top#(ok(s(cons(cons(from(s(from(cons(_x91, _x92)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(cons(active(_x91), _x92)))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(from(active(_x91))))), _x52), _x42)))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(from(from(from(s(length(cons(_x72, _x71)))))))) → top#(from(from(from(s(mark(s(length1(_x71))))))))top#(ok(from(cons(from(cons(s(cons(_x81, _x82)), _x62)), _x42)))) → top#(from(cons(from(cons(s(cons(active(_x81), _x82)), _x62)), _x42)))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(s(cons(cons(from(s(cons(_x81, _x82))), _x52), _x42)))) → top#(s(cons(cons(from(s(cons(active(_x81), _x82))), _x52), _x42)))top#(ok(s(cons(cons(from(s(s(cons(_x91, _x92)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(cons(active(_x91), _x92)))), _x52), _x42)))
top#(ok(s(cons(from(_x51), _x42)))) → top#(s(cons(from(active(_x51)), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(ok(from(s(ok(length1(_x81))))))))
top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(mark(from(from(ok(s(ok(length1(_x81))))))))top#(ok(s(cons(cons(from(_x61), _x52), _x42)))) → top#(s(cons(cons(mark(cons(_x61, from(s(_x61)))), _x52), _x42)))
top#(ok(s(cons(cons(from(cons(_x71, _x72)), _x52), _x42)))) → top#(s(cons(cons(from(cons(active(_x71), _x72)), _x52), _x42)))top#(ok(from(cons(cons(from(s(length(cons(_x82, _x81)))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(s(length1(_x81))))), _x52), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32)))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(mark(from(cons(length(_x51), _x32)))) 
top#(from(mark(cons(ok(length(_x71)), _x32)))) 
Thus, the rule top#(ok(from(cons(length1(_x51), _x32)))) → top#(from(mark(cons(length(_x51), _x32)))) is replaced by the following rules:
top#(ok(from(cons(length1(_x51), _x32)))) → top#(mark(from(cons(length(_x51), _x32))))top#(ok(from(cons(length1(ok(_x71)), _x32)))) → top#(from(mark(cons(ok(length(_x71)), _x32))))

Problem 31: ForwardNarrowing

Dependency Pair Problem

Dependency Pairs

top#(ok(s(cons(cons(cons(length(cons(_x72, _x71)), _x52), _x52), _x42)))) → top#(s(cons(cons(mark(cons(s(length1(_x71)), _x52)), _x52), _x42)))top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(mark(cons(_x61, from(s(_x61))))))))
top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(mark(cons(_x61, from(s(_x61))))), _x22))top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(mark(cons(_x61, from(s(_x61))))), _x42)))
top#(ok(s(cons(from(_x51), _x42)))) → top#(s(cons(mark(cons(_x51, from(s(_x51)))), _x42)))top#(ok(s(s(from(s(from(cons(from(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(mark(cons(_x91, from(s(_x91)))), _x82)))))))
top#(ok(s(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))top#(ok(s(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))
top#(ok(s(length1(_x41)))) → top#(mark(s(length(_x41))))top#(ok(s(s(from(s(from(s(s(from(from(_x111))))))))))) → top#(s(s(from(s(from(s(s(from(mark(cons(_x111, from(s(_x111)))))))))))))
top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(mark(cons(_x61, from(s(_x61))))))))top#(ok(s(s(from(s(from(s(from(_x91))))))))) → top#(s(s(from(s(from(s(mark(cons(_x91, from(s(_x91)))))))))))
top#(ok(from(length(cons(_x42, _x41))))) → top#(mark(from(s(length1(_x41)))))top#(ok(length1(_x21))) → top#(mark(length(_x21)))
top#(ok(s(cons(cons(from(length(nil)), _x42), _x42)))) → top#(s(cons(mark(cons(from(0), _x42)), _x42)))top#(ok(s(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(mark(s(cons(s(ok(length1(_x71))), _x32))))
top#(ok(s(from(_x41)))) → top#(s(mark(cons(_x41, from(s(_x41))))))top#(ok(s(s(from(cons(from(_x71), _x62)))))) → top#(s(s(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)))))
top#(ok(s(s(length1(ok(_x61)))))) → top#(mark(s(s(ok(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x32)))) → top#(mark(from(cons(s(ok(ok(length1(_x81)))), _x32))))
top#(ok(s(cons(cons(length1(_x61), _x42), _x42)))) → top#(s(cons(mark(cons(length(_x61), _x42)), _x42)))top#(ok(s(s(cons(from(_x61), _x52))))) → top#(s(s(cons(mark(cons(_x61, from(s(_x61)))), _x52))))
top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(active(_x91))))), _x52), _x42)))top#(ok(s(s(from(s(from(s(s(from(_x101)))))))))) → top#(s(s(from(s(from(s(s(mark(cons(_x101, from(s(_x101))))))))))))
top#(ok(s(s(from(s(from(s(s(from(cons(from(_x121), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(mark(cons(_x121, from(s(_x121)))), _x112))))))))))top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(s(ok(length1(_x71)))))))
top#(ok(s(s(from(s(from(s(s(from(cons(length(nil), _x102))))))))))) → top#(s(s(from(s(from(s(s(mark(from(cons(0, _x102)))))))))))top#(ok(from(cons(cons(from(length1(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(mark(length(_x71))), _x52), _x42)))
top#(ok(s(s(from(s(from(s(s(from(length1(ok(_x121)))))))))))) → top#(s(s(from(s(from(mark(s(s(ok(from(length(_x121))))))))))))top#(ok(s(s(from(cons(length1(_x71), _x62)))))) → top#(s(s(from(cons(mark(length(_x71)), _x62)))))
top#(ok(s(s(cons(cons(_x61, _x62), _x52))))) → top#(s(s(cons(cons(active(_x61), _x62), _x52))))top#(ok(from(from(from(s(cons(length(cons(_x82, ok(_x111))), _x62))))))) → top#(from(from(from(mark(s(cons(s(ok(length1(_x111))), _x62)))))))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(mark(from(ok(from(s(ok(length1(_x81))))))))top#(ok(s(cons(cons(from(s(s(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(s(length1(_x91)))))), _x52), _x42)))
top#(ok(s(s(s(_x51))))) → top#(s(s(s(active(_x51)))))top#(ok(from(cons(cons(from(s(from(cons(_x91, _x92)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(cons(active(_x91), _x92)))), _x52), _x42)))
top#(mark(from(0))) → top#(ok(from(0)))top#(ok(s(cons(length1(_x51), _x32)))) → top#(s(mark(cons(length(_x51), _x32))))
top#(mark(from(nil))) → top#(from(ok(nil)))top#(ok(s(cons(cons(from(s(from(length1(ok(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(ok(from(length(_x101)))))), _x52), _x42)))
top#(ok(s(s(from(s(from(s(s(from(cons(length1(_x121), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(mark(length(_x121)), _x112))))))))))top#(ok(s(s(from(s(from(s(length(nil))))))))) → top#(s(s(from(s(from(s(mark(0))))))))
top#(ok(s(cons(cons(from(s(s(length1(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(length(_x91))))), _x52), _x42)))top#(ok(s(cons(cons(from(length1(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(mark(length(_x71))), _x52), _x42)))
top#(ok(from(cons(from(cons(s(length(cons(_x82, ok(_x101)))), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(s(ok(length1(_x101))))), _x62)), _x42)))top#(ok(s(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(s(cons(cons(from(from(active(_x71))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(length(nil)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(0)))), _x52), _x42)))top#(mark(s(_x21))) → top#(s(proper(_x21)))
top#(ok(from(cons(cons(from(s(cons(_x81, _x82))), _x52), _x42)))) → top#(from(cons(cons(from(s(cons(active(_x81), _x82))), _x52), _x42)))top#(ok(from(from(from(s(cons(s(_x81), _x72))))))) → top#(from(from(from(s(cons(s(active(_x81)), _x72))))))
top#(ok(s(s(from(s(from(s(s(length(nil)))))))))) → top#(s(s(from(s(from(s(s(mark(0)))))))))top#(ok(s(cons(cons(from(s(length(nil))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(0))), _x52), _x42)))
top#(ok(from(length1(ok(ok(ok(ok(_x81)))))))) → top#(from(mark(ok(ok(ok(ok(length(_x81))))))))top#(ok(s(s(from(s(length(nil))))))) → top#(s(s(from(s(mark(0))))))
top#(ok(s(s(from(s(from(s(s(from(from(_x111))))))))))) → top#(s(s(from(s(from(s(s(from(from(active(_x111)))))))))))top#(ok(s(s(cons(length(cons(_x62, _x61)), _x52))))) → top#(s(s(cons(mark(s(length1(_x61))), _x52))))
top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x32)))) → top#(from(mark(cons(ok(s(ok(length1(_x81)))), _x32))))top#(ok(from(cons(length(cons(_x52, _x51)), _x32)))) → top#(from(mark(cons(s(length1(_x51)), _x32))))
top#(mark(from(s(_x41)))) → top#(from(s(proper(_x41))))top#(ok(from(cons(from(length(nil)), _x42)))) → top#(from(cons(mark(from(0)), _x42)))
top#(ok(from(cons(length(cons(_x52, ok(ok(ok(ok(_x101)))))), _x42)))) → top#(from(cons(mark(s(ok(ok(ok(ok(length1(_x101))))))), _x42)))top#(ok(s(cons(cons(length(cons(_x62, _x61)), _x52), _x42)))) → top#(s(cons(cons(mark(s(length1(_x61))), _x52), _x42)))
top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(_x101)))), _x52)))))) → top#(s(s(from(mark(cons(s(ok(ok(length1(_x101)))), _x52))))))top#(ok(s(s(from(s(from(s(s(from(length(nil))))))))))) → top#(s(s(from(s(from(s(s(from(mark(0))))))))))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(from(active(_x71))), _x52), _x42)))top#(ok(s(cons(cons(cons(length1(_x71), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(mark(length(_x71)), _x62), _x52), _x42)))
top#(ok(cons(s(length1(_x61)), _x22))) → top#(cons(s(mark(length(_x61))), _x22))top#(ok(s(s(from(cons(cons(_x71, _x72), _x62)))))) → top#(s(s(from(cons(cons(active(_x71), _x72), _x62)))))
top#(ok(s(s(from(s(length(cons(_x72, _x71)))))))) → top#(s(s(from(s(mark(s(length1(_x71))))))))top#(ok(cons(length(nil), _x32))) → top#(mark(cons(0, _x32)))
top#(ok(from(cons(from(length1(_x61)), _x42)))) → top#(from(cons(mark(from(length(_x61))), _x42)))top#(ok(from(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(from(active(_x91))))), _x52), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(s(mark(ok(s(length1(_x91))))), _x52), _x42)))top#(ok(s(s(from(s(from(s(from(_x91))))))))) → top#(s(s(from(s(from(s(from(active(_x91)))))))))
top#(ok(from(cons(cons(from(s(s(length(nil)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(mark(0)))), _x52), _x42)))top#(ok(from(from(from(s(length1(_x71))))))) → top#(from(from(from(s(mark(length(_x71)))))))
top#(ok(cons(s(length(nil)), _x22))) → top#(cons(s(mark(0)), _x22))top#(ok(from(cons(cons(from(s(from(length(nil)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(mark(0)))), _x52), _x42)))
top#(ok(from(cons(cons(from(length(nil)), _x52), _x42)))) → top#(from(cons(cons(from(mark(0)), _x52), _x42)))top#(ok(from(from(from(s(from(length(cons(_x82, _x81))))))))) → top#(from(from(from(mark(s(from(s(length1(_x81)))))))))
top#(ok(s(s(cons(from(_x61), _x52))))) → top#(s(s(cons(from(active(_x61)), _x52))))top#(ok(from(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(from(active(_x91))))), _x52), _x42)))
top#(ok(s(s(from(from(_x61)))))) → top#(s(s(from(from(active(_x61))))))top#(ok(from(cons(cons(s(length(cons(_x72, _x71))), _x42), _x42)))) → top#(from(cons(mark(cons(s(s(length1(_x71))), _x42)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(from(from(ok(s(length1(_x71)))))))top#(ok(from(cons(cons(s(length(nil)), _x52), _x42)))) → top#(from(cons(cons(s(mark(0)), _x52), _x42)))
top#(ok(from(cons(from(cons(s(length(nil)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(0)), _x62)), _x42)))top#(ok(s(s(from(length(cons(_x62, _x61))))))) → top#(s(mark(s(from(s(length1(_x61)))))))
top#(ok(s(cons(cons(from(s(from(length1(ok(ok(_x111)))))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(from(ok(ok(length(_x111))))))), _x52), _x42)))top#(ok(from(cons(from(s(_x61)), _x42)))) → top#(from(cons(from(s(active(_x61))), _x42)))
top#(ok(from(cons(cons(cons(_x61, _x62), _x52), _x42)))) → top#(from(cons(cons(cons(active(_x61), _x62), _x52), _x42)))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x42)))) → top#(from(cons(mark(ok(s(length1(_x71)))), _x42)))
top#(ok(from(cons(cons(s(s(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(s(active(_x71))), _x52), _x42)))top#(ok(from(from(from(length(nil)))))) → top#(from(from(from(mark(0)))))
top#(ok(s(s(from(length(nil)))))) → top#(s(s(from(mark(0)))))top#(ok(s(from(_x41)))) → top#(s(from(active(_x41))))
top#(ok(from(from(s(_x51))))) → top#(from(from(s(active(_x51)))))top#(ok(from(from(from(cons(_x61, _x62)))))) → top#(from(from(from(cons(active(_x61), _x62)))))
top#(ok(cons(s(length(cons(_x62, _x61))), _x22))) → top#(cons(s(mark(s(length1(_x61)))), _x22))top#(ok(from(from(length1(ok(_x61)))))) → top#(from(mark(ok(from(length(_x61))))))
top#(ok(s(length(nil)))) → top#(mark(s(0)))top#(ok(s(s(from(length1(_x61)))))) → top#(s(s(from(mark(length(_x61))))))
top#(ok(s(s(from(cons(length(nil), _x52)))))) → top#(s(s(mark(from(cons(0, _x52))))))top#(ok(from(from(from(length(cons(_x62, _x61))))))) → top#(from(from(from(mark(s(length1(_x61)))))))
top#(ok(from(cons(cons(from(length(cons(_x72, _x71))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(length1(_x71)))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))
top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(from(active(_x81))), _x62)), _x42)))top#(mark(cons(_x21, _x22))) → top#(cons(proper(_x21), proper(_x22)))
top#(ok(cons(s(from(_x61)), _x22))) → top#(cons(s(from(active(_x61))), _x22))top#(ok(s(s(from(s(from(cons(from(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(from(active(_x91)), _x82)))))))
top#(ok(s(s(from(s(from(s(s(from(length1(ok(_x121)))))))))))) → top#(s(s(from(s(mark(from(s(s(from(ok(length(_x121))))))))))))top#(ok(from(cons(cons(from(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(cons(_x61, from(s(_x61)))), _x52), _x42)))
top#(ok(from(cons(cons(from(s(s(length1(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(mark(length(_x91))))), _x52), _x42)))top#(ok(s(length1(ok(_x51))))) → top#(s(mark(ok(length(_x51)))))
top#(ok(cons(from(_x41), _x22))) → top#(cons(from(active(_x41)), _x22))top#(mark(from(length(_x41)))) → top#(from(length(proper(_x41))))
top#(ok(s(s(from(s(length1(_x71))))))) → top#(s(s(from(s(mark(length(_x71)))))))top#(ok(s(s(from(s(cons(_x71, _x72))))))) → top#(s(s(from(s(cons(active(_x71), _x72))))))
top#(ok(cons(s(s(_x61)), _x22))) → top#(cons(s(s(active(_x61))), _x22))top#(ok(from(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(from(mark(cons(s(ok(length1(_x71))), _x32))))
top#(ok(from(from(from(s(length(nil))))))) → top#(from(from(from(s(mark(0))))))top#(ok(s(s(from(length(cons(_x62, ok(_x81)))))))) → top#(s(s(from(mark(s(ok(length1(_x81))))))))
top#(ok(from(from(from(from(_x61)))))) → top#(from(from(from(from(active(_x61))))))top#(ok(s(cons(cons(length(nil), _x52), _x42)))) → top#(s(cons(cons(mark(0), _x52), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(mark(s(s(ok(length1(_x91))))), _x52), _x42)))top#(mark(from(length1(_x41)))) → top#(from(length1(proper(_x41))))
top#(ok(from(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))top#(ok(s(s(from(s(from(cons(s(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(s(active(_x91)), _x82)))))))
top#(ok(s(cons(length(cons(_x52, ok(_x71))), _x32)))) → top#(s(mark(cons(ok(s(length1(_x71))), _x32))))top#(ok(from(cons(from(cons(s(from(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(cons(_x81, from(s(_x81))))), _x62)), _x42)))
top#(ok(from(cons(cons(from(s(from(_x81))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(cons(_x81, from(s(_x81)))))), _x52), _x42)))top#(ok(from(from(from(s(from(length1(_x81)))))))) → top#(from(from(from(s(from(mark(length(_x81))))))))
top#(ok(from(from(from(s(cons(length(nil), _x62))))))) → top#(from(from(from(s(mark(cons(0, _x62)))))))top#(ok(from(cons(cons(from(s(s(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(mark(s(length1(_x91)))))), _x52), _x42)))
top#(ok(s(s(length1(ok(ok(_x71))))))) → top#(s(mark(s(ok(ok(length(_x71)))))))top#(ok(from(length(cons(_x42, ok(ok(_x71))))))) → top#(mark(from(s(ok(ok(length1(_x71)))))))
top#(ok(s(s(from(s(from(_x71))))))) → top#(s(s(from(s(mark(cons(_x71, from(s(_x71)))))))))top#(ok(from(cons(length1(ok(_x71)), _x32)))) → top#(from(mark(cons(ok(length(_x71)), _x32))))
top#(ok(from(cons(cons(from(s(length(nil))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(0))), _x52), _x42)))top#(ok(from(cons(from(length1(ok(_x71))), _x42)))) → top#(from(cons(from(mark(ok(length(_x71)))), _x42)))
top#(ok(from(cons(from(cons(s(length(cons(_x82, _x81))), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(s(length1(_x81)))), _x62)), _x42)))top#(ok(s(s(from(cons(length(cons(_x72, ok(_x91))), _x52)))))) → top#(s(s(from(mark(cons(ok(s(length1(_x91))), _x52))))))
top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(_x131))))))))))))) → top#(s(s(from(s(from(mark(s(s(from(ok(ok(length(_x131)))))))))))))top#(ok(from(cons(length1(_x51), _x32)))) → top#(mark(from(cons(length(_x51), _x32))))
top#(ok(from(length1(ok(ok(_x61)))))) → top#(mark(from(ok(ok(length(_x61))))))top#(ok(from(cons(length(nil), _x32)))) → top#(mark(from(cons(0, _x32))))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(ok(s(ok(length1(_x81))))))))top#(ok(from(from(from(s(from(from(_x81)))))))) → top#(from(from(from(s(from(mark(cons(_x81, from(s(_x81))))))))))
top#(ok(s(length(cons(_x42, _x41))))) → top#(mark(s(s(length1(_x41)))))top#(ok(s(s(from(s(from(cons(length(cons(_x92, _x91)), _x82)))))))) → top#(s(s(from(s(from(cons(mark(s(length1(_x91))), _x82)))))))
top#(ok(from(cons(cons(from(s(from(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(mark(s(length1(_x91)))))), _x52), _x42)))top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(_x101))))), _x52), _x42)))) → top#(from(cons(cons(mark(s(s(ok(ok(length1(_x101)))))), _x52), _x42)))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(cons(_x81, from(s(_x81)))), _x72))))))top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(ok(_x141)))))))))))))) → top#(s(s(from(s(from(s(s(mark(from(ok(ok(ok(length(_x141))))))))))))))
top#(ok(s(s(cons(length(nil), _x52))))) → top#(s(s(cons(mark(0), _x52))))top#(ok(s(s(from(cons(length(cons(_x72, _x71)), _x52)))))) → top#(s(s(from(mark(cons(s(length1(_x71)), _x52))))))
top#(ok(s(cons(cons(from(s(length(cons(_x82, _x81)))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(s(length1(_x81))))), _x52), _x42)))top#(ok(from(from(length1(ok(ok(_x71))))))) → top#(from(mark(from(ok(ok(length(_x71)))))))
top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(_x131))))))))))))) → top#(s(s(from(s(from(s(s(mark(ok(from(ok(length(_x131)))))))))))))top#(ok(from(cons(from(cons(length(cons(_x72, ok(_x91))), _x62)), _x42)))) → top#(from(cons(from(cons(mark(s(ok(length1(_x91)))), _x62)), _x42)))
top#(ok(from(from(from(s(from(cons(_x81, _x82)))))))) → top#(from(from(from(s(from(cons(active(_x81), _x82)))))))top#(ok(s(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(s(cons(mark(s(ok(ok(length1(_x81))))), _x42)))
top#(ok(from(from(from(s(from(length(cons(_x82, ok(_x101)))))))))) → top#(from(from(from(s(from(mark(s(ok(length1(_x101))))))))))top#(mark(from(cons(_x41, _x42)))) → top#(from(cons(proper(_x41), proper(_x42))))
top#(ok(from(from(length1(ok(ok(ok(_x81)))))))) → top#(from(from(mark(ok(ok(ok(length(_x81))))))))top#(ok(from(from(length(cons(_x52, _x51)))))) → top#(mark(from(from(s(length1(_x51))))))
top#(ok(cons(cons(_x41, _x42), _x22))) → top#(cons(cons(active(_x41), _x42), _x22))top#(ok(s(cons(cons(from(s(s(length(nil)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(mark(0)))), _x52), _x42)))
top#(ok(from(from(from(s(from(length(cons(_x82, ok(_x101)))))))))) → top#(from(from(from(s(mark(from(s(ok(length1(_x101))))))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(ok(ok(s(length1(_x81))))))))
top#(ok(from(from(length(cons(_x52, ok(_x71))))))) → top#(mark(ok(from(from(s(length1(_x71)))))))top#(ok(from(from(from(s(cons(cons(_x81, _x82), _x72))))))) → top#(from(from(from(s(cons(cons(active(_x81), _x82), _x72))))))
top#(mark(from(from(_x41)))) → top#(from(from(proper(_x41))))top#(ok(s(s(cons(s(_x61), _x52))))) → top#(s(s(cons(s(active(_x61)), _x52))))
top#(ok(from(cons(from(cons(length(nil), _x62)), _x42)))) → top#(from(cons(from(cons(mark(0), _x62)), _x42)))top#(ok(s(s(from(s(from(s(cons(_x91, _x92))))))))) → top#(s(s(from(s(from(s(cons(active(_x91), _x92))))))))
top#(ok(s(cons(cons(cons(cons(_x71, _x72), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(cons(active(_x71), _x72), _x62), _x52), _x42)))top#(ok(from(cons(cons(from(s(s(cons(_x91, _x92)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(cons(active(_x91), _x92)))), _x52), _x42)))
top#(ok(from(cons(cons(length1(_x61), _x52), _x42)))) → top#(from(cons(cons(mark(length(_x61)), _x52), _x42)))top#(ok(cons(length(cons(_x42, _x41)), _x32))) → top#(mark(cons(s(length1(_x41)), _x32)))
top#(ok(s(cons(cons(s(_x61), _x52), _x42)))) → top#(s(cons(cons(s(active(_x61)), _x52), _x42)))top#(ok(from(length(nil)))) → top#(from(mark(0)))
top#(ok(from(cons(cons(s(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(length1(_x81))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(length(_x81)))), _x52), _x42)))
top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(_x101)))), _x62)))))) → top#(s(s(from(cons(mark(ok(s(ok(length1(_x101))))), _x62)))))top#(ok(from(from(from(s(cons(length(cons(_x82, ok(_x111))), _x62))))))) → top#(from(from(from(s(mark(cons(s(ok(length1(_x111))), _x62)))))))
top#(mark(length1(_x21))) → top#(length1(proper(_x21)))top#(ok(s(cons(cons(from(length(cons(_x72, ok(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(mark(s(ok(length1(_x91))))), _x52), _x42)))
top#(ok(from(cons(length1(ok(_x61)), _x42)))) → top#(from(cons(mark(ok(length(_x61))), _x42)))top#(ok(from(from(cons(_x51, _x52))))) → top#(from(from(cons(active(_x51), _x52))))
top#(ok(from(from(from(s(from(length(nil)))))))) → top#(from(from(from(s(from(mark(0)))))))top#(ok(from(_x21))) → top#(mark(cons(_x21, from(s(_x21)))))
top#(ok(from(from(from(s(s(_x71))))))) → top#(from(from(from(s(s(active(_x71)))))))top#(ok(s(cons(length(cons(_x52, _x51)), _x32)))) → top#(s(mark(cons(s(length1(_x51)), _x32))))
top#(ok(s(s(cons(length1(_x61), _x52))))) → top#(s(s(cons(mark(length(_x61)), _x52))))top#(ok(from(cons(cons(from(s(from(length1(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(mark(length(_x91))))), _x52), _x42)))
top#(ok(cons(s(cons(_x61, _x62)), _x22))) → top#(cons(s(cons(active(_x61), _x62)), _x22))top#(ok(from(length(cons(_x42, ok(ok(_x71))))))) → top#(from(mark(ok(ok(s(length1(_x71)))))))
top#(ok(s(s(from(s(from(s(s(length(cons(_x102, _x101))))))))))) → top#(s(s(from(s(from(s(s(mark(s(length1(_x101)))))))))))top#(ok(from(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(mark(cons(_x91, from(s(_x91))))))), _x52), _x42)))
top#(ok(s(s(from(_x51))))) → top#(s(s(mark(cons(_x51, from(s(_x51)))))))top#(ok(s(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(s(cons(mark(ok(s(ok(length1(_x81))))), _x42)))
top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(_x101))))), _x52), _x42)))) → top#(from(cons(cons(s(mark(ok(s(ok(length1(_x101)))))), _x52), _x42)))top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(from(active(_x71)), _x62)), _x42)))
top#(ok(s(cons(cons(cons(length(nil), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(mark(0), _x62), _x52), _x42)))top#(ok(s(cons(cons(cons(from(_x71), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(from(active(_x71)), _x62), _x52), _x42)))
top#(ok(s(s(from(s(from(s(s(s(_x101)))))))))) → top#(s(s(from(s(from(s(s(s(active(_x101))))))))))top#(ok(s(s(from(s(from(s(length1(_x91))))))))) → top#(s(s(from(s(from(s(mark(length(_x91)))))))))
top#(ok(s(cons(cons(from(s(from(s(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(s(active(_x91))))), _x52), _x42)))top#(ok(s(s(from(length(cons(_x62, ok(_x81)))))))) → top#(s(s(mark(from(s(ok(length1(_x81))))))))
top#(ok(s(cons(length1(ok(_x61)), _x42)))) → top#(s(cons(mark(ok(length(_x61))), _x42)))top#(ok(s(cons(cons(from(s(from(length1(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(mark(s(from(length(_x91))))), _x52), _x42)))
top#(ok(from(length(cons(_x42, ok(ok(_x71))))))) → top#(mark(from(ok(s(ok(length1(_x71)))))))top#(ok(s(s(length1(ok(ok(_x71))))))) → top#(s(s(mark(ok(ok(length(_x71)))))))
top#(ok(s(s(from(s(from(s(s(from(cons(s(_x121), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(s(active(_x121)), _x112))))))))))top#(ok(s(s(from(s(from(s(length(cons(_x92, _x91)))))))))) → top#(s(s(from(s(from(s(mark(s(length1(_x91))))))))))
top#(ok(s(s(length(cons(_x52, _x51)))))) → top#(s(s(mark(s(length1(_x51))))))top#(ok(from(from(from(_x51))))) → top#(from(from(mark(cons(_x51, from(s(_x51)))))))
top#(ok(s(cons(cons(from(s(from(_x81))), _x52), _x42)))) → top#(s(cons(cons(from(s(mark(cons(_x81, from(s(_x81)))))), _x52), _x42)))top#(ok(from(cons(cons(from(s(s(s(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(s(s(active(_x91))))), _x52), _x42)))
top#(ok(from(length(cons(_x42, ok(ok(ok(_x81)))))))) → top#(from(mark(s(ok(ok(ok(length1(_x81))))))))top#(ok(s(s(from(s(from(s(s(from(length(cons(_x112, ok(_x131))))))))))))) → top#(s(s(from(s(from(s(s(from(mark(s(ok(length1(_x131)))))))))))))
top#(ok(s(s(from(s(from(s(s(from(cons(length(cons(_x122, _x121)), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(mark(s(length1(_x121))), _x112))))))))))top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(from(mark(ok(s(length1(_x61))))))
top#(ok(s(s(length1(_x51))))) → top#(s(mark(s(length(_x51)))))top#(ok(s(cons(cons(cons(length(cons(_x72, ok(_x91))), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(mark(s(ok(length1(_x91)))), _x62), _x52), _x42)))
top#(ok(s(cons(cons(length1(ok(_x71)), _x52), _x42)))) → top#(s(cons(cons(mark(ok(length(_x71))), _x52), _x42)))top#(ok(from(from(from(s(cons(length1(_x81), _x72))))))) → top#(from(from(from(s(cons(mark(length(_x81)), _x72))))))
top#(ok(cons(from(_x41), _x22))) → top#(cons(mark(cons(_x41, from(s(_x41)))), _x22))top#(ok(from(cons(cons(from(s(length1(ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(ok(length(_x91))))), _x52), _x42)))
top#(ok(s(s(from(s(from(cons(length(nil), _x82)))))))) → top#(s(s(from(s(from(cons(mark(0), _x82)))))))top#(ok(s(cons(cons(from(s(s(s(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(s(active(_x91))))), _x52), _x42)))
top#(ok(s(cons(cons(cons(from(_x71), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(mark(cons(_x71, from(s(_x71)))), _x62), _x52), _x42)))top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(ok(ok(_x151))))))))))))))) → top#(s(s(from(s(from(s(s(mark(from(ok(ok(ok(ok(length(_x151)))))))))))))))
top#(ok(s(cons(cons(from(s(from(length(cons(_x92, _x91))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(s(length1(_x91)))))), _x52), _x42)))top#(ok(s(s(from(cons(length(cons(_x72, ok(_x91))), _x52)))))) → top#(s(s(from(mark(cons(s(ok(length1(_x91))), _x52))))))
top#(ok(from(cons(length(cons(_x52, ok(ok(ok(_x91))))), _x32)))) → top#(from(mark(cons(s(ok(ok(ok(length1(_x91))))), _x32))))top#(ok(from(from(from(s(cons(length(cons(_x82, ok(_x101))), _x72))))))) → top#(from(from(from(s(cons(mark(s(ok(length1(_x101)))), _x72))))))
top#(ok(from(from(from(length1(_x61)))))) → top#(from(from(mark(from(length(_x61))))))top#(ok(from(cons(length(cons(_x52, ok(ok(_x81)))), _x42)))) → top#(from(cons(mark(ok(s(ok(length1(_x81))))), _x42)))
top#(ok(from(from(from(s(cons(from(_x81), _x72))))))) → top#(from(from(from(s(cons(from(active(_x81)), _x72))))))top#(ok(s(s(from(s(from(s(s(from(cons(from(_x121), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(from(active(_x121)), _x112))))))))))
top#(ok(s(s(from(s(from(s(s(cons(_x101, _x102)))))))))) → top#(s(s(from(s(from(s(s(cons(active(_x101), _x102)))))))))top#(ok(s(cons(cons(cons(s(_x71), _x62), _x52), _x42)))) → top#(s(cons(cons(cons(s(active(_x71)), _x62), _x52), _x42)))
top#(ok(from(from(from(s(from(from(_x81)))))))) → top#(from(from(from(s(from(from(active(_x81))))))))top#(ok(from(length1(ok(_x51))))) → top#(mark(from(ok(length(_x51)))))
top#(ok(s(s(from(s(from(from(_x81)))))))) → top#(s(s(from(s(from(mark(cons(_x81, from(s(_x81))))))))))top#(ok(from(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(from(active(_x71))), _x52), _x42)))
top#(ok(s(length(cons(_x42, ok(_x61)))))) → top#(s(mark(s(ok(length1(_x61))))))top#(ok(s(s(from(s(from(length1(_x81)))))))) → top#(s(s(from(s(from(mark(length(_x81))))))))
top#(ok(cons(length1(_x41), _x22))) → top#(cons(mark(length(_x41)), _x22))top#(ok(from(from(length1(ok(_x61)))))) → top#(mark(from(from(ok(length(_x61))))))
top#(ok(from(cons(length(cons(_x52, ok(ok(ok(_x101))))), _x32)))) → top#(from(mark(cons(s(ok(ok(ok(length1(_x101))))), _x32))))top#(ok(s(s(length(nil))))) → top#(s(mark(s(0))))
top#(ok(s(s(from(s(from(from(_x81)))))))) → top#(s(s(from(s(from(from(active(_x81))))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(from(mark(s(ok(ok(length1(_x81))))))))
top#(ok(s(s(from(s(from(s(s(from(length1(_x111))))))))))) → top#(s(s(from(s(from(s(mark(s(from(length(_x111)))))))))))top#(ok(s(cons(cons(from(s(from(length1(ok(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(mark(s(from(ok(length(_x101)))))), _x52), _x42)))
top#(ok(s(s(from(s(from(cons(cons(_x91, _x92), _x82)))))))) → top#(s(s(from(s(from(cons(cons(active(_x91), _x92), _x82)))))))top#(ok(s(s(from(s(from(length(cons(_x82, ok(_x101)))))))))) → top#(s(s(from(s(from(mark(s(ok(length1(_x101))))))))))
top#(ok(s(s(from(s(from(s(s(from(length(cons(_x112, _x111)))))))))))) → top#(s(s(from(s(from(s(s(mark(from(s(length1(_x111))))))))))))top#(ok(length(cons(_x22, _x21)))) → top#(mark(s(length1(_x21))))
top#(ok(s(s(from(cons(length(cons(_x72, ok(ok(ok(_x111))))), _x62)))))) → top#(s(s(from(cons(mark(s(ok(ok(ok(length1(_x111)))))), _x62)))))top#(ok(cons(length(cons(_x42, ok(_x71))), _x22))) → top#(cons(mark(s(ok(length1(_x71)))), _x22))
top#(ok(s(cons(cons(from(length(cons(_x72, _x71))), _x52), _x42)))) → top#(s(cons(cons(mark(from(s(length1(_x71)))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(length1(ok(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(mark(ok(length(_x101)))))), _x52), _x42)))
top#(ok(from(cons(from(from(_x61)), _x42)))) → top#(from(cons(from(from(active(_x61))), _x42)))top#(ok(from(cons(from(_x51), _x42)))) → top#(from(cons(mark(cons(_x51, from(s(_x51)))), _x42)))
top#(ok(from(from(from(s(cons(length(cons(_x82, _x81)), _x62))))))) → top#(from(from(mark(from(s(cons(s(length1(_x81)), _x62)))))))top#(ok(from(cons(from(cons(cons(_x71, _x72), _x62)), _x42)))) → top#(from(cons(from(cons(cons(active(_x71), _x72), _x62)), _x42)))
top#(ok(from(cons(cons(from(s(from(s(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(s(from(s(active(_x91))))), _x52), _x42)))top#(ok(s(cons(length(cons(_x52, ok(ok(_x91)))), _x32)))) → top#(s(mark(cons(s(ok(ok(length1(_x91)))), _x32))))
top#(ok(from(cons(cons(length(cons(_x62, _x61)), _x52), _x42)))) → top#(from(cons(cons(mark(s(length1(_x61))), _x52), _x42)))top#(ok(from(cons(cons(s(length1(_x71)), _x52), _x42)))) → top#(from(cons(cons(s(mark(length(_x71))), _x52), _x42)))
top#(ok(from(cons(cons(from(from(_x71)), _x52), _x42)))) → top#(from(cons(cons(from(mark(cons(_x71, from(s(_x71))))), _x52), _x42)))top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(_x131))))))))))))) → top#(s(s(from(s(from(s(mark(s(from(ok(ok(length(_x131)))))))))))))
top#(ok(s(s(from(cons(s(_x71), _x62)))))) → top#(s(s(from(cons(s(active(_x71)), _x62)))))top#(ok(from(length1(ok(ok(ok(_x71))))))) → top#(mark(from(ok(ok(ok(length(_x71)))))))
top#(ok(from(cons(from(cons(length(cons(_x72, _x71)), _x52)), _x42)))) → top#(from(cons(from(mark(cons(s(length1(_x71)), _x52))), _x42)))top#(ok(s(s(from(s(from(s(s(from(length1(ok(ok(ok(ok(ok(_x161)))))))))))))))) → top#(s(s(from(s(from(s(s(from(mark(ok(ok(ok(ok(ok(length(_x161))))))))))))))))
top#(ok(from(from(from(s(from(_x71))))))) → top#(from(from(from(s(mark(cons(_x71, from(s(_x71)))))))))top#(ok(s(s(from(cons(from(_x71), _x62)))))) → top#(s(s(from(cons(from(active(_x71)), _x62)))))
top#(ok(s(cons(s(_x51), _x42)))) → top#(s(cons(s(active(_x51)), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(from(mark(ok(s(ok(length1(_x81))))))))
top#(ok(s(s(from(s(from(length(nil)))))))) → top#(s(s(mark(from(s(from(0)))))))top#(ok(from(cons(cons(s(length(cons(_x72, ok(ok(ok(_x111)))))), _x52), _x42)))) → top#(from(cons(cons(s(mark(s(ok(ok(ok(length1(_x111))))))), _x52), _x42)))
top#(ok(from(from(length(nil))))) → top#(mark(from(from(0))))top#(ok(s(s(from(s(from(length(cons(_x82, _x81))))))))) → top#(s(s(from(s(mark(from(s(length1(_x81)))))))))
top#(ok(from(cons(cons(s(cons(_x71, _x72)), _x52), _x42)))) → top#(from(cons(cons(s(cons(active(_x71), _x72)), _x52), _x42)))top#(ok(from(cons(from(cons(s(s(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(s(active(_x81))), _x62)), _x42)))
top#(mark(length(_x21))) → top#(length(proper(_x21)))top#(ok(from(cons(cons(from(cons(_x71, _x72)), _x52), _x42)))) → top#(from(cons(cons(from(cons(active(_x71), _x72)), _x52), _x42)))
top#(ok(from(cons(from(cons(from(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(cons(_x71, from(s(_x71)))), _x62)), _x42)))top#(ok(s(cons(length(nil), _x42)))) → top#(s(cons(mark(0), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(ok(_x91))))))))) → top#(from(mark(from(ok(s(ok(ok(length1(_x91)))))))))top#(ok(s(s(from(s(from(s(s(from(length1(ok(_x121)))))))))))) → top#(s(s(from(s(from(s(mark(s(ok(from(length(_x121))))))))))))
top#(ok(s(s(from(s(s(_x71))))))) → top#(s(s(from(s(s(active(_x71)))))))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(from(s(ok(ok(length1(_x81))))))))
top#(ok(from(from(from(length1(ok(_x71))))))) → top#(from(from(from(mark(ok(length(_x71)))))))top#(ok(s(s(from(s(from(cons(length1(_x91), _x82)))))))) → top#(s(s(from(s(from(cons(mark(length(_x91)), _x82)))))))
top#(ok(from(cons(cons(from(s(length1(_x81))), _x52), _x42)))) → top#(from(cons(cons(mark(from(s(length(_x81)))), _x52), _x42)))top#(ok(from(cons(from(length(cons(_x62, _x61))), _x42)))) → top#(from(cons(from(mark(s(length1(_x61)))), _x42)))
top#(ok(s(s(from(s(from(s(s(length1(_x101)))))))))) → top#(s(s(from(s(from(s(s(mark(length(_x101))))))))))top#(ok(from(cons(cons(from(s(length1(ok(_x91)))), _x52), _x42)))) → top#(from(cons(cons(from(mark(s(ok(length(_x91))))), _x52), _x42)))
top#(ok(from(length(cons(_x42, ok(_x61)))))) → top#(mark(from(s(ok(length1(_x61))))))top#(ok(s(s(length1(ok(_x61)))))) → top#(s(mark(ok(s(length(_x61))))))
top#(ok(s(s(from(s(from(s(s(from(cons(cons(_x121, _x122), _x112))))))))))) → top#(s(s(from(s(from(s(s(from(cons(cons(active(_x121), _x122), _x112))))))))))top#(ok(from(from(length1(_x51))))) → top#(from(mark(from(length(_x51)))))
top#(ok(from(from(from(s(from(s(_x81)))))))) → top#(from(from(from(s(from(s(active(_x81))))))))top#(ok(from(cons(from(cons(s(length1(_x81)), _x62)), _x42)))) → top#(from(cons(from(cons(s(mark(length(_x81))), _x62)), _x42)))
top#(ok(from(cons(cons(length(nil), _x52), _x42)))) → top#(from(cons(cons(mark(0), _x52), _x42)))top#(ok(from(cons(length(cons(_x52, ok(ok(ok(_x91))))), _x42)))) → top#(from(cons(mark(ok(s(ok(ok(length1(_x91)))))), _x42)))
top#(ok(s(cons(cons(from(s(from(cons(_x91, _x92)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(cons(active(_x91), _x92)))), _x52), _x42)))top#(ok(s(cons(cons(from(s(s(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(from(active(_x91))))), _x52), _x42)))
top#(ok(s(s(from(s(from(s(s(from(s(_x111))))))))))) → top#(s(s(from(s(from(s(s(from(s(active(_x111)))))))))))top#(ok(from(length1(_x41)))) → top#(mark(from(length(_x41))))
top#(ok(from(from(from(s(length(cons(_x72, _x71)))))))) → top#(from(from(from(s(mark(s(length1(_x71))))))))top#(ok(from(cons(from(cons(s(cons(_x81, _x82)), _x62)), _x42)))) → top#(from(cons(from(cons(s(cons(active(_x81), _x82)), _x62)), _x42)))
top#(ok(from(cons(s(_x51), _x42)))) → top#(from(cons(s(active(_x51)), _x42)))top#(ok(from(from(_x41)))) → top#(from(mark(cons(_x41, from(s(_x41))))))
top#(ok(from(length(cons(_x42, ok(ok(ok(_x81)))))))) → top#(from(mark(ok(s(ok(ok(length1(_x81))))))))top#(ok(s(cons(cons(from(s(cons(_x81, _x82))), _x52), _x42)))) → top#(s(cons(cons(from(s(cons(active(_x81), _x82))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(s(cons(_x91, _x92)))), _x52), _x42)))) → top#(s(cons(cons(from(s(s(cons(active(_x91), _x92)))), _x52), _x42)))top#(ok(s(cons(from(_x51), _x42)))) → top#(s(cons(from(active(_x51)), _x42)))
top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(from(mark(ok(from(s(ok(length1(_x81))))))))top#(ok(from(s(_x41)))) → top#(from(s(active(_x41))))
top#(ok(from(cons(from(cons(length1(_x71), _x62)), _x42)))) → top#(from(cons(from(cons(mark(length(_x71)), _x62)), _x42)))top#(ok(from(from(length(cons(_x52, ok(ok(_x81)))))))) → top#(mark(from(from(ok(s(ok(length1(_x81))))))))
top#(ok(s(cons(cons(from(_x61), _x52), _x42)))) → top#(s(cons(cons(mark(cons(_x61, from(s(_x61)))), _x52), _x42)))top#(ok(s(cons(cons(from(cons(_x71, _x72)), _x52), _x42)))) → top#(s(cons(cons(from(cons(active(_x71), _x72)), _x52), _x42)))
top#(ok(from(cons(cons(from(s(length(cons(_x82, _x81)))), _x52), _x42)))) → top#(from(cons(cons(from(s(mark(s(length1(_x81))))), _x52), _x42)))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

The right-hand side of the rule top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(active(_x91))))), _x52), _x42))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
top#(s(cons(cons(from(s(from(from(mark(s(length1(_x101))))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(mark(length(_x101)))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(s(active(_x101)))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(cons(active(_x101), _x102))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(from(active(_x101)))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(mark(cons(_x101, from(s(_x101)))))))), _x52), _x42))) 
top#(s(cons(cons(from(s(from(from(mark(0))))), _x52), _x42))) 
Thus, the rule top#(ok(s(cons(cons(from(s(from(from(_x91)))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(active(_x91))))), _x52), _x42))) is replaced by the following rules:
top#(ok(s(cons(cons(from(s(from(from(length1(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(mark(length(_x101)))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(from(s(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(s(active(_x101)))))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(from(from(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(from(active(_x101)))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(from(length(cons(_x102, _x101)))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(mark(s(length1(_x101))))))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(from(from(_x101))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(mark(cons(_x101, from(s(_x101)))))))), _x52), _x42)))top#(ok(s(cons(cons(from(s(from(from(cons(_x101, _x102))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(cons(active(_x101), _x102))))), _x52), _x42)))
top#(ok(s(cons(cons(from(s(from(from(length(nil))))), _x52), _x42)))) → top#(s(cons(cons(from(s(from(from(mark(0))))), _x52), _x42)))

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

length1#(ok(X)) → length1#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length1#(ok(X)) → length1#(X)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

length#(ok(X)) → length#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(ok(X)) → length#(X)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

cons#(mark(X1), X2) → cons#(X1, X2)cons#(ok(X1), ok(X2)) → cons#(X1, X2)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

active#(from(X)) → active#(X)active#(s(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(s(X)) → active#(X)active#(from(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

from#(mark(X)) → from#(X)from#(ok(X)) → from#(X)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

proper#(length1(X)) → proper#(X)proper#(s(X)) → proper#(X)
proper#(length(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(from(X)) → proper#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(length(nil)) → mark(0)
active(length(cons(X, Y))) → mark(s(length1(Y)))active(length1(X)) → mark(length(X))
active(from(X)) → from(active(X))active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))from(mark(X)) → mark(from(X))
cons(mark(X1), X2) → mark(cons(X1, X2))s(mark(X)) → mark(s(X))
proper(from(X)) → from(proper(X))proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))proper(length(X)) → length(proper(X))
proper(nil) → ok(nil)proper(0) → ok(0)
proper(length1(X)) → length1(proper(X))from(ok(X)) → ok(from(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))length1(ok(X)) → ok(length1(X))
top(mark(X)) → top(proper(X))top(ok(X)) → top(active(X))

Original Signature

Termination of terms over the following signature is verified: 0, s, length, active, mark, ok, from, length1, proper, cons, nil, top

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(length(X)) → proper#(X)proper#(length1(X)) → proper#(X)
proper#(s(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(cons(X1, X2)) → proper#(X2)proper#(from(X)) → proper#(X)