NO Termination w.r.t. Q proof of Transformed_CSR_04_Ex5_DLMMU04_Z.ari

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

0 QTRS
↳1 QTRSRRRProof (⇔, 80 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 17 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 0 ms)
↳8 QTRS
↳9 QTRSRRRProof (⇔, 0 ms)
↳10 QTRS
↳11 QTRSRRRProof (⇔, 5 ms)
↳12 QTRS
↳13 DependencyPairsProof (⇔, 0 ms)
↳14 QDP
↳15 DependencyGraphProof (⇔, 0 ms)
↳16 AND
    ↳17 QDP
        ↳18 UsableRulesProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 QDPSizeChangeProof (⇔, 0 ms)
        ↳21 YES
    ↳22 QDP
        ↳23 UsableRulesProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 NonTerminationLoopProof (⇒, 0 ms)
        ↳26 NO

(0) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = 2·x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__incr(x1)) = x1   
POL(n__repItems(x1)) = 1 + x1   
POL(n__take(x1, x2)) = x1 + x2   
POL(n__zip(x1, x2)) = 1 + x1 + x2   
POL(nil) = 0   
POL(oddNs) = 0   
POL(pair(x1, x2)) = x1 + 2·x2   
POL(pairNs) = 0   
POL(repItems(x1)) = 2 + 2·x1   
POL(s(x1)) = 2·x1   
POL(tail(x1)) = x1   
POL(take(x1, x2)) = x1 + 2·x2   
POL(zip(x1, x2)) = 2 + 2·x1 + 2·x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

zip(nil, XS) → nil
zip(X, nil) → nil
repItems(nil) → nil
zip(X1, X2) → n__zip(X1, X2)
repItems(X) → n__repItems(X)


(2) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = 2·x1 + x2   
POL(n__incr(x1)) = 2·x1   
POL(n__repItems(x1)) = 2 + 2·x1   
POL(n__take(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(n__zip(x1, x2)) = x1 + 2·x2   
POL(nil) = 1   
POL(oddNs) = 0   
POL(pair(x1, x2)) = x1 + 2·x2   
POL(pairNs) = 0   
POL(repItems(x1)) = 2 + 2·x1   
POL(s(x1)) = 2·x1   
POL(tail(x1)) = 2·x1   
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(zip(x1, x2)) = x1 + 2·x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

take(0, XS) → nil


(4) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
take(X1, X2) → n__take(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = 2·x1   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__incr(x1)) = x1   
POL(n__repItems(x1)) = x1   
POL(n__take(x1, x2)) = 1 + x1 + x2   
POL(n__zip(x1, x2)) = x1 + x2   
POL(oddNs) = 0   
POL(pair(x1, x2)) = x1 + 2·x2   
POL(pairNs) = 0   
POL(repItems(x1)) = 2·x1   
POL(s(x1)) = x1   
POL(tail(x1)) = 1 + 2·x1   
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(zip(x1, x2)) = 2·x1 + 2·x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
tail(cons(X, XS)) → activate(XS)
take(X1, X2) → n__take(X1, X2)


(6) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = 2·x1 + x2   
POL(n__incr(x1)) = 2·x1   
POL(n__repItems(x1)) = 2·x1   
POL(n__take(x1, x2)) = 2 + x1 + 2·x2   
POL(n__zip(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(oddNs) = 0   
POL(pair(x1, x2)) = x1 + 2·x2   
POL(pairNs) = 0   
POL(repItems(x1)) = 2·x1   
POL(s(x1)) = 2·x1   
POL(take(x1, x2)) = 1 + x1 + x2   
POL(zip(x1, x2)) = 2 + 2·x1 + 2·x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

activate(n__take(X1, X2)) → take(X1, X2)


(8) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(9) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = 2·x1   
POL(cons(x1, x2)) = x1 + x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__incr(x1)) = x1   
POL(n__repItems(x1)) = 1 + x1   
POL(n__zip(x1, x2)) = 1 + x1 + x2   
POL(oddNs) = 0   
POL(pair(x1, x2)) = x1 + x2   
POL(pairNs) = 0   
POL(repItems(x1)) = 2 + 2·x1   
POL(s(x1)) = x1   
POL(zip(x1, x2)) = 2 + 2·x1 + 2·x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))


(10) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__repItems(X)) → repItems(X)
activate(X) → X

Q is empty.

(11) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(incr(x1)) = 2·x1   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__incr(x1)) = 2·x1   
POL(n__repItems(x1)) = 2 + 2·x1   
POL(n__zip(x1, x2)) = 2 + x1 + x2   
POL(oddNs) = 0   
POL(pairNs) = 0   
POL(repItems(x1)) = 1 + x1   
POL(s(x1)) = x1   
POL(zip(x1, x2)) = 1 + x1 + x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

activate(n__zip(X1, X2)) → zip(X1, X2)
activate(n__repItems(X)) → repItems(X)


(12) Obligation:

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

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

Q is empty.

(13) DependencyPairsProof (EQUIVALENT transformation)

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

(14) Obligation:

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

PAIRNS → CONS(0, n__incr(oddNs))
PAIRNS → ODDNS
ODDNS → INCR(pairNs)
ODDNS → PAIRNS
INCR(cons(X, XS)) → CONS(s(X), n__incr(activate(XS)))
INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

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

(15) DependencyGraphProof (EQUIVALENT transformation)

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

(16) Complex Obligation (AND)

(17) Obligation:

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

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

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

(18) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(19) Obligation:

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

INCR(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__incr(X)) → INCR(X)

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

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACTIVATE(n__incr(X)) → INCR(X)
    The graph contains the following edges 1 > 1

  • INCR(cons(X, XS)) → ACTIVATE(XS)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

PAIRNS → ODDNS
ODDNS → PAIRNS

The TRS R consists of the following rules:

pairNs → cons(0, n__incr(oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
incr(X) → n__incr(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__incr(X)) → incr(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X

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

(23) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

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

PAIRNS → ODDNS
ODDNS → PAIRNS

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

(25) NonTerminationLoopProof (COMPLETE transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ODDNS evaluates to t =ODDNS

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

ODDNS → PAIRNS
with rule ODDNS → PAIRNS at position [] and matcher [ ]

PAIRNS → ODDNS
with rule PAIRNS → ODDNS

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(26) NO