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

(0) Obligation:

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

merge(Cons(x, xs), Nil) → Cons(x, xs)
merge(Cons(x', xs'), Cons(x, xs)) → merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs))
merge(Nil, ys) → ys
goal(xs, ys) → merge(xs, ys)

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

<=(S(x), S(y)) → <=(x, y)
<=(0, y) → True
<=(S(x), 0) → False
merge[Ite](False, xs', Cons(x, xs)) → Cons(x, merge(xs', xs))
merge[Ite](True, Cons(x, xs), ys) → Cons(x, merge(xs, ys))

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1)
<=(0, z0) → True
<=(S(z0), 0) → False
merge[Ite](False, z0, Cons(z1, z2)) → Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) → Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) → Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) → z0
goal(z0, z1) → merge(z0, z1)

Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
<='(0, z0) → c1
<='(S(z0), 0) → c2
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7
GOAL(z0, z1) → c8(MERGE(z0, z1))

S tuples:

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7
GOAL(z0, z1) → c8(MERGE(z0, z1))

K tuples:none
Defined Rule Symbols:

merge, goal, <=, merge[Ite]

Defined Pair Symbols:

<=', MERGE[ITE], MERGE, GOAL

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c8(MERGE(z0, z1))

Removed 2 trailing nodes:

<='(S(z0), 0) → c2
<='(0, z0) → c1

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1)
<=(0, z0) → True
<=(S(z0), 0) → False
merge[Ite](False, z0, Cons(z1, z2)) → Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) → Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) → Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) → z0
goal(z0, z1) → merge(z0, z1)

Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

S tuples:

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

K tuples:none
Defined Rule Symbols:

merge, goal, <=, merge[Ite]

Defined Pair Symbols:

<=', MERGE[ITE], MERGE

Compound Symbols:

c, c3, c4, c5, c6, c7

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

merge[Ite](False, z0, Cons(z1, z2)) → Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) → Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) → Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) → z0
goal(z0, z1) → merge(z0, z1)

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1)
<=(0, z0) → True
<=(S(z0), 0) → False

Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

S tuples:

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

K tuples:none
Defined Rule Symbols:

<=

Defined Pair Symbols:

<=', MERGE[ITE], MERGE

Compound Symbols:

c, c3, c4, c5, c6, c7

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

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

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Nil, z0) → c7

We considered the (Usable) Rules:

<=(0, z0) → True
<=(S(z0), S(z1)) → <=(z0, z1)
<=(S(z0), 0) → False

And the Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<=(x₁, x₂)) = [1]   
POL(<='(x₁, x₂)) = 0   
POL(Cons(x₁, x₂)) = 0   
POL(False) = [1]   
POL(MERGE(x₁, x₂)) = [1]   
POL(MERGE[ITE](x₁, x₂, x₃)) = x₂ + [3]x₃ + x₁² + [2]x₂²   
POL(Nil) = 0   
POL(S(x₁)) = 0   
POL(True) = [1]   
POL(c(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5) = 0   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1)
<=(0, z0) → True
<=(S(z0), 0) → False

Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

S tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))

K tuples:

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Nil, z0) → c7

Defined Rule Symbols:

<=

Defined Pair Symbols:

<=', MERGE[ITE], MERGE

Compound Symbols:

c, c3, c4, c5, c6, c7

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

MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))

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

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [3]   
POL(<=(x₁, x₂)) = 0   
POL(<='(x₁, x₂)) = 0   
POL(Cons(x₁, x₂)) = [1] + x₂   
POL(False) = [2]   
POL(MERGE(x₁, x₂)) = [1] + x₁ + x₂   
POL(MERGE[ITE](x₁, x₂, x₃)) = x₂ + x₃   
POL(Nil) = 0   
POL(S(x₁)) = 0   
POL(True) = 0   
POL(c(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5) = 0   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

<=(S(z0), S(z1)) → <=(z0, z1)
<=(0, z0) → True
<=(S(z0), 0) → False

Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1))
MERGE[ITE](False, z0, Cons(z1, z2)) → c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) → c4(MERGE(z1, z2))
MERGE(Cons(z0, z1), Nil) → c5
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) → c7

S tuples:none
K tuples:

MERGE(Cons(z0, z1), Nil) → c5
MERGE(Nil, z0) → c7
MERGE(Cons(z0, z1), Cons(z2, z3)) → c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))

Defined Rule Symbols:

<=

Defined Pair Symbols:

<=', MERGE[ITE], MERGE

Compound Symbols:

c, c3, c4, c5, c6, c7

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

The set S is empty

(12) BOUNDS(1, 1)