Runtime Complexity (innermost) proof of /tmp/tmpazUG0P/bubblesort.xml

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), 8 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CdtProblem

↳11 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtUsableRulesProof (⇔, 0 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 192 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 61 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 341 ms)

↳22 CdtProblem

↳23 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳24 CdtProblem

↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1490 ms)

↳26 CdtProblem

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

↳28 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:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +(S(0), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0
bubble(x, Nil) → Cons(x, Nil)
bsort(0, xs) → xs
bubblesort(xs) → bsort(len(xs), xs)

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

+(x, S(0)) → S(x)
+(S(0), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

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:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +(S(0), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0
bubble(x, Nil) → Cons(x, Nil)
bsort(0, xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+(x, S(0)) → S(x)
+(S(0), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BSORT(0, z0) → c1
LEN(Cons(z0, z1)) → c2(+'(S(0), len(z1)), LEN(z1))
LEN(Nil) → c3
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLE(z0, Nil) → c5
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
+'(z0, S(0)) → c7
+'(S(0), z0) → c8
<'(S(z0), S(z1)) → c9(<'(z0, z1))
<'(0, S(z0)) → c10
<'(z0, 0) → c11
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BSORT(0, z0) → c1
LEN(Cons(z0, z1)) → c2(+'(S(0), len(z1)), LEN(z1))
LEN(Nil) → c3
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLE(z0, Nil) → c5
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
+'(z0, S(0)) → c7
+'(S(0), z0) → c8
<'(S(z0), S(z1)) → c9(<'(z0, z1))
<'(0, S(z0)) → c10
<'(z0, 0) → c11
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, LEN, BUBBLE, BUBBLESORT, +', <', BUBBLE[ITE][FALSE][ITE]

Compound Symbols:

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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing nodes:

+'(S(0), z0) → c8
LEN(Nil) → c3
<'(0, S(z0)) → c10
<'(z0, 0) → c11
+'(z0, S(0)) → c7
BSORT(0, z0) → c1
BUBBLE(z0, Nil) → c5

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(+'(S(0), len(z1)), LEN(z1))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(+'(S(0), len(z1)), LEN(z1))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, LEN, BUBBLE, BUBBLESORT, <', BUBBLE[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c4, c6, c9, c12, c13

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLESORT(z0) → c6(BSORT(len(z0), z0), LEN(z0))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))

K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, BUBBLE, BUBBLESORT, <', BUBBLE[ITE][FALSE][ITE], LEN

Compound Symbols:

c, c4, c6, c9, c12, c13, c2

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

Split RHS of tuples not part of any SCC

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
BUBBLESORT(z0) → c1(LEN(z0))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
BUBBLESORT(z0) → c1(LEN(z0))

K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

BUBBLESORT(z0) → c1(LEN(z0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

K tuples:none
Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubblesort(z0) → bsort(len(z0), z0)
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

Defined Rule Symbols:

bsort, len, bubble, bubblesort, +, <, bubble[Ite][False][Ite]

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

(15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

bsort(S(z0), Cons(z1, z2)) → bsort(z0, bubble(z1, z2))
bsort(0, z0) → z0
bubblesort(z0) → bsort(len(z0), z0)

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

LEN(Cons(z0, z1)) → c2(LEN(z1))

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

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

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

POL(+(x₁, x₂)) = 0
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(BSORT(x₁, x₂)) = 0
POL(BUBBLE(x₁, x₂)) = 0
POL(BUBBLESORT(x₁)) = 0
POL(BUBBLE[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(Cons(x₁, x₂)) = [1] + x₂
POL(False) = 0
POL(LEN(x₁)) = x₁
POL(Nil) = 0
POL(S(x₁)) = 0
POL(True) = 0
POL(bubble(x₁, x₂)) = 0
POL(bubble[Ite][False][Ite](x₁, x₂, x₃)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(len(x₁)) = 0

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
LEN(Cons(z0, z1)) → c2(LEN(z1))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))

We considered the (Usable) Rules:

len(Nil) → 0
len(Cons(z0, z1)) → +(S(0), len(z1))
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

And the Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

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

POL(+(x₁, x₂)) = x₁ + x₂
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(BSORT(x₁, x₂)) = [1] + x₁
POL(BUBBLE(x₁, x₂)) = 0
POL(BUBBLESORT(x₁)) = [1] + x₁
POL(BUBBLE[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(Cons(x₁, x₂)) = [1] + x₂
POL(False) = 0
POL(LEN(x₁)) = 0
POL(Nil) = 0
POL(S(x₁)) = [1] + x₁
POL(True) = 0
POL(bubble(x₁, x₂)) = 0
POL(bubble[Ite][False][Ite](x₁, x₂, x₃)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(len(x₁)) = x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))

We considered the (Usable) Rules:

bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
len(Nil) → 0
bubble(z0, Nil) → Cons(z0, Nil)
len(Cons(z0, z1)) → +(S(0), len(z1))
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))

And the Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

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

POL(+(x₁, x₂)) = x₁ + x₂
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = 0
POL(BSORT(x₁, x₂)) = [1] + x₁·x₂
POL(BUBBLE(x₁, x₂)) = [2] + x₂
POL(BUBBLESORT(x₁)) = [2] + [2]x₁ + [2]x₁²
POL(BUBBLE[ITE][FALSE][ITE](x₁, x₂, x₃)) = [1] + x₃
POL(Cons(x₁, x₂)) = [1] + x₂
POL(False) = 0
POL(LEN(x₁)) = 0
POL(Nil) = 0
POL(S(x₁)) = [2] + x₁
POL(True) = 0
POL(bubble(x₁, x₂)) = [1] + x₂
POL(bubble[Ite][False][Ite](x₁, x₂, x₃)) = [1] + x₃
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(len(x₁)) = [2]x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:

<'(S(z0), S(z1)) → c9(<'(z0, z1))

K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

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

<'(S(z0), S(z1)) → c9(<'(z0, z1))

We considered the (Usable) Rules:

bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
len(Nil) → 0
bubble(z0, Nil) → Cons(z0, Nil)
len(Cons(z0, z1)) → +(S(0), len(z1))
bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))

And the Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

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

POL(+(x₁, x₂)) = [1] + x₁·x₂
POL(0) = 0
POL(<(x₁, x₂)) = 0
POL(<'(x₁, x₂)) = x₂
POL(BSORT(x₁, x₂)) = x₁·x₂²
POL(BUBBLE(x₁, x₂)) = [1] + x₂ + x₂²
POL(BUBBLESORT(x₁)) = x₁ + x₁² + x₁³
POL(BUBBLE[ITE][FALSE][ITE](x₁, x₂, x₃)) = x₃²
POL(Cons(x₁, x₂)) = [1] + x₁ + x₂
POL(False) = 0
POL(LEN(x₁)) = 0
POL(Nil) = 0
POL(S(x₁)) = [1] + x₁
POL(True) = 0
POL(bubble(x₁, x₂)) = [1] + x₁ + x₂
POL(bubble[Ite][False][Ite](x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c9(x₁)) = x₁
POL(len(x₁)) = [1] + x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

bubble(z0, Cons(z1, z2)) → bubble[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
bubble(z0, Nil) → Cons(z0, Nil)
bubble[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, bubble(z0, z2))
bubble[Ite][False][Ite](True, z0, Cons(z1, z2)) → Cons(z0, bubble(z1, z2))
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
len(Cons(z0, z1)) → +(S(0), len(z1))
len(Nil) → 0
+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)

Tuples:

BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c9(<'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BUBBLESORT(z0) → c1(BSORT(len(z0), z0))

S tuples:none
K tuples:

BUBBLESORT(z0) → c1(BSORT(len(z0), z0))
LEN(Cons(z0, z1)) → c2(LEN(z1))
BSORT(S(z0), Cons(z1, z2)) → c(BSORT(z0, bubble(z1, z2)), BUBBLE(z1, z2))
BUBBLE(z0, Cons(z1, z2)) → c4(BUBBLE[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
BUBBLE[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c12(BUBBLE(z0, z2))
BUBBLE[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c13(BUBBLE(z1, z2))
<'(S(z0), S(z1)) → c9(<'(z0, z1))

Defined Rule Symbols:

bubble, bubble[Ite][False][Ite], <, len, +

Defined Pair Symbols:

BSORT, BUBBLE, <', BUBBLE[ITE][FALSE][ITE], LEN, BUBBLESORT

Compound Symbols:

c, c4, c9, c12, c13, c2, c1

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

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

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

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

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

(10) Obligation:

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(12) Obligation:

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

(14) Obligation:

(15) CdtUsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) BOUNDS(1, 1)