YES Termination w.r.t. Q proof of Transformed_CSR_04_Ex1_Luc04b_iGM.ari

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

0 QTRS
↳1 QTRSRRRProof (⇔, 78 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 QDPSizeChangeProof (⇔, 0 ms)
        ↳23 YES
    ↳24 QDP
        ↳25 UsableRulesProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 QDPSizeChangeProof (⇔, 0 ms)
        ↳28 YES
    ↳29 QDP
        ↳30 UsableRulesProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 QDPSizeChangeProof (⇔, 0 ms)
        ↳33 YES
    ↳34 QDP
        ↳35 MRRProof (⇔, 4 ms)
        ↳36 QDP
        ↳37 QDPOrderProof (⇔, 70 ms)
        ↳38 QDP
        ↳39 DependencyGraphProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 QDPOrderProof (⇔, 30 ms)
        ↳42 QDP
        ↳43 QDPOrderProof (⇔, 4 ms)
        ↳44 QDP
        ↳45 QDPOrderProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 PisEmptyProof (⇔, 0 ms)
        ↳48 YES

(0) Obligation:

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

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
active(head(cons(X, XS))) → mark(X)
active(tail(cons(X, XS))) → mark(XS)
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(head(x1)) = 1 + x1   
POL(incr(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nats) = 0   
POL(odds) = 0   
POL(pairs) = 0   
POL(s(x1)) = 2·x1   
POL(tail(x1)) = 2·x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(head(cons(X, XS))) → mark(X)


(2) Obligation:

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

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
active(tail(cons(X, XS))) → mark(XS)
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(active(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(head(x1)) = 1 + 2·x1   
POL(incr(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nats) = 0   
POL(odds) = 0   
POL(pairs) = 0   
POL(s(x1)) = x1   
POL(tail(x1)) = 2 + 2·x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(tail(cons(X, XS))) → mark(XS)


(4) Obligation:

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

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.

(5) DependencyPairsProof (EQUIVALENT transformation)

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

(6) Obligation:

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

ACTIVE(nats) → MARK(cons(0, incr(nats)))
ACTIVE(nats) → CONS(0, incr(nats))
ACTIVE(nats) → INCR(nats)
ACTIVE(pairs) → MARK(cons(0, incr(odds)))
ACTIVE(pairs) → CONS(0, incr(odds))
ACTIVE(pairs) → INCR(odds)
ACTIVE(odds) → MARK(incr(pairs))
ACTIVE(odds) → INCR(pairs)
ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
ACTIVE(incr(cons(X, XS))) → CONS(s(X), incr(XS))
ACTIVE(incr(cons(X, XS))) → S(X)
ACTIVE(incr(cons(X, XS))) → INCR(XS)
MARK(nats) → ACTIVE(nats)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(0) → ACTIVE(0)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → INCR(mark(X))
MARK(incr(X)) → MARK(X)
MARK(pairs) → ACTIVE(pairs)
MARK(odds) → ACTIVE(odds)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(head(X)) → HEAD(mark(X))
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(tail(X)) → TAIL(mark(X))
MARK(tail(X)) → MARK(X)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
INCR(mark(X)) → INCR(X)
INCR(active(X)) → INCR(X)
S(mark(X)) → S(X)
S(active(X)) → S(X)
HEAD(mark(X)) → HEAD(X)
HEAD(active(X)) → HEAD(X)
TAIL(mark(X)) → TAIL(X)
TAIL(active(X)) → TAIL(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

TAIL(active(X)) → TAIL(X)
TAIL(mark(X)) → TAIL(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(10) 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.

(11) Obligation:

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

TAIL(active(X)) → TAIL(X)
TAIL(mark(X)) → TAIL(X)

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

(12) 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:

  • TAIL(active(X)) → TAIL(X)
    The graph contains the following edges 1 > 1

  • TAIL(mark(X)) → TAIL(X)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

HEAD(active(X)) → HEAD(X)
HEAD(mark(X)) → HEAD(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(15) 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.

(16) Obligation:

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

HEAD(active(X)) → HEAD(X)
HEAD(mark(X)) → HEAD(X)

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

(17) 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:

  • HEAD(active(X)) → HEAD(X)
    The graph contains the following edges 1 > 1

  • HEAD(mark(X)) → HEAD(X)
    The graph contains the following edges 1 > 1

(18) YES

(19) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(20) 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.

(21) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

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

(22) 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:

  • S(active(X)) → S(X)
    The graph contains the following edges 1 > 1

  • S(mark(X)) → S(X)
    The graph contains the following edges 1 > 1

(23) YES

(24) Obligation:

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

INCR(active(X)) → INCR(X)
INCR(mark(X)) → INCR(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(25) 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.

(26) Obligation:

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

INCR(active(X)) → INCR(X)
INCR(mark(X)) → INCR(X)

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

(27) 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:

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

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

(28) YES

(29) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(30) 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.

(31) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

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

(32) 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:

  • CONS(X1, mark(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • CONS(mark(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(active(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(X1, active(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(33) YES

(34) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)
ACTIVE(nats) → MARK(cons(0, incr(nats)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(pairs) → ACTIVE(pairs)
ACTIVE(pairs) → MARK(cons(0, incr(odds)))
MARK(odds) → ACTIVE(odds)
ACTIVE(odds) → MARK(incr(pairs))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(tail(X)) → MARK(X)

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(35) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MARK(head(X)) → MARK(X)
MARK(tail(X)) → MARK(X)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVE(x1)) = 1 + x1   
POL(MARK(x1)) = 1 + x1   
POL(active(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(head(x1)) = 2 + x1   
POL(incr(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nats) = 0   
POL(odds) = 0   
POL(pairs) = 0   
POL(s(x1)) = x1   
POL(tail(x1)) = 1 + x1   

(36) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)
ACTIVE(nats) → MARK(cons(0, incr(nats)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(pairs) → ACTIVE(pairs)
ACTIVE(pairs) → MARK(cons(0, incr(odds)))
MARK(odds) → ACTIVE(odds)
ACTIVE(odds) → MARK(incr(pairs))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(tail(X)) → ACTIVE(tail(mark(X)))

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(nats) → MARK(cons(0, incr(nats)))
ACTIVE(pairs) → MARK(cons(0, incr(odds)))
ACTIVE(odds) → MARK(incr(pairs))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  x1
cons(x1, x2)  =  x1
ACTIVE(x1)  =  x1
mark(x1)  =  x1
incr(x1)  =  x1
s(x1)  =  x1
nats  =  nats
0  =  0
pairs  =  pairs
odds  =  odds
head(x1)  =  head
tail(x1)  =  tail
active(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
nats > 0

and weight map:

nats=1
tail=2
0=1
head=2
odds=3
pairs=2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
mark(incr(X)) → active(incr(mark(X)))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(0) → active(0)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
head(active(X)) → head(X)
head(mark(X)) → head(X)
tail(active(X)) → tail(X)
tail(mark(X)) → tail(X)

(38) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(pairs) → ACTIVE(pairs)
MARK(odds) → ACTIVE(odds)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(tail(X)) → ACTIVE(tail(mark(X)))

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(40) Obligation:

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

ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → MARK(X1)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(tail(X)) → ACTIVE(tail(mark(X)))

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(41) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  x1
incr(x1)  =  x1
cons(x1, x2)  =  cons(x1)
MARK(x1)  =  x1
s(x1)  =  x1
mark(x1)  =  x1
head(x1)  =  head
tail(x1)  =  tail
active(x1)  =  x1
nats  =  nats
0  =  0
pairs  =  pairs
odds  =  odds

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

nats=4
tail=1
pairs=4
0=2
head=2
odds=5
cons_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

s(active(X)) → s(X)
s(mark(X)) → s(X)
incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
mark(incr(X)) → active(incr(mark(X)))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
mark(0) → active(0)
head(active(X)) → head(X)
head(mark(X)) → head(X)
tail(active(X)) → tail(X)
tail(mark(X)) → tail(X)

(42) Obligation:

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

ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(tail(X)) → ACTIVE(tail(mark(X)))

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(43) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → MARK(X)
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(tail(X)) → ACTIVE(tail(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = max{0, -2}

POL( MARK(x1) ) = max{0, 2x1 - 1}

POL( cons(x1, x2) ) = max{0, -2}

POL( s(x1) ) = 2x1 + 2

POL( active(x1) ) = max{0, 2x1 - 1}

POL( mark(x1) ) = max{0, x1 - 1}

POL( incr(x1) ) = 2x1 + 2

POL( head(x1) ) = 2x1 + 2

POL( tail(x1) ) = 2x1 + 2

POL( nats ) = 2

POL( 0 ) = 0

POL( pairs ) = 2

POL( odds ) = 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)

(44) Obligation:

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

ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))

The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(incr(cons(X, XS))) → MARK(cons(s(X), incr(XS)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  x1
incr(x1)  =  incr
cons(x1, x2)  =  cons
MARK(x1)  =  MARK

Knuth-Bendix order [KBO] with precedence:
MARK > cons

and weight map:

MARK=1
incr=2
cons=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)

(46) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(nats) → mark(cons(0, incr(nats)))
active(pairs) → mark(cons(0, incr(odds)))
active(odds) → mark(incr(pairs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
mark(nats) → active(nats)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(pairs) → active(pairs)
mark(odds) → active(odds)
mark(s(X)) → active(s(mark(X)))
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

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

(47) PisEmptyProof (EQUIVALENT transformation)

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

(48) YES