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
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
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
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
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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'

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'

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → 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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'

Generator Equations:

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:

Induction Base:
true'

Induction Step:
true'

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

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → 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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'

Lemmas:

Generator Equations:

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'.

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → 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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'

Lemmas:

Generator Equations:

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'.

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → 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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
qsort'

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

Rules:
lt'(0', s'(X)) → true'
lt'(s'(X), 0') → false'
lt'(s'(X), s'(Y)) → lt'(X, Y)
append'(nil', Y) → 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:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'
_hole_pair'3 :: pair'