Runtime Complexity TRS:
The TRS R consists of the following rules:

lt(0, s(X)) → true
lt(s(X), 0) → false
lt(s(X), s(Y)) → lt(X, Y)
append(nil, Y) → Y
append(add(N, X), Y) → add(N, append(X, Y))
split(N, nil) → pair(nil, nil)
split(N, add(M, Y)) → f_1(split(N, Y), N, M, Y)
f_1(pair(X, Z), N, M, Y) → f_2(lt(N, M), N, M, Y, X, Z)
f_2(true, N, M, Y, X, Z) → pair(X, add(M, Z))
f_2(false, N, M, Y, X, Z) → pair(add(M, X), Z)
qsort(nil) → nil
qsort(add(N, X)) → f_3(split(N, X), N, X)
f_3(pair(Y, Z), N, X) → append(qsort(Y), add(X, qsort(Z)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → Y
append'(add'(N, X), Y) → add'(N, append'(X, Y))
split'(N, nil') → pair'(nil', nil')
split'(N, add'(M, Y)) → f_1'(split'(N, Y), N, M, Y)
f_1'(pair'(X, Z), N, M, Y) → f_2'(lt'(N, M), N, M, Y, X, Z)
f_2'(true', N, M, Y, X, Z) → pair'(X, add'(M, Z))
f_2'(false', N, M, Y, X, Z) → pair'(add'(M, X), Z)
qsort'(nil') → nil'
qsort'(add'(N, X)) → f_3'(split'(N, X), N, X)
f_3'(pair'(Y, Z), N, X) → append'(qsort'(Y), add'(X, qsort'(Z)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
f_1'/3
f_2'/1
f_2'/3
f_3'/1

Runtime Complexity TRS:
The TRS R consists of the following rules:

lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → Y
append'(add'(N, X), Y) → add'(N, append'(X, Y))
split'(N, nil') → pair'(nil', nil')
split'(N, add'(M, Y)) → f_1'(split'(N, Y), N, M)
f_1'(pair'(X, Z), N, M) → f_2'(lt'(N, M), M, X, Z)
f_2'(true', M, X, Z) → pair'(X, add'(M, Z))
f_2'(false', M, X, Z) → pair'(add'(M, X), Z)
qsort'(nil') → nil'
qsort'(add'(N, X)) → f_3'(split'(N, X), X)
f_3'(pair'(Y, Z), X) → append'(qsort'(Y), add'(X, qsort'(Z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → Y
append'(add'(N, X), Y) → add'(N, append'(X, Y))
split'(N, nil') → pair'(nil', nil')
split'(N, add'(M, Y)) → f_1'(split'(N, Y), N, M)
f_1'(pair'(X, Z), N, M) → f_2'(lt'(N, M), M, X, Z)
f_2'(true', M, X, Z) → pair'(X, add'(M, Z))
f_2'(false', M, X, Z) → pair'(add'(M, X), Z)
qsort'(nil') → nil'
qsort'(add'(N, X)) → f_3'(split'(N, X), X)
f_3'(pair'(Y, Z), X) → append'(qsort'(Y), add'(X, qsort'(Z)))

Types:
lt' :: 0':s':nil':add' → 0':s':nil':add' → true':false'
0' :: 0':s':nil':add'
s' :: 0':s':nil':add' → 0':s':nil':add'
true' :: true':false'
false' :: true':false'
append' :: 0':s':nil':add' → 0':s':nil':add' → 0':s':nil':add'
nil' :: 0':s':nil':add'
add' :: 0':s':nil':add' → 0':s':nil':add' → 0':s':nil':add'
split' :: 0':s':nil':add' → 0':s':nil':add' → pair'
pair' :: 0':s':nil':add' → 0':s':nil':add' → pair'
f_1' :: pair' → 0':s':nil':add' → 0':s':nil':add' → pair'
f_2' :: true':false' → 0':s':nil':add' → 0':s':nil':add' → 0':s':nil':add' → pair'
qsort' :: 0':s':nil':add' → 0':s':nil':add'
f_3' :: pair' → 0':s':nil':add' → 0':s':nil':add'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':add'2 :: 0':s':nil':add'
_hole_pair'3 :: pair'
_gen_0':s':nil':add'4 :: Nat → 0':s':nil':add'

Heuristically decided to analyse the following defined symbols:
lt', append', split', qsort'

They will be analysed ascendingly in the following order:
append' < qsort'
split' < qsort'

Generator Equations:
_gen_0':s':nil':add'4(0) ⇔ 0'
_gen_0':s':nil':add'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':add'4(x))

The following defined symbols remain to be analysed:
lt', append', split', qsort'

They will be analysed ascendingly in the following order:
append' < qsort'
split' < qsort'

Proved the following rewrite lemma:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)

Induction Base:
lt'(_gen_0':s':nil':add'4(0), _gen_0':s':nil':add'4(+(1, 0))) →_R^Ω(1)
true'

Induction Step:
lt'(_gen_0':s':nil':add'4(+(_$n7, 1)), _gen_0':s':nil':add'4(+(1, +(_$n7, 1)))) →_R^Ω(1)
lt'(_gen_0':s':nil':add'4(_$n7), _gen_0':s':nil':add'4(+(1, _$n7))) →_IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)

Generator Equations:
_gen_0':s':nil':add'4(0) ⇔ 0'
_gen_0':s':nil':add'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':add'4(x))

The following defined symbols remain to be analysed:
append', split', qsort'

They will be analysed ascendingly in the following order:
append' < qsort'
split' < qsort'

Could not prove a rewrite lemma for the defined symbol append'.

Lemmas:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)

Generator Equations:
_gen_0':s':nil':add'4(0) ⇔ 0'
_gen_0':s':nil':add'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':add'4(x))

The following defined symbols remain to be analysed:
split', qsort'

They will be analysed ascendingly in the following order:
split' < qsort'

Could not prove a rewrite lemma for the defined symbol split'.

Lemmas:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)

Generator Equations:
_gen_0':s':nil':add'4(0) ⇔ 0'
_gen_0':s':nil':add'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':add'4(x))

The following defined symbols remain to be analysed:
qsort'

Could not prove a rewrite lemma for the defined symbol qsort'.

Lemmas:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)

Generator Equations:
_gen_0':s':nil':add'4(0) ⇔ 0'
_gen_0':s':nil':add'4(+(x, 1)) ⇔ s'(_gen_0':s':nil':add'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
lt'(_gen_0':s':nil':add'4(_n6), _gen_0':s':nil':add'4(+(1, _n6))) → true', rt ∈ Ω(1 + _n6)