WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox2/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), 6208 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 33 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 305 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 46 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 83 ms]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 25 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 18 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 62 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:

   GCD(z0, z1) -> c1(GCD2(z0, z1, 0))
   GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0))
   GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0))
   GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
   GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
   GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
   IF1(true, z0, z1, z2, z3, z4, z5) -> c7
   IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
   IF2(true, z0, z1, z2, z3, z4) -> c9
   IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
   IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
   IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
   IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
   IF4(true, z0, z1, z2) -> c14
   INC(0) -> c15
   INC(s(z0)) -> c16(INC(z0))
   LE(s(z0), 0) -> c17
   LE(0, z0) -> c18
   LE(s(z0), s(z1)) -> c19(LE(z0, z1))
   MINUS(z0, 0) -> c20
   MINUS(0, z0) -> c21
   MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
   A -> c23
   A -> c24

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

   gcd(z0, z1) -> gcd2(z0, z1, 0)
   gcd2(z0, z1, z2) -> if1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
   if1(true, z0, z1, z2, z3, z4, z5) -> pair(result(z4), neededIterations(z5))
   if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
   if2(true, z0, z1, z2, z3, z4) -> pair(result(z2), neededIterations(z4))
   if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
   if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
   if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
   if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
   if4(true, z0, z1, z2) -> pair(result(z0), neededIterations(z2))
   inc(0) -> 0
   inc(s(z0)) -> s(inc(z0))
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(0, z0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   a -> b
   a -> c

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:

   GCD(z0, z1) -> c1(GCD2(z0, z1, 0))
   GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0))
   GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0))
   GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
   GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
   GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
   IF1(true, z0, z1, z2, z3, z4, z5) -> c7
   IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
   IF2(true, z0, z1, z2, z3, z4) -> c9
   IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
   IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
   IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
   IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
   IF4(true, z0, z1, z2) -> c14
   INC(0) -> c15
   INC(s(z0)) -> c16(INC(z0))
   LE(s(z0), 0) -> c17
   LE(0, z0) -> c18
   LE(s(z0), s(z1)) -> c19(LE(z0, z1))
   MINUS(z0, 0) -> c20
   MINUS(0, z0) -> c21
   MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
   A -> c23
   A -> c24

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

   gcd(z0, z1) -> gcd2(z0, z1, 0)
   gcd2(z0, z1, z2) -> if1(le(z0, 0), le(z1, 0), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
   if1(true, z0, z1, z2, z3, z4, z5) -> pair(result(z4), neededIterations(z5))
   if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
   if2(true, z0, z1, z2, z3, z4) -> pair(result(z2), neededIterations(z4))
   if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
   if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
   if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
   if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
   if4(true, z0, z1, z2) -> pair(result(z0), neededIterations(z2))
   inc(0) -> 0
   inc(s(z0)) -> s(inc(z0))
   le(s(z0), 0) -> false
   le(0, z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(0, z0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   a -> b
   a -> c

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:

   GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
   GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
   GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
   GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
   GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
   GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
   IF1(true, z0, z1, z2, z3, z4, z5) -> c7
   IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
   IF2(true, z0, z1, z2, z3, z4) -> c9
   IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
   IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
   IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
   IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
   IF4(true, z0, z1, z2) -> c14
   INC(0') -> c15
   INC(s(z0)) -> c16(INC(z0))
   LE(s(z0), 0') -> c17
   LE(0', z0) -> c18
   LE(s(z0), s(z1)) -> c19(LE(z0, z1))
   MINUS(z0, 0') -> c20
   MINUS(0', z0) -> c21
   MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
   A -> c23
   A -> c24

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

   gcd(z0, z1) -> gcd2(z0, z1, 0')
   gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
   if1(true, z0, z1, z2, z3, z4, z5) -> pair(result(z4), neededIterations(z5))
   if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
   if2(true, z0, z1, z2, z3, z4) -> pair(result(z2), neededIterations(z4))
   if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
   if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
   if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
   if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
   if4(true, z0, z1, z2) -> pair(result(z0), neededIterations(z2))
   inc(0') -> 0'
   inc(s(z0)) -> s(inc(z0))
   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0') -> z0
   minus(0', z0) -> 0'
   minus(s(z0), s(z1)) -> minus(z0, z1)
   a -> b
   a -> c

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
pair/0
pair/1
result/0
neededIterations/0

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

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

   GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
   GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
   GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
   GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
   GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
   GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
   IF1(true, z0, z1, z2, z3, z4, z5) -> c7
   IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
   IF2(true, z0, z1, z2, z3, z4) -> c9
   IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
   IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
   IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
   IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
   IF4(true, z0, z1, z2) -> c14
   INC(0') -> c15
   INC(s(z0)) -> c16(INC(z0))
   LE(s(z0), 0') -> c17
   LE(0', z0) -> c18
   LE(s(z0), s(z1)) -> c19(LE(z0, z1))
   MINUS(z0, 0') -> c20
   MINUS(0', z0) -> c21
   MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
   A -> c23
   A -> c24

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

   gcd(z0, z1) -> gcd2(z0, z1, 0')
   gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
   if1(true, z0, z1, z2, z3, z4, z5) -> pair
   if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
   if2(true, z0, z1, z2, z3, z4) -> pair
   if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
   if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
   if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
   if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
   if4(true, z0, z1, z2) -> pair
   inc(0') -> 0'
   inc(s(z0)) -> s(inc(z0))
   le(s(z0), 0') -> false
   le(0', z0) -> true
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0') -> z0
   minus(0', z0) -> 0'
   minus(s(z0), s(z1)) -> minus(z0, z1)
   a -> b
   a -> c

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

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

(8)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GCD2, le, inc, LE, INC, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
le < GCD2
inc < GCD2
LE < GCD2
INC < GCD2
minus < GCD2
MINUS < GCD2
le < gcd2
inc < gcd2
minus < gcd2

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

(10)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
le, GCD2, inc, LE, INC, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
le < GCD2
inc < GCD2
LE < GCD2
INC < GCD2
minus < GCD2
MINUS < GCD2
le < gcd2
inc < gcd2
minus < gcd2

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)

Induction Base:
le(gen_0':s15_25(+(1, 0)), gen_0':s15_25(0)) ->_R^Omega(0)
false

Induction Step:
le(gen_0':s15_25(+(1, +(n20_25, 1))), gen_0':s15_25(+(n20_25, 1))) ->_R^Omega(0)
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) ->_IH
false

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

(12)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
inc, GCD2, LE, INC, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
inc < GCD2
LE < GCD2
INC < GCD2
minus < GCD2
MINUS < GCD2
inc < gcd2
minus < gcd2

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)

Induction Base:
inc(gen_0':s15_25(0)) ->_R^Omega(0)
0'

Induction Step:
inc(gen_0':s15_25(+(n507_25, 1))) ->_R^Omega(0)
s(inc(gen_0':s15_25(n507_25))) ->_IH
s(gen_0':s15_25(c508_25))

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

(14)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
LE, GCD2, INC, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
LE < GCD2
INC < GCD2
minus < GCD2
MINUS < GCD2
minus < gcd2

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25)) -> gen_c17:c18:c1916_25(n877_25), rt in Omega(1 + n877_25)

Induction Base:
LE(gen_0':s15_25(+(1, 0)), gen_0':s15_25(0)) ->_R^Omega(1)
c17

Induction Step:
LE(gen_0':s15_25(+(1, +(n877_25, 1))), gen_0':s15_25(+(n877_25, 1))) ->_R^Omega(1)
c19(LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25))) ->_IH
c19(gen_c17:c18:c1916_25(c878_25))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
LE, GCD2, INC, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
LE < GCD2
INC < GCD2
minus < GCD2
MINUS < GCD2
minus < gcd2

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)
LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25)) -> gen_c17:c18:c1916_25(n877_25), rt in Omega(1 + n877_25)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
INC, GCD2, minus, MINUS, gcd2

They will be analysed ascendingly in the following order:
INC < GCD2
minus < GCD2
MINUS < GCD2
minus < gcd2

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INC(gen_0':s15_25(n1663_25)) -> gen_c15:c1617_25(n1663_25), rt in Omega(1 + n1663_25)

Induction Base:
INC(gen_0':s15_25(0)) ->_R^Omega(1)
c15

Induction Step:
INC(gen_0':s15_25(+(n1663_25, 1))) ->_R^Omega(1)
c16(INC(gen_0':s15_25(n1663_25))) ->_IH
c16(gen_c15:c1617_25(c1664_25))

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

(22)
Obligation:
Innermost TRS:
Rules:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)
LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25)) -> gen_c17:c18:c1916_25(n877_25), rt in Omega(1 + n877_25)
INC(gen_0':s15_25(n1663_25)) -> gen_c15:c1617_25(n1663_25), rt in Omega(1 + n1663_25)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
minus, GCD2, MINUS, gcd2

They will be analysed ascendingly in the following order:
minus < GCD2
MINUS < GCD2
minus < gcd2

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_0':s15_25(n2106_25), gen_0':s15_25(n2106_25)) -> gen_0':s15_25(0), rt in Omega(0)

Induction Base:
minus(gen_0':s15_25(0), gen_0':s15_25(0)) ->_R^Omega(0)
gen_0':s15_25(0)

Induction Step:
minus(gen_0':s15_25(+(n2106_25, 1)), gen_0':s15_25(+(n2106_25, 1))) ->_R^Omega(0)
minus(gen_0':s15_25(n2106_25), gen_0':s15_25(n2106_25)) ->_IH
gen_0':s15_25(0)

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:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)
LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25)) -> gen_c17:c18:c1916_25(n877_25), rt in Omega(1 + n877_25)
INC(gen_0':s15_25(n1663_25)) -> gen_c15:c1617_25(n1663_25), rt in Omega(1 + n1663_25)
minus(gen_0':s15_25(n2106_25), gen_0':s15_25(n2106_25)) -> gen_0':s15_25(0), rt in Omega(0)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
MINUS, GCD2, gcd2

They will be analysed ascendingly in the following order:
MINUS < GCD2

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_0':s15_25(n2952_25), gen_0':s15_25(n2952_25)) -> gen_c20:c21:c2218_25(n2952_25), rt in Omega(1 + n2952_25)

Induction Base:
MINUS(gen_0':s15_25(0), gen_0':s15_25(0)) ->_R^Omega(1)
c20

Induction Step:
MINUS(gen_0':s15_25(+(n2952_25, 1)), gen_0':s15_25(+(n2952_25, 1))) ->_R^Omega(1)
c22(MINUS(gen_0':s15_25(n2952_25), gen_0':s15_25(n2952_25))) ->_IH
c22(gen_c20:c21:c2218_25(c2953_25))

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:
GCD(z0, z1) -> c1(GCD2(z0, z1, 0'))
GCD2(z0, z1, z2) -> c2(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, 0'))
GCD2(z0, z1, z2) -> c3(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, 0'))
GCD2(z0, z1, z2) -> c4(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z0, z1))
GCD2(z0, z1, z2) -> c5(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), LE(z1, z0))
GCD2(z0, z1, z2) -> c6(IF1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2)), INC(z2))
IF1(true, z0, z1, z2, z3, z4, z5) -> c7
IF1(false, z0, z1, z2, z3, z4, z5) -> c8(IF2(z0, z1, z2, z3, z4, z5))
IF2(true, z0, z1, z2, z3, z4) -> c9
IF2(false, z0, z1, z2, z3, z4) -> c10(IF3(z0, z1, z2, z3, z4))
IF3(false, z0, z1, z2, z3) -> c11(GCD2(minus(z1, z2), z2, z3), MINUS(z1, z2))
IF3(true, z0, z1, z2, z3) -> c12(IF4(z0, z1, z2, z3))
IF4(false, z0, z1, z2) -> c13(GCD2(z0, minus(z1, z0), z2), MINUS(z1, z0))
IF4(true, z0, z1, z2) -> c14
INC(0') -> c15
INC(s(z0)) -> c16(INC(z0))
LE(s(z0), 0') -> c17
LE(0', z0) -> c18
LE(s(z0), s(z1)) -> c19(LE(z0, z1))
MINUS(z0, 0') -> c20
MINUS(0', z0) -> c21
MINUS(s(z0), s(z1)) -> c22(MINUS(z0, z1))
A -> c23
A -> c24
gcd(z0, z1) -> gcd2(z0, z1, 0')
gcd2(z0, z1, z2) -> if1(le(z0, 0'), le(z1, 0'), le(z0, z1), le(z1, z0), z0, z1, inc(z2))
if1(true, z0, z1, z2, z3, z4, z5) -> pair
if1(false, z0, z1, z2, z3, z4, z5) -> if2(z0, z1, z2, z3, z4, z5)
if2(true, z0, z1, z2, z3, z4) -> pair
if2(false, z0, z1, z2, z3, z4) -> if3(z0, z1, z2, z3, z4)
if3(false, z0, z1, z2, z3) -> gcd2(minus(z1, z2), z2, z3)
if3(true, z0, z1, z2, z3) -> if4(z0, z1, z2, z3)
if4(false, z0, z1, z2) -> gcd2(z0, minus(z1, z0), z2)
if4(true, z0, z1, z2) -> pair
inc(0') -> 0'
inc(s(z0)) -> s(inc(z0))
le(s(z0), 0') -> false
le(0', z0) -> true
le(s(z0), s(z1)) -> le(z0, z1)
minus(z0, 0') -> z0
minus(0', z0) -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
a -> b
a -> c

Types:
GCD :: 0':s -> 0':s -> c1
c1 :: c2:c3:c4:c5:c6 -> c1
GCD2 :: 0':s -> 0':s -> 0':s -> c2:c3:c4:c5:c6
0' :: 0':s
c2 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c7:c8
le :: 0':s -> 0':s -> true:false
inc :: 0':s -> 0':s
LE :: 0':s -> 0':s -> c17:c18:c19
c3 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c4 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c5 :: c7:c8 -> c17:c18:c19 -> c2:c3:c4:c5:c6
c6 :: c7:c8 -> c15:c16 -> c2:c3:c4:c5:c6
INC :: 0':s -> c15:c16
true :: true:false
c7 :: c7:c8
false :: true:false
c8 :: c9:c10 -> c7:c8
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> c9:c10
c9 :: c9:c10
c10 :: c11:c12 -> c9:c10
IF3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> c11:c12
c11 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c11:c12
minus :: 0':s -> 0':s -> 0':s
MINUS :: 0':s -> 0':s -> c20:c21:c22
c12 :: c13:c14 -> c11:c12
IF4 :: true:false -> 0':s -> 0':s -> 0':s -> c13:c14
c13 :: c2:c3:c4:c5:c6 -> c20:c21:c22 -> c13:c14
c14 :: c13:c14
c15 :: c15:c16
s :: 0':s -> 0':s
c16 :: c15:c16 -> c15:c16
c17 :: c17:c18:c19
c18 :: c17:c18:c19
c19 :: c17:c18:c19 -> c17:c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
A :: c23:c24
c23 :: c23:c24
c24 :: c23:c24
gcd :: 0':s -> 0':s -> pair
gcd2 :: 0':s -> 0':s -> 0':s -> pair
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
pair :: pair
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if3 :: true:false -> true:false -> 0':s -> 0':s -> 0':s -> pair
if4 :: true:false -> 0':s -> 0':s -> 0':s -> pair
a :: b:c
b :: b:c
c :: b:c
hole_c11_25 :: c1
hole_0':s2_25 :: 0':s
hole_c2:c3:c4:c5:c63_25 :: c2:c3:c4:c5:c6
hole_c7:c84_25 :: c7:c8
hole_c17:c18:c195_25 :: c17:c18:c19
hole_true:false6_25 :: true:false
hole_c15:c167_25 :: c15:c16
hole_c9:c108_25 :: c9:c10
hole_c11:c129_25 :: c11:c12
hole_c20:c21:c2210_25 :: c20:c21:c22
hole_c13:c1411_25 :: c13:c14
hole_c23:c2412_25 :: c23:c24
hole_pair13_25 :: pair
hole_b:c14_25 :: b:c
gen_0':s15_25 :: Nat -> 0':s
gen_c17:c18:c1916_25 :: Nat -> c17:c18:c19
gen_c15:c1617_25 :: Nat -> c15:c16
gen_c20:c21:c2218_25 :: Nat -> c20:c21:c22


Lemmas:
le(gen_0':s15_25(+(1, n20_25)), gen_0':s15_25(n20_25)) -> false, rt in Omega(0)
inc(gen_0':s15_25(n507_25)) -> gen_0':s15_25(n507_25), rt in Omega(0)
LE(gen_0':s15_25(+(1, n877_25)), gen_0':s15_25(n877_25)) -> gen_c17:c18:c1916_25(n877_25), rt in Omega(1 + n877_25)
INC(gen_0':s15_25(n1663_25)) -> gen_c15:c1617_25(n1663_25), rt in Omega(1 + n1663_25)
minus(gen_0':s15_25(n2106_25), gen_0':s15_25(n2106_25)) -> gen_0':s15_25(0), rt in Omega(0)
MINUS(gen_0':s15_25(n2952_25), gen_0':s15_25(n2952_25)) -> gen_c20:c21:c2218_25(n2952_25), rt in Omega(1 + n2952_25)


Generator Equations:
gen_0':s15_25(0) <=> 0'
gen_0':s15_25(+(x, 1)) <=> s(gen_0':s15_25(x))
gen_c17:c18:c1916_25(0) <=> c17
gen_c17:c18:c1916_25(+(x, 1)) <=> c19(gen_c17:c18:c1916_25(x))
gen_c15:c1617_25(0) <=> c15
gen_c15:c1617_25(+(x, 1)) <=> c16(gen_c15:c1617_25(x))
gen_c20:c21:c2218_25(0) <=> c20
gen_c20:c21:c2218_25(+(x, 1)) <=> c22(gen_c20:c21:c2218_25(x))


The following defined symbols remain to be analysed:
GCD2, gcd2