The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, 1).

0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 16 ms)
↳2 CpxTRS
↳3 RcToIrcProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTRS
↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(n__add(sqr(activate(X)), dbl(activate(X))))
dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(0, X) → X
add(s(X), Y) → s(n__add(activate(X), Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))
terms(X) → n__terms(X)
add(X1, X2) → n__add(X1, X2)
s(X) → n__s(X)
dbl(X) → n__dbl(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(X)
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__s(X)) → s(X)
activate(n__dbl(X)) → dbl(X)
activate(n__first(X1, X2)) → first(X1, X2)
activate(X) → X

Rewrite Strategy: FULL

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
sqr(s(X)) → s(n__add(sqr(activate(X)), dbl(activate(X))))
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(s(X), Y) → s(n__add(activate(X), Y))
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))

(2) Obligation:

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

dbl(0) → 0
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
first(0, X) → nil
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__dbl(X)) → dbl(X)
activate(X) → X
add(X1, X2) → n__add(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__terms(X)) → terms(X)
sqr(0) → 0
add(0, X) → X
first(X1, X2) → n__first(X1, X2)
dbl(X) → n__dbl(X)
s(X) → n__s(X)
activate(n__s(X)) → s(X)

Rewrite Strategy: FULL

(3) RcToIrcProof (BOTH BOUNDS(ID, ID) transformation)

Converted rc-obligation to irc-obligation.

As the TRS does not nest defined symbols, we have rc = irc.

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

dbl(0) → 0
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
first(0, X) → nil
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__dbl(X)) → dbl(X)
activate(X) → X
add(X1, X2) → n__add(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__terms(X)) → terms(X)
sqr(0) → 0
add(0, X) → X
first(X1, X2) → n__first(X1, X2)
dbl(X) → n__dbl(X)
s(X) → n__s(X)
activate(n__s(X)) → s(X)

Rewrite Strategy: INNERMOST

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

dbl(0) → 0
dbl(z0) → n__dbl(z0)
terms(z0) → n__terms(z0)
terms(z0) → cons(recip(sqr(z0)), n__terms(s(z0)))
first(0, z0) → nil
first(z0, z1) → n__first(z0, z1)
activate(n__add(z0, z1)) → add(z0, z1)
activate(n__dbl(z0)) → dbl(z0)
activate(z0) → z0
activate(n__first(z0, z1)) → first(z0, z1)
activate(n__terms(z0)) → terms(z0)
activate(n__s(z0)) → s(z0)
add(z0, z1) → n__add(z0, z1)
add(0, z0) → z0
sqr(0) → 0
s(z0) → n__s(z0)
Tuples:

DBL(0) → c
DBL(z0) → c1
TERMS(z0) → c2
TERMS(z0) → c3(SQR(z0), S(z0))
FIRST(0, z0) → c4
FIRST(z0, z1) → c5
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
ACTIVATE(n__s(z0)) → c11(S(z0))
ADD(z0, z1) → c12
ADD(0, z0) → c13
SQR(0) → c14
S(z0) → c15
S tuples:

DBL(0) → c
DBL(z0) → c1
TERMS(z0) → c2
TERMS(z0) → c3(SQR(z0), S(z0))
FIRST(0, z0) → c4
FIRST(z0, z1) → c5
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
ACTIVATE(n__s(z0)) → c11(S(z0))
ADD(z0, z1) → c12
ADD(0, z0) → c13
SQR(0) → c14
S(z0) → c15
K tuples:none
Defined Rule Symbols:

dbl, terms, first, activate, add, sqr, s

Defined Pair Symbols:

DBL, TERMS, FIRST, ACTIVATE, ADD, SQR, S

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 16 trailing nodes:

ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
DBL(0) → c
SQR(0) → c14
ACTIVATE(z0) → c8
FIRST(z0, z1) → c5
FIRST(0, z0) → c4
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
TERMS(z0) → c3(SQR(z0), S(z0))
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
ADD(0, z0) → c13
S(z0) → c15
DBL(z0) → c1
ACTIVATE(n__s(z0)) → c11(S(z0))
ADD(z0, z1) → c12
TERMS(z0) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

dbl(0) → 0
dbl(z0) → n__dbl(z0)
terms(z0) → n__terms(z0)
terms(z0) → cons(recip(sqr(z0)), n__terms(s(z0)))
first(0, z0) → nil
first(z0, z1) → n__first(z0, z1)
activate(n__add(z0, z1)) → add(z0, z1)
activate(n__dbl(z0)) → dbl(z0)
activate(z0) → z0
activate(n__first(z0, z1)) → first(z0, z1)
activate(n__terms(z0)) → terms(z0)
activate(n__s(z0)) → s(z0)
add(z0, z1) → n__add(z0, z1)
add(0, z0) → z0
sqr(0) → 0
s(z0) → n__s(z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

dbl, terms, first, activate, add, sqr, s

Defined Pair Symbols:none

Compound Symbols:none

(9) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(10) BOUNDS(1, 1)