YES(O(1), O(n^1)) 6.72/2.15 YES(O(1), O(n^1)) 6.72/2.19 6.72/2.19 6.72/2.19 6.72/2.19 6.72/2.19 6.72/2.19 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 6.72/2.19 6.72/2.19 6.72/2.19
6.72/2.19
6.72/2.19
6.72/2.19
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxRelTRS
6.72/2.19 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
6.72/2.19 
↳2 CdtProblem
6.72/2.19 
↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
6.72/2.19 
↳4 CdtProblem
6.72/2.19 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
6.72/2.19 
↳6 CdtProblem
6.72/2.19 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.72/2.19 
↳8 CdtProblem
6.72/2.19 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.72/2.19 
↳10 CdtProblem
6.72/2.19 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.72/2.19 
↳12 CdtProblem
6.72/2.19 
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))
6.72/2.19 
↳14 BOUNDS(O(1), O(1))
6.72/2.19
6.72/2.19 6.72/2.19
6.72/2.19
6.72/2.19

(0) Obligation:

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

lt0(Nil, Cons(x', xs)) → True 6.72/2.19
lt0(Cons(x', xs'), Cons(x, xs)) → lt0(xs', xs) 6.72/2.19
g(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 6.72/2.19
f(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 6.72/2.19
notEmpty(Cons(x, xs)) → True 6.72/2.19
notEmpty(Nil) → False 6.72/2.19
lt0(x, Nil) → False 6.72/2.19
g(x, Cons(x', xs)) → g[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs)) 6.72/2.19
f(x, Cons(x', xs)) → f[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs)) 6.72/2.19
number4(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 6.72/2.19
goal(x, y) → Cons(f(x, y), Cons(g(x, y), Nil))

The (relative) TRS S consists of the following rules:

g[Ite][False][Ite](False, Cons(x, xs), y) → g(xs, Cons(Cons(Nil, Nil), y)) 6.72/2.19
g[Ite][False][Ite](True, x', Cons(x, xs)) → g(x', xs) 6.72/2.19
f[Ite][False][Ite](False, Cons(x, xs), y) → f(xs, Cons(Cons(Nil, Nil), y)) 7.17/2.22
f[Ite][False][Ite](True, x', Cons(x, xs)) → f(x', xs)

Rewrite Strategy: INNERMOST
7.17/2.22
7.17/2.22

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
7.17/2.22
7.17/2.22

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.22
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.22
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.22
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.22
lt0(Nil, Cons(z0, z1)) → True 7.17/2.22
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.22
lt0(z0, Nil) → False 7.17/2.22
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.22
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.22
notEmpty(Cons(z0, z1)) → True 7.17/2.22
notEmpty(Nil) → False 7.17/2.22
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.22
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.22
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.22
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.22
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.22
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
GOAL(z0, z1) → c14(F(z0, z1), G(z0, z1))
S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.22
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
GOAL(z0, z1) → c14(F(z0, z1), G(z0, z1))
K tuples:none
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F, GOAL

Compound Symbols:

c, c1, c2, c3, c5, c8, c10, c14

7.17/2.22
7.17/2.22

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

Split RHS of tuples not part of any SCC
7.17/2.22
7.17/2.22

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.22
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.22
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.22
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.22
lt0(Nil, Cons(z0, z1)) → True 7.17/2.22
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.22
lt0(z0, Nil) → False 7.17/2.22
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.22
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.22
notEmpty(Cons(z0, z1)) → True 7.17/2.22
notEmpty(Nil) → False 7.17/2.22
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.22
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.22
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.22
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.22
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.22
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.22
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
GOAL(z0, z1) → c4(F(z0, z1)) 7.17/2.22
GOAL(z0, z1) → c4(G(z0, z1))
S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.22
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.22
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
GOAL(z0, z1) → c4(F(z0, z1)) 7.17/2.25
GOAL(z0, z1) → c4(G(z0, z1))
K tuples:none
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F, GOAL

Compound Symbols:

c, c1, c2, c3, c5, c8, c10, c4

7.17/2.25
7.17/2.25

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c4(G(z0, z1)) 7.17/2.25
GOAL(z0, z1) → c4(F(z0, z1))
7.17/2.25
7.17/2.25

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.25
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.25
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.25
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.25
lt0(Nil, Cons(z0, z1)) → True 7.17/2.25
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.25
lt0(z0, Nil) → False 7.17/2.25
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.25
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.25
notEmpty(Cons(z0, z1)) → True 7.17/2.25
notEmpty(Nil) → False 7.17/2.25
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.25
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.25
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
K tuples:none
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F

Compound Symbols:

c, c1, c2, c3, c5, c8, c10

7.17/2.25
7.17/2.25

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

G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
We considered the (Usable) Rules:

lt0(Nil, Cons(z0, z1)) → True 7.17/2.25
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.25
lt0(z0, Nil) → False
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.25
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.25
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
The order we found is given by the following interpretation:
Polynomial interpretation : 7.17/2.25

POL(Cons(x1, x2)) = [1] + x2    7.17/2.25
POL(F(x1, x2)) = 0    7.17/2.25
POL(F[ITE][FALSE][ITE](x1, x2, x3)) = 0    7.17/2.25
POL(False) = 0    7.17/2.25
POL(G(x1, x2)) = [2] + [5]x1 + x2    7.17/2.25
POL(G[ITE][FALSE][ITE](x1, x2, x3)) = [1] + [5]x2 + x3    7.17/2.25
POL(LT0(x1, x2)) = 0    7.17/2.25
POL(Nil) = 0    7.17/2.25
POL(True) = 0    7.17/2.25
POL(c(x1)) = x1    7.17/2.25
POL(c1(x1)) = x1    7.17/2.25
POL(c10(x1, x2)) = x1 + x2    7.17/2.25
POL(c2(x1)) = x1    7.17/2.25
POL(c3(x1)) = x1    7.17/2.25
POL(c5(x1)) = x1    7.17/2.25
POL(c8(x1, x2)) = x1 + x2    7.17/2.25
POL(lt0(x1, x2)) = 0   
7.17/2.25
7.17/2.25

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.25
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.25
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.25
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.25
lt0(Nil, Cons(z0, z1)) → True 7.17/2.25
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.25
lt0(z0, Nil) → False 7.17/2.25
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.25
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.25
notEmpty(Cons(z0, z1)) → True 7.17/2.25
notEmpty(Nil) → False 7.17/2.25
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.25
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.25
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.25
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
K tuples:

G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F

Compound Symbols:

c, c1, c2, c3, c5, c8, c10

7.17/2.25
7.17/2.25

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

F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
We considered the (Usable) Rules:

lt0(Nil, Cons(z0, z1)) → True 7.17/2.25
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.25
lt0(z0, Nil) → False
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.25
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.25
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.25
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.25
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.25
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
The order we found is given by the following interpretation:
Polynomial interpretation : 7.17/2.25

POL(Cons(x1, x2)) = [4] + x2    7.17/2.25
POL(F(x1, x2)) = [4] + [2]x1 + x2    7.17/2.25
POL(F[ITE][FALSE][ITE](x1, x2, x3)) = [2]x2 + x3    7.17/2.25
POL(False) = 0    7.17/2.25
POL(G(x1, x2)) = [3] + [2]x1 + x2    7.17/2.25
POL(G[ITE][FALSE][ITE](x1, x2, x3)) = [2]x2 + x3    7.17/2.25
POL(LT0(x1, x2)) = [3]    7.17/2.25
POL(Nil) = 0    7.17/2.25
POL(True) = 0    7.17/2.25
POL(c(x1)) = x1    7.17/2.25
POL(c1(x1)) = x1    7.17/2.25
POL(c10(x1, x2)) = x1 + x2    7.17/2.25
POL(c2(x1)) = x1    7.17/2.25
POL(c3(x1)) = x1    7.17/2.25
POL(c5(x1)) = x1    7.17/2.25
POL(c8(x1, x2)) = x1 + x2    7.17/2.26
POL(lt0(x1, x2)) = 0   
7.17/2.26
7.17/2.26

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.26
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.26
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.26
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.26
lt0(Nil, Cons(z0, z1)) → True 7.17/2.26
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.26
lt0(z0, Nil) → False 7.17/2.26
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.26
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.26
notEmpty(Cons(z0, z1)) → True 7.17/2.26
notEmpty(Nil) → False 7.17/2.26
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.26
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.26
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.26
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
K tuples:

G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F

Compound Symbols:

c, c1, c2, c3, c5, c8, c10

7.17/2.26
7.17/2.26

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

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

LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
We considered the (Usable) Rules:

lt0(Nil, Cons(z0, z1)) → True 7.17/2.26
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.26
lt0(z0, Nil) → False
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.26
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.26
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.26
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
The order we found is given by the following interpretation:
Polynomial interpretation : 7.17/2.26

POL(Cons(x1, x2)) = [4] + x2    7.17/2.26
POL(F(x1, x2)) = [4] + [2]x1 + x2    7.17/2.26
POL(F[ITE][FALSE][ITE](x1, x2, x3)) = [2]x2 + x3    7.17/2.26
POL(False) = 0    7.17/2.26
POL(G(x1, x2)) = [4] + [5]x1 + [4]x2    7.17/2.26
POL(G[ITE][FALSE][ITE](x1, x2, x3)) = [5]x2 + [4]x3    7.17/2.26
POL(LT0(x1, x2)) = x2    7.17/2.26
POL(Nil) = 0    7.17/2.26
POL(True) = 0    7.17/2.26
POL(c(x1)) = x1    7.17/2.26
POL(c1(x1)) = x1    7.17/2.26
POL(c10(x1, x2)) = x1 + x2    7.17/2.26
POL(c2(x1)) = x1    7.17/2.26
POL(c3(x1)) = x1    7.17/2.26
POL(c5(x1)) = x1    7.17/2.26
POL(c8(x1, x2)) = x1 + x2    7.17/2.26
POL(lt0(x1, x2)) = 0   
7.17/2.26
7.17/2.26

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.26
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2) 7.17/2.26
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2)) 7.17/2.26
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2) 7.17/2.26
lt0(Nil, Cons(z0, z1)) → True 7.17/2.26
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3) 7.17/2.26
lt0(z0, Nil) → False 7.17/2.26
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.26
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) 7.17/2.26
notEmpty(Cons(z0, z1)) → True 7.17/2.26
notEmpty(Nil) → False 7.17/2.26
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) 7.17/2.26
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2)) 7.17/2.26
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2))) 7.17/2.26
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2)) 7.17/2.26
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3)) 7.17/2.26
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
S tuples:none
K tuples:

G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) 7.17/2.26
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

G[ITE][FALSE][ITE], F[ITE][FALSE][ITE], LT0, G, F

Compound Symbols:

c, c1, c2, c3, c5, c8, c10

7.17/2.26
7.17/2.26

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

The set S is empty
7.17/2.26
7.17/2.26

(14) BOUNDS(O(1), O(1))

7.17/2.26
7.17/2.26
7.51/2.37 EOF