YES(O(1), O(n^1)) 4.27/1.56 YES(O(1), O(n^1)) 4.27/1.58 4.27/1.58 4.27/1.58 4.27/1.58 4.27/1.58 4.27/1.58 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 4.27/1.58 4.27/1.58 4.27/1.58
4.27/1.58
4.27/1.58
4.27/1.58
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
4.27/1.58 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
4.27/1.58 
↳2 CdtProblem
4.27/1.58 
↳3 CdtUnreachableProof (⇔)
4.27/1.58 
↳4 CdtProblem
4.27/1.58 
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
4.27/1.58 
↳6 CdtProblem
4.27/1.58 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
4.27/1.58 
↳8 CdtProblem
4.27/1.58 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.27/1.58 
↳10 CdtProblem
4.27/1.58 
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
4.27/1.58 
↳12 CdtProblem
4.27/1.58 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.27/1.58 
↳14 CdtProblem
4.27/1.58 
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.27/1.58 
↳16 CdtProblem
4.27/1.58 
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.27/1.58 
↳18 CdtProblem
4.27/1.58 
↳19 SIsEmptyProof (BOTH BOUNDS(ID, ID))
4.27/1.58 
↳20 BOUNDS(O(1), O(1))
4.27/1.58
4.27/1.58 4.27/1.58
4.27/1.58
4.27/1.58

(0) Obligation:

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

fact(X) → if(zero(X), n__s(n__0), n__prod(X, n__fact(n__p(X)))) 4.27/1.58
add(0, X) → X 4.27/1.58
add(s(X), Y) → s(add(X, Y)) 4.27/1.58
prod(0, X) → 0 4.27/1.58
prod(s(X), Y) → add(Y, prod(X, Y)) 4.27/1.58
if(true, X, Y) → activate(X) 4.27/1.58
if(false, X, Y) → activate(Y) 4.27/1.58
zero(0) → true 4.27/1.58
zero(s(X)) → false 4.27/1.58
p(s(X)) → X 4.27/1.58
s(X) → n__s(X) 4.27/1.58
0 → n__0 4.27/1.58
prod(X1, X2) → n__prod(X1, X2) 4.27/1.58
fact(X) → n__fact(X) 4.27/1.58
p(X) → n__p(X) 4.27/1.58
activate(n__s(X)) → s(activate(X)) 4.27/1.58
activate(n__0) → 0 4.27/1.58
activate(n__prod(X1, X2)) → prod(activate(X1), activate(X2)) 4.27/1.58
activate(n__fact(X)) → fact(activate(X)) 4.27/1.58
activate(n__p(X)) → p(activate(X)) 4.27/1.58
activate(X) → X

Rewrite Strategy: INNERMOST
4.27/1.58
4.27/1.58

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

Converted CpxTRS to CDT
4.27/1.58
4.27/1.58

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.27/1.59
fact(z0) → n__fact(z0) 4.27/1.59
add(0, z0) → z0 4.27/1.59
add(s(z0), z1) → s(add(z0, z1)) 4.27/1.59
prod(0, z0) → 0 4.27/1.59
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.27/1.59
prod(z0, z1) → n__prod(z0, z1) 4.27/1.59
if(true, z0, z1) → activate(z0) 4.27/1.59
if(false, z0, z1) → activate(z1) 4.27/1.59
zero(0) → true 4.27/1.59
zero(s(z0)) → false 4.27/1.59
p(s(z0)) → z0 4.27/1.59
p(z0) → n__p(z0) 4.27/1.59
s(z0) → n__s(z0) 4.27/1.59
0 → n__0 4.27/1.59
activate(n__s(z0)) → s(activate(z0)) 4.27/1.59
activate(n__0) → 0 4.27/1.59
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.27/1.59
activate(n__fact(z0)) → fact(activate(z0)) 4.27/1.59
activate(n__p(z0)) → p(activate(z0)) 4.27/1.59
activate(z0) → z0
Tuples:

FACT(z0) → c(IF(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))), ZERO(z0)) 4.27/1.59
ADD(s(z0), z1) → c3(S(add(z0, z1)), ADD(z0, z1)) 4.27/1.59
PROD(0, z0) → c4(0') 4.27/1.59
PROD(s(z0), z1) → c5(ADD(z1, prod(z0, z1)), PROD(z0, z1)) 4.27/1.59
IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__s(z0)) → c15(S(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16(0') 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(PROD(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(P(activate(z0)), ACTIVATE(z0))
S tuples:

FACT(z0) → c(IF(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))), ZERO(z0)) 4.27/1.59
ADD(s(z0), z1) → c3(S(add(z0, z1)), ADD(z0, z1)) 4.27/1.59
PROD(0, z0) → c4(0') 4.27/1.59
PROD(s(z0), z1) → c5(ADD(z1, prod(z0, z1)), PROD(z0, z1)) 4.27/1.59
IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__s(z0)) → c15(S(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16(0') 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(PROD(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(P(activate(z0)), ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

FACT, ADD, PROD, IF, ACTIVATE

Compound Symbols:

c, c3, c4, c5, c7, c8, c15, c16, c17, c18, c19

4.27/1.59
4.27/1.59

(3) CdtUnreachableProof (EQUIVALENT transformation)

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

ADD(s(z0), z1) → c3(S(add(z0, z1)), ADD(z0, z1)) 4.27/1.59
PROD(0, z0) → c4(0') 4.27/1.59
PROD(s(z0), z1) → c5(ADD(z1, prod(z0, z1)), PROD(z0, z1))
4.27/1.59
4.27/1.59

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.27/1.59
fact(z0) → n__fact(z0) 4.27/1.59
add(0, z0) → z0 4.27/1.59
add(s(z0), z1) → s(add(z0, z1)) 4.27/1.59
prod(0, z0) → 0 4.27/1.59
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.27/1.59
prod(z0, z1) → n__prod(z0, z1) 4.27/1.59
if(true, z0, z1) → activate(z0) 4.27/1.59
if(false, z0, z1) → activate(z1) 4.27/1.59
zero(0) → true 4.27/1.59
zero(s(z0)) → false 4.27/1.59
p(s(z0)) → z0 4.27/1.59
p(z0) → n__p(z0) 4.27/1.59
s(z0) → n__s(z0) 4.27/1.59
0 → n__0 4.27/1.59
activate(n__s(z0)) → s(activate(z0)) 4.27/1.59
activate(n__0) → 0 4.27/1.59
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.27/1.59
activate(n__fact(z0)) → fact(activate(z0)) 4.27/1.59
activate(n__p(z0)) → p(activate(z0)) 4.27/1.59
activate(z0) → z0
Tuples:

FACT(z0) → c(IF(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))), ZERO(z0)) 4.27/1.59
IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__s(z0)) → c15(S(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16(0') 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(PROD(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(P(activate(z0)), ACTIVATE(z0))
S tuples:

FACT(z0) → c(IF(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))), ZERO(z0)) 4.27/1.59
IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__s(z0)) → c15(S(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16(0') 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(PROD(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(P(activate(z0)), ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

FACT, IF, ACTIVATE

Compound Symbols:

c, c7, c8, c15, c16, c17, c18, c19

4.27/1.59
4.27/1.59

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

Removed 6 trailing tuple parts
4.27/1.59
4.27/1.59

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.27/1.59
fact(z0) → n__fact(z0) 4.27/1.59
add(0, z0) → z0 4.27/1.59
add(s(z0), z1) → s(add(z0, z1)) 4.27/1.59
prod(0, z0) → 0 4.27/1.59
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.27/1.59
prod(z0, z1) → n__prod(z0, z1) 4.27/1.59
if(true, z0, z1) → activate(z0) 4.27/1.59
if(false, z0, z1) → activate(z1) 4.27/1.59
zero(0) → true 4.27/1.59
zero(s(z0)) → false 4.27/1.59
p(s(z0)) → z0 4.27/1.59
p(z0) → n__p(z0) 4.27/1.59
s(z0) → n__s(z0) 4.27/1.59
0 → n__0 4.27/1.59
activate(n__s(z0)) → s(activate(z0)) 4.27/1.59
activate(n__0) → 0 4.27/1.59
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.27/1.59
activate(n__fact(z0)) → fact(activate(z0)) 4.27/1.59
activate(n__p(z0)) → p(activate(z0)) 4.27/1.59
activate(z0) → z0
Tuples:

IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
FACT(z0) → c 4.27/1.59
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.27/1.59
IF(false, z0, z1) → c8(ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.27/1.59
FACT(z0) → c 4.27/1.59
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.27/1.59
ACTIVATE(n__0) → c16 4.27/1.59
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.27/1.59
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

IF, ACTIVATE, FACT

Compound Symbols:

c7, c8, c18, c, c15, c16, c17, c19

4.68/1.60
4.68/1.60

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

IF(true, z0, z1) → c7(ACTIVATE(z0)) 4.68/1.60
IF(false, z0, z1) → c8(ACTIVATE(z1))
Removed 2 trailing nodes:

FACT(z0) → c 4.68/1.60
ACTIVATE(n__0) → c16
4.68/1.60
4.68/1.60

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.60
fact(z0) → n__fact(z0) 4.68/1.60
add(0, z0) → z0 4.68/1.60
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.60
prod(0, z0) → 0 4.68/1.60
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.60
prod(z0, z1) → n__prod(z0, z1) 4.68/1.60
if(true, z0, z1) → activate(z0) 4.68/1.60
if(false, z0, z1) → activate(z1) 4.68/1.60
zero(0) → true 4.68/1.60
zero(s(z0)) → false 4.68/1.60
p(s(z0)) → z0 4.68/1.61
p(z0) → n__p(z0) 4.68/1.61
s(z0) → n__s(z0) 4.68/1.61
0 → n__0 4.68/1.61
activate(n__s(z0)) → s(activate(z0)) 4.68/1.61
activate(n__0) → 0 4.68/1.61
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.61
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.61
activate(n__p(z0)) → p(activate(z0)) 4.68/1.61
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.61
FACT(z0) → c 4.68/1.61
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.61
ACTIVATE(n__0) → c16 4.68/1.61
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.61
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.61
FACT(z0) → c 4.68/1.61
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.61
ACTIVATE(n__0) → c16 4.68/1.61
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
K tuples:none
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0))
We considered the (Usable) Rules:

activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
0 → n__0 4.68/1.62
s(z0) → n__s(z0)
And the Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.68/1.62

POL(0) = 0    4.68/1.62
POL(ACTIVATE(x1)) = [4]x1    4.68/1.62
POL(FACT(x1)) = 0    4.68/1.62
POL(activate(x1)) = [4]x1    4.68/1.62
POL(c) = 0    4.68/1.62
POL(c15(x1)) = x1    4.68/1.62
POL(c16) = 0    4.68/1.62
POL(c17(x1, x2)) = x1 + x2    4.68/1.62
POL(c18(x1, x2)) = x1 + x2    4.68/1.62
POL(c19(x1)) = x1    4.68/1.62
POL(fact(x1)) = [2] + x1    4.68/1.62
POL(if(x1, x2, x3)) = 0    4.68/1.62
POL(n__0) = 0    4.68/1.62
POL(n__fact(x1)) = [2] + x1    4.68/1.62
POL(n__p(x1)) = x1    4.68/1.62
POL(n__prod(x1, x2)) = x1 + x2    4.68/1.62
POL(n__s(x1)) = [2] + x1    4.68/1.62
POL(p(x1)) = x1    4.68/1.62
POL(prod(x1, x2)) = x1 + x2    4.68/1.62
POL(s(x1)) = [4] + x1    4.68/1.62
POL(zero(x1)) = 0   
4.68/1.62
4.68/1.62

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
add(0, z0) → z0 4.68/1.62
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.62
prod(0, z0) → 0 4.68/1.62
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
if(true, z0, z1) → activate(z0) 4.68/1.62
if(false, z0, z1) → activate(z1) 4.68/1.62
zero(0) → true 4.68/1.62
zero(s(z0)) → false 4.68/1.62
p(s(z0)) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
s(z0) → n__s(z0) 4.68/1.62
0 → n__0 4.68/1.62
activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

FACT(z0) → c 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
K tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0))
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

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

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

FACT(z0) → c
4.68/1.62
4.68/1.62

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
add(0, z0) → z0 4.68/1.62
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.62
prod(0, z0) → 0 4.68/1.62
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
if(true, z0, z1) → activate(z0) 4.68/1.62
if(false, z0, z1) → activate(z1) 4.68/1.62
zero(0) → true 4.68/1.62
zero(s(z0)) → false 4.68/1.62
p(s(z0)) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
s(z0) → n__s(z0) 4.68/1.62
0 → n__0 4.68/1.62
activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
K tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__0) → c16
We considered the (Usable) Rules:

activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
0 → n__0 4.68/1.62
s(z0) → n__s(z0)
And the Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.68/1.62

POL(0) = [3]    4.68/1.62
POL(ACTIVATE(x1)) = [4]x1    4.68/1.62
POL(FACT(x1)) = [1]    4.68/1.62
POL(activate(x1)) = 0    4.68/1.62
POL(c) = 0    4.68/1.62
POL(c15(x1)) = x1    4.68/1.62
POL(c16) = 0    4.68/1.62
POL(c17(x1, x2)) = x1 + x2    4.68/1.62
POL(c18(x1, x2)) = x1 + x2    4.68/1.62
POL(c19(x1)) = x1    4.68/1.62
POL(fact(x1)) = [3]    4.68/1.62
POL(if(x1, x2, x3)) = [3]    4.68/1.62
POL(n__0) = [2]    4.68/1.62
POL(n__fact(x1)) = [1] + x1    4.68/1.62
POL(n__p(x1)) = x1    4.68/1.62
POL(n__prod(x1, x2)) = x1 + x2    4.68/1.62
POL(n__s(x1)) = x1    4.68/1.62
POL(p(x1)) = [3] + [3]x1    4.68/1.62
POL(prod(x1, x2)) = [3]    4.68/1.62
POL(s(x1)) = [3] + [3]x1    4.68/1.62
POL(zero(x1)) = [3] + [3]x1   
4.68/1.62
4.68/1.62

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
add(0, z0) → z0 4.68/1.62
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.62
prod(0, z0) → 0 4.68/1.62
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
if(true, z0, z1) → activate(z0) 4.68/1.62
if(false, z0, z1) → activate(z1) 4.68/1.62
zero(0) → true 4.68/1.62
zero(s(z0)) → false 4.68/1.62
p(s(z0)) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
s(z0) → n__s(z0) 4.68/1.62
0 → n__0 4.68/1.62
activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
K tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__0) → c16
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
We considered the (Usable) Rules:

activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
0 → n__0 4.68/1.62
s(z0) → n__s(z0)
And the Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.68/1.62

POL(0) = [3]    4.68/1.62
POL(ACTIVATE(x1)) = [4]x1    4.68/1.62
POL(FACT(x1)) = [5]    4.68/1.62
POL(activate(x1)) = 0    4.68/1.62
POL(c) = 0    4.68/1.62
POL(c15(x1)) = x1    4.68/1.62
POL(c16) = 0    4.68/1.62
POL(c17(x1, x2)) = x1 + x2    4.68/1.62
POL(c18(x1, x2)) = x1 + x2    4.68/1.62
POL(c19(x1)) = x1    4.68/1.62
POL(fact(x1)) = [3]    4.68/1.62
POL(if(x1, x2, x3)) = [3]    4.68/1.62
POL(n__0) = 0    4.68/1.62
POL(n__fact(x1)) = [4] + x1    4.68/1.62
POL(n__p(x1)) = [1] + x1    4.68/1.62
POL(n__prod(x1, x2)) = x1 + x2    4.68/1.62
POL(n__s(x1)) = x1    4.68/1.62
POL(p(x1)) = [3] + [3]x1    4.68/1.62
POL(prod(x1, x2)) = [3]    4.68/1.62
POL(s(x1)) = [3] + [3]x1    4.68/1.62
POL(zero(x1)) = [3] + [3]x1   
4.68/1.62
4.68/1.62

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
add(0, z0) → z0 4.68/1.62
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.62
prod(0, z0) → 0 4.68/1.62
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
if(true, z0, z1) → activate(z0) 4.68/1.62
if(false, z0, z1) → activate(z1) 4.68/1.62
zero(0) → true 4.68/1.62
zero(s(z0)) → false 4.68/1.62
p(s(z0)) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
s(z0) → n__s(z0) 4.68/1.62
0 → n__0 4.68/1.62
activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:

ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1))
K tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1))
We considered the (Usable) Rules:

activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
0 → n__0 4.68/1.62
s(z0) → n__s(z0)
And the Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.68/1.62

POL(0) = [3]    4.68/1.62
POL(ACTIVATE(x1)) = [4] + [2]x1    4.68/1.62
POL(FACT(x1)) = 0    4.68/1.62
POL(activate(x1)) = 0    4.68/1.62
POL(c) = 0    4.68/1.62
POL(c15(x1)) = x1    4.68/1.62
POL(c16) = 0    4.68/1.62
POL(c17(x1, x2)) = x1 + x2    4.68/1.62
POL(c18(x1, x2)) = x1 + x2    4.68/1.62
POL(c19(x1)) = x1    4.68/1.62
POL(fact(x1)) = [3]    4.68/1.62
POL(if(x1, x2, x3)) = [3]    4.68/1.62
POL(n__0) = 0    4.68/1.62
POL(n__fact(x1)) = x1    4.68/1.62
POL(n__p(x1)) = x1    4.68/1.62
POL(n__prod(x1, x2)) = [4] + x1 + x2    4.68/1.62
POL(n__s(x1)) = x1    4.68/1.62
POL(p(x1)) = [3] + [3]x1    4.68/1.62
POL(prod(x1, x2)) = [3]    4.68/1.62
POL(s(x1)) = [3] + [3]x1    4.68/1.62
POL(zero(x1)) = [3] + [3]x1   
4.68/1.62
4.68/1.62

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

fact(z0) → if(zero(z0), n__s(n__0), n__prod(z0, n__fact(n__p(z0)))) 4.68/1.62
fact(z0) → n__fact(z0) 4.68/1.62
add(0, z0) → z0 4.68/1.62
add(s(z0), z1) → s(add(z0, z1)) 4.68/1.62
prod(0, z0) → 0 4.68/1.62
prod(s(z0), z1) → add(z1, prod(z0, z1)) 4.68/1.62
prod(z0, z1) → n__prod(z0, z1) 4.68/1.62
if(true, z0, z1) → activate(z0) 4.68/1.62
if(false, z0, z1) → activate(z1) 4.68/1.62
zero(0) → true 4.68/1.62
zero(s(z0)) → false 4.68/1.62
p(s(z0)) → z0 4.68/1.62
p(z0) → n__p(z0) 4.68/1.62
s(z0) → n__s(z0) 4.68/1.62
0 → n__0 4.68/1.62
activate(n__s(z0)) → s(activate(z0)) 4.68/1.62
activate(n__0) → 0 4.68/1.62
activate(n__prod(z0, z1)) → prod(activate(z0), activate(z1)) 4.68/1.62
activate(n__fact(z0)) → fact(activate(z0)) 4.68/1.62
activate(n__p(z0)) → p(activate(z0)) 4.68/1.62
activate(z0) → z0
Tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1)) 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0))
S tuples:none
K tuples:

ACTIVATE(n__fact(z0)) → c18(FACT(activate(z0)), ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__s(z0)) → c15(ACTIVATE(z0)) 4.68/1.62
FACT(z0) → c 4.68/1.62
ACTIVATE(n__0) → c16 4.68/1.62
ACTIVATE(n__p(z0)) → c19(ACTIVATE(z0)) 4.68/1.62
ACTIVATE(n__prod(z0, z1)) → c17(ACTIVATE(z0), ACTIVATE(z1))
Defined Rule Symbols:

fact, add, prod, if, zero, p, s, 0, activate

Defined Pair Symbols:

ACTIVATE, FACT

Compound Symbols:

c18, c, c15, c16, c17, c19

4.68/1.62
4.68/1.62

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

The set S is empty
4.68/1.62
4.68/1.62

(20) BOUNDS(O(1), O(1))

4.68/1.62
4.68/1.62
4.68/1.68 EOF