Runtime Complexity (innermost) proof of /tmp/tmpgLpZPs/thetrickSize.xml

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

0 CpxRelTRS

↳1 CpxTrsToCdtProof (UPPER BOUND(ID), 0 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳4 CdtProblem

↳5 CdtUsableRulesProof (⇔, 0 ms)

↳6 CdtProblem

↳7 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 248 ms)

↳8 CdtProblem

↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 54 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 48 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 50 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 47 ms)

↳16 CdtProblem

↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 BOUNDS(1, 1)

(0) Obligation:

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

lt0(Nil, Cons(x', xs)) → True
lt0(Cons(x', xs'), Cons(x, xs)) → lt0(xs', xs)
g(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lt0(x, Nil) → False
g(x, Cons(x', xs)) → g[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
f(x, Cons(x', xs)) → f[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
number4(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
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))
g[Ite][False][Ite](True, x', Cons(x, xs)) → g(x', xs)
f[Ite][False][Ite](False, Cons(x, xs), y) → f(xs, Cons(Cons(Nil, Nil), y))
f[Ite][False][Ite](True, x', Cons(x, xs)) → f(x', xs)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)
lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
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)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Nil, Cons(z0, z1)) → c4
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
LT0(z0, Nil) → c6
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
NOTEMPTY(Cons(z0, z1)) → c11
NOTEMPTY(Nil) → c12
NUMBER4(z0) → c13
GOAL(z0, z1) → c14(F(z0, z1), G(z0, z1))

S tuples:

LT0(Nil, Cons(z0, z1)) → c4
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
LT0(z0, Nil) → c6
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
NOTEMPTY(Cons(z0, z1)) → c11
NOTEMPTY(Nil) → c12
NUMBER4(z0) → c13
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, NOTEMPTY, NUMBER4, GOAL

Compound Symbols:

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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c14(F(z0, z1), G(z0, z1))

Removed 5 trailing nodes:

NOTEMPTY(Cons(z0, z1)) → c11
NUMBER4(z0) → c13
NOTEMPTY(Nil) → c12
LT0(Nil, Cons(z0, z1)) → c4
LT0(z0, Nil) → c6

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)
lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
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)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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, c7, c8, c9, c10

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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

Defined Pair Symbols:

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

Compound Symbols:

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

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

G(z0, Nil) → c7

We considered the (Usable) Rules:none
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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 :

POL(Cons(x₁, x₂)) = 0
POL(F(x₁, x₂)) = 0
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(False) = [2]
POL(G(x₁, x₂)) = [4]
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = [4]
POL(LT0(x₁, x₂)) = 0
POL(Nil) = 0
POL(True) = [3]
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7) = 0
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9) = 0
POL(lt0(x₁, x₂)) = [2] + [3]x₁

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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))
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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, Nil) → c7

Defined Rule Symbols:

lt0

Defined Pair Symbols:

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

Compound Symbols:

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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

F(z0, Nil) → c9

We considered the (Usable) Rules:none
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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 :

POL(Cons(x₁, x₂)) = 0
POL(F(x₁, x₂)) = [1]
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [1]
POL(False) = 0
POL(G(x₁, x₂)) = 0
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(LT0(x₁, x₂)) = 0
POL(Nil) = [2]
POL(True) = [2]
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7) = 0
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9) = 0
POL(lt0(x₁, x₂)) = 0

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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))
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
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, Nil) → c7
F(z0, Nil) → c9

Defined Rule Symbols:

lt0

Defined Pair Symbols:

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

Compound Symbols:

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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(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:none
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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 :

POL(Cons(x₁, x₂)) = [4] + x₂
POL(F(x₁, x₂)) = [4] + [2]x₁ + x₂
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [2]x₂ + x₃
POL(False) = [4]
POL(G(x₁, x₂)) = 0
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(LT0(x₁, x₂)) = 0
POL(Nil) = [2]
POL(True) = [2]
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7) = 0
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9) = 0
POL(lt0(x₁, x₂)) = [4] + [2]x₁ + [2]x₂

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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))
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

K tuples:

G(z0, Nil) → c7
F(z0, Nil) → c9
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

Defined Pair Symbols:

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

Compound Symbols:

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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(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:none
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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 :

POL(Cons(x₁, x₂)) = [4] + x₂
POL(F(x₁, x₂)) = [4] + [5]x₁ + [4]x₂
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [5]x₂ + [4]x₃
POL(False) = 0
POL(G(x₁, x₂)) = [2] + [5]x₁ + [4]x₂
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = [5]x₂ + [4]x₃
POL(LT0(x₁, x₂)) = [1]
POL(Nil) = [4]
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7) = 0
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9) = 0
POL(lt0(x₁, x₂)) = 0

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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, Nil) → c7
F(z0, Nil) → c9
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
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

Defined Pair Symbols:

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

Compound Symbols:

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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(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:none
And the Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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 :

POL(Cons(x₁, x₂)) = [4] + x₂
POL(F(x₁, x₂)) = [4] + [3]x₁ + [2]x₂
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [3]x₂ + [2]x₃
POL(False) = 0
POL(G(x₁, x₂)) = [4] + [5]x₁ + [4]x₂
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = [5]x₂ + [4]x₃
POL(LT0(x₁, x₂)) = x₂
POL(Nil) = 0
POL(True) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c2(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c7) = 0
POL(c8(x₁, x₂)) = x₁ + x₂
POL(c9) = 0
POL(lt0(x₁, x₂)) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c1(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c2(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c3(F(z0, z2))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))
G(z0, Nil) → c7
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c9
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, Nil) → c7
F(z0, Nil) → c9
F(z0, Cons(z1, z2)) → c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G(z0, Cons(z1, z2)) → c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
LT0(Cons(z0, z1), Cons(z2, z3)) → c5(LT0(z1, z3))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

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

Compound Symbols:

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

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

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(4) Obligation:

(5) CdtUsableRulesProof (EQUIVALENT transformation)

(6) Obligation:

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(8) Obligation:

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(10) Obligation:

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(12) Obligation:

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

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

(18) BOUNDS(1, 1)