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

double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'

Heuristically decided to analyse the following defined symbols:
permute', ack', plus'

They will be analysed ascendingly in the following order:
ack' < permute'
plus' < ack'

Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'

Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))

The following defined symbols remain to be analysed:
plus', permute', ack'

They will be analysed ascendingly in the following order:
ack' < permute'
plus' < ack'

Proved the following rewrite lemma:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)

Induction Base:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, 0))))

Induction Step:
plus'(_gen_false':true':0':s'3(_a1642), _gen_false':true':0':s'3(+(2, *(2, +(_\$n6, 1))))) →RΩ(1)
s'(plus'(s'(_gen_false':true':0':s'3(_a1642)), _gen_false':true':0':s'3(+(2, *(2, _\$n6))))) →RΩ(1)
s'(plus'(_gen_false':true':0':s'3(_a1642), s'(_gen_false':true':0':s'3(+(2, *(2, _\$n6)))))) →RΩ(1)
s'(s'(plus'(s'(_gen_false':true':0':s'3(_a1642)), _gen_false':true':0':s'3(+(1, *(2, _\$n6)))))) →RΩ(1)
s'(s'(plus'(_gen_false':true':0':s'3(_a1642), s'(_gen_false':true':0':s'3(+(1, *(2, _\$n6))))))) →IH
s'(s'(_*4))

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

Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'

Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))

The following defined symbols remain to be analysed:
ack', permute'

They will be analysed ascendingly in the following order:
ack' < permute'

Proved the following rewrite lemma:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)

Induction Base:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, 0)))

Induction Step:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, +(_\$n4751, 1)))) →RΩ(1)
ack'(_gen_false':true':0':s'3(0), ack'(s'(_gen_false':true':0':s'3(0)), _gen_false':true':0':s'3(+(1, _\$n4751)))) →IH
ack'(_gen_false':true':0':s'3(0), _*4)

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

Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'

Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)

Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))

The following defined symbols remain to be analysed:
permute'

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

Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'

Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'

Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)

Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)