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:

loop(Cons(x, xs), Nil, pp, ss) → False
loop(Cons(x', xs'), Cons(x, xs), pp, ss) → loop[Ite](!EQ(x', x), Cons(x', xs'), Cons(x, xs), pp, ss)
loop(Nil, s, pp, ss) → True
match1(p, s) → loop(p, s, p, s)

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

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
loop[Ite](False, p, s, pp, Cons(x, xs)) → loop(pp, xs, pp, xs)
loop[Ite](True, Cons(x', xs'), Cons(x, xs), pp, ss) → loop(xs', xs, pp, ss)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
loop[Ite](False, z0, z1, z2, Cons(z3, z4)) → loop(z2, z4, z2, z4)
loop[Ite](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → loop(z1, z3, z4, z5)
loop(Cons(z0, z1), Nil, z2, z3) → False
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5)
loop(Nil, z0, z1, z2) → True
match1(z0, z1) → loop(z0, z1, z0, z1)

Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c1
!EQ'(S(z0), 0) → c2
!EQ'(0, 0) → c3
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8
MATCH1(z0, z1) → c9(LOOP(z0, z1, z0, z1))

S tuples:

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8
MATCH1(z0, z1) → c9(LOOP(z0, z1, z0, z1))

K tuples:none
Defined Rule Symbols:

loop, match1, !EQ, loop[Ite]

Defined Pair Symbols:

!EQ', LOOP[ITE], LOOP, MATCH1

Compound Symbols:

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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

MATCH1(z0, z1) → c9(LOOP(z0, z1, z0, z1))

Removed 3 trailing nodes:

!EQ'(0, S(z0)) → c1
!EQ'(0, 0) → c3
!EQ'(S(z0), 0) → c2

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
loop[Ite](False, z0, z1, z2, Cons(z3, z4)) → loop(z2, z4, z2, z4)
loop[Ite](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → loop(z1, z3, z4, z5)
loop(Cons(z0, z1), Nil, z2, z3) → False
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5)
loop(Nil, z0, z1, z2) → True
match1(z0, z1) → loop(z0, z1, z0, z1)

Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

S tuples:

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

K tuples:none
Defined Rule Symbols:

loop, match1, !EQ, loop[Ite]

Defined Pair Symbols:

!EQ', LOOP[ITE], LOOP

Compound Symbols:

c, c4, c5, c6, c7, c8

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

loop[Ite](False, z0, z1, z2, Cons(z3, z4)) → loop(z2, z4, z2, z4)
loop[Ite](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → loop(z1, z3, z4, z5)
loop(Cons(z0, z1), Nil, z2, z3) → False
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5)
loop(Nil, z0, z1, z2) → True
match1(z0, z1) → loop(z0, z1, z0, z1)

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True

Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

S tuples:

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

K tuples:none
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

!EQ', LOOP[ITE], LOOP

Compound Symbols:

c, c4, c5, c6, c7, c8

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

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Nil, z0, z1, z2) → c8

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

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

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

POL(!EQ(x₁, x₂)) = 0   
POL(!EQ'(x₁, x₂)) = 0   
POL(0) = [3]   
POL(Cons(x₁, x₂)) = 0   
POL(False) = 0   
POL(LOOP(x₁, x₂, x₃, x₄)) = [4]   
POL(LOOP[ITE](x₁, x₂, x₃, x₄, x₅)) = [4]   
POL(Nil) = 0   
POL(S(x₁)) = [2]   
POL(True) = 0   
POL(c(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c6) = 0   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True

Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))

K tuples:

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Nil, z0, z1, z2) → c8

Defined Rule Symbols:

!EQ

Defined Pair Symbols:

!EQ', LOOP[ITE], LOOP

Compound Symbols:

c, c4, c5, c6, c7, c8

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

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

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))

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

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

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

POL(!EQ(x₁, x₂)) = 0   
POL(!EQ'(x₁, x₂)) = 0   
POL(0) = 0   
POL(Cons(x₁, x₂)) = [2] + x₂   
POL(False) = 0   
POL(LOOP(x₁, x₂, x₃, x₄)) = [2] + x₂ + x₄²   
POL(LOOP[ITE](x₁, x₂, x₃, x₄, x₅)) = x₃ + x₅²   
POL(Nil) = 0   
POL(S(x₁)) = 0   
POL(True) = 0   
POL(c(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c6) = 0   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True

Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c4(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP(Nil, z0, z1, z2) → c8

S tuples:none
K tuples:

LOOP(Cons(z0, z1), Nil, z2, z3) → c6
LOOP(Nil, z0, z1, z2) → c8
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c7(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))

Defined Rule Symbols:

!EQ

Defined Pair Symbols:

!EQ', LOOP[ITE], LOOP

Compound Symbols:

c, c4, c5, c6, c7, c8

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

The set S is empty

(12) BOUNDS(1, 1)