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)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
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)))
Sliced the following arguments:
if'/0
<='/0
<='/1
Runtime Complexity TRS:
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'(.'(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)))
Infered types.
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'(.'(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)))
Types:
bsort' :: nil':.':if':0' → nil':.':if':0'
nil' :: nil':.':if':0'
.' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
last' :: nil':.':if':0' → nil':.':if':0'
bubble' :: nil':.':if':0' → nil':.':if':0'
butlast' :: nil':.':if':0' → nil':.':if':0'
if' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
0' :: nil':.':if':0'
_hole_nil':.':if':0'1 :: nil':.':if':0'
_gen_nil':.':if':0'2 :: Nat → nil':.':if':0'
Heuristically decided to analyse the following defined symbols:
bsort', last', bubble', butlast'
They will be analysed ascendingly in the following order:
last' < bsort'
bubble' < bsort'
butlast' < bsort'
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'(.'(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)))
Types:
bsort' :: nil':.':if':0' → nil':.':if':0'
nil' :: nil':.':if':0'
.' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
last' :: nil':.':if':0' → nil':.':if':0'
bubble' :: nil':.':if':0' → nil':.':if':0'
butlast' :: nil':.':if':0' → nil':.':if':0'
if' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
0' :: nil':.':if':0'
_hole_nil':.':if':0'1 :: nil':.':if':0'
_gen_nil':.':if':0'2 :: Nat → nil':.':if':0'
Generator Equations:
_gen_nil':.':if':0'2(0) ⇔ nil'
_gen_nil':.':if':0'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.':if':0'2(x))
The following defined symbols remain to be analysed:
last', bsort', bubble', butlast'
They will be analysed ascendingly in the following order:
last' < bsort'
bubble' < bsort'
butlast' < bsort'
Proved the following rewrite lemma:
last'(_gen_nil':.':if':0'2(+(1, _n4))) → _gen_nil':.':if':0'2(0), rt ∈ Ω(1 + n4)
Induction Base:
last'(_gen_nil':.':if':0'2(+(1, 0))) →RΩ(1)
nil'
Induction Step:
last'(_gen_nil':.':if':0'2(+(1, +(_$n5, 1)))) →RΩ(1)
last'(.'(nil', _gen_nil':.':if':0'2(_$n5))) →IH
_gen_nil':.':if':0'2(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
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'(.'(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)))
Types:
bsort' :: nil':.':if':0' → nil':.':if':0'
nil' :: nil':.':if':0'
.' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
last' :: nil':.':if':0' → nil':.':if':0'
bubble' :: nil':.':if':0' → nil':.':if':0'
butlast' :: nil':.':if':0' → nil':.':if':0'
if' :: nil':.':if':0' → nil':.':if':0' → nil':.':if':0'
0' :: nil':.':if':0'
_hole_nil':.':if':0'1 :: nil':.':if':0'
_gen_nil':.':if':0'2 :: Nat → nil':.':if':0'
Lemmas:
last'(_gen_nil':.':if':0'2(+(1, _n4))) → _gen_nil':.':if':0'2(0), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':.':if':0'2(0) ⇔ nil'
_gen_nil':.':if':0'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.':if':0'2(x))
The following defined symbols remain to be analysed:
bubble', bsort', butlast'
They will be analysed ascendingly in the following order:
bubble' < bsort'
butlast' < bsort'
Proved the following rewrite lemma:
bubble'(_gen_nil':.':if':0'2(+(2, _n505))) → _*3, rt ∈ Ω(2n)
Induction Base:
bubble'(_gen_nil':.':if':0'2(+(2, 0)))
Induction Step:
bubble'(_gen_nil':.':if':0'2(+(2, +(_$n506, 1)))) →RΩ(1)
if'(.'(nil', bubble'(.'(nil', _gen_nil':.':if':0'2(+(1, _$n506))))), .'(nil', bubble'(.'(nil', _gen_nil':.':if':0'2(+(1, _$n506)))))) →IH
if'(.'(nil', _*3), .'(nil', bubble'(.'(nil', _gen_nil':.':if':0'2(+(1, _$n506)))))) →IH
if'(.'(nil', _*3), .'(nil', _*3))
We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)