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

ack(Cons(x, xs), Nil) → ack(xs, Cons(Nil, Nil))
ack(Cons(x', xs'), Cons(x, xs)) → ack(xs', ack(Cons(x', xs'), xs))
ack(Nil, n) → Cons(Cons(Nil, Nil), n)
goal(m, n) → ack(m, n)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


ack'(Cons'(x, xs), Nil') → ack'(xs, Cons'(Nil', Nil'))
ack'(Cons'(x', xs'), Cons'(x, xs)) → ack'(xs', ack'(Cons'(x', xs'), xs))
ack'(Nil', n) → Cons'(Cons'(Nil', Nil'), n)
goal'(m, n) → ack'(m, n)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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


ack'(Cons'(xs), Nil') → ack'(xs, Cons'(Nil'))
ack'(Cons'(xs'), Cons'(xs)) → ack'(xs', ack'(Cons'(xs'), xs))
ack'(Nil', n) → Cons'(n)
goal'(m, n) → ack'(m, n)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
ack'(Cons'(xs), Nil') → ack'(xs, Cons'(Nil'))
ack'(Cons'(xs'), Cons'(xs)) → ack'(xs', ack'(Cons'(xs'), xs))
ack'(Nil', n) → Cons'(n)
goal'(m, n) → ack'(m, n)

Types:
ack' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
ack'

Rules:
ack'(Cons'(xs), Nil') → ack'(xs, Cons'(Nil'))
ack'(Cons'(xs'), Cons'(xs)) → ack'(xs', ack'(Cons'(xs'), xs))
ack'(Nil', n) → Cons'(n)
goal'(m, n) → ack'(m, n)

Types:
ack' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
ack'

Proved the following rewrite lemma:
ack'(_gen_Cons':Nil'2(1), _gen_Cons':Nil'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Induction Base:
ack'(_gen_Cons':Nil'2(1), _gen_Cons':Nil'2(+(1, 0)))

Induction Step:
ack'(_gen_Cons':Nil'2(1), _gen_Cons':Nil'2(+(1, +(_$n5, 1)))) →RΩ(1)
ack'(_gen_Cons':Nil'2(0), ack'(Cons'(_gen_Cons':Nil'2(0)), _gen_Cons':Nil'2(+(1, _$n5)))) →IH
ack'(_gen_Cons':Nil'2(0), _*3)

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

Rules:
ack'(Cons'(xs), Nil') → ack'(xs, Cons'(Nil'))
ack'(Cons'(xs'), Cons'(xs)) → ack'(xs', ack'(Cons'(xs'), xs))
ack'(Nil', n) → Cons'(n)
goal'(m, n) → ack'(m, n)

Types:
ack' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
ack'(_gen_Cons':Nil'2(1), _gen_Cons':Nil'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
ack'(_gen_Cons':Nil'2(1), _gen_Cons':Nil'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)