WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 68.1 s]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) typed CpxTrs
(7) OrderProof [LOWER BOUND(ID), 36 ms]
(8) typed CpxTrs
(9) RewriteLemmaProof [LOWER BOUND(ID), 273 ms]
(10) BEST
    (11) proven lower bound
        (12) LowerBoundPropagationProof [FINISHED, 0 ms]
        (13) BOUNDS(n^1, INF)
    (14) typed CpxTrs
        (15) RewriteLemmaProof [LOWER BOUND(ID), 38 ms]
        (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 4 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 84 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 74 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 1404 ms]
        (26) typed CpxTrs


----------------------------------------

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


The TRS R consists of the following rules:

   @'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
   @'(Nil, z0) -> c11
   GT0(Cons(z0, z1), Nil) -> c12
   GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
   GT0(Nil, z0) -> c14
   GCD(Nil, Nil) -> c15
   GCD(Nil, Cons(z0, z1)) -> c16
   GCD(Cons(z0, z1), Nil) -> c17
   GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
   LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
   LGTH(Nil) -> c20
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
   EQLIST(Cons(z0, z1), Nil) -> c23
   EQLIST(Nil, Cons(z0, z1)) -> c24
   EQLIST(Nil, Nil) -> c25
   MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
   GOAL(z0, z1) -> c27(GCD(z0, z1))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
   MONUS[ITE](True, Cons(z0, z1), z2) -> c5
   GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
   GCD[ITE](True, z0, z1) -> c7
   GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
   GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
   monus[Ite](True, Cons(z0, z1), z2) -> z1
   gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
   gcd[Ite](True, z0, z1) -> z0
   gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
   gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
   @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
   @(Nil, z0) -> z0
   gt0(Cons(z0, z1), Nil) -> True
   gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
   gt0(Nil, z0) -> False
   gcd(Nil, Nil) -> Nil
   gcd(Nil, Cons(z0, z1)) -> Nil
   gcd(Cons(z0, z1), Nil) -> Nil
   gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
   lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
   lgth(Nil) -> Nil
   eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
   eqList(Cons(z0, z1), Nil) -> False
   eqList(Nil, Cons(z0, z1)) -> False
   eqList(Nil, Nil) -> True
   monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
   goal(z0, z1) -> gcd(z0, z1)

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   @'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
   @'(Nil, z0) -> c11
   GT0(Cons(z0, z1), Nil) -> c12
   GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
   GT0(Nil, z0) -> c14
   GCD(Nil, Nil) -> c15
   GCD(Nil, Cons(z0, z1)) -> c16
   GCD(Cons(z0, z1), Nil) -> c17
   GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
   LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
   LGTH(Nil) -> c20
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
   EQLIST(Cons(z0, z1), Nil) -> c23
   EQLIST(Nil, Cons(z0, z1)) -> c24
   EQLIST(Nil, Nil) -> c25
   MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
   GOAL(z0, z1) -> c27(GCD(z0, z1))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
   MONUS[ITE](True, Cons(z0, z1), z2) -> c5
   GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
   GCD[ITE](True, z0, z1) -> c7
   GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
   GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
   monus[Ite](True, Cons(z0, z1), z2) -> z1
   gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
   gcd[Ite](True, z0, z1) -> z0
   gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
   gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
   @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
   @(Nil, z0) -> z0
   gt0(Cons(z0, z1), Nil) -> True
   gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
   gt0(Nil, z0) -> False
   gcd(Nil, Nil) -> Nil
   gcd(Nil, Cons(z0, z1)) -> Nil
   gcd(Cons(z0, z1), Nil) -> Nil
   gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
   lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
   lgth(Nil) -> Nil
   eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
   eqList(Cons(z0, z1), Nil) -> False
   eqList(Nil, Cons(z0, z1)) -> False
   eqList(Nil, Nil) -> True
   monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
   goal(z0, z1) -> gcd(z0, z1)

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   @'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
   @'(Nil, z0) -> c11
   GT0(Cons(z0, z1), Nil) -> c12
   GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
   GT0(Nil, z0) -> c14
   GCD(Nil, Nil) -> c15
   GCD(Nil, Cons(z0, z1)) -> c16
   GCD(Cons(z0, z1), Nil) -> c17
   GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
   LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
   LGTH(Nil) -> c20
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
   EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
   EQLIST(Cons(z0, z1), Nil) -> c23
   EQLIST(Nil, Cons(z0, z1)) -> c24
   EQLIST(Nil, Nil) -> c25
   MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
   GOAL(z0, z1) -> c27(GCD(z0, z1))

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

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
   MONUS[ITE](True, Cons(z0, z1), z2) -> c5
   GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
   GCD[ITE](True, z0, z1) -> c7
   GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
   GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
   monus[Ite](True, Cons(z0, z1), z2) -> z1
   gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
   gcd[Ite](True, z0, z1) -> z0
   gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
   gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
   @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
   @(Nil, z0) -> z0
   gt0(Cons(z0, z1), Nil) -> True
   gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
   gt0(Nil, z0) -> False
   gcd(Nil, Nil) -> Nil
   gcd(Nil, Cons(z0, z1)) -> Nil
   gcd(Cons(z0, z1), Nil) -> Nil
   gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
   lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
   lgth(Nil) -> Nil
   eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
   eqList(Cons(z0, z1), Nil) -> False
   eqList(Nil, Cons(z0, z1)) -> False
   eqList(Nil, Nil) -> True
   monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
   goal(z0, z1) -> gcd(z0, z1)

Rewrite Strategy: INNERMOST
----------------------------------------

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(6)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20

----------------------------------------

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
@', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @

They will be analysed ascendingly in the following order:
@' < LGTH
GT0 < GCD
eqList < GCD
EQLIST < GCD
MONUS < GCD
gt0 < GCD
monus < GCD
eqList < EQLIST
eqList < MONUS
eqList < monus
eqList < gcd
EQLIST < MONUS
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
gt0 < gcd
monus < gcd

----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


The following defined symbols remain to be analysed:
@', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @

They will be analysed ascendingly in the following order:
@' < LGTH
GT0 < GCD
eqList < GCD
EQLIST < GCD
MONUS < GCD
gt0 < GCD
monus < GCD
eqList < EQLIST
eqList < MONUS
eqList < monus
eqList < gcd
EQLIST < MONUS
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
gt0 < gcd
monus < gcd

----------------------------------------

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)

Induction Base:
@'(gen_Cons:Nil15_28(0), gen_Cons:Nil15_28(b)) ->_R^Omega(1)
c11

Induction Step:
@'(gen_Cons:Nil15_28(+(n20_28, 1)), gen_Cons:Nil15_28(b)) ->_R^Omega(1)
c10(@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b))) ->_IH
c10(gen_c10:c1114_28(c21_28))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(10)
Complex Obligation (BEST)

----------------------------------------

(11)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


The following defined symbols remain to be analysed:
@', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @

They will be analysed ascendingly in the following order:
@' < LGTH
GT0 < GCD
eqList < GCD
EQLIST < GCD
MONUS < GCD
gt0 < GCD
monus < GCD
eqList < EQLIST
eqList < MONUS
eqList < monus
eqList < gcd
EQLIST < MONUS
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
gt0 < gcd
monus < gcd

----------------------------------------

(12) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(13)
BOUNDS(n^1, INF)

----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


The following defined symbols remain to be analysed:
GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @

They will be analysed ascendingly in the following order:
GT0 < GCD
eqList < GCD
EQLIST < GCD
MONUS < GCD
gt0 < GCD
monus < GCD
eqList < EQLIST
eqList < MONUS
eqList < monus
eqList < gcd
EQLIST < MONUS
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
gt0 < gcd
monus < gcd

----------------------------------------

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)

Induction Base:
GT0(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(1)
c12

Induction Step:
GT0(gen_Cons:Nil15_28(+(1, +(n1084_28, 1))), gen_Cons:Nil15_28(+(n1084_28, 1))) ->_R^Omega(1)
c13(GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28))) ->_IH
c13(gen_c12:c13:c1416_28(c1085_28))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


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

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

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)

Induction Base:
eqList(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(0)
False

Induction Step:
eqList(gen_Cons:Nil15_28(+(1, +(n2068_28, 1))), gen_Cons:Nil15_28(+(n2068_28, 1))) ->_R^Omega(0)
and(eqList(Nil, Nil), eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28))) ->_R^Omega(0)
and(True, eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28))) ->_IH
and(True, False) ->_R^Omega(0)
False

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


The following defined symbols remain to be analysed:
EQLIST, GCD, LGTH, lgth, MONUS, gt0, monus, gcd, @

They will be analysed ascendingly in the following order:
EQLIST < GCD
MONUS < GCD
gt0 < GCD
monus < GCD
EQLIST < MONUS
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
gt0 < gcd
monus < gcd

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0)

Induction Base:
gt0(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(0)
True

Induction Step:
gt0(gen_Cons:Nil15_28(+(1, +(n3442_28, 1))), gen_Cons:Nil15_28(+(n3442_28, 1))) ->_R^Omega(0)
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) ->_IH
True

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


The following defined symbols remain to be analysed:
@, GCD, LGTH, lgth, MONUS, monus, gcd

They will be analysed ascendingly in the following order:
MONUS < GCD
monus < GCD
lgth < LGTH
LGTH < MONUS
lgth < MONUS
lgth < monus
@ < lgth
monus < gcd

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
@(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0)

Induction Base:
@(gen_Cons:Nil15_28(0), gen_Cons:Nil15_28(b)) ->_R^Omega(0)
gen_Cons:Nil15_28(b)

Induction Step:
@(gen_Cons:Nil15_28(+(n4101_28, 1)), gen_Cons:Nil15_28(b)) ->_R^Omega(0)
Cons(Nil, @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b))) ->_IH
Cons(Nil, gen_Cons:Nil15_28(+(b, c4102_28)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0)
@(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


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

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

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0)

Induction Base:
lgth(gen_Cons:Nil15_28(0)) ->_R^Omega(0)
Nil

Induction Step:
lgth(gen_Cons:Nil15_28(+(n6126_28, 1))) ->_R^Omega(0)
@(Cons(Nil, Nil), lgth(gen_Cons:Nil15_28(n6126_28))) ->_IH
@(Cons(Nil, Nil), gen_Cons:Nil15_28(c6127_28)) ->_L^Omega(0)
gen_Cons:Nil15_28(+(+(0, 1), n6126_28))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0)
@(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0)
lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


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

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

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LGTH(gen_Cons:Nil15_28(+(1, n7147_28))) -> *19_28, rt in Omega(n7147_28)

Induction Base:
LGTH(gen_Cons:Nil15_28(+(1, 0)))

Induction Step:
LGTH(gen_Cons:Nil15_28(+(1, +(n7147_28, 1)))) ->_R^Omega(1)
c19(@'(Cons(Nil, Nil), lgth(gen_Cons:Nil15_28(+(1, n7147_28)))), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_L^Omega(0)
c19(@'(Cons(Nil, Nil), gen_Cons:Nil15_28(+(1, n7147_28))), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_L^Omega(2)
c19(gen_c10:c1114_28(+(0, 1)), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_IH
c19(gen_c10:c1114_28(1), *19_28)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
@'(Cons(z0, z1), z2) -> c10(@'(z1, z2))
@'(Nil, z0) -> c11
GT0(Cons(z0, z1), Nil) -> c12
GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3))
GT0(Nil, z0) -> c14
GCD(Nil, Nil) -> c15
GCD(Nil, Cons(z0, z1)) -> c16
GCD(Cons(z0, z1), Nil) -> c17
GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3)))
LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1))
LGTH(Nil) -> c20
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2))
EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3))
EQLIST(Cons(z0, z1), Nil) -> c23
EQLIST(Nil, Cons(z0, z1)) -> c24
EQLIST(Nil, Nil) -> c25
MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1))
GOAL(z0, z1) -> c27(GCD(z0, z1))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3))
MONUS[ITE](True, Cons(z0, z1), z2) -> c5
GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1))
GCD[ITE](True, z0, z1) -> c7
GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0))
GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1))
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3)
monus[Ite](True, Cons(z0, z1), z2) -> z1
gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1)
gcd[Ite](True, z0, z1) -> z0
gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0))
gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1)
@(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2))
@(Nil, z0) -> z0
gt0(Cons(z0, z1), Nil) -> True
gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3)
gt0(Nil, z0) -> False
gcd(Nil, Nil) -> Nil
gcd(Nil, Cons(z0, z1)) -> Nil
gcd(Cons(z0, z1), Nil) -> Nil
gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3))
lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1))
lgth(Nil) -> Nil
eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3))
eqList(Cons(z0, z1), Nil) -> False
eqList(Nil, Cons(z0, z1)) -> False
eqList(Nil, Nil) -> True
monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1)
goal(z0, z1) -> gcd(z0, z1)

Types:
@' :: Cons:Nil -> Cons:Nil -> c10:c11
Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil
c10 :: c10:c11 -> c10:c11
Nil :: Cons:Nil
c11 :: c10:c11
GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14 -> c12:c13:c14
c14 :: c12:c13:c14
GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18
c15 :: c15:c16:c17:c18
c16 :: c15:c16:c17:c18
c17 :: c15:c16:c17:c18
c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18
GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7
eqList :: Cons:Nil -> Cons:Nil -> False:True
EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25
LGTH :: Cons:Nil -> c19:c20
c19 :: c10:c11 -> c19:c20 -> c19:c20
lgth :: Cons:Nil -> Cons:Nil
c20 :: c19:c20
c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
AND :: False:True -> False:True -> c:c1:c2:c3
c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25
c23 :: c21:c22:c23:c24:c25
c24 :: c21:c22:c23:c24:c25
c25 :: c21:c22:c23:c24:c25
MONUS :: Cons:Nil -> Cons:Nil -> c26
c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26
MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5
GOAL :: Cons:Nil -> Cons:Nil -> c27
c27 :: c15:c16:c17:c18 -> c27
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
c4 :: c26 -> c4:c5
c5 :: c4:c5
c6 :: c8:c9 -> c12:c13:c14 -> c6:c7
GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9
gt0 :: Cons:Nil -> Cons:Nil -> False:True
c7 :: c6:c7
c8 :: c15:c16:c17:c18 -> c26 -> c8:c9
monus :: Cons:Nil -> Cons:Nil -> Cons:Nil
c9 :: c15:c16:c17:c18 -> c26 -> c8:c9
and :: False:True -> False:True -> False:True
monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil
@ :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c10:c111_28 :: c10:c11
hole_Cons:Nil2_28 :: Cons:Nil
hole_c12:c13:c143_28 :: c12:c13:c14
hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18
hole_c6:c75_28 :: c6:c7
hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25
hole_False:True7_28 :: False:True
hole_c19:c208_28 :: c19:c20
hole_c:c1:c2:c39_28 :: c:c1:c2:c3
hole_c2610_28 :: c26
hole_c4:c511_28 :: c4:c5
hole_c2712_28 :: c27
hole_c8:c913_28 :: c8:c9
gen_c10:c1114_28 :: Nat -> c10:c11
gen_Cons:Nil15_28 :: Nat -> Cons:Nil
gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14
gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25
gen_c19:c2018_28 :: Nat -> c19:c20


Lemmas:
@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28)
GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28)
eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0)
gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0)
@(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0)
lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0)
LGTH(gen_Cons:Nil15_28(+(1, n7147_28))) -> *19_28, rt in Omega(n7147_28)


Generator Equations:
gen_c10:c1114_28(0) <=> c11
gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x))
gen_Cons:Nil15_28(0) <=> Nil
gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x))
gen_c12:c13:c1416_28(0) <=> c12
gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x))
gen_c21:c22:c23:c24:c2517_28(0) <=> c23
gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x))
gen_c19:c2018_28(0) <=> c20
gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x))


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

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