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:

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

(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:

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)

S is empty.
Rewrite Strategy: INNERMOST

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

Infered types.

(4) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

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

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

(6) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(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

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

Proved the following rewrite lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

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

Induction Step:
+'(gen_s:0'3_0(+(n5_0, 1)), gen_s:0'3_0(+(n5_0, 1))) →_R^Ω(1)
s(s(+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)))) →_IH
s(s(gen_s:0'3_0(*(2, c6_0))))

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

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(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

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)

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

Induction Step:
*'(gen_s:0'3_0(+(1, +(n705_0, 1))), gen_s:0'3_0(+(1, +(n705_0, 1)))) →_R^Ω(1)
s(+'(gen_s:0'3_0(+(1, n705_0)), +'(gen_s:0'3_0(+(1, n705_0)), *'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0)))))) →_IH
s(+'(gen_s:0'3_0(+(1, n705_0)), +'(gen_s:0'3_0(+(1, n705_0)), *4_0)))

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

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(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

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)

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

Induction Step:
gt(gen_s:0'3_0(+(n35821_0, 1)), gen_s:0'3_0(+(n35821_0, 1))) →_R^Ω(1)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) →_IH
False

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

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)

Generator Equations:
gen_s:0'3_0(0) ⇔ 0'
gen_s:0'3_0(+(x, 1)) ⇔ s(gen_s:0'3_0(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

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n36357₀)

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

Induction Step:
d(gen_s:0'3_0(+(n36357_0, 1)), gen_s:0'3_0(+(n36357_0, 1))) →_R^Ω(1)
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) →_IH
gen_s:0'3_0(0)

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

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n36357₀)

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

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

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(20) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n36357₀)

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

The following defined symbols remain to be analysed:
gcd

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(22) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n36357₀)

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

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(24) BOUNDS(n^1, INF)

(25) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)
d(gen_s:0'3_0(n36357_0), gen_s:0'3_0(n36357_0)) → gen_s:0'3_0(0), rt ∈ Ω(1 + n36357₀)

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

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(27) BOUNDS(n^1, INF)

(28) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)
gt(gen_s:0'3_0(n35821_0), gen_s:0'3_0(n35821_0)) → False, rt ∈ Ω(1 + n35821₀)

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

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(30) BOUNDS(n^1, INF)

(31) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)
*'(gen_s:0'3_0(+(1, n705_0)), gen_s:0'3_0(+(1, n705_0))) → *4_0, rt ∈ Ω(n705₀)

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

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
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_0 :: s:0'
hole_False:True2_0 :: False:True
gen_s:0'3_0 :: Nat → s:0'

Lemmas:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

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

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
+'(gen_s:0'3_0(n5_0), gen_s:0'3_0(n5_0)) → gen_s:0'3_0(*(2, n5_0)), rt ∈ Ω(1 + n5₀)

(36) BOUNDS(n^1, INF)