The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

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

fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0, x8) → True
leq#2(S(x12), 0) → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

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

fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
fold#3, insert_ord#2, leq#2

They will be analysed ascendingly in the following order:
insert_ord#2 < fold#3
leq#2 < insert_ord#2

(6) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

Generator Equations:
gen_Nil:Cons6_7(0) ⇔ Nil
gen_Nil:Cons6_7(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons6_7(x))
gen_0':S7_7(0) ⇔ 0'
gen_0':S7_7(+(x, 1)) ⇔ S(gen_0':S7_7(x))

The following defined symbols remain to be analysed:
leq#2, fold#3, insert_ord#2

They will be analysed ascendingly in the following order:
insert_ord#2 < fold#3
leq#2 < insert_ord#2

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

Induction Base:
leq#2(gen_0':S7_7(0), gen_0':S7_7(0)) →_R^Ω(1)
True

Induction Step:
leq#2(gen_0':S7_7(+(n9_7, 1)), gen_0':S7_7(+(n9_7, 1))) →_R^Ω(1)
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) →_IH
True

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

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

Lemmas:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

Generator Equations:
gen_Nil:Cons6_7(0) ⇔ Nil
gen_Nil:Cons6_7(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons6_7(x))
gen_0':S7_7(0) ⇔ 0'
gen_0':S7_7(+(x, 1)) ⇔ S(gen_0':S7_7(x))

The following defined symbols remain to be analysed:
insert_ord#2, fold#3

They will be analysed ascendingly in the following order:
insert_ord#2 < fold#3

(10) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol insert_ord#2.

(11) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

Lemmas:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

Generator Equations:
gen_Nil:Cons6_7(0) ⇔ Nil
gen_Nil:Cons6_7(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons6_7(x))
gen_0':S7_7(0) ⇔ 0'
gen_0':S7_7(+(x, 1)) ⇔ S(gen_0':S7_7(x))

The following defined symbols remain to be analysed:
fold#3

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol fold#3.

(13) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

Lemmas:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

Generator Equations:
gen_Nil:Cons6_7(0) ⇔ Nil
gen_Nil:Cons6_7(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons6_7(x))
gen_0':S7_7(0) ⇔ 0'
gen_0':S7_7(+(x, 1)) ⇔ S(gen_0':S7_7(x))

No more defined symbols left to analyse.

(14) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

(15) BOUNDS(n^1, INF)

(16) Obligation:

Innermost TRS:
Rules:
fold#3(insert_ord(x2), Nil) → Nil
fold#3(insert_ord(x6), Cons(x4, x2)) → insert_ord#2(x6, x4, fold#3(insert_ord(x6), x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x0, x5, x2) → Cons(x5, insert_ord#2(leq, x0, x2))
insert_ord#2(leq, x2, Nil) → Cons(x2, Nil)
insert_ord#2(leq, x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0', x8) → True
leq#2(S(x12), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x3) → fold#3(insert_ord(leq), x3)

Types:
fold#3 :: insert_ord → Nil:Cons → Nil:Cons
insert_ord :: leq → insert_ord
Nil :: Nil:Cons
Cons :: 0':S → Nil:Cons → Nil:Cons
insert_ord#2 :: leq → 0':S → Nil:Cons → Nil:Cons
cond_insert_ord_x_ys_1 :: True:False → 0':S → 0':S → Nil:Cons → Nil:Cons
True :: True:False
False :: True:False
leq :: leq
leq#2 :: 0':S → 0':S → True:False
0' :: 0':S
S :: 0':S → 0':S
main :: Nil:Cons → Nil:Cons
hole_Nil:Cons1_7 :: Nil:Cons
hole_insert_ord2_7 :: insert_ord
hole_leq3_7 :: leq
hole_0':S4_7 :: 0':S
hole_True:False5_7 :: True:False
gen_Nil:Cons6_7 :: Nat → Nil:Cons
gen_0':S7_7 :: Nat → 0':S

Lemmas:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

Generator Equations:
gen_Nil:Cons6_7(0) ⇔ Nil
gen_Nil:Cons6_7(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons6_7(x))
gen_0':S7_7(0) ⇔ 0'
gen_0':S7_7(+(x, 1)) ⇔ S(gen_0':S7_7(x))

No more defined symbols left to analyse.

(17) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
leq#2(gen_0':S7_7(n9_7), gen_0':S7_7(n9_7)) → True, rt ∈ Ω(1 + n9₇)

(18) BOUNDS(n^1, INF)