(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y)) → activate(X)
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(activate(x1)) = x1
POL(adx(x1)) = 2 + 2·x1
POL(cons(x1, x2)) = x1 + x2
POL(hd(x1)) = 2 + 2·x1
POL(incr(x1)) = x1
POL(n__0) = 0
POL(n__adx(x1)) = 2 + 2·x1
POL(n__incr(x1)) = x1
POL(n__s(x1)) = x1
POL(n__zeros) = 0
POL(nats) = 2
POL(s(x1)) = x1
POL(tl(x1)) = 2·x1
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
hd(cons(X, Y)) → activate(X)
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
nats → adx(zeros)
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(activate(x1)) = x1
POL(adx(x1)) = 1 + x1
POL(cons(x1, x2)) = x1 + x2
POL(incr(x1)) = x1
POL(n__0) = 0
POL(n__adx(x1)) = 1 + x1
POL(n__incr(x1)) = x1
POL(n__s(x1)) = x1
POL(n__zeros) = 0
POL(nats) = 2
POL(s(x1)) = x1
POL(tl(x1)) = x1
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
nats → adx(zeros)
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
tl(cons(X, Y)) → activate(Y)
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(activate(x1)) = x1
POL(adx(x1)) = 2 + 2·x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(incr(x1)) = x1
POL(n__0) = 0
POL(n__adx(x1)) = 2 + 2·x1
POL(n__incr(x1)) = x1
POL(n__s(x1)) = x1
POL(n__zeros) = 0
POL(s(x1)) = x1
POL(tl(x1)) = 2 + 2·x1
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
tl(cons(X, Y)) → activate(Y)
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(X)
INCR(cons(X, Y)) → ACTIVATE(Y)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 01
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__s(X)) → S(X)
ACTIVATE(n__incr(X)) → INCR(activate(X))
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ACTIVATE(n__adx(X)) → ACTIVATE(X)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
INCR(cons(X, Y)) → ACTIVATE(X)
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__adx(X)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) 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:
ACTIVATE(n__adx(X)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(X)
ADX(cons(X, Y)) → ACTIVATE(Y)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(ADX(x1)) = 2 + 2·x1
POL(INCR(x1)) = x1
POL(activate(x1)) = x1
POL(adx(x1)) = 2 + 2·x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(incr(x1)) = x1
POL(n__0) = 0
POL(n__adx(x1)) = 2 + 2·x1
POL(n__incr(x1)) = x1
POL(n__s(x1)) = x1
POL(n__zeros) = 2
POL(s(x1)) = x1
POL(zeros) = 2
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
INCR(cons(X, Y)) → ACTIVATE(X)
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
INCR(cons(X, Y)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(ACTIVATE(x1)) = | 5A | + | 5A | · | x1 |
POL(n__incr(x1)) = | 5A | + | 0A | · | x1 |
POL(INCR(x1)) = | 5A | + | 5A | · | x1 |
POL(activate(x1)) = | 0A | + | 0A | · | x1 |
POL(cons(x1, x2)) = | 5A | + | 1A | · | x1 | + | 0A | · | x2 |
POL(n__adx(x1)) = | 1A | + | 0A | · | x1 |
POL(ADX(x1)) = | 5A | + | 5A | · | x1 |
POL(n__s(x1)) = | -I | + | 0A | · | x1 |
POL(incr(x1)) = | 5A | + | 0A | · | x1 |
POL(adx(x1)) = | 1A | + | 0A | · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
incr(X) → n__incr(X)
adx(X) → n__adx(X)
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
zeros → cons(n__0, n__zeros)
zeros → n__zeros
0 → n__0
s(X) → n__s(X)
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
ACTIVATE(n__incr(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( n__incr(x1) ) = x1 + 1 |
POL( cons(x1, x2) ) = max{0, x2 - 1} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
incr(X) → n__incr(X)
adx(X) → n__adx(X)
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
zeros → cons(n__0, n__zeros)
zeros → n__zeros
0 → n__0
s(X) → n__s(X)
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(17) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__incr(
X)) →
INCR(
activate(
X)) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__incr(n__0)) → INCR(0) → ACTIVATE(n__incr(n__0)) → INCR(0)
ACTIVATE(n__incr(n__zeros)) → INCR(zeros) → ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0)) → ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0))) → ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0))) → ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0) → ACTIVATE(n__incr(x0)) → INCR(x0)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__0)) → INCR(0)
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__adx(
X)) →
ADX(
activate(
X)) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__adx(n__0)) → ADX(0) → ACTIVATE(n__adx(n__0)) → ADX(0)
ACTIVATE(n__adx(n__zeros)) → ADX(zeros) → ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0)) → ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0))) → ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0))) → ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0) → ACTIVATE(n__adx(x0)) → ADX(x0)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__0)) → INCR(0)
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__incr(
n__0)) →
INCR(
0) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__incr(n__0)) → INCR(n__0) → ACTIVATE(n__incr(n__0)) → INCR(n__0)
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__0)) → INCR(n__0)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__incr(
n__zeros)) →
INCR(
zeros) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros)) → ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros) → ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros)
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(n__s(x0))) → INCR(s(x0))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__incr(
n__s(
x0))) →
INCR(
s(
x0)) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__incr(n__s(x0))) → INCR(n__s(x0)) → ACTIVATE(n__incr(n__s(x0))) → INCR(n__s(x0))
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__incr(n__s(x0))) → INCR(n__s(x0))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__0)) → ADX(0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__adx(
n__0)) →
ADX(
0) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__adx(n__0)) → ADX(n__0) → ACTIVATE(n__adx(n__0)) → ADX(n__0)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__0)) → ADX(n__0)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__adx(
n__zeros)) →
ADX(
zeros) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros)) → ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros) → ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros)
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros)
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → 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 1 less node.
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__s(x0))) → ADX(s(x0))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
ACTIVATE(
n__adx(
n__s(
x0))) →
ADX(
s(
x0)) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__adx(n__s(x0))) → ADX(n__s(x0)) → ACTIVATE(n__adx(n__s(x0))) → ADX(n__s(x0))
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__s(x0))) → ADX(n__s(x0))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → 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.
ACTIVATE(n__incr(n__zeros)) → INCR(cons(n__0, n__zeros))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( adx(x1) ) = max{0, -2} |
POL( ACTIVATE(x1) ) = x1 + 2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
incr(X) → n__incr(X)
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
adx(X) → n__adx(X)
zeros → cons(n__0, n__zeros)
zeros → n__zeros
0 → n__0
s(X) → n__s(X)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(47) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = [4]x1
POL(ADX(x1)) = [2] + [2]x1
POL(INCR(x1)) = [2]x1
POL(activate(x1)) = x1
POL(adx(x1)) = [1/2] + x1
POL(cons(x1, x2)) = [4]x1 + [2]x2
POL(incr(x1)) = [1/2]x1
POL(n__0) = 0
POL(n__adx(x1)) = [1/2] + x1
POL(n__incr(x1)) = [1/2]x1
POL(n__s(x1)) = 0
POL(n__zeros) = 0
POL(s(x1)) = 0
POL(zeros) = 0
The value of delta used in the strict ordering is 1.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
incr(X) → n__incr(X)
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
adx(X) → n__adx(X)
zeros → cons(n__0, n__zeros)
zeros → n__zeros
0 → n__0
s(X) → n__s(X)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, Y)) → ACTIVATE(Y)
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(x0)) → INCR(x0)
ACTIVATE(n__adx(n__incr(x0))) → ADX(incr(activate(x0)))
ADX(cons(X, Y)) → INCR(cons(activate(X), n__adx(activate(Y))))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__adx(n__zeros)) → ADX(cons(n__0, n__zeros))
The TRS R consists of the following rules:
zeros → cons(n__0, n__zeros)
incr(cons(X, Y)) → cons(n__s(activate(X)), n__incr(activate(Y)))
adx(cons(X, Y)) → incr(cons(activate(X), n__adx(activate(Y))))
0 → n__0
zeros → n__zeros
s(X) → n__s(X)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
activate(n__0) → 0
activate(n__zeros) → zeros
activate(n__s(X)) → s(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(49) 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 =
ACTIVATE(
n__adx(
activate(
n__zeros))) evaluates to t =
ACTIVATE(
n__adx(
activate(
n__zeros)))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceACTIVATE(n__adx(activate(n__zeros))) →
ACTIVATE(
n__adx(
n__zeros))
with rule
activate(
X) →
X at position [0,0] and matcher [
X /
n__zeros]
ACTIVATE(n__adx(n__zeros)) →
ADX(
cons(
n__0,
n__zeros))
with rule
ACTIVATE(
n__adx(
n__zeros)) →
ADX(
cons(
n__0,
n__zeros)) at position [] and matcher [ ]
ADX(cons(n__0, n__zeros)) →
INCR(
cons(
activate(
n__0),
n__adx(
activate(
n__zeros))))
with rule
ADX(
cons(
X',
Y')) →
INCR(
cons(
activate(
X'),
n__adx(
activate(
Y')))) at position [] and matcher [
X' /
n__0,
Y' /
n__zeros]
INCR(cons(activate(n__0), n__adx(activate(n__zeros)))) →
ACTIVATE(
n__adx(
activate(
n__zeros)))
with rule
INCR(
cons(
X,
Y)) →
ACTIVATE(
Y)
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.
(50) NO