YES
proof of Transformed_CSR_04_ExIntrod_GM04_iGM.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


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

(0) QTRS
(1) QTRSRRRProof [EQUIVALENT, 71 ms]
(2) QTRS
(3) QTRSRRRProof [EQUIVALENT, 6 ms]
(4) QTRS
(5) DependencyPairsProof [EQUIVALENT, 0 ms]
(6) QDP
(7) DependencyGraphProof [EQUIVALENT, 0 ms]
(8) AND
    (9) QDP
        (10) UsableRulesProof [EQUIVALENT, 0 ms]
        (11) QDP
        (12) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (13) YES
    (14) QDP
        (15) UsableRulesProof [EQUIVALENT, 0 ms]
        (16) QDP
        (17) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (18) YES
    (19) QDP
        (20) UsableRulesProof [EQUIVALENT, 0 ms]
        (21) QDP
        (22) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (23) YES
    (24) QDP
        (25) UsableRulesProof [EQUIVALENT, 0 ms]
        (26) QDP
        (27) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (28) YES
    (29) QDP
        (30) UsableRulesProof [EQUIVALENT, 0 ms]
        (31) QDP
        (32) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (33) YES
    (34) QDP
        (35) UsableRulesProof [EQUIVALENT, 0 ms]
        (36) QDP
        (37) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (38) YES
    (39) QDP
        (40) MRRProof [EQUIVALENT, 21 ms]
        (41) QDP
        (42) MRRProof [EQUIVALENT, 0 ms]
        (43) QDP
        (44) MRRProof [EQUIVALENT, 19 ms]
        (45) QDP
        (46) TransformationProof [EQUIVALENT, 0 ms]
        (47) QDP
        (48) DependencyGraphProof [EQUIVALENT, 0 ms]
        (49) QDP
        (50) QDPOrderProof [EQUIVALENT, 133 ms]
        (51) QDP
        (52) QDPOrderProof [EQUIVALENT, 0 ms]
        (53) QDP
        (54) PisEmptyProof [EQUIVALENT, 0 ms]
        (55) YES


----------------------------------------

(0)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   active(nats) -> mark(adx(zeros))
   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   active(hd(cons(X, Y))) -> mark(X)
   active(tl(cons(X, Y))) -> mark(Y)
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

Q is empty.

----------------------------------------

(1) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(adx(x_1)) = x_1
   POL(cons(x_1, x_2)) = 2*x_1 + x_2
   POL(hd(x_1)) = 1 + x_1
   POL(incr(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(nats) = 2
   POL(s(x_1)) = x_1
   POL(tl(x_1)) = 2 + 2*x_1
   POL(zeros) = 2
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   active(hd(cons(X, Y))) -> mark(X)
   active(tl(cons(X, Y))) -> mark(Y)




----------------------------------------

(2)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   active(nats) -> mark(adx(zeros))
   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

Q is empty.

----------------------------------------

(3) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(active(x_1)) = x_1
   POL(adx(x_1)) = x_1
   POL(cons(x_1, x_2)) = 2*x_1 + x_2
   POL(hd(x_1)) = 2 + 2*x_1
   POL(incr(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(nats) = 2
   POL(s(x_1)) = x_1
   POL(tl(x_1)) = 2 + x_1
   POL(zeros) = 1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   active(nats) -> mark(adx(zeros))




----------------------------------------

(4)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

Q is empty.

----------------------------------------

(5) DependencyPairsProof (EQUIVALENT)
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(zeros) -> MARK(cons(0, zeros))
   ACTIVE(zeros) -> CONS(0, zeros)
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   ACTIVE(incr(cons(X, Y))) -> CONS(s(X), incr(Y))
   ACTIVE(incr(cons(X, Y))) -> S(X)
   ACTIVE(incr(cons(X, Y))) -> INCR(Y)
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   ACTIVE(adx(cons(X, Y))) -> INCR(cons(X, adx(Y)))
   ACTIVE(adx(cons(X, Y))) -> CONS(X, adx(Y))
   ACTIVE(adx(cons(X, Y))) -> ADX(Y)
   MARK(nats) -> ACTIVE(nats)
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   MARK(adx(X)) -> ADX(mark(X))
   MARK(adx(X)) -> MARK(X)
   MARK(zeros) -> ACTIVE(zeros)
   MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2))
   MARK(0) -> ACTIVE(0)
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> INCR(mark(X))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(hd(X)) -> HD(mark(X))
   MARK(hd(X)) -> MARK(X)
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(tl(X)) -> TL(mark(X))
   MARK(tl(X)) -> MARK(X)
   ADX(mark(X)) -> ADX(X)
   ADX(active(X)) -> ADX(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)
   HD(mark(X)) -> HD(X)
   HD(active(X)) -> HD(X)
   TL(mark(X)) -> TL(X)
   TL(active(X)) -> TL(X)

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(7) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 13 less nodes.
----------------------------------------

(8)
Complex Obligation (AND)

----------------------------------------

(9)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   TL(active(X)) -> TL(X)
   TL(mark(X)) -> TL(X)

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(10) UsableRulesProof (EQUIVALENT)
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:

   TL(active(X)) -> TL(X)
   TL(mark(X)) -> TL(X)

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

(12) QDPSizeChangeProof (EQUIVALENT)
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:
*TL(active(X)) -> TL(X)
The graph contains the following edges 1 > 1


*TL(mark(X)) -> TL(X)
The graph contains the following edges 1 > 1


----------------------------------------

(13)
YES

----------------------------------------

(14)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   HD(active(X)) -> HD(X)
   HD(mark(X)) -> HD(X)

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(15) UsableRulesProof (EQUIVALENT)
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:

   HD(active(X)) -> HD(X)
   HD(mark(X)) -> HD(X)

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

(17) QDPSizeChangeProof (EQUIVALENT)
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:
*HD(active(X)) -> HD(X)
The graph contains the following edges 1 > 1


*HD(mark(X)) -> HD(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(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(20) UsableRulesProof (EQUIVALENT)
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)
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(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(25) UsableRulesProof (EQUIVALENT)
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)
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(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(30) UsableRulesProof (EQUIVALENT)
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)
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:

   ADX(active(X)) -> ADX(X)
   ADX(mark(X)) -> ADX(X)

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(35) UsableRulesProof (EQUIVALENT)
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.
----------------------------------------

(36)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   ADX(active(X)) -> ADX(X)
   ADX(mark(X)) -> ADX(X)

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

(37) QDPSizeChangeProof (EQUIVALENT)
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:
*ADX(active(X)) -> ADX(X)
The graph contains the following edges 1 > 1


*ADX(mark(X)) -> ADX(X)
The graph contains the following edges 1 > 1


----------------------------------------

(38)
YES

----------------------------------------

(39)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(adx(X)) -> MARK(X)
   MARK(zeros) -> ACTIVE(zeros)
   ACTIVE(zeros) -> MARK(cons(0, zeros))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(hd(X)) -> MARK(X)
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(tl(X)) -> MARK(X)

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(40) MRRProof (EQUIVALENT)
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(tl(X)) -> MARK(X)


Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(ACTIVE(x_1)) = 2*x_1
   POL(MARK(x_1)) = 2*x_1
   POL(active(x_1)) = x_1
   POL(adx(x_1)) = 2*x_1
   POL(cons(x_1, x_2)) = 2*x_1 + 2*x_2
   POL(hd(x_1)) = 2*x_1
   POL(incr(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(nats) = 1
   POL(s(x_1)) = x_1
   POL(tl(x_1)) = 1 + x_1
   POL(zeros) = 0


----------------------------------------

(41)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(adx(X)) -> MARK(X)
   MARK(zeros) -> ACTIVE(zeros)
   ACTIVE(zeros) -> MARK(cons(0, zeros))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(hd(X)) -> MARK(X)
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(42) MRRProof (EQUIVALENT)
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(adx(X)) -> MARK(X)


Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(ACTIVE(x_1)) = 2 + 2*x_1
   POL(MARK(x_1)) = 2 + 2*x_1
   POL(active(x_1)) = x_1
   POL(adx(x_1)) = 2 + 2*x_1
   POL(cons(x_1, x_2)) = 2*x_1 + x_2
   POL(hd(x_1)) = x_1
   POL(incr(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(nats) = 1
   POL(s(x_1)) = x_1
   POL(tl(x_1)) = 2 + x_1
   POL(zeros) = 2


----------------------------------------

(43)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(zeros) -> ACTIVE(zeros)
   ACTIVE(zeros) -> MARK(cons(0, zeros))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(hd(X)) -> MARK(X)
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(44) MRRProof (EQUIVALENT)
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(hd(X)) -> MARK(X)


Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(ACTIVE(x_1)) = 2 + 2*x_1
   POL(MARK(x_1)) = 2 + 2*x_1
   POL(active(x_1)) = x_1
   POL(adx(x_1)) = 1 + 2*x_1
   POL(cons(x_1, x_2)) = x_1 + x_2
   POL(hd(x_1)) = 1 + 2*x_1
   POL(incr(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(nats) = 1
   POL(s(x_1)) = x_1
   POL(tl(x_1)) = 2 + x_1
   POL(zeros) = 2


----------------------------------------

(45)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(zeros) -> ACTIVE(zeros)
   ACTIVE(zeros) -> MARK(cons(0, zeros))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(46) TransformationProof (EQUIVALENT)
By narrowing [LPAR04] the rule MARK(cons(X1, X2)) -> ACTIVE(cons(X1, X2)) at position [0] we obtained the following new rules [LPAR04]:

   (MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1)),MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1)))
   (MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1)),MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1)))
   (MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1)),MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1)))
   (MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1)),MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1)))


----------------------------------------

(47)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(zeros) -> ACTIVE(zeros)
   ACTIVE(zeros) -> MARK(cons(0, zeros))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1))
   MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(48) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
----------------------------------------

(49)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(incr(X)) -> MARK(X)
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1))
   MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(50) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   MARK(adx(X)) -> ACTIVE(adx(mark(X)))
   ACTIVE(incr(cons(X, Y))) -> MARK(cons(s(X), incr(Y)))
   MARK(incr(X)) -> ACTIVE(incr(mark(X)))
   MARK(incr(X)) -> MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ACTIVE_1(x_1) ) = x_1 + 1
POL( adx_1(x_1) ) = 2
POL( hd_1(x_1) ) = 2x_1
POL( incr_1(x_1) ) = 2x_1 + 1
POL( tl_1(x_1) ) = max{0, -2}
POL( mark_1(x_1) ) = 2x_1
POL( nats ) = 1
POL( active_1(x_1) ) = x_1
POL( cons_2(x_1, x_2) ) = max{0, -1}
POL( zeros ) = 2
POL( 0 ) = 2
POL( s_1(x_1) ) = 0
POL( MARK_1(x_1) ) = 2x_1 + 1

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

   mark(nats) -> active(nats)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   mark(adx(X)) -> active(adx(mark(X)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(zeros) -> active(zeros)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   mark(0) -> active(0)
   adx(active(X)) -> adx(X)
   adx(mark(X)) -> adx(X)
   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)
   hd(active(X)) -> hd(X)
   hd(mark(X)) -> hd(X)
   tl(active(X)) -> tl(X)
   tl(mark(X)) -> tl(X)


----------------------------------------

(51)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1))
   MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1))

The TRS R consists of the following rules:

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

(52) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   ACTIVE(adx(cons(X, Y))) -> MARK(incr(cons(X, adx(Y))))
   MARK(s(X)) -> ACTIVE(s(X))
   MARK(hd(X)) -> ACTIVE(hd(mark(X)))
   MARK(tl(X)) -> ACTIVE(tl(mark(X)))
   MARK(cons(mark(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, mark(x1))) -> ACTIVE(cons(x0, x1))
   MARK(cons(active(x0), x1)) -> ACTIVE(cons(x0, x1))
   MARK(cons(x0, active(x1))) -> ACTIVE(cons(x0, x1))
The remaining pairs can at least be oriented weakly.
Used ordering:  Combined order from the following AFS and order.
ACTIVE(x1)  =  ACTIVE

MARK(x1)  =  x1

incr(x1)  =  incr

s(x1)  =  s

hd(x1)  =  hd

tl(x1)  =  tl

cons(x1, x2)  =  cons


Knuth-Bendix order [KBO] with precedence:s > ACTIVE > incr

and weight map:

   s=1
   hd=2
   ACTIVE=1
   cons=2
   tl=2
   incr=1

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

   incr(active(X)) -> incr(X)
   incr(mark(X)) -> incr(X)


----------------------------------------

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

   active(zeros) -> mark(cons(0, zeros))
   active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
   active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
   mark(nats) -> active(nats)
   mark(adx(X)) -> active(adx(mark(X)))
   mark(zeros) -> active(zeros)
   mark(cons(X1, X2)) -> active(cons(X1, X2))
   mark(0) -> active(0)
   mark(incr(X)) -> active(incr(mark(X)))
   mark(s(X)) -> active(s(X))
   mark(hd(X)) -> active(hd(mark(X)))
   mark(tl(X)) -> active(tl(mark(X)))
   adx(mark(X)) -> adx(X)
   adx(active(X)) -> adx(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)
   hd(mark(X)) -> hd(X)
   hd(active(X)) -> hd(X)
   tl(mark(X)) -> tl(X)
   tl(active(X)) -> tl(X)

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

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

(55)
YES