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

minus(X, s(Y)) → pred(minus(X, Y))
minus(X, 0) → X
pred(s(X)) → X
le(s(X), s(Y)) → le(X, Y)
le(s(X), 0) → false
le(0, Y) → true
gcd(0, Y) → 0
gcd(s(X), 0) → s(X)
gcd(s(X), s(Y)) → if(le(Y, X), s(X), s(Y))
if(true, s(X), s(Y)) → gcd(minus(X, Y), s(Y))
if(false, s(X), s(Y)) → gcd(minus(Y, X), s(X))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: 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:
minus', le', gcd'

They will be analysed ascendingly in the following order:
minus' < gcd'
le' < gcd'

Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: 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'

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:
minus', le', gcd'

They will be analysed ascendingly in the following order:
minus' < gcd'
le' < gcd'

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

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

Induction Step:
minus'(_gen_s':0'3(_a955), _gen_s':0'3(+(1, +(_\$n6, 1)))) →RΩ(1)
pred'(minus'(_gen_s':0'3(_a955), _gen_s':0'3(+(1, _\$n6)))) →IH
pred'(_*4)

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

Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: 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'

Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(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:
le', gcd'

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

Proved the following rewrite lemma:
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)

Induction Base:
le'(_gen_s':0'3(+(1, 0)), _gen_s':0'3(0)) →RΩ(1)
false'

Induction Step:
le'(_gen_s':0'3(+(1, +(_\$n1419, 1))), _gen_s':0'3(+(_\$n1419, 1))) →RΩ(1)
le'(_gen_s':0'3(+(1, _\$n1419)), _gen_s':0'3(_\$n1419)) →IH
false'

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

Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: 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'

Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)

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'.

Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))

Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: 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'

Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)

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:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)