The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

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

@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

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:

@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Rewrite Strategy: INNERMOST

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

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

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

Heuristically decided to analyse the following defined symbols:
@, gt0, gcd, eqList, lgth, monus

They will be analysed ascendingly in the following order:
@ < lgth
gt0 < gcd
eqList < gcd
monus < gcd
eqList < monus
lgth < monus

(6) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

The following defined symbols remain to be analysed:
@, gt0, gcd, eqList, lgth, monus

They will be analysed ascendingly in the following order:
@ < lgth
gt0 < gcd
eqList < gcd
monus < gcd
eqList < monus
lgth < monus

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

Proved the following rewrite lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

Induction Base:
@(gen_Cons:Nil3_1(0), gen_Cons:Nil3_1(b)) →_R^Ω(1)
gen_Cons:Nil3_1(b)

Induction Step:
@(gen_Cons:Nil3_1(+(n5_1, 1)), gen_Cons:Nil3_1(b)) →_R^Ω(1)
Cons(Nil, @(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b))) →_IH
Cons(Nil, gen_Cons:Nil3_1(+(b, c6_1)))

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

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

The following defined symbols remain to be analysed:
gt0, gcd, eqList, lgth, monus

They will be analysed ascendingly in the following order:
gt0 < gcd
eqList < gcd
monus < gcd
eqList < monus
lgth < monus

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

Proved the following rewrite lemma:
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)

Induction Base:
gt0(gen_Cons:Nil3_1(+(1, 0)), gen_Cons:Nil3_1(0)) →_R^Ω(1)
True

Induction Step:
gt0(gen_Cons:Nil3_1(+(1, +(n978_1, 1))), gen_Cons:Nil3_1(+(n978_1, 1))) →_R^Ω(1)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) →_IH
True

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

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

The following defined symbols remain to be analysed:
eqList, gcd, lgth, monus

They will be analysed ascendingly in the following order:
eqList < gcd
monus < gcd
eqList < monus
lgth < monus

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

Proved the following rewrite lemma:
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)

Induction Base:
eqList(gen_Cons:Nil3_1(+(1, 0)), gen_Cons:Nil3_1(0)) →_R^Ω(1)
False

Induction Step:
eqList(gen_Cons:Nil3_1(+(1, +(n1471_1, 1))), gen_Cons:Nil3_1(+(n1471_1, 1))) →_R^Ω(1)
and(eqList(Nil, Nil), eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1))) →_R^Ω(1)
and(True, eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1))) →_IH
and(True, False) →_R^Ω(0)
False

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

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

The following defined symbols remain to be analysed:
lgth, gcd, monus

They will be analysed ascendingly in the following order:
monus < gcd
lgth < monus

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

Proved the following rewrite lemma:
lgth(gen_Cons:Nil3_1(n2126_1)) → gen_Cons:Nil3_1(n2126_1), rt ∈ Ω(1 + n2126₁)

Induction Base:
lgth(gen_Cons:Nil3_1(0)) →_R^Ω(1)
Nil

Induction Step:
lgth(gen_Cons:Nil3_1(+(n2126_1, 1))) →_R^Ω(1)
@(Cons(Nil, Nil), lgth(gen_Cons:Nil3_1(n2126_1))) →_IH
@(Cons(Nil, Nil), gen_Cons:Nil3_1(c2127_1)) →_L^Ω(2)
gen_Cons:Nil3_1(+(+(0, 1), n2126_1))

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

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)
lgth(gen_Cons:Nil3_1(n2126_1)) → gen_Cons:Nil3_1(n2126_1), rt ∈ Ω(1 + n2126₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

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

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

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

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

(20) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)
lgth(gen_Cons:Nil3_1(n2126_1)) → gen_Cons:Nil3_1(n2126_1), rt ∈ Ω(1 + n2126₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(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:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)
lgth(gen_Cons:Nil3_1(n2126_1)) → gen_Cons:Nil3_1(n2126_1), rt ∈ Ω(1 + n2126₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

(24) BOUNDS(n^1, INF)

(25) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)
lgth(gen_Cons:Nil3_1(n2126_1)) → gen_Cons:Nil3_1(n2126_1), rt ∈ Ω(1 + n2126₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

(27) BOUNDS(n^1, INF)

(28) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)
eqList(gen_Cons:Nil3_1(+(1, n1471_1)), gen_Cons:Nil3_1(n1471_1)) → False, rt ∈ Ω(1 + n1471₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

(30) BOUNDS(n^1, INF)

(31) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)
gt0(gen_Cons:Nil3_1(+(1, n978_1)), gen_Cons:Nil3_1(n978_1)) → True, rt ∈ Ω(1 + n978₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
Rules:
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))

Types:
@ :: Cons:Nil → Cons:Nil → Cons:Nil
Cons :: Cons:Nil → Cons:Nil → Cons:Nil
Nil :: Cons:Nil
gt0 :: Cons:Nil → Cons:Nil → True:False
True :: True:False
gcd :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
eqList :: Cons:Nil → Cons:Nil → True:False
lgth :: Cons:Nil → Cons:Nil
and :: True:False → True:False → True:False
False :: True:False
monus :: Cons:Nil → Cons:Nil → Cons:Nil
monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
goal :: Cons:Nil → Cons:Nil → Cons:Nil
gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil
hole_Cons:Nil1_1 :: Cons:Nil
hole_True:False2_1 :: True:False
gen_Cons:Nil3_1 :: Nat → Cons:Nil

Lemmas:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

Generator Equations:
gen_Cons:Nil3_1(0) ⇔ Nil
gen_Cons:Nil3_1(+(x, 1)) ⇔ Cons(Nil, gen_Cons:Nil3_1(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
@(gen_Cons:Nil3_1(n5_1), gen_Cons:Nil3_1(b)) → gen_Cons:Nil3_1(+(n5_1, b)), rt ∈ Ω(1 + n5₁)

(36) BOUNDS(n^1, INF)