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

p(s(N)) → N
+(N, 0) → N
+(s(N), s(M)) → s(s(+(N, M)))
*(N, 0) → 0
*(s(N), s(M)) → s(+(N, +(M, *(N, M))))
gt(0, M) → False
gt(NzN, 0) → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0) → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0, N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0)
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0
gcd(0, N) → 0
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

p'(s'(N)) → N
+'(N, 0') → N
+'(s'(N), s'(M)) → s'(s'(+'(N, M)))
*'(N, 0') → 0'
*'(s'(N), s'(M)) → s'(+'(N, +'(M, *'(N, M))))
gt'(0', M) → False'
gt'(NzN, 0') → u_4'(is_NzNat'(NzN))
u_4'(True') → True'
is_NzNat'(0') → False'
is_NzNat'(s'(N)) → True'
gt'(s'(N), s'(M)) → gt'(N, M)
lt'(N, M) → gt'(M, N)
d'(0', N) → N
d'(s'(N), s'(M)) → d'(N, M)
quot'(N, NzM) → u_11'(is_NzNat'(NzM), N, NzM)
u_11'(True', N, NzM) → u_1'(gt'(N, NzM), N, NzM)
u_1'(True', N, NzM) → s'(quot'(d'(N, NzM), NzM))
quot'(NzM, NzM) → u_01'(is_NzNat'(NzM))
u_01'(True') → s'(0')
quot'(N, NzM) → u_21'(is_NzNat'(NzM), NzM, N)
u_21'(True', NzM, N) → u_2'(gt'(NzM, N))
u_2'(True') → 0'
gcd'(0', N) → 0'
gcd'(NzM, NzM) → u_02'(is_NzNat'(NzM), NzM)
u_02'(True', NzM) → NzM
gcd'(NzN, NzM) → u_31'(is_NzNat'(NzN), is_NzNat'(NzM), NzN, NzM)
u_31'(True', True', NzN, NzM) → u_3'(gt'(NzN, NzM), NzN, NzM)
u_3'(True', NzN, NzM) → gcd'(d'(NzN, NzM), NzM)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
p'(s'(N)) → N
+'(N, 0') → N
+'(s'(N), s'(M)) → s'(s'(+'(N, M)))
*'(N, 0') → 0'
*'(s'(N), s'(M)) → s'(+'(N, +'(M, *'(N, M))))
gt'(0', M) → False'
gt'(NzN, 0') → u_4'(is_NzNat'(NzN))
u_4'(True') → True'
is_NzNat'(0') → False'
is_NzNat'(s'(N)) → True'
gt'(s'(N), s'(M)) → gt'(N, M)
lt'(N, M) → gt'(M, N)
d'(0', N) → N
d'(s'(N), s'(M)) → d'(N, M)
quot'(N, NzM) → u_11'(is_NzNat'(NzM), N, NzM)
u_11'(True', N, NzM) → u_1'(gt'(N, NzM), N, NzM)
u_1'(True', N, NzM) → s'(quot'(d'(N, NzM), NzM))
quot'(NzM, NzM) → u_01'(is_NzNat'(NzM))
u_01'(True') → s'(0')
quot'(N, NzM) → u_21'(is_NzNat'(NzM), NzM, N)
u_21'(True', NzM, N) → u_2'(gt'(NzM, N))
u_2'(True') → 0'
gcd'(0', N) → 0'
gcd'(NzM, NzM) → u_02'(is_NzNat'(NzM), NzM)
u_02'(True', NzM) → NzM
gcd'(NzN, NzM) → u_31'(is_NzNat'(NzN), is_NzNat'(NzM), NzN, NzM)
u_31'(True', True', NzN, NzM) → u_3'(gt'(NzN, NzM), NzN, NzM)
u_3'(True', NzN, NzM) → gcd'(d'(NzN, NzM), NzM)

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
+' :: s':0' → s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
gt' :: s':0' → s':0' → False':True'
False' :: False':True'
u_4' :: False':True' → False':True'
is_NzNat' :: s':0' → False':True'
True' :: False':True'
lt' :: s':0' → s':0' → False':True'
d' :: s':0' → s':0' → s':0'
quot' :: s':0' → s':0' → s':0'
u_11' :: False':True' → s':0' → s':0' → s':0'
u_1' :: False':True' → s':0' → s':0' → s':0'
u_01' :: False':True' → s':0'
u_21' :: False':True' → s':0' → s':0' → s':0'
u_2' :: False':True' → s':0'
gcd' :: s':0' → s':0' → s':0'
u_02' :: False':True' → s':0' → s':0'
u_31' :: False':True' → False':True' → s':0' → s':0' → s':0'
u_3' :: False':True' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_False':True'2 :: False':True'
_gen_s':0'3 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
+', *', gt', d', quot', gcd'

They will be analysed ascendingly in the following order:
+' < *'
gt' < quot'
gt' < gcd'
d' < quot'
d' < gcd'

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

The following defined symbols remain to be analysed:
+', *', gt', d', quot', gcd'

They will be analysed ascendingly in the following order:
+' < *'
gt' < quot'
gt' < gcd'
d' < quot'
d' < gcd'

Proved the following rewrite lemma:
+'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → _gen_s':0'3(*(2, _n5)), rt ∈ Ω(1 + _n5)

Induction Base:
+'(_gen_s':0'3(0), _gen_s':0'3(0)) →_R^Ω(1)
_gen_s':0'3(0)

Induction Step:
+'(_gen_s':0'3(+(_$n6, 1)), _gen_s':0'3(+(_$n6, 1))) →_R^Ω(1)
s'(s'(+'(_gen_s':0'3(_$n6), _gen_s':0'3(_$n6)))) →_IH
s'(s'(_gen_s':0'3(*(2, _$n6))))

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

Lemmas:
+'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → _gen_s':0'3(*(2, _n5)), rt ∈ Ω(1 + _n5)

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

The following defined symbols remain to be analysed:
*', gt', d', quot', gcd'

They will be analysed ascendingly in the following order:
gt' < quot'
gt' < gcd'
d' < quot'
d' < gcd'

Proved the following rewrite lemma:
*'(_gen_s':0'3(+(1, _n1561)), _gen_s':0'3(+(1, _n1561))) → _*4, rt ∈ Ω(_n1561)

Induction Base:
*'(_gen_s':0'3(+(1, 0)), _gen_s':0'3(+(1, 0)))

Induction Step:
*'(_gen_s':0'3(+(1, +(_$n1562, 1))), _gen_s':0'3(+(1, +(_$n1562, 1)))) →_R^Ω(1)
s'(+'(_gen_s':0'3(+(1, _$n1562)), +'(_gen_s':0'3(+(1, _$n1562)), *'(_gen_s':0'3(+(1, _$n1562)), _gen_s':0'3(+(1, _$n1562)))))) →_IH
s'(+'(_gen_s':0'3(+(1, _$n1562)), +'(_gen_s':0'3(+(1, _$n1562)), _*4)))

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

Lemmas:
+'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → _gen_s':0'3(*(2, _n5)), rt ∈ Ω(1 + _n5)
*'(_gen_s':0'3(+(1, _n1561)), _gen_s':0'3(+(1, _n1561))) → _*4, rt ∈ Ω(_n1561)

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

The following defined symbols remain to be analysed:
gt', d', quot', gcd'

They will be analysed ascendingly in the following order:
gt' < quot'
gt' < gcd'
d' < quot'
d' < gcd'

Proved the following rewrite lemma:
gt'(_gen_s':0'3(_n50016), _gen_s':0'3(_n50016)) → False', rt ∈ Ω(1 + _n50016)

Induction Base:
gt'(_gen_s':0'3(0), _gen_s':0'3(0)) →_R^Ω(1)
False'

Induction Step:
gt'(_gen_s':0'3(+(_$n50017, 1)), _gen_s':0'3(+(_$n50017, 1))) →_R^Ω(1)
gt'(_gen_s':0'3(_$n50017), _gen_s':0'3(_$n50017)) →_IH
False'

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

Lemmas:
+'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → _gen_s':0'3(*(2, _n5)), rt ∈ Ω(1 + _n5)
*'(_gen_s':0'3(+(1, _n1561)), _gen_s':0'3(+(1, _n1561))) → _*4, rt ∈ Ω(_n1561)
gt'(_gen_s':0'3(_n50016), _gen_s':0'3(_n50016)) → False', rt ∈ Ω(1 + _n50016)

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

The following defined symbols remain to be analysed:
d', quot', gcd'

They will be analysed ascendingly in the following order:
d' < quot'
d' < gcd'

Proved the following rewrite lemma:
d'(_gen_s':0'3(_n51478), _gen_s':0'3(_n51478)) → _gen_s':0'3(0), rt ∈ Ω(1 + _n51478)

Induction Base:
d'(_gen_s':0'3(0), _gen_s':0'3(0)) →_R^Ω(1)
_gen_s':0'3(0)

Induction Step:
d'(_gen_s':0'3(+(_$n51479, 1)), _gen_s':0'3(+(_$n51479, 1))) →_R^Ω(1)
d'(_gen_s':0'3(_$n51479), _gen_s':0'3(_$n51479)) →_IH
_gen_s':0'3(0)

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

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

The following defined symbols remain to be analysed:
quot', gcd'

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

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

The following defined symbols remain to be analysed:
gcd'

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

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → _gen_s':0'3(*(2, _n5)), rt ∈ Ω(1 + _n5)