MAYBE 178.57/154.77 MAYBE 178.57/154.80 178.57/154.80 178.57/154.80 178.57/154.80 178.57/154.80 178.57/154.80 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 178.57/154.80 178.57/154.80 178.57/154.80
178.57/154.80
178.57/154.80
178.57/154.80
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
178.57/154.80 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳2 CdtProblem
178.57/154.80 
↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳4 CdtProblem
178.57/154.80 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
178.57/154.80 
↳6 CdtProblem
178.57/154.80 
↳7 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳8 CdtProblem
178.57/154.80 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
178.57/154.80 
↳10 CdtProblem
178.57/154.80 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
178.57/154.80 
↳12 CdtProblem
178.57/154.80 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
178.57/154.80 
↳14 CdtProblem
178.57/154.80 
↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳16 CdtProblem
178.57/154.80 
↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳18 CdtProblem
178.57/154.80 
↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳20 CdtProblem
178.57/154.80 
↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳22 CdtProblem
178.57/154.80 
↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳24 CdtProblem
178.57/154.80 
↳25 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳26 CdtProblem
178.57/154.80 
↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳28 CdtProblem
178.57/154.80 
↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳30 CdtProblem
178.57/154.80 
↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳32 CdtProblem
178.57/154.80 
↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳34 CdtProblem
178.57/154.80 
↳35 CdtRewritingProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳36 CdtProblem
178.57/154.80 
↳37 CdtLeafRemovalProof (ComplexityIfPolyImplication)
178.57/154.80 
↳38 CdtProblem
178.57/154.80 
↳39 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳40 CdtProblem
178.57/154.80 
↳41 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳42 CdtProblem
178.57/154.80 
↳43 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳44 CdtProblem
178.57/154.80 
↳45 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳46 CdtProblem
178.57/154.80 
↳47 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳48 CdtProblem
178.57/154.80 
↳49 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳50 CdtProblem
178.57/154.80 
↳51 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳52 CdtProblem
178.57/154.80 
↳53 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳54 CdtProblem
178.57/154.80 
↳55 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
178.57/154.80 
↳56 CdtProblem
178.57/154.80
178.57/154.80 178.57/154.80
178.57/154.80
178.57/154.80

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

fib(N) → sel(N, fib1(s(0), s(0))) 178.57/154.80
fib1(X, Y) → cons(X, n__fib1(Y, add(X, Y))) 178.57/154.80
add(0, X) → X 178.57/154.80
add(s(X), Y) → s(add(X, Y)) 178.57/154.80
sel(0, cons(X, XS)) → X 178.57/154.80
sel(s(N), cons(X, XS)) → sel(N, activate(XS)) 178.57/154.80
fib1(X1, X2) → n__fib1(X1, X2) 178.57/154.80
activate(n__fib1(X1, X2)) → fib1(X1, X2) 178.57/154.80
activate(X) → X

Rewrite Strategy: INNERMOST
178.57/154.80
178.57/154.80

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

Converted CpxTRS to CDT
178.57/154.80
178.57/154.80

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.57/154.80
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.57/154.80
fib1(z0, z1) → n__fib1(z0, z1) 178.57/154.80
add(0, z0) → z0 178.57/154.80
add(s(z0), z1) → s(add(z0, z1)) 178.57/154.80
sel(0, cons(z0, z1)) → z0 178.57/154.80
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.57/154.80
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.57/154.80
activate(z0) → z0
Tuples:

FIB(z0) → c(SEL(z0, fib1(s(0), s(0))), FIB1(s(0), s(0))) 178.57/154.80
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.57/154.80
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.57/154.80
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.57/154.80
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
S tuples:

FIB(z0) → c(SEL(z0, fib1(s(0), s(0))), FIB1(s(0), s(0))) 178.57/154.80
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.57/154.80
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.57/154.80
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.57/154.80
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
K tuples:none
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB, FIB1, ADD, SEL, ACTIVATE

Compound Symbols:

c, c1, c4, c6, c7

178.57/154.80
178.57/154.80

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

Split RHS of tuples not part of any SCC
178.57/154.80
178.57/154.80

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.57/154.80
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.57/154.80
fib1(z0, z1) → n__fib1(z0, z1) 178.57/154.80
add(0, z0) → z0 178.57/154.80
add(s(z0), z1) → s(add(z0, z1)) 178.57/154.80
sel(0, cons(z0, z1)) → z0 178.57/154.80
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.57/154.80
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.57/154.80
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.57/154.80
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.57/154.80
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.57/154.80
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.57/154.80
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.57/154.80
FIB(z0) → c2(FIB1(s(0), s(0)))
S tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.57/154.80
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.57/154.80
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.57/154.80
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.57/154.80
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.57/154.80
FIB(z0) → c2(FIB1(s(0), s(0)))
K tuples:none
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.57/154.80
178.57/154.80

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

FIB(z0) → c2(FIB1(s(0), s(0)))
178.57/154.80
178.57/154.80

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.57/154.80
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.57/154.80
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.82
add(0, z0) → z0 178.76/154.82
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.82
sel(0, cons(z0, z1)) → z0 178.76/154.82
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.82
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.82
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.82
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.82
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.82
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.82
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
S tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.82
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.82
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.82
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.82
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
K tuples:none
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.76/154.82
178.76/154.82

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

The following tuples could be moved from S to K by knowledge propagation:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
178.76/154.82
178.76/154.82

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.82
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.82
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.82
add(0, z0) → z0 178.76/154.82
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.82
sel(0, cons(z0, z1)) → z0 178.76/154.82
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.82
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
S tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.76/154.83
178.76/154.83

(9) 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.

FIB1(z0, z1) → c1(ADD(z0, z1))
We considered the (Usable) Rules:

fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
And the Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation : 178.76/154.83

POL(0) = 0    178.76/154.83
POL(ACTIVATE(x1)) = [1]    178.76/154.83
POL(ADD(x1, x2)) = 0    178.76/154.83
POL(FIB(x1)) = [4] + [3]x1    178.76/154.83
POL(FIB1(x1, x2)) = [1]    178.76/154.83
POL(SEL(x1, x2)) = x1    178.76/154.83
POL(activate(x1)) = 0    178.76/154.83
POL(add(x1, x2)) = [4] + [4]x1 + [4]x2    178.76/154.83
POL(c1(x1)) = x1    178.76/154.83
POL(c2(x1)) = x1    178.76/154.83
POL(c4(x1)) = x1    178.76/154.83
POL(c6(x1, x2)) = x1 + x2    178.76/154.83
POL(c7(x1)) = x1    178.76/154.83
POL(cons(x1, x2)) = x1    178.76/154.83
POL(fib1(x1, x2)) = 0    178.76/154.83
POL(n__fib1(x1, x2)) = 0    178.76/154.83
POL(s(x1)) = [1] + x1   
178.76/154.83
178.76/154.83

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.76/154.83
178.76/154.83

(11) 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.

ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
We considered the (Usable) Rules:

fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
And the Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation : 178.76/154.83

POL(0) = 0    178.76/154.83
POL(ACTIVATE(x1)) = [2]    178.76/154.83
POL(ADD(x1, x2)) = [1]    178.76/154.83
POL(FIB(x1)) = [4] + [3]x1    178.76/154.83
POL(FIB1(x1, x2)) = [1]    178.76/154.83
POL(SEL(x1, x2)) = x1    178.76/154.83
POL(activate(x1)) = 0    178.76/154.83
POL(add(x1, x2)) = [1] + [5]x2    178.76/154.83
POL(c1(x1)) = x1    178.76/154.83
POL(c2(x1)) = x1    178.76/154.83
POL(c4(x1)) = x1    178.76/154.83
POL(c6(x1, x2)) = x1 + x2    178.76/154.83
POL(c7(x1)) = x1    178.76/154.83
POL(cons(x1, x2)) = 0    178.76/154.83
POL(fib1(x1, x2)) = [2]    178.76/154.83
POL(n__fib1(x1, x2)) = 0    178.76/154.83
POL(s(x1)) = [2] + x1   
178.76/154.83
178.76/154.83

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.76/154.83
178.76/154.83

(13) 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)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
We considered the (Usable) Rules:

fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
And the Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation : 178.76/154.83

POL(0) = 0    178.76/154.83
POL(ACTIVATE(x1)) = [5]    178.76/154.83
POL(ADD(x1, x2)) = 0    178.76/154.83
POL(FIB(x1)) = [3] + [5]x1    178.76/154.83
POL(FIB1(x1, x2)) = [4]    178.76/154.83
POL(SEL(x1, x2)) = [4]x1    178.76/154.83
POL(activate(x1)) = 0    178.76/154.83
POL(add(x1, x2)) = [2]x1 + x2    178.76/154.83
POL(c1(x1)) = x1    178.76/154.83
POL(c2(x1)) = x1    178.76/154.83
POL(c4(x1)) = x1    178.76/154.83
POL(c6(x1, x2)) = x1 + x2    178.76/154.83
POL(c7(x1)) = x1    178.76/154.83
POL(cons(x1, x2)) = x1    178.76/154.83
POL(fib1(x1, x2)) = 0    178.76/154.83
POL(n__fib1(x1, x2)) = [1]    178.76/154.83
POL(s(x1)) = [4] + x1   
178.76/154.83
178.76/154.83

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, SEL, ACTIVATE, FIB

Compound Symbols:

c1, c4, c6, c7, c2

178.76/154.83
178.76/154.83

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2)) by

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0))
178.76/154.83
178.76/154.83

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, FIB, SEL

Compound Symbols:

c1, c4, c7, c2, c6

178.76/154.83
178.76/154.83

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) by

FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) 178.76/154.83
FIB(x0) → c2(SEL(x0, n__fib1(s(0), s(0))))
178.76/154.83
178.76/154.83

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) 178.76/154.83
FIB(x0) → c2(SEL(x0, n__fib1(s(0), s(0))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c2

178.76/154.83
178.76/154.83

(19) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
178.76/154.83
178.76/154.83

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) 178.76/154.83
FIB(x0) → c2
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB(z0) → c2(SEL(z0, fib1(s(0), s(0)))) 178.76/154.83
FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(z0), cons(z1, z2)) → c6(SEL(z0, activate(z2)), ACTIVATE(z2))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c2, c2

178.76/154.83
178.76/154.83

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

Removed 1 trailing nodes:

FIB(x0) → c2
178.76/154.83
178.76/154.83

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0))))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c2

178.76/154.83
178.76/154.83

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1))) by

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, n__fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1)))
178.76/154.83
178.76/154.83

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, n__fib1(z0, z1)), ACTIVATE(n__fib1(z0, z1)))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c2

178.76/154.83
178.76/154.83

(25) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
178.76/154.83
178.76/154.83

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1)))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c2, c6

178.76/154.83
178.76/154.83

(27) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), add(s(0), s(0)))))) by

FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0)))))))
178.76/154.83
178.76/154.83

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0)))))))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

FIB1(z0, z1) → c1(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

FIB1, ADD, ACTIVATE, SEL, FIB

Compound Symbols:

c1, c4, c7, c6, c6, c2

178.76/154.83
178.76/154.83

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace FIB1(z0, z1) → c1(ADD(z0, z1)) by

FIB1(s(y0), z1) → c1(ADD(s(y0), z1))
178.76/154.83
178.76/154.83

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1)) 178.76/154.83
ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0))))))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1))
S tuples:

ADD(s(z0), z1) → c4(ADD(z0, z1))
K tuples:

ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

ADD, ACTIVATE, SEL, FIB, FIB1

Compound Symbols:

c4, c7, c6, c6, c2, c1

178.76/154.83
178.76/154.83

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace ADD(s(z0), z1) → c4(ADD(z0, z1)) by

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
178.76/154.83
178.76/154.83

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0))))))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

ACTIVATE, SEL, FIB, FIB1, ADD

Compound Symbols:

c7, c6, c6, c2, c1, c4

178.76/154.83
178.76/154.83

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace ACTIVATE(n__fib1(z0, z1)) → c7(FIB1(z0, z1)) by

ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
178.76/154.83
178.76/154.83

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0))))))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c2, c1, c4, c7

178.76/154.83
178.76/154.83

(35) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace FIB(x0) → c2(SEL(x0, cons(s(0), n__fib1(s(0), s(add(0, s(0))))))) by FIB(z0) → c2(SEL(z0, cons(s(0), n__fib1(s(0), s(s(0))))))
178.76/154.83
178.76/154.83

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
FIB(z0) → c2(SEL(z0, cons(s(0), n__fib1(s(0), s(s(0))))))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE, FIB

Compound Symbols:

c6, c6, c1, c4, c7, c2

178.76/154.83
178.76/154.83

(37) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

FIB(z0) → c2(SEL(z0, cons(s(0), n__fib1(s(0), s(s(0))))))
178.76/154.83
178.76/154.83

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace SEL(s(x0), cons(x1, z0)) → c6(SEL(x0, z0), ACTIVATE(z0)) by

SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2)), ACTIVATE(cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3))), ACTIVATE(cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(SEL(z0, n__fib1(s(y0), y1)), ACTIVATE(n__fib1(s(y0), y1)))
178.76/154.83
178.76/154.83

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2)), ACTIVATE(cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3))), ACTIVATE(cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(SEL(z0, n__fib1(s(y0), y1)), ACTIVATE(n__fib1(s(y0), y1)))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(41) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing tuple parts
178.76/154.83
178.76/154.83

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1)))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(ACTIVATE(n__fib1(z0, z1))) by

SEL(s(z0), cons(z1, n__fib1(s(y0), z3))) → c6(ACTIVATE(n__fib1(s(y0), z3)))
178.76/154.83
178.76/154.83

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1)))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c1, c4, c7, c6

178.76/154.83
178.76/154.83

(45) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace FIB1(s(y0), z1) → c1(ADD(s(y0), z1)) by

FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1))
178.76/154.83
178.76/154.83

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1))
S tuples:

ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1))
K tuples:

ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, ADD, ACTIVATE, FIB1

Compound Symbols:

c6, c4, c7, c6, c1

178.76/154.83
178.76/154.83

(47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace ADD(s(s(y0)), z1) → c4(ADD(s(y0), z1)) by

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
178.76/154.83
178.76/154.83

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
S tuples:

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
K tuples:

ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, ACTIVATE, FIB1, ADD

Compound Symbols:

c6, c7, c6, c1, c4

178.76/154.83
178.76/154.83

(49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace ACTIVATE(n__fib1(s(y0), z1)) → c7(FIB1(s(y0), z1)) by

ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
178.76/154.83
178.76/154.83

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
S tuples:

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
K tuples:

FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace SEL(s(s(y0)), cons(z1, cons(y1, y2))) → c6(SEL(s(y0), cons(y1, y2))) by

SEL(s(s(z0)), cons(z1, cons(z2, n__fib1(y2, y3)))) → c6(SEL(s(z0), cons(z2, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__fib1(y3, y4))))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, n__fib1(y3, y4))))) 178.76/154.83
SEL(s(s(z0)), cons(z1, cons(z2, n__fib1(s(y2), y3)))) → c6(SEL(s(z0), cons(z2, n__fib1(s(y2), y3))))
178.76/154.83
178.76/154.83

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1)) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__fib1(y3, y4))))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, n__fib1(y3, y4))))) 178.76/154.83
SEL(s(s(z0)), cons(z1, cons(z2, n__fib1(s(y2), y3)))) → c6(SEL(s(z0), cons(z2, n__fib1(s(y2), y3))))
S tuples:

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
K tuples:

FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) by

SEL(s(z0), cons(z1, n__fib1(s(s(y0)), z3))) → c6(ACTIVATE(n__fib1(s(s(y0)), z3)))
178.76/154.83
178.76/154.83

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(y0), y1))) → c6(ACTIVATE(n__fib1(s(y0), y1))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1)) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__fib1(y3, y4))))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, n__fib1(y3, y4))))) 178.76/154.83
SEL(s(s(z0)), cons(z1, cons(z2, n__fib1(s(y2), y3)))) → c6(SEL(s(z0), cons(z2, n__fib1(s(y2), y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(s(y0)), z3))) → c6(ACTIVATE(n__fib1(s(s(y0)), z3)))
S tuples:

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
K tuples:

FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83

(55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace SEL(s(z0), cons(z1, n__fib1(s(y0), z3))) → c6(ACTIVATE(n__fib1(s(y0), z3))) by

SEL(s(z0), cons(z1, n__fib1(s(s(y0)), z3))) → c6(ACTIVATE(n__fib1(s(s(y0)), z3)))
178.76/154.83
178.76/154.83

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

fib(z0) → sel(z0, fib1(s(0), s(0))) 178.76/154.83
fib1(z0, z1) → cons(z0, n__fib1(z1, add(z0, z1))) 178.76/154.83
fib1(z0, z1) → n__fib1(z0, z1) 178.76/154.83
add(0, z0) → z0 178.76/154.83
add(s(z0), z1) → s(add(z0, z1)) 178.76/154.83
sel(0, cons(z0, z1)) → z0 178.76/154.83
sel(s(z0), cons(z1, z2)) → sel(z0, activate(z2)) 178.76/154.83
activate(n__fib1(z0, z1)) → fib1(z0, z1) 178.76/154.83
activate(z0) → z0
Tuples:

SEL(s(x0), cons(x1, n__fib1(z0, z1))) → c6(SEL(x0, cons(z0, n__fib1(z1, add(z0, z1)))), ACTIVATE(n__fib1(z0, z1))) 178.76/154.83
SEL(s(s(y0)), cons(z1, cons(y1, n__fib1(y2, y3)))) → c6(SEL(s(y0), cons(y1, n__fib1(y2, y3)))) 178.76/154.83
FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1)) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, y3)))) 178.76/154.83
SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, n__fib1(y3, y4))))) → c6(SEL(s(s(y0)), cons(z2, cons(y2, n__fib1(y3, y4))))) 178.76/154.83
SEL(s(s(z0)), cons(z1, cons(z2, n__fib1(s(y2), y3)))) → c6(SEL(s(z0), cons(z2, n__fib1(s(y2), y3)))) 178.76/154.83
SEL(s(z0), cons(z1, n__fib1(s(s(y0)), z3))) → c6(ACTIVATE(n__fib1(s(s(y0)), z3)))
S tuples:

ADD(s(s(s(y0))), z1) → c4(ADD(s(s(y0)), z1))
K tuples:

FIB1(s(s(y0)), z1) → c1(ADD(s(s(y0)), z1)) 178.76/154.83
ACTIVATE(n__fib1(s(s(y0)), z1)) → c7(FIB1(s(s(y0)), z1))
Defined Rule Symbols:

fib, fib1, add, sel, activate

Defined Pair Symbols:

SEL, FIB1, ADD, ACTIVATE

Compound Symbols:

c6, c6, c1, c4, c7

178.76/154.83
178.76/154.83
178.76/154.89 EOF