The Runtime Complexity (full) 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:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
fstsplit(s(n), cons(h, t)) →⁺ cons(h, fstsplit(n, t))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [n / s(n), t / cons(h, t)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

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

fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
if2(store, m, false) → process(app(map_f(self, nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(self, nil), store)), m)

S is empty.
Rewrite Strategy: FULL

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
cons/0
map_f/0
f/0
f/1

(6) Obligation:

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

fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

S is empty.
Rewrite Strategy: FULL

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

Infered types.

(8) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
fstsplit, sndsplit, leq, length, app, map_f, process

They will be analysed ascendingly in the following order:
fstsplit < process
sndsplit < process
leq < process
length < process
app < map_f
app < process
map_f < process

(10) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
fstsplit, sndsplit, leq, length, app, map_f, process

They will be analysed ascendingly in the following order:
fstsplit < process
sndsplit < process
leq < process
length < process
app < map_f
app < process
map_f < process

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

Induction Base:
fstsplit(gen_0':s6_0(0), gen_nil:cons:f5_0(0)) →_R^Ω(1)
nil

Induction Step:
fstsplit(gen_0':s6_0(+(n8_0, 1)), gen_nil:cons:f5_0(+(n8_0, 1))) →_R^Ω(1)
cons(fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0))) →_IH
cons(gen_nil:cons:f5_0(c9_0))

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

(12) Complex Obligation (BEST)

(13) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
sndsplit, leq, length, app, map_f, process

They will be analysed ascendingly in the following order:
sndsplit < process
leq < process
length < process
app < map_f
app < process
map_f < process

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)

Induction Base:
sndsplit(gen_0':s6_0(0), gen_nil:cons:f5_0(0)) →_R^Ω(1)
gen_nil:cons:f5_0(0)

Induction Step:
sndsplit(gen_0':s6_0(+(n526_0, 1)), gen_nil:cons:f5_0(+(n526_0, 1))) →_R^Ω(1)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) →_IH
gen_nil:cons:f5_0(0)

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

(15) Complex Obligation (BEST)

(16) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
leq, length, app, map_f, process

They will be analysed ascendingly in the following order:
leq < process
length < process
app < map_f
app < process
map_f < process

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)

Induction Base:
leq(gen_0':s6_0(0), gen_0':s6_0(0)) →_R^Ω(1)
true

Induction Step:
leq(gen_0':s6_0(+(n1102_0, 1)), gen_0':s6_0(+(n1102_0, 1))) →_R^Ω(1)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) →_IH
true

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

(18) Complex Obligation (BEST)

(19) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
length, app, map_f, process

They will be analysed ascendingly in the following order:
length < process
app < map_f
app < process
map_f < process

(20) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)

Induction Base:
length(gen_nil:cons:f5_0(0)) →_R^Ω(1)
0'

Induction Step:
length(gen_nil:cons:f5_0(+(n1461_0, 1))) →_R^Ω(1)
s(length(gen_nil:cons:f5_0(n1461_0))) →_IH
s(gen_0':s6_0(c1462_0))

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

(21) Complex Obligation (BEST)

(22) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
app, map_f, process

They will be analysed ascendingly in the following order:
app < map_f
app < process
map_f < process

(23) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)

Induction Base:
app(gen_nil:cons:f5_0(0), gen_nil:cons:f5_0(b)) →_R^Ω(1)
gen_nil:cons:f5_0(b)

Induction Step:
app(gen_nil:cons:f5_0(+(n1749_0, 1)), gen_nil:cons:f5_0(b)) →_R^Ω(1)
cons(app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b))) →_IH
cons(gen_nil:cons:f5_0(+(b, c1750_0)))

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

(24) Complex Obligation (BEST)

(25) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
map_f, process

They will be analysed ascendingly in the following order:
map_f < process

(26) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
map_f(gen_nil:cons:f5_0(+(1, n2646_0))) → *7_0, rt ∈ Ω(n2646₀)

Induction Base:
map_f(gen_nil:cons:f5_0(+(1, 0)))

Induction Step:
map_f(gen_nil:cons:f5_0(+(1, +(n2646_0, 1)))) →_R^Ω(1)
app(f, map_f(gen_nil:cons:f5_0(+(1, n2646_0)))) →_IH
app(f, *7_0)

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

(27) Complex Obligation (BEST)

(28) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)
map_f(gen_nil:cons:f5_0(+(1, n2646_0))) → *7_0, rt ∈ Ω(n2646₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

The following defined symbols remain to be analysed:
process

(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol process.

(30) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)
map_f(gen_nil:cons:f5_0(+(1, n2646_0))) → *7_0, rt ∈ Ω(n2646₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(32) BOUNDS(n^1, INF)

(33) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)
map_f(gen_nil:cons:f5_0(+(1, n2646_0))) → *7_0, rt ∈ Ω(n2646₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(34) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(35) BOUNDS(n^1, INF)

(36) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)
app(gen_nil:cons:f5_0(n1749_0), gen_nil:cons:f5_0(b)) → gen_nil:cons:f5_0(+(n1749_0, b)), rt ∈ Ω(1 + n1749₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(37) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(38) BOUNDS(n^1, INF)

(39) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)
length(gen_nil:cons:f5_0(n1461_0)) → gen_0':s6_0(n1461_0), rt ∈ Ω(1 + n1461₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(40) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(41) BOUNDS(n^1, INF)

(42) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)
leq(gen_0':s6_0(n1102_0), gen_0':s6_0(n1102_0)) → true, rt ∈ Ω(1 + n1102₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(43) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(44) BOUNDS(n^1, INF)

(45) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)
sndsplit(gen_0':s6_0(n526_0), gen_nil:cons:f5_0(n526_0)) → gen_nil:cons:f5_0(0), rt ∈ Ω(1 + n526₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(46) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(47) BOUNDS(n^1, INF)

(48) Obligation:

TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(t)) → cons(fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(t)) → s(length(t))
app(nil, x) → x
app(cons(t), x) → cons(app(t, x))
map_f(nil) → nil
map_f(cons(t)) → app(f, map_f(t))
process(store, m) → if1(store, m, leq(m, length(store)))
if1(store, m, true) → if2(store, m, empty(fstsplit(m, store)))
if1(store, m, false) → if3(store, m, empty(fstsplit(m, app(map_f(nil), store))))
if2(store, m, false) → process(app(map_f(nil), sndsplit(m, store)), m)
if3(store, m, false) → process(sndsplit(m, app(map_f(nil), store)), m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: nil:cons:f → nil:cons:f
f :: nil:cons:f
process :: nil:cons:f → 0':s → process:if1:if2:if3
if1 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if2 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
if3 :: nil:cons:f → 0':s → true:false → process:if1:if2:if3
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_process:if1:if2:if34_0 :: process:if1:if2:if3
gen_nil:cons:f5_0 :: Nat → nil:cons:f
gen_0':s6_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_nil:cons:f5_0(0) ⇔ nil
gen_nil:cons:f5_0(+(x, 1)) ⇔ cons(gen_nil:cons:f5_0(x))
gen_0':s6_0(0) ⇔ 0'
gen_0':s6_0(+(x, 1)) ⇔ s(gen_0':s6_0(x))

No more defined symbols left to analyse.

(49) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s6_0(n8_0), gen_nil:cons:f5_0(n8_0)) → gen_nil:cons:f5_0(n8_0), rt ∈ Ω(1 + n8₀)

(50) BOUNDS(n^1, INF)