WORST_CASE(NON_POLY,?)
proof of input_cVt3xPQAeT.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(EXP, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 7 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 93.0 s]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [FINISHED, 2955 ms]
        (18) BOUNDS(EXP, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   bsort(nil) -> nil
   bsort(.(x, y)) -> last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
   bubble(nil) -> nil
   bubble(.(x, nil)) -> .(x, nil)
   bubble(.(x, .(y, z))) -> if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
   last(nil) -> 0
   last(.(x, nil)) -> x
   last(.(x, .(y, z))) -> last(.(y, z))
   butlast(nil) -> nil
   butlast(.(x, nil)) -> nil
   butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   bsort(nil) -> nil
   bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
   bubble(nil) -> nil
   bubble(.(z0, nil)) -> .(z0, nil)
   bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
   last(nil) -> 0
   last(.(z0, nil)) -> z0
   last(.(z0, .(z1, z2))) -> last(.(z1, z2))
   butlast(nil) -> nil
   butlast(.(z0, nil)) -> nil
   butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))
Tuples:
   BSORT(nil) -> c
   BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
   BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
   BUBBLE(nil) -> c3
   BUBBLE(.(z0, nil)) -> c4
   BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
   BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
   LAST(nil) -> c7
   LAST(.(z0, nil)) -> c8
   LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
   BUTLAST(nil) -> c10
   BUTLAST(.(z0, nil)) -> c11
   BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
S tuples:
   BSORT(nil) -> c
   BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
   BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
   BUBBLE(nil) -> c3
   BUBBLE(.(z0, nil)) -> c4
   BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
   BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
   LAST(nil) -> c7
   LAST(.(z0, nil)) -> c8
   LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
   BUTLAST(nil) -> c10
   BUTLAST(.(z0, nil)) -> c11
   BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
K tuples:none
Defined Rule Symbols:   bsort_1, bubble_1, last_1, butlast_1

Defined Pair Symbols:   BSORT_1, BUBBLE_1, LAST_1, BUTLAST_1

Compound Symbols:   c, c1_2, c2_4, c3, c4, c5_1, c6_1, c7, c8, c9_1, c10, c11, c12_1


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   BSORT(nil) -> c
   BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
   BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
   BUBBLE(nil) -> c3
   BUBBLE(.(z0, nil)) -> c4
   BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
   BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
   LAST(nil) -> c7
   LAST(.(z0, nil)) -> c8
   LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
   BUTLAST(nil) -> c10
   BUTLAST(.(z0, nil)) -> c11
   BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))

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

   bsort(nil) -> nil
   bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
   bubble(nil) -> nil
   bubble(.(z0, nil)) -> .(z0, nil)
   bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
   last(nil) -> 0
   last(.(z0, nil)) -> z0
   last(.(z0, .(z1, z2))) -> last(.(z1, z2))
   butlast(nil) -> nil
   butlast(.(z0, nil)) -> nil
   butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   BSORT(nil) -> c
   BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
   BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
   BUBBLE(nil) -> c3
   BUBBLE(.(z0, nil)) -> c4
   BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
   BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
   LAST(nil) -> c7
   LAST(.(z0, nil)) -> c8
   LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
   BUTLAST(nil) -> c10
   BUTLAST(.(z0, nil)) -> c11
   BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))

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

   bsort(nil) -> nil
   bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
   bubble(nil) -> nil
   bubble(.(z0, nil)) -> .(z0, nil)
   bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
   last(nil) -> 0'
   last(.(z0, nil)) -> z0
   last(.(z0, .(z1, z2))) -> last(.(z1, z2))
   butlast(nil) -> nil
   butlast(.(z0, nil)) -> nil
   butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
BSORT(nil) -> c
BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
BUBBLE(nil) -> c3
BUBBLE(.(z0, nil)) -> c4
BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
LAST(nil) -> c7
LAST(.(z0, nil)) -> c8
LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
BUTLAST(nil) -> c10
BUTLAST(.(z0, nil)) -> c11
BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
bsort(nil) -> nil
bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
bubble(nil) -> nil
bubble(.(z0, nil)) -> .(z0, nil)
bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
last(nil) -> 0'
last(.(z0, nil)) -> z0
last(.(z0, .(z1, z2))) -> last(.(z1, z2))
butlast(nil) -> nil
butlast(.(z0, nil)) -> nil
butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Types:
BSORT :: nil:.:if:0' -> c:c1:c2
nil :: nil:.:if:0'
c :: c:c1:c2
. :: nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
c1 :: c7:c8:c9 -> c3:c4:c5:c6 -> c:c1:c2
LAST :: nil:.:if:0' -> c7:c8:c9
bubble :: nil:.:if:0' -> nil:.:if:0'
bsort :: nil:.:if:0' -> nil:.:if:0'
butlast :: nil:.:if:0' -> nil:.:if:0'
BUBBLE :: nil:.:if:0' -> c3:c4:c5:c6
c2 :: c7:c8:c9 -> c:c1:c2 -> c10:c11:c12 -> c3:c4:c5:c6 -> c:c1:c2
BUTLAST :: nil:.:if:0' -> c10:c11:c12
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
last :: nil:.:if:0' -> nil:.:if:0'
if :: <= -> nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
<= :: nil:.:if:0' -> nil:.:if:0' -> <=
0' :: nil:.:if:0'
hole_c:c1:c21_13 :: c:c1:c2
hole_nil:.:if:0'2_13 :: nil:.:if:0'
hole_c7:c8:c93_13 :: c7:c8:c9
hole_c3:c4:c5:c64_13 :: c3:c4:c5:c6
hole_c10:c11:c125_13 :: c10:c11:c12
hole_<=6_13 :: <=
gen_c:c1:c27_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'8_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c99_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c610_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1211_13 :: Nat -> c10:c11:c12

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
BSORT, LAST, bubble, bsort, butlast, BUBBLE, BUTLAST, last

They will be analysed ascendingly in the following order:
LAST < BSORT
bubble < BSORT
bsort < BSORT
butlast < BSORT
BUBBLE < BSORT
BUTLAST < BSORT
bubble < bsort
butlast < bsort
last < bsort

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
BSORT(nil) -> c
BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
BUBBLE(nil) -> c3
BUBBLE(.(z0, nil)) -> c4
BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
LAST(nil) -> c7
LAST(.(z0, nil)) -> c8
LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
BUTLAST(nil) -> c10
BUTLAST(.(z0, nil)) -> c11
BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
bsort(nil) -> nil
bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
bubble(nil) -> nil
bubble(.(z0, nil)) -> .(z0, nil)
bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
last(nil) -> 0'
last(.(z0, nil)) -> z0
last(.(z0, .(z1, z2))) -> last(.(z1, z2))
butlast(nil) -> nil
butlast(.(z0, nil)) -> nil
butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Types:
BSORT :: nil:.:if:0' -> c:c1:c2
nil :: nil:.:if:0'
c :: c:c1:c2
. :: nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
c1 :: c7:c8:c9 -> c3:c4:c5:c6 -> c:c1:c2
LAST :: nil:.:if:0' -> c7:c8:c9
bubble :: nil:.:if:0' -> nil:.:if:0'
bsort :: nil:.:if:0' -> nil:.:if:0'
butlast :: nil:.:if:0' -> nil:.:if:0'
BUBBLE :: nil:.:if:0' -> c3:c4:c5:c6
c2 :: c7:c8:c9 -> c:c1:c2 -> c10:c11:c12 -> c3:c4:c5:c6 -> c:c1:c2
BUTLAST :: nil:.:if:0' -> c10:c11:c12
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
last :: nil:.:if:0' -> nil:.:if:0'
if :: <= -> nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
<= :: nil:.:if:0' -> nil:.:if:0' -> <=
0' :: nil:.:if:0'
hole_c:c1:c21_13 :: c:c1:c2
hole_nil:.:if:0'2_13 :: nil:.:if:0'
hole_c7:c8:c93_13 :: c7:c8:c9
hole_c3:c4:c5:c64_13 :: c3:c4:c5:c6
hole_c10:c11:c125_13 :: c10:c11:c12
hole_<=6_13 :: <=
gen_c:c1:c27_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'8_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c99_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c610_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1211_13 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c27_13(0) <=> c
gen_c:c1:c27_13(+(x, 1)) <=> c2(c7, gen_c:c1:c27_13(x), c10, c3)
gen_nil:.:if:0'8_13(0) <=> nil
gen_nil:.:if:0'8_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'8_13(x))
gen_c7:c8:c99_13(0) <=> c7
gen_c7:c8:c99_13(+(x, 1)) <=> c9(gen_c7:c8:c99_13(x))
gen_c3:c4:c5:c610_13(0) <=> c3
gen_c3:c4:c5:c610_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c610_13(x))
gen_c10:c11:c1211_13(0) <=> c10
gen_c10:c11:c1211_13(+(x, 1)) <=> c12(gen_c10:c11:c1211_13(x))


The following defined symbols remain to be analysed:
LAST, BSORT, bubble, bsort, butlast, BUBBLE, BUTLAST, last

They will be analysed ascendingly in the following order:
LAST < BSORT
bubble < BSORT
bsort < BSORT
butlast < BSORT
BUBBLE < BSORT
BUTLAST < BSORT
bubble < bsort
butlast < bsort
last < bsort

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LAST(gen_nil:.:if:0'8_13(+(2, n13_13))) -> *12_13, rt in Omega(n13_13)

Induction Base:
LAST(gen_nil:.:if:0'8_13(+(2, 0)))

Induction Step:
LAST(gen_nil:.:if:0'8_13(+(2, +(n13_13, 1)))) ->_R^Omega(1)
c9(LAST(.(nil, gen_nil:.:if:0'8_13(+(1, n13_13))))) ->_IH
c9(*12_13)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
BSORT(nil) -> c
BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
BUBBLE(nil) -> c3
BUBBLE(.(z0, nil)) -> c4
BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
LAST(nil) -> c7
LAST(.(z0, nil)) -> c8
LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
BUTLAST(nil) -> c10
BUTLAST(.(z0, nil)) -> c11
BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
bsort(nil) -> nil
bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
bubble(nil) -> nil
bubble(.(z0, nil)) -> .(z0, nil)
bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
last(nil) -> 0'
last(.(z0, nil)) -> z0
last(.(z0, .(z1, z2))) -> last(.(z1, z2))
butlast(nil) -> nil
butlast(.(z0, nil)) -> nil
butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Types:
BSORT :: nil:.:if:0' -> c:c1:c2
nil :: nil:.:if:0'
c :: c:c1:c2
. :: nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
c1 :: c7:c8:c9 -> c3:c4:c5:c6 -> c:c1:c2
LAST :: nil:.:if:0' -> c7:c8:c9
bubble :: nil:.:if:0' -> nil:.:if:0'
bsort :: nil:.:if:0' -> nil:.:if:0'
butlast :: nil:.:if:0' -> nil:.:if:0'
BUBBLE :: nil:.:if:0' -> c3:c4:c5:c6
c2 :: c7:c8:c9 -> c:c1:c2 -> c10:c11:c12 -> c3:c4:c5:c6 -> c:c1:c2
BUTLAST :: nil:.:if:0' -> c10:c11:c12
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
last :: nil:.:if:0' -> nil:.:if:0'
if :: <= -> nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
<= :: nil:.:if:0' -> nil:.:if:0' -> <=
0' :: nil:.:if:0'
hole_c:c1:c21_13 :: c:c1:c2
hole_nil:.:if:0'2_13 :: nil:.:if:0'
hole_c7:c8:c93_13 :: c7:c8:c9
hole_c3:c4:c5:c64_13 :: c3:c4:c5:c6
hole_c10:c11:c125_13 :: c10:c11:c12
hole_<=6_13 :: <=
gen_c:c1:c27_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'8_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c99_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c610_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1211_13 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c27_13(0) <=> c
gen_c:c1:c27_13(+(x, 1)) <=> c2(c7, gen_c:c1:c27_13(x), c10, c3)
gen_nil:.:if:0'8_13(0) <=> nil
gen_nil:.:if:0'8_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'8_13(x))
gen_c7:c8:c99_13(0) <=> c7
gen_c7:c8:c99_13(+(x, 1)) <=> c9(gen_c7:c8:c99_13(x))
gen_c3:c4:c5:c610_13(0) <=> c3
gen_c3:c4:c5:c610_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c610_13(x))
gen_c10:c11:c1211_13(0) <=> c10
gen_c10:c11:c1211_13(+(x, 1)) <=> c12(gen_c10:c11:c1211_13(x))


The following defined symbols remain to be analysed:
LAST, BSORT, bubble, bsort, butlast, BUBBLE, BUTLAST, last

They will be analysed ascendingly in the following order:
LAST < BSORT
bubble < BSORT
bsort < BSORT
butlast < BSORT
BUBBLE < BSORT
BUTLAST < BSORT
bubble < bsort
butlast < bsort
last < bsort

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
BSORT(nil) -> c
BSORT(.(z0, z1)) -> c1(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BUBBLE(.(z0, z1)))
BSORT(.(z0, z1)) -> c2(LAST(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1)))))), BSORT(butlast(bubble(.(z0, z1)))), BUTLAST(bubble(.(z0, z1))), BUBBLE(.(z0, z1)))
BUBBLE(nil) -> c3
BUBBLE(.(z0, nil)) -> c4
BUBBLE(.(z0, .(z1, z2))) -> c5(BUBBLE(.(z0, z2)))
BUBBLE(.(z0, .(z1, z2))) -> c6(BUBBLE(.(z1, z2)))
LAST(nil) -> c7
LAST(.(z0, nil)) -> c8
LAST(.(z0, .(z1, z2))) -> c9(LAST(.(z1, z2)))
BUTLAST(nil) -> c10
BUTLAST(.(z0, nil)) -> c11
BUTLAST(.(z0, .(z1, z2))) -> c12(BUTLAST(.(z1, z2)))
bsort(nil) -> nil
bsort(.(z0, z1)) -> last(.(bubble(.(z0, z1)), bsort(butlast(bubble(.(z0, z1))))))
bubble(nil) -> nil
bubble(.(z0, nil)) -> .(z0, nil)
bubble(.(z0, .(z1, z2))) -> if(<=(z0, z1), .(z1, bubble(.(z0, z2))), .(z0, bubble(.(z1, z2))))
last(nil) -> 0'
last(.(z0, nil)) -> z0
last(.(z0, .(z1, z2))) -> last(.(z1, z2))
butlast(nil) -> nil
butlast(.(z0, nil)) -> nil
butlast(.(z0, .(z1, z2))) -> .(z0, butlast(.(z1, z2)))

Types:
BSORT :: nil:.:if:0' -> c:c1:c2
nil :: nil:.:if:0'
c :: c:c1:c2
. :: nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
c1 :: c7:c8:c9 -> c3:c4:c5:c6 -> c:c1:c2
LAST :: nil:.:if:0' -> c7:c8:c9
bubble :: nil:.:if:0' -> nil:.:if:0'
bsort :: nil:.:if:0' -> nil:.:if:0'
butlast :: nil:.:if:0' -> nil:.:if:0'
BUBBLE :: nil:.:if:0' -> c3:c4:c5:c6
c2 :: c7:c8:c9 -> c:c1:c2 -> c10:c11:c12 -> c3:c4:c5:c6 -> c:c1:c2
BUTLAST :: nil:.:if:0' -> c10:c11:c12
c3 :: c3:c4:c5:c6
c4 :: c3:c4:c5:c6
c5 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c6 :: c3:c4:c5:c6 -> c3:c4:c5:c6
c7 :: c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
last :: nil:.:if:0' -> nil:.:if:0'
if :: <= -> nil:.:if:0' -> nil:.:if:0' -> nil:.:if:0'
<= :: nil:.:if:0' -> nil:.:if:0' -> <=
0' :: nil:.:if:0'
hole_c:c1:c21_13 :: c:c1:c2
hole_nil:.:if:0'2_13 :: nil:.:if:0'
hole_c7:c8:c93_13 :: c7:c8:c9
hole_c3:c4:c5:c64_13 :: c3:c4:c5:c6
hole_c10:c11:c125_13 :: c10:c11:c12
hole_<=6_13 :: <=
gen_c:c1:c27_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'8_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c99_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c610_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1211_13 :: Nat -> c10:c11:c12


Lemmas:
LAST(gen_nil:.:if:0'8_13(+(2, n13_13))) -> *12_13, rt in Omega(n13_13)


Generator Equations:
gen_c:c1:c27_13(0) <=> c
gen_c:c1:c27_13(+(x, 1)) <=> c2(c7, gen_c:c1:c27_13(x), c10, c3)
gen_nil:.:if:0'8_13(0) <=> nil
gen_nil:.:if:0'8_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'8_13(x))
gen_c7:c8:c99_13(0) <=> c7
gen_c7:c8:c99_13(+(x, 1)) <=> c9(gen_c7:c8:c99_13(x))
gen_c3:c4:c5:c610_13(0) <=> c3
gen_c3:c4:c5:c610_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c610_13(x))
gen_c10:c11:c1211_13(0) <=> c10
gen_c10:c11:c1211_13(+(x, 1)) <=> c12(gen_c10:c11:c1211_13(x))


The following defined symbols remain to be analysed:
bubble, BSORT, bsort, butlast, BUBBLE, BUTLAST, last

They will be analysed ascendingly in the following order:
bubble < BSORT
bsort < BSORT
butlast < BSORT
BUBBLE < BSORT
BUTLAST < BSORT
bubble < bsort
butlast < bsort
last < bsort

----------------------------------------

(17) RewriteLemmaProof (FINISHED)
Proved the following rewrite lemma:
bubble(gen_nil:.:if:0'8_13(+(2, n73459_13))) -> *12_13, rt in Omega(EXP)

Induction Base:
bubble(gen_nil:.:if:0'8_13(+(2, 0)))

Induction Step:
bubble(gen_nil:.:if:0'8_13(+(2, +(n73459_13, 1)))) ->_R^Omega(0)
if(<=(nil, nil), .(nil, bubble(.(nil, gen_nil:.:if:0'8_13(+(1, n73459_13))))), .(nil, bubble(.(nil, gen_nil:.:if:0'8_13(+(1, n73459_13)))))) ->_IH
if(<=(nil, nil), .(nil, *12_13), .(nil, bubble(.(nil, gen_nil:.:if:0'8_13(+(1, n73459_13)))))) ->_IH
if(<=(nil, nil), .(nil, *12_13), .(nil, *12_13))

We have rt in EXP and sz in O(n). Thus, we have irc_R in EXP
----------------------------------------

(18)
BOUNDS(EXP, INF)