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

0 CpxTRS
169.35/137.68 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳2 CdtProblem
169.35/137.68 
↳3 CdtUnreachableProof (⇔)
169.35/137.68 
↳4 CdtProblem
169.35/137.68 
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳6 CdtProblem
169.35/137.68 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
169.35/137.68 
↳8 CdtProblem
169.35/137.68 
↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳10 CdtProblem
169.35/137.68 
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳12 CdtProblem
169.35/137.68 
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳14 CdtProblem
169.35/137.68 
↳15 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳16 CdtProblem
169.35/137.68 
↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳18 CdtProblem
169.35/137.68 
↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳20 CdtProblem
169.35/137.68 
↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳22 CdtProblem
169.35/137.68 
↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳24 CdtProblem
169.35/137.68 
↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳26 CdtProblem
169.35/137.68 
↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳28 CdtProblem
169.35/137.68 
↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳30 CdtProblem
169.35/137.68 
↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳32 CdtProblem
169.35/137.68 
↳33 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳34 CdtProblem
169.35/137.68 
↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳36 CdtProblem
169.35/137.68 
↳37 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳38 CdtProblem
169.35/137.68 
↳39 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳40 CdtProblem
169.35/137.68 
↳41 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳42 CdtProblem
169.35/137.68 
↳43 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳44 CdtProblem
169.35/137.68 
↳45 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳46 CdtProblem
169.35/137.68 
↳47 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳48 CdtProblem
169.35/137.68 
↳49 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳50 CdtProblem
169.35/137.68 
↳51 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳52 CdtProblem
169.35/137.68 
↳53 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳54 CdtProblem
169.35/137.68 
↳55 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳56 CdtProblem
169.35/137.68 
↳57 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳58 CdtProblem
169.35/137.68 
↳59 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳60 CdtProblem
169.35/137.68 
↳61 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
169.35/137.68 
↳62 CdtProblem
169.35/137.68
169.35/137.68 169.35/137.68
169.35/137.68
169.35/137.68

(0) Obligation:

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

and(true, X) → activate(X) 169.35/137.68
and(false, Y) → false 169.35/137.68
if(true, X, Y) → activate(X) 169.35/137.68
if(false, X, Y) → activate(Y) 169.35/137.68
add(0, X) → activate(X) 169.35/137.68
add(s(X), Y) → s(n__add(activate(X), activate(Y))) 169.35/137.68
first(0, X) → nil 169.35/137.68
first(s(X), cons(Y, Z)) → cons(activate(Y), n__first(activate(X), activate(Z))) 169.35/137.68
from(X) → cons(activate(X), n__from(n__s(activate(X)))) 169.35/137.68
add(X1, X2) → n__add(X1, X2) 169.35/137.68
first(X1, X2) → n__first(X1, X2) 169.35/137.68
from(X) → n__from(X) 169.35/137.68
s(X) → n__s(X) 169.35/137.68
activate(n__add(X1, X2)) → add(X1, X2) 169.35/137.68
activate(n__first(X1, X2)) → first(X1, X2) 169.35/137.68
activate(n__from(X)) → from(X) 169.35/137.68
activate(n__s(X)) → s(X) 169.35/137.68
activate(X) → X

Rewrite Strategy: INNERMOST
169.35/137.68
169.35/137.68

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

Converted CpxTRS to CDT
169.35/137.68
169.35/137.68

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
ADD(s(z0), z1) → c5(S(n__add(activate(z0), activate(z1))), ACTIVATE(z0), ACTIVATE(z1)) 169.35/137.68
FIRST(s(z0), cons(z1, z2)) → c8(ACTIVATE(z1), ACTIVATE(z0), ACTIVATE(z2)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14(FIRST(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__s(z0)) → c16(S(z0))
S tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
ADD(s(z0), z1) → c5(S(n__add(activate(z0), activate(z1))), ACTIVATE(z0), ACTIVATE(z1)) 169.35/137.68
FIRST(s(z0), cons(z1, z2)) → c8(ACTIVATE(z1), ACTIVATE(z0), ACTIVATE(z2)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14(FIRST(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__s(z0)) → c16(S(z0))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

AND, IF, ADD, FIRST, FROM, ACTIVATE

Compound Symbols:

c, c2, c3, c4, c5, c8, c10, c13, c14, c15, c16

169.35/137.68
169.35/137.68

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

ADD(s(z0), z1) → c5(S(n__add(activate(z0), activate(z1))), ACTIVATE(z0), ACTIVATE(z1)) 169.35/137.68
FIRST(s(z0), cons(z1, z2)) → c8(ACTIVATE(z1), ACTIVATE(z0), ACTIVATE(z2))
169.35/137.68
169.35/137.68

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14(FIRST(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__s(z0)) → c16(S(z0))
S tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14(FIRST(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__s(z0)) → c16(S(z0))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

AND, IF, ADD, FROM, ACTIVATE

Compound Symbols:

c, c2, c3, c4, c10, c13, c14, c15, c16

169.35/137.68
169.35/137.68

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

Removed 2 trailing tuple parts
169.35/137.68
169.35/137.68

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16
S tuples:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1)) 169.35/137.68
ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

AND, IF, ADD, FROM, ACTIVATE

Compound Symbols:

c, c2, c3, c4, c10, c13, c15, c14, c16

169.35/137.68
169.35/137.68

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 3 leading nodes:

AND(true, z0) → c(ACTIVATE(z0)) 169.35/137.68
IF(true, z0, z1) → c2(ACTIVATE(z0)) 169.35/137.68
IF(false, z0, z1) → c3(ACTIVATE(z1))
Removed 2 trailing nodes:

ACTIVATE(n__s(z0)) → c16 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14
169.35/137.68
169.35/137.68

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16
S tuples:

ADD(0, z0) → c4(ACTIVATE(z0)) 169.35/137.68
FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ADD, FROM, ACTIVATE

Compound Symbols:

c4, c10, c13, c15, c14, c16

169.35/137.68
169.35/137.68

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

Use forward instantiation to replace ADD(0, z0) → c4(ACTIVATE(z0)) by

ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
169.35/137.68
169.35/137.68

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
S tuples:

FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

FROM, ACTIVATE, ADD

Compound Symbols:

c10, c13, c15, c14, c16, c4

169.35/137.68
169.35/137.68

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

Removed 4 trailing nodes:

ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
169.35/137.68
169.35/137.68

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
S tuples:

FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) 169.35/137.68
ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

FROM, ACTIVATE, ADD

Compound Symbols:

c10, c13, c15, c14, c16, c4

169.35/137.68
169.35/137.68

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

Use forward instantiation to replace FROM(z0) → c10(ACTIVATE(z0), ACTIVATE(z0)) by

FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c10(ACTIVATE(n__first(y0, y1)), ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c10(ACTIVATE(n__s(y0)), ACTIVATE(n__s(y0)))
169.35/137.68
169.35/137.68

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c10(ACTIVATE(n__first(y0, y1)), ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c10(ACTIVATE(n__s(y0)), ACTIVATE(n__s(y0)))
S tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c10(ACTIVATE(n__first(y0, y1)), ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c10(ACTIVATE(n__s(y0)), ACTIVATE(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c13, c15, c14, c16, c4, c10

169.35/137.68
169.35/137.68

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

Split RHS of tuples not part of any SCC
169.35/137.68
169.35/137.68

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0)))
S tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c13, c15, c14, c16, c4, c10, c

169.35/137.68
169.35/137.68

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

Removed 6 trailing nodes:

FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1)))
169.35/137.68
169.35/137.68

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0)))
S tuples:

ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) 169.35/137.68
ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c13, c15, c14, c16, c4, c10, c

169.35/137.68
169.35/137.68

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

Use forward instantiation to replace ACTIVATE(n__add(z0, z1)) → c13(ADD(z0, z1)) by

ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
169.35/137.68
169.35/137.68

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
S tuples:

ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c15, c14, c16, c4, c10, c, c13

169.35/137.68
169.35/137.68

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

Removed 8 trailing nodes:

FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
169.35/137.68
169.35/137.68

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
S tuples:

ACTIVATE(n__from(z0)) → c15(FROM(z0)) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c15, c14, c16, c4, c10, c, c13

169.35/137.68
169.35/137.68

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

Use forward instantiation to replace ACTIVATE(n__from(z0)) → c15(FROM(z0)) by

ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0)))
169.35/137.68
169.35/137.68

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0)))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.68
169.35/137.68

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

Removed 10 trailing nodes:

FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
169.35/137.68
169.35/137.68

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0)))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0)))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.68
169.35/137.68

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

Use forward instantiation to replace ADD(0, n__add(y0, y1)) → c4(ACTIVATE(n__add(y0, y1))) by

ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.68
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
169.35/137.68
169.35/137.68

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.68
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.68
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.68
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.68
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.68
169.35/137.68

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

Removed 12 trailing nodes:

FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.68
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0)))
169.35/137.68
169.35/137.68

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.68
and(false, z0) → false 169.35/137.68
if(true, z0, z1) → activate(z0) 169.35/137.68
if(false, z0, z1) → activate(z1) 169.35/137.68
add(0, z0) → activate(z0) 169.35/137.68
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.68
add(z0, z1) → n__add(z0, z1) 169.35/137.68
first(0, z0) → nil 169.35/137.68
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.68
first(z0, z1) → n__first(z0, z1) 169.35/137.68
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.68
from(z0) → n__from(z0) 169.35/137.68
s(z0) → n__s(z0) 169.35/137.68
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.68
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.68
activate(n__from(z0)) → from(z0) 169.35/137.68
activate(n__s(z0)) → s(z0) 169.35/137.68
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.68
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.68
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.68
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.68
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.68
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.68
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.68
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.68
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.68
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.68
ACTIVATE(n__s(z0)) → c16 169.35/137.68
ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) 169.35/137.68
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.68
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.68
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.68
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace ADD(0, n__from(y0)) → c4(ACTIVATE(n__from(y0))) by

ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0))))
169.35/137.69
169.35/137.69

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.69
169.35/137.69

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

Removed 14 trailing nodes:

ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace FROM(n__add(y0, y1)) → c10(ACTIVATE(n__add(y0, y1)), ACTIVATE(n__add(y0, y1))) by

FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c10(ACTIVATE(n__add(0, n__first(y0, y1))), ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c10(ACTIVATE(n__add(0, n__s(y0))), ACTIVATE(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c10(ACTIVATE(n__add(0, n__first(y0, y1))), ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c10(ACTIVATE(n__add(0, n__s(y0))), ACTIVATE(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c10(ACTIVATE(n__add(0, n__first(y0, y1))), ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c10(ACTIVATE(n__add(0, n__s(y0))), ACTIVATE(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15

169.35/137.69
169.35/137.69

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

Split RHS of tuples not part of any SCC
169.35/137.69
169.35/137.69

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15, c1

169.35/137.69
169.35/137.69

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

Removed 16 trailing nodes:

ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c10, c, c13, c15, c1

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace FROM(n__from(y0)) → c10(ACTIVATE(n__from(y0)), ACTIVATE(n__from(y0))) by

FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c10(ACTIVATE(n__from(n__first(y0, y1))), ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c10(ACTIVATE(n__from(n__s(y0))), ACTIVATE(n__from(n__s(y0))))
169.35/137.69
169.35/137.69

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c10(ACTIVATE(n__from(n__first(y0, y1))), ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c10(ACTIVATE(n__from(n__s(y0))), ACTIVATE(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c10(ACTIVATE(n__from(n__first(y0, y1))), ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c10(ACTIVATE(n__from(n__s(y0))), ACTIVATE(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1

169.35/137.69
169.35/137.69

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

Split RHS of tuples not part of any SCC
169.35/137.69
169.35/137.69

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Removed 18 trailing nodes:

ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace ACTIVATE(n__add(0, n__add(y0, y1))) → c13(ADD(0, n__add(y0, y1))) by

ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Removed 20 trailing nodes:

ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace ACTIVATE(n__add(0, n__from(y0))) → c13(ADD(0, n__from(y0))) by

ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
169.35/137.69
169.35/137.69

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Removed 22 trailing nodes:

ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
169.35/137.69
169.35/137.69

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Use forward instantiation to replace ACTIVATE(n__from(n__add(y0, y1))) → c15(FROM(n__add(y0, y1))) by

ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0))))
169.35/137.69
169.35/137.69

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.69
and(false, z0) → false 169.35/137.69
if(true, z0, z1) → activate(z0) 169.35/137.69
if(false, z0, z1) → activate(z1) 169.35/137.69
add(0, z0) → activate(z0) 169.35/137.69
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.69
add(z0, z1) → n__add(z0, z1) 169.35/137.69
first(0, z0) → nil 169.35/137.69
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.69
first(z0, z1) → n__first(z0, z1) 169.35/137.69
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.69
from(z0) → n__from(z0) 169.35/137.69
s(z0) → n__s(z0) 169.35/137.69
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.69
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.69
activate(n__from(z0)) → from(z0) 169.35/137.69
activate(n__s(z0)) → s(z0) 169.35/137.69
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.69
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.69
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.69
169.35/137.69

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

Removed 24 trailing nodes:

ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.69
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.69
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.69
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.69
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.69
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.69
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.69
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__s(z0)) → c16 169.35/137.69
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.69
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.69
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.69
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.69
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.69
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.69
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
169.35/137.70
169.35/137.70

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.70
and(false, z0) → false 169.35/137.70
if(true, z0, z1) → activate(z0) 169.35/137.70
if(false, z0, z1) → activate(z1) 169.35/137.70
add(0, z0) → activate(z0) 169.35/137.70
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.70
add(z0, z1) → n__add(z0, z1) 169.35/137.70
first(0, z0) → nil 169.35/137.70
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.70
first(z0, z1) → n__first(z0, z1) 169.35/137.70
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.70
from(z0) → n__from(z0) 169.35/137.70
s(z0) → n__s(z0) 169.35/137.70
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.70
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.70
activate(n__from(z0)) → from(z0) 169.35/137.70
activate(n__s(z0)) → s(z0) 169.35/137.70
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.70
169.35/137.70

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

Use forward instantiation to replace ACTIVATE(n__from(n__from(y0))) → c15(FROM(n__from(y0))) by

ACTIVATE(n__from(n__from(n__add(y0, y1)))) → c15(FROM(n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__from(y0)))) → c15(FROM(n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0))))
169.35/137.70
169.35/137.70

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.70
and(false, z0) → false 169.35/137.70
if(true, z0, z1) → activate(z0) 169.35/137.70
if(false, z0, z1) → activate(z1) 169.35/137.70
add(0, z0) → activate(z0) 169.35/137.70
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.70
add(z0, z1) → n__add(z0, z1) 169.35/137.70
first(0, z0) → nil 169.35/137.70
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.70
first(z0, z1) → n__first(z0, z1) 169.35/137.70
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.70
from(z0) → n__from(z0) 169.35/137.70
s(z0) → n__s(z0) 169.35/137.70
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.70
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.70
activate(n__from(z0)) → from(z0) 169.35/137.70
activate(n__s(z0)) → s(z0) 169.35/137.70
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__add(y0, y1)))) → c15(FROM(n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__from(y0)))) → c15(FROM(n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__add(y0, y1)))) → c15(FROM(n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__from(y0)))) → c15(FROM(n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.70
169.35/137.70

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

Removed 26 trailing nodes:

ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0))))
169.35/137.70
169.35/137.70

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(true, z0) → activate(z0) 169.35/137.70
and(false, z0) → false 169.35/137.70
if(true, z0, z1) → activate(z0) 169.35/137.70
if(false, z0, z1) → activate(z1) 169.35/137.70
add(0, z0) → activate(z0) 169.35/137.70
add(s(z0), z1) → s(n__add(activate(z0), activate(z1))) 169.35/137.70
add(z0, z1) → n__add(z0, z1) 169.35/137.70
first(0, z0) → nil 169.35/137.70
first(s(z0), cons(z1, z2)) → cons(activate(z1), n__first(activate(z0), activate(z2))) 169.35/137.70
first(z0, z1) → n__first(z0, z1) 169.35/137.70
from(z0) → cons(activate(z0), n__from(n__s(activate(z0)))) 169.35/137.70
from(z0) → n__from(z0) 169.35/137.70
s(z0) → n__s(z0) 169.35/137.70
activate(n__add(z0, z1)) → add(z0, z1) 169.35/137.70
activate(n__first(z0, z1)) → first(z0, z1) 169.35/137.70
activate(n__from(z0)) → from(z0) 169.35/137.70
activate(n__s(z0)) → s(z0) 169.35/137.70
activate(z0) → z0
Tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__add(y0, y1)))) → c15(FROM(n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__from(y0)))) → c15(FROM(n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0))))
S tuples:

ACTIVATE(n__first(z0, z1)) → c14 169.35/137.70
ACTIVATE(n__s(z0)) → c16 169.35/137.70
ADD(0, n__first(y0, y1)) → c4(ACTIVATE(n__first(y0, y1))) 169.35/137.70
ADD(0, n__s(y0)) → c4(ACTIVATE(n__s(y0))) 169.35/137.70
FROM(n__first(y0, y1)) → c(ACTIVATE(n__first(y0, y1))) 169.35/137.70
FROM(n__s(y0)) → c(ACTIVATE(n__s(y0))) 169.35/137.70
ACTIVATE(n__add(0, n__first(y0, y1))) → c13(ADD(0, n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__add(0, n__s(y0))) → c13(ADD(0, n__s(y0))) 169.35/137.70
ACTIVATE(n__from(n__first(y0, y1))) → c15(FROM(n__first(y0, y1))) 169.35/137.70
ACTIVATE(n__from(n__s(y0))) → c15(FROM(n__s(y0))) 169.35/137.70
ADD(0, n__add(0, n__add(y0, y1))) → c4(ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__from(y0))) → c4(ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
ADD(0, n__add(0, n__first(y0, y1))) → c4(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
ADD(0, n__add(0, n__s(y0))) → c4(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
ADD(0, n__from(n__add(y0, y1))) → c4(ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__from(y0))) → c4(ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
ADD(0, n__from(n__first(y0, y1))) → c4(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
ADD(0, n__from(n__s(y0))) → c4(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
FROM(n__add(0, n__add(y0, y1))) → c10(ACTIVATE(n__add(0, n__add(y0, y1))), ACTIVATE(n__add(0, n__add(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__from(y0))) → c10(ACTIVATE(n__add(0, n__from(y0))), ACTIVATE(n__add(0, n__from(y0)))) 169.35/137.70
FROM(n__add(0, n__first(y0, y1))) → c1(ACTIVATE(n__add(0, n__first(y0, y1)))) 169.35/137.70
FROM(n__add(0, n__s(y0))) → c1(ACTIVATE(n__add(0, n__s(y0)))) 169.35/137.70
FROM(n__from(n__add(y0, y1))) → c10(ACTIVATE(n__from(n__add(y0, y1))), ACTIVATE(n__from(n__add(y0, y1)))) 169.35/137.70
FROM(n__from(n__from(y0))) → c10(ACTIVATE(n__from(n__from(y0))), ACTIVATE(n__from(n__from(y0)))) 169.35/137.70
FROM(n__from(n__first(y0, y1))) → c2(ACTIVATE(n__from(n__first(y0, y1)))) 169.35/137.70
FROM(n__from(n__s(y0))) → c2(ACTIVATE(n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__add(y0, y1)))) → c13(ADD(0, n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__from(y0)))) → c13(ADD(0, n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__first(y0, y1)))) → c13(ADD(0, n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__add(0, n__s(y0)))) → c13(ADD(0, n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__add(y0, y1)))) → c13(ADD(0, n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__from(y0)))) → c13(ADD(0, n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__first(y0, y1)))) → c13(ADD(0, n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__add(0, n__from(n__s(y0)))) → c13(ADD(0, n__from(n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__add(y0, y1)))) → c15(FROM(n__add(0, n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__from(y0)))) → c15(FROM(n__add(0, n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__first(y0, y1)))) → c15(FROM(n__add(0, n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__add(0, n__s(y0)))) → c15(FROM(n__add(0, n__s(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__add(y0, y1)))) → c15(FROM(n__from(n__add(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__from(y0)))) → c15(FROM(n__from(n__from(y0)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__first(y0, y1)))) → c15(FROM(n__from(n__first(y0, y1)))) 169.35/137.70
ACTIVATE(n__from(n__from(n__s(y0)))) → c15(FROM(n__from(n__s(y0))))
K tuples:none
Defined Rule Symbols:

and, if, add, first, from, s, activate

Defined Pair Symbols:

ACTIVATE, ADD, FROM

Compound Symbols:

c14, c16, c4, c, c13, c15, c10, c1, c2

169.35/137.70
169.35/137.70
169.69/137.76 EOF