WORST_CASE(NON_POLY,?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

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


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

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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

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

(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) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
if/0
<=/0
<=/1

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

(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(.(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))
Infered 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(.(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'
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
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'7_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c98_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c69_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1210_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(.(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'
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
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'7_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c98_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c69_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1210_13 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(c7, gen_c:c1:c26_13(x), c10, c3)
gen_nil:.:if:0'7_13(0) <=> nil
gen_nil:.:if:0'7_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'7_13(x))
gen_c7:c8:c98_13(0) <=> c7
gen_c7:c8:c98_13(+(x, 1)) <=> c9(gen_c7:c8:c98_13(x))
gen_c3:c4:c5:c69_13(0) <=> c3
gen_c3:c4:c5:c69_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c69_13(x))
gen_c10:c11:c1210_13(0) <=> c10
gen_c10:c11:c1210_13(+(x, 1)) <=> c12(gen_c10:c11:c1210_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'7_13(+(2, n12_13))) -> *11_13, rt in Omega(n12_13)

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

Induction Step:
LAST(gen_nil:.:if:0'7_13(+(2, +(n12_13, 1)))) ->_R^Omega(1)
c9(LAST(.(nil, gen_nil:.:if:0'7_13(+(1, n12_13))))) ->_IH
c9(*11_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(.(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'
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
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'7_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c98_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c69_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1210_13 :: Nat -> c10:c11:c12


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(c7, gen_c:c1:c26_13(x), c10, c3)
gen_nil:.:if:0'7_13(0) <=> nil
gen_nil:.:if:0'7_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'7_13(x))
gen_c7:c8:c98_13(0) <=> c7
gen_c7:c8:c98_13(+(x, 1)) <=> c9(gen_c7:c8:c98_13(x))
gen_c3:c4:c5:c69_13(0) <=> c3
gen_c3:c4:c5:c69_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c69_13(x))
gen_c10:c11:c1210_13(0) <=> c10
gen_c10:c11:c1210_13(+(x, 1)) <=> c12(gen_c10:c11:c1210_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(.(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'
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
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_nil:.:if:0'7_13 :: Nat -> nil:.:if:0'
gen_c7:c8:c98_13 :: Nat -> c7:c8:c9
gen_c3:c4:c5:c69_13 :: Nat -> c3:c4:c5:c6
gen_c10:c11:c1210_13 :: Nat -> c10:c11:c12


Lemmas:
LAST(gen_nil:.:if:0'7_13(+(2, n12_13))) -> *11_13, rt in Omega(n12_13)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(c7, gen_c:c1:c26_13(x), c10, c3)
gen_nil:.:if:0'7_13(0) <=> nil
gen_nil:.:if:0'7_13(+(x, 1)) <=> .(nil, gen_nil:.:if:0'7_13(x))
gen_c7:c8:c98_13(0) <=> c7
gen_c7:c8:c98_13(+(x, 1)) <=> c9(gen_c7:c8:c98_13(x))
gen_c3:c4:c5:c69_13(0) <=> c3
gen_c3:c4:c5:c69_13(+(x, 1)) <=> c5(gen_c3:c4:c5:c69_13(x))
gen_c10:c11:c1210_13(0) <=> c10
gen_c10:c11:c1210_13(+(x, 1)) <=> c12(gen_c10:c11:c1210_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'7_13(+(2, n73458_13))) -> *11_13, rt in Omega(EXP)

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

Induction Step:
bubble(gen_nil:.:if:0'7_13(+(2, +(n73458_13, 1)))) ->_R^Omega(0)
if(.(nil, bubble(.(nil, gen_nil:.:if:0'7_13(+(1, n73458_13))))), .(nil, bubble(.(nil, gen_nil:.:if:0'7_13(+(1, n73458_13)))))) ->_IH
if(.(nil, *11_13), .(nil, bubble(.(nil, gen_nil:.:if:0'7_13(+(1, n73458_13)))))) ->_IH
if(.(nil, *11_13), .(nil, *11_13))

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

(18)
BOUNDS(EXP, INF)