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

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳6 CdtProblem
↳7 CdtUsableRulesProof (⇔, 0 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 120 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 144 ms)
↳12 CdtProblem
↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CdtProblem
↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1231 ms)
↳16 CdtProblem
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 BOUNDS(1, 1)

(0) Obligation:

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


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) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

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


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)
!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

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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)
!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)
Tuples:

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

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

loop, match1, !EQ, loop[Ite]

Defined Pair Symbols:

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

Compound Symbols:

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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

MATCH1(z0, z1) → c3(LOOP(z0, z1, z0, z1))
Removed 5 trailing nodes:

LOOP(Cons(z0, z1), Nil, z2, z3) → c
!EQ'(0, 0) → c7
!EQ'(S(z0), 0) → c6
!EQ'(0, S(z0)) → c5
LOOP(Nil, z0, z1, z2) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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)
!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)
Tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
K tuples:none
Defined Rule Symbols:

loop, match1, !EQ, loop[Ite]

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

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

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

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
K tuples:none
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

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

LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
We considered the (Usable) Rules:none
And the Tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = 0   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(LOOP(x1, x2, x3, x4)) = x4   
POL(LOOP[ITE](x1, x2, x3, x4, x5)) = x5   
POL(S(x1)) = 0   
POL(True) = 0   
POL(c1(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   

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

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
K tuples:

LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

(11) 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[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
We considered the (Usable) Rules:none
And the Tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = 0   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(LOOP(x1, x2, x3, x4)) = [1] + x1 + x2 + x4 + x42 + x3·x4   
POL(LOOP[ITE](x1, x2, x3, x4, x5)) = [1] + x2 + x3 + x5 + x52 + x4·x5   
POL(S(x1)) = [2]   
POL(True) = 0   
POL(c1(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   

(12) 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:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
K tuples:

LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

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

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

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))

(14) 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:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
K tuples:

LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

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

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = [1] + x1   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(False) = 0   
POL(LOOP(x1, x2, x3, x4)) = x1 + x3·x4 + x12 + x32·x4   
POL(LOOP[ITE](x1, x2, x3, x4, x5)) = x4·x5 + x22 + x42·x5   
POL(S(x1)) = [1] + x1   
POL(True) = 0   
POL(c1(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   

(16) 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:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
S tuples:none
K tuples:

LOOP[ITE](False, z0, z1, z2, Cons(z3, z4)) → c8(LOOP(z2, z4, z2, z4))
LOOP[ITE](True, Cons(z0, z1), Cons(z2, z3), z4, z5) → c9(LOOP(z1, z3, z4, z5))
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c1(LOOP[ITE](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1))
Defined Rule Symbols:

!EQ

Defined Pair Symbols:

LOOP, !EQ', LOOP[ITE]

Compound Symbols:

c1, c4, c8, c9

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

The set S is empty

(18) BOUNDS(1, 1)