207.77/155.35
207.77/155.35
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(O(1), INFINITE).
0 CpxTRS
207.77/155.35
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳2 CdtProblem
207.77/155.35
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
207.77/155.35
↳4 CdtProblem
207.77/155.35
↳5 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳6 CdtProblem
207.77/155.35
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳8 CdtProblem
207.77/155.35
↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳10 CdtProblem
207.77/155.35
↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳12 CdtProblem
207.77/155.35
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳14 CdtProblem
207.77/155.35
↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳16 CdtProblem
207.77/155.35
↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳18 CdtProblem
207.77/155.35
↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳20 CdtProblem
207.77/155.35
↳21 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳22 CdtProblem
207.77/155.35
↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳24 CdtProblem
207.77/155.35
↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳26 CdtProblem
207.77/155.35
↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳28 CdtProblem
207.77/155.35
↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳30 CdtProblem
207.77/155.35
↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳32 CdtProblem
207.77/155.35
↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳34 CdtProblem
207.77/155.35
↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
207.77/155.35
↳36 CdtProblem
207.77/155.35
207.77/155.35
207.77/155.35
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(X) → cons(X, n__f(g(X)))
207.77/155.35
g(0) → s(0)
207.77/155.35
g(s(X)) → s(s(g(X)))
207.77/155.35
sel(0, cons(X, Y)) → X
207.77/155.35
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
207.77/155.35
f(X) → n__f(X)
207.77/155.35
activate(n__f(X)) → f(X)
207.77/155.35
activate(X) → X
Rewrite Strategy: INNERMOST
207.77/155.35
207.77/155.35
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
207.77/155.35
207.77/155.35
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.35
f(z0) → n__f(z0)
207.77/155.35
g(0) → s(0)
207.77/155.35
g(s(z0)) → s(s(g(z0)))
207.77/155.35
sel(0, cons(z0, z1)) → z0
207.77/155.35
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.35
activate(n__f(z0)) → f(z0)
207.77/155.35
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.35
G(s(z0)) → c3(G(z0))
207.77/155.35
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.35
ACTIVATE(n__f(z0)) → c6(F(z0))
S tuples:
F(z0) → c(G(z0))
207.77/155.35
G(s(z0)) → c3(G(z0))
207.77/155.35
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.35
ACTIVATE(n__f(z0)) → c6(F(z0))
K tuples:none
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, SEL, ACTIVATE
Compound Symbols:
c, c3, c5, c6
207.77/155.35
207.77/155.35
(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
We considered the (Usable) Rules:
activate(n__f(z0)) → f(z0)
207.77/155.35
activate(z0) → z0
207.77/155.35
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.35
f(z0) → n__f(z0)
207.77/155.35
g(0) → s(0)
207.77/155.35
g(s(z0)) → s(s(g(z0)))
And the Tuples:
F(z0) → c(G(z0))
207.77/155.35
G(s(z0)) → c3(G(z0))
207.77/155.35
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.35
ACTIVATE(n__f(z0)) → c6(F(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
207.77/155.35
POL(0) = [3]
207.77/155.35
POL(ACTIVATE(x1)) = 0
207.77/155.35
POL(F(x1)) = 0
207.77/155.35
POL(G(x1)) = 0
207.77/155.35
POL(SEL(x1, x2)) = [2]x1
207.77/155.35
POL(activate(x1)) = 0
207.77/155.35
POL(c(x1)) = x1
207.77/155.35
POL(c3(x1)) = x1
207.77/155.35
POL(c5(x1, x2)) = x1 + x2
207.77/155.35
POL(c6(x1)) = x1
207.77/155.35
POL(cons(x1, x2)) = x1
207.77/155.35
POL(f(x1)) = [3] + [3]x1
207.77/155.35
POL(g(x1)) = [1]
207.77/155.35
POL(n__f(x1)) = 0
207.77/155.35
POL(s(x1)) = [4] + x1
207.77/155.35
207.77/155.35
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
S tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, SEL, ACTIVATE
Compound Symbols:
c, c3, c5, c6
207.77/155.36
207.77/155.36
(5) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(z0) → c(G(z0))
207.77/155.36
207.77/155.36
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
S tuples:
G(s(z0)) → c3(G(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(z0) → c(G(z0))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, SEL, ACTIVATE
Compound Symbols:
c, c3, c5, c6
207.77/155.36
207.77/155.36
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
SEL(
s(
z0),
cons(
z1,
z2)) →
c5(
SEL(
z0,
activate(
z2)),
ACTIVATE(
z2)) by
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, f(z0)), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
207.77/155.36
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, f(z0)), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
S tuples:
G(s(z0)) → c3(G(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(z0) → c(G(z0))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, ACTIVATE, SEL
Compound Symbols:
c, c3, c6, c5
207.77/155.36
207.77/155.36
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
SEL(
s(
x0),
cons(
x1,
n__f(
z0))) →
c5(
SEL(
x0,
f(
z0)),
ACTIVATE(
n__f(
z0))) by
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, n__f(z0)), ACTIVATE(n__f(z0)))
207.77/155.36
207.77/155.36
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, n__f(z0)), ACTIVATE(n__f(z0)))
S tuples:
G(s(z0)) → c3(G(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(z0) → c(G(z0))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, ACTIVATE, SEL
Compound Symbols:
c, c3, c6, c5
207.77/155.36
207.77/155.36
(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
207.77/155.36
207.77/155.36
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
F(z0) → c(G(z0))
207.77/155.36
G(s(z0)) → c3(G(z0))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
S tuples:
G(s(z0)) → c3(G(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(z0) → c(G(z0))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
F, G, ACTIVATE, SEL
Compound Symbols:
c, c3, c6, c5, c5
207.77/155.36
207.77/155.36
(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
z0) →
c(
G(
z0)) by
F(s(y0)) → c(G(s(y0)))
207.77/155.36
207.77/155.36
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
G(s(z0)) → c3(G(z0))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
S tuples:
G(s(z0)) → c3(G(z0))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
G, ACTIVATE, SEL, F
Compound Symbols:
c3, c6, c5, c5, c
207.77/155.36
207.77/155.36
(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
G(
s(
z0)) →
c3(
G(
z0)) by
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
207.77/155.36
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(z0)) → c6(F(z0))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
ACTIVATE, SEL, F, G
Compound Symbols:
c6, c5, c5, c, c3
207.77/155.36
207.77/155.36
(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
ACTIVATE(
n__f(
z0)) →
c6(
F(
z0)) by
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
207.77/155.36
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, z0)) → c5(SEL(x0, z0), ACTIVATE(z0))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
SEL(
s(
x0),
cons(
x1,
z0)) →
c5(
SEL(
x0,
z0),
ACTIVATE(
z0)) by
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)), ACTIVATE(cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))), ACTIVATE(cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(SEL(z0, n__f(s(y0))), ACTIVATE(n__f(s(y0))))
207.77/155.36
207.77/155.36
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)), ACTIVATE(cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))), ACTIVATE(cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(SEL(z0, n__f(s(y0))), ACTIVATE(n__f(s(y0))))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
207.77/155.36
207.77/155.36
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(x0), cons(x1, n__f(z0))) → c5(ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
SEL(
s(
x0),
cons(
x1,
n__f(
z0))) →
c5(
ACTIVATE(
n__f(
z0))) by
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
207.77/155.36
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(y0)) → c(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c, c3, c6, c5
207.77/155.36
207.77/155.36
(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
y0)) →
c(
G(
s(
y0))) by
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
207.77/155.36
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
G(s(s(y0))) → c3(G(s(y0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
S tuples:
G(s(s(y0))) → c3(G(s(y0)))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, G, ACTIVATE, F
Compound Symbols:
c5, c3, c6, c5, c
207.77/155.36
207.77/155.36
(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
G(
s(
s(
y0))) →
c3(
G(
s(
y0))) by
G(s(s(s(y0)))) → c3(G(s(s(y0))))
207.77/155.36
207.77/155.36
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
G(s(s(s(y0)))) → c3(G(s(s(y0))))
S tuples:
G(s(s(s(y0)))) → c3(G(s(s(y0))))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
ACTIVATE(n__f(s(y0))) → c6(F(s(y0)))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, ACTIVATE, F, G
Compound Symbols:
c5, c6, c5, c, c3
207.77/155.36
207.77/155.36
(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
ACTIVATE(
n__f(
s(
y0))) →
c6(
F(
s(
y0))) by
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
207.77/155.36
207.77/155.36
(30) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c5(SEL(s(y0), cons(y1, y2)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
G(s(s(s(y0)))) → c3(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
S tuples:
G(s(s(s(y0)))) → c3(G(s(s(y0))))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
SEL(
s(
s(
y0)),
cons(
z1,
cons(
y1,
y2))) →
c5(
SEL(
s(
y0),
cons(
y1,
y2))) by
SEL(s(s(z0)), cons(z1, cons(z2, n__f(y2)))) → c5(SEL(s(z0), cons(z2, n__f(y2))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__f(y3))))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, n__f(y3)))))
207.77/155.36
SEL(s(s(z0)), cons(z1, cons(z2, n__f(s(y2))))) → c5(SEL(s(z0), cons(z2, n__f(s(y2)))))
207.77/155.36
207.77/155.36
(32) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
G(s(s(s(y0)))) → c3(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__f(y3))))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, n__f(y3)))))
207.77/155.36
SEL(s(s(z0)), cons(z1, cons(z2, n__f(s(y2))))) → c5(SEL(s(z0), cons(z2, n__f(s(y2)))))
S tuples:
G(s(s(s(y0)))) → c3(G(s(s(y0))))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
SEL(
s(
z0),
cons(
z1,
n__f(
s(
y0)))) →
c5(
ACTIVATE(
n__f(
s(
y0)))) by
SEL(s(z0), cons(z1, n__f(s(s(y0))))) → c5(ACTIVATE(n__f(s(s(y0)))))
207.77/155.36
207.77/155.36
(34) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(y0)))) → c5(ACTIVATE(n__f(s(y0))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
G(s(s(s(y0)))) → c3(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__f(y3))))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, n__f(y3)))))
207.77/155.36
SEL(s(s(z0)), cons(z1, cons(z2, n__f(s(y2))))) → c5(SEL(s(z0), cons(z2, n__f(s(y2)))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(s(y0))))) → c5(ACTIVATE(n__f(s(s(y0)))))
S tuples:
G(s(s(s(y0)))) → c3(G(s(s(y0))))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36
207.77/155.36
(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
SEL(
s(
z0),
cons(
z1,
n__f(
s(
y0)))) →
c5(
ACTIVATE(
n__f(
s(
y0)))) by
SEL(s(z0), cons(z1, n__f(s(s(y0))))) → c5(ACTIVATE(n__f(s(s(y0)))))
207.77/155.36
207.77/155.36
(36) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → cons(z0, n__f(g(z0)))
207.77/155.36
f(z0) → n__f(z0)
207.77/155.36
g(0) → s(0)
207.77/155.36
g(s(z0)) → s(s(g(z0)))
207.77/155.36
sel(0, cons(z0, z1)) → z0
207.77/155.36
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2))
207.77/155.36
activate(n__f(z0)) → f(z0)
207.77/155.36
activate(z0) → z0
Tuples:
SEL(s(x0), cons(x1, n__f(z0))) → c5(SEL(x0, cons(z0, n__f(g(z0)))), ACTIVATE(n__f(z0)))
207.77/155.36
SEL(s(s(y0)), cons(z1, cons(y1, n__f(y2)))) → c5(SEL(s(y0), cons(y1, n__f(y2))))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
G(s(s(s(y0)))) → c3(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
207.77/155.36
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__f(y3))))) → c5(SEL(s(s(y0)), cons(z2, cons(y2, n__f(y3)))))
207.77/155.36
SEL(s(s(z0)), cons(z1, cons(z2, n__f(s(y2))))) → c5(SEL(s(z0), cons(z2, n__f(s(y2)))))
207.77/155.36
SEL(s(z0), cons(z1, n__f(s(s(y0))))) → c5(ACTIVATE(n__f(s(s(y0)))))
S tuples:
G(s(s(s(y0)))) → c3(G(s(s(y0))))
K tuples:
SEL(s(z0), cons(z1, z2)) → c5(SEL(z0, activate(z2)), ACTIVATE(z2))
207.77/155.36
F(s(s(y0))) → c(G(s(s(y0))))
207.77/155.36
ACTIVATE(n__f(s(s(y0)))) → c6(F(s(s(y0))))
Defined Rule Symbols:
f, g, sel, activate
Defined Pair Symbols:
SEL, F, G, ACTIVATE
Compound Symbols:
c5, c5, c, c3, c6
207.77/155.36