(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
nats → adx(zeros)
zeros → cons(0, n__zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → activate(L)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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·x1
POL(cons(x1, x2)) = x1 + x2
POL(head(x1)) = 2 + x1
POL(incr(x1)) = x1
POL(n__adx(x1)) = 2·x1
POL(n__incr(x1)) = x1
POL(n__zeros) = 0
POL(nats) = 2
POL(nil) = 0
POL(s(x1)) = x1
POL(tail(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:
nats → adx(zeros)
head(cons(X, L)) → X
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
tail(cons(X, L)) → activate(L)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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)) = x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(incr(x1)) = x1
POL(n__adx(x1)) = x1
POL(n__incr(x1)) = x1
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(tail(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:
tail(cons(X, L)) → activate(L)
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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·x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(incr(x1)) = x1
POL(n__adx(x1)) = 2·x1
POL(n__incr(x1)) = x1
POL(n__zeros) = 0
POL(nil) = 1
POL(s(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:
adx(nil) → nil
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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, L)) → ACTIVATE(L)
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
ADX(cons(X, L)) → ACTIVATE(L)
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)
ACTIVATE(n__zeros) → ZEROS
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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 1 less node.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
INCR(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
ADX(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__adx(X)) → ACTIVATE(X)
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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:
ADX(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__adx(X)) → ACTIVATE(X)
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)) = x1 + x2
POL(incr(x1)) = x1
POL(n__adx(x1)) = 2 + 2·x1
POL(n__incr(x1)) = x1
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(zeros) = 0
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
INCR(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__incr(X)) → ACTIVATE(X)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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.
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 + 2 |
POL( cons(x1, x2) ) = max{0, x2 - 2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
adx(X) → n__adx(X)
incr(nil) → nil
incr(X) → n__incr(X)
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
zeros → n__zeros
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVATE(n__incr(X)) → INCR(activate(X))
INCR(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) 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__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(n__zeros)) → INCR(zeros) → ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(x0)) → INCR(x0) → ACTIVATE(n__incr(x0)) → INCR(x0)
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
ACTIVATE(n__adx(X)) → ADX(activate(X))
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(x0)) → INCR(x0)
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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__adx(
X)) →
ADX(
activate(
X)) at position [0] we obtained the following new rules [LPAR04]:
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(n__zeros)) → ADX(zeros) → ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(x0)) → ADX(x0) → ACTIVATE(n__adx(x0)) → ADX(x0)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__incr(n__incr(x0))) → INCR(incr(activate(x0)))
ACTIVATE(n__incr(n__adx(x0))) → INCR(adx(activate(x0)))
ACTIVATE(n__incr(n__zeros)) → INCR(zeros)
ACTIVATE(n__incr(x0)) → INCR(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__zeros)) → ADX(zeros)
ACTIVATE(n__adx(x0)) → ADX(x0)
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
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__incr(
n__zeros)) →
INCR(
zeros) at position [0] we obtained the following new rules [LPAR04]:
ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros)) → ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros))
ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros) → ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
ADX(cons(X, L)) → INCR(cons(X, n__adx(activate(L))))
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)))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros))
ACTIVATE(n__incr(n__zeros)) → INCR(n__zeros)
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(22) 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, L)) → ACTIVATE(L)
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, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(n__zeros)) → ADX(zeros)
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) 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(0, n__zeros)) → ACTIVATE(n__adx(n__zeros)) → ADX(cons(0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros) → ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros)
(24) 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, L)) → ACTIVATE(L)
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, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(n__zeros)
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
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, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__incr(n__zeros)) → INCR(cons(0, n__zeros))
ACTIVATE(n__adx(n__zeros)) → ADX(cons(0, n__zeros))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) 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(0, n__zeros))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( n__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__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
incr(X) → n__incr(X)
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
adx(X) → n__adx(X)
zeros → cons(0, n__zeros)
zeros → n__zeros
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
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, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__adx(n__adx(x0))) → ADX(adx(activate(x0)))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__adx(n__zeros)) → ADX(cons(0, n__zeros))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) 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) = [1/4]
POL(ACTIVATE(x1)) = [2] + [4]x1
POL(ADX(x1)) = [4] + x1
POL(INCR(x1)) = [2] + [2]x1
POL(activate(x1)) = x1
POL(adx(x1)) = [1/2] + [1/2]x1
POL(cons(x1, x2)) = [2]x2
POL(incr(x1)) = [1/2]x1
POL(n__adx(x1)) = [1/2] + [1/2]x1
POL(n__incr(x1)) = [1/2]x1
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = [4]
POL(zeros) = 0
The value of delta used in the strict ordering is 1/2.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
incr(X) → n__incr(X)
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
adx(X) → n__adx(X)
zeros → cons(0, n__zeros)
zeros → n__zeros
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INCR(cons(X, L)) → ACTIVATE(L)
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, L)) → INCR(cons(X, n__adx(activate(L))))
ACTIVATE(n__adx(x0)) → ADX(x0)
ACTIVATE(n__adx(n__zeros)) → ADX(cons(0, n__zeros))
The TRS R consists of the following rules:
incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
zeros → cons(0, n__zeros)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) 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(
0,
n__zeros))
with rule
ACTIVATE(
n__adx(
n__zeros)) →
ADX(
cons(
0,
n__zeros)) at position [] and matcher [ ]
ADX(cons(0, n__zeros)) →
INCR(
cons(
0,
n__adx(
activate(
n__zeros))))
with rule
ADX(
cons(
X',
L')) →
INCR(
cons(
X',
n__adx(
activate(
L')))) at position [] and matcher [
X' /
0,
L' /
n__zeros]
INCR(cons(0, n__adx(activate(n__zeros)))) →
ACTIVATE(
n__adx(
activate(
n__zeros)))
with rule
INCR(
cons(
X,
L)) →
ACTIVATE(
L)
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.
(32) NO