Termination proof of /tmp/tmpmoA2OQ/Ex5

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), incr(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, take(N, XS))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), zip(XS, YS))
tail(cons(X, XS)) → XS
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, cons(X, repItems(XS)))

The replacement map contains the following entries:

pairNs: empty set
cons: {1}
0: empty set
incr: {1}
oddNs: empty set
s: {1}
take: {1, 2}
nil: empty set
zip: {1, 2}
pair: {1, 2}
tail: {1}
repItems: {1}

↳ CSR

  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

pairNs → cons(0, incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), incr(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, take(N, XS))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), zip(XS, YS))
tail(cons(X, XS)) → XS
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, cons(X, repItems(XS)))

The replacement map contains the following entries:

pairNs: empty set
cons: {1}
0: empty set
incr: {1}
oddNs: empty set
s: {1}
take: {1, 2}
nil: empty set
zip: {1, 2}
pair: {1, 2}
tail: {1}
repItems: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, take, zip, pair, tail, repItems, INCR, TAIL, TAKE, ZIP, REPITEMS} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

ODDNS → INCR(pairNs)
ODDNS → PAIRNS

The collapsing dependency pairs are DP_c:

TAIL(cons(X, XS)) → XS

The hidden terms of R are:

incr(oddNs)
oddNs
incr(XS)
take(N, XS)
zip(XS, YS)
repItems(XS)

Every hiding context is built from:

incr on positions {1}
take on positions {1, 2}
zip on positions {1, 2}
repItems on positions {1}
cons on positions {1}

Hence, the new unhiding pairs DP_u are :

TAIL(cons(X, XS)) → U(XS)
U(incr(x_0)) → U(x_0)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zip(x_0, x_1)) → U(x_0)
U(zip(x_0, x_1)) → U(x_1)
U(repItems(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)
U(incr(oddNs)) → INCR(oddNs)
U(oddNs) → ODDNS
U(incr(XS)) → INCR(XS)
U(take(N, XS)) → TAKE(N, XS)
U(zip(XS, YS)) → ZIP(XS, YS)
U(repItems(XS)) → REPITEMS(XS)

The TRS R consists of the following rules:

pairNs → cons(0, incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), incr(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, take(N, XS))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), zip(XS, YS))
tail(cons(X, XS)) → XS
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, cons(X, repItems(XS)))

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 9 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ QCSDP

          ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, take, zip, pair, tail, repItems} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(incr(x_0)) → U(x_0)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zip(x_0, x_1)) → U(x_0)
U(zip(x_0, x_1)) → U(x_1)
U(repItems(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)

The TRS R consists of the following rules:

pairNs → cons(0, incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), incr(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, take(N, XS))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), zip(XS, YS))
tail(cons(X, XS)) → XS
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, cons(X, repItems(XS)))

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(incr(x_0)) → U(x_0)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zip(x_0, x_1)) → U(x_0)
U(zip(x_0, x_1)) → U(x_1)
U(repItems(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ QCSDP

          ↳ QCSDPSubtermProof

            ↳ QCSDP

              ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {incr, s, take, zip, pair, tail, repItems} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

pairNs → cons(0, incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), incr(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, take(N, XS))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), zip(XS, YS))
tail(cons(X, XS)) → XS
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, cons(X, repItems(XS)))

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.