Termination w.r.t. Q proof of /tmp/tmpY38e9n/Ex14_AEGL02

Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 QDPOrderProof (⇔)

    ↳9 QDP

  ↳10 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FROM(X) → CONS(X, n__from(n__s(X)))
LENGTH(n__cons(X, Y)) → S(length1(activate(Y)))
LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH(n__cons(X, Y)) → ACTIVATE(Y)
LENGTH1(X) → LENGTH(activate(X))
LENGTH1(X) → ACTIVATE(X)
ACTIVATE(n__from(X)) → FROM(activate(X))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 8 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__from(X)) → ACTIVATE(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1) = ACTIVATE(x1)
n__s(x1) = x1
n__from(x1) = n__from(x1)
n__cons(x1, x2) = x1
from(x1) = from(x1)
cons(x1, x2) = x1
length(x1) = length
n__nil = n__nil
0 = 0
s(x1) = x1
length1(x1) = length1
activate(x1) = x1
nil = nil

Recursive path order with status [RPO].
Quasi-Precedence:

[n_{_from₁}, from₁] > [ACTIVATE₁, length, 0, length1]
[n_{_nil}, nil] > [ACTIVATE₁, length, 0, length1]

Status:

ACTIVATE₁: multiset
n_{_from₁}: multiset
from₁: multiset
length: multiset
n_{_nil}: multiset
0: multiset
length1: multiset
nil: multiset

The following usable rules [FROCOS05] were oriented:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1) = ACTIVATE(x1)
n__s(x1) = x1
n__cons(x1, x2) = n__cons(x1)
from(x1) = from(x1)
cons(x1, x2) = cons(x1)
n__from(x1) = n__from(x1)
length(x1) = length
n__nil = n__nil
0 = 0
s(x1) = x1
length1(x1) = length1
activate(x1) = activate(x1)
nil = nil

Recursive path order with status [RPO].
Quasi-Precedence:

activate₁ > [from₁, cons₁] > n_{_cons₁} > [length, length1] > 0
activate₁ > [from₁, cons₁] > n_{_from₁}
activate₁ > nil > n_{_nil} > 0

Status:

ACTIVATE₁: multiset
n_{_cons₁}: multiset
from₁: multiset
cons₁: multiset
n_{_from₁}: multiset
length: multiset
n_{_nil}: multiset
0: multiset
length1: multiset
activate₁: multiset
nil: multiset

The following usable rules [FROCOS05] were oriented:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(n__cons(X, Y)) → LENGTH1(activate(Y))
LENGTH1(X) → LENGTH(activate(X))

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
s(X) → n__s(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.