WORST_CASE(Omega(n^1),?)
proof of input_hM1XZaZ0ki.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 6 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 309 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 120 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 94 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 65 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 295 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 148 ms]
        (26) typed CpxTrs


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

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


The TRS R consists of the following rules:

   lcm(x, y) -> lcmIter(x, y, 0, times(x, y))
   lcmIter(x, y, z, u) -> if(or(ge(0, x), ge(z, u)), x, y, z, u)
   if(true, x, y, z, u) -> z
   if(false, x, y, z, u) -> if2(divisible(z, y), x, y, z, u)
   if2(true, x, y, z, u) -> z
   if2(false, x, y, z, u) -> lcmIter(x, y, plus(x, z), u)
   plus(0, y) -> y
   plus(s(x), y) -> s(plus(x, y))
   times(x, y) -> ifTimes(ge(0, x), x, y)
   ifTimes(true, x, y) -> 0
   ifTimes(false, x, y) -> plus(y, times(y, p(x)))
   p(s(x)) -> x
   p(0) -> s(s(0))
   ge(x, 0) -> true
   ge(0, s(y)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   or(true, y) -> true
   or(false, y) -> y
   divisible(0, s(y)) -> true
   divisible(s(x), s(y)) -> div(s(x), s(y), s(y))
   div(x, y, 0) -> divisible(x, y)
   div(0, y, s(z)) -> false
   div(s(x), y, s(z)) -> div(x, y, z)
   a -> b
   a -> c

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lcm(z0, z1) -> lcmIter(z0, z1, 0, times(z0, z1))
   lcmIter(z0, z1, z2, z3) -> if(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> z2
   if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
   if2(true, z0, z1, z2, z3) -> z2
   if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> ifTimes(ge(0, z0), z0, z1)
   ifTimes(true, z0, z1) -> 0
   ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
   p(s(z0)) -> z0
   p(0) -> s(s(0))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   divisible(0, s(z0)) -> true
   divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
   div(z0, z1, 0) -> divisible(z0, z1)
   div(0, z0, s(z1)) -> false
   div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
   a -> b
   a -> c
Tuples:
   LCM(z0, z1) -> c1(LCMITER(z0, z1, 0, times(z0, z1)), TIMES(z0, z1))
   LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(0, z0))
   LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(z2, z3))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
   IF2(true, z0, z1, z2, z3) -> c6
   IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
   PLUS(0, z0) -> c8
   PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
   TIMES(z0, z1) -> c10(IFTIMES(ge(0, z0), z0, z1), GE(0, z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   OR(true, z0) -> c18
   OR(false, z0) -> c19
   DIVISIBLE(0, s(z0)) -> c20
   DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
   DIV(z0, z1, 0) -> c22(DIVISIBLE(z0, z1))
   DIV(0, z0, s(z1)) -> c23
   DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
   A -> c25
   A -> c26
S tuples:
   LCM(z0, z1) -> c1(LCMITER(z0, z1, 0, times(z0, z1)), TIMES(z0, z1))
   LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(0, z0))
   LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(z2, z3))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
   IF2(true, z0, z1, z2, z3) -> c6
   IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
   PLUS(0, z0) -> c8
   PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
   TIMES(z0, z1) -> c10(IFTIMES(ge(0, z0), z0, z1), GE(0, z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   OR(true, z0) -> c18
   OR(false, z0) -> c19
   DIVISIBLE(0, s(z0)) -> c20
   DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
   DIV(z0, z1, 0) -> c22(DIVISIBLE(z0, z1))
   DIV(0, z0, s(z1)) -> c23
   DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
   A -> c25
   A -> c26
K tuples:none
Defined Rule Symbols:   lcm_2, lcmIter_4, if_5, if2_5, plus_2, times_2, ifTimes_3, p_1, ge_2, or_2, divisible_2, div_3, a

Defined Pair Symbols:   LCM_2, LCMITER_4, IF_5, IF2_5, PLUS_2, TIMES_2, IFTIMES_3, P_1, GE_2, OR_2, DIVISIBLE_2, DIV_3, A

Compound Symbols:   c1_2, c2_3, c3_3, c4, c5_2, c6, c7_2, c8, c9_1, c10_2, c11, c12_3, c13, c14, c15, c16, c17_1, c18, c19, c20, c21_1, c22_1, c23, c24_1, c25, c26


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   LCM(z0, z1) -> c1(LCMITER(z0, z1, 0, times(z0, z1)), TIMES(z0, z1))
   LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(0, z0))
   LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0, z0), ge(z2, z3)), GE(z2, z3))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
   IF2(true, z0, z1, z2, z3) -> c6
   IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
   PLUS(0, z0) -> c8
   PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
   TIMES(z0, z1) -> c10(IFTIMES(ge(0, z0), z0, z1), GE(0, z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   GE(z0, 0) -> c15
   GE(0, s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   OR(true, z0) -> c18
   OR(false, z0) -> c19
   DIVISIBLE(0, s(z0)) -> c20
   DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
   DIV(z0, z1, 0) -> c22(DIVISIBLE(z0, z1))
   DIV(0, z0, s(z1)) -> c23
   DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
   A -> c25
   A -> c26

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

   lcm(z0, z1) -> lcmIter(z0, z1, 0, times(z0, z1))
   lcmIter(z0, z1, z2, z3) -> if(or(ge(0, z0), ge(z2, z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> z2
   if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
   if2(true, z0, z1, z2, z3) -> z2
   if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> ifTimes(ge(0, z0), z0, z1)
   ifTimes(true, z0, z1) -> 0
   ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
   p(s(z0)) -> z0
   p(0) -> s(s(0))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   divisible(0, s(z0)) -> true
   divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
   div(z0, z1, 0) -> divisible(z0, z1)
   div(0, z0, s(z1)) -> false
   div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
   a -> b
   a -> c

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

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

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

   LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
   LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
   LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
   IF(true, z0, z1, z2, z3) -> c4
   IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
   IF2(true, z0, z1, z2, z3) -> c6
   IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
   PLUS(0', z0) -> c8
   PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
   TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
   P(s(z0)) -> c13
   P(0') -> c14
   GE(z0, 0') -> c15
   GE(0', s(z0)) -> c16
   GE(s(z0), s(z1)) -> c17(GE(z0, z1))
   OR(true, z0) -> c18
   OR(false, z0) -> c19
   DIVISIBLE(0', s(z0)) -> c20
   DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
   DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
   DIV(0', z0, s(z1)) -> c23
   DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
   A -> c25
   A -> c26

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

   lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
   lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> z2
   if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
   if2(true, z0, z1, z2, z3) -> z2
   if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
   ifTimes(true, z0, z1) -> 0'
   ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
   p(s(z0)) -> z0
   p(0') -> s(s(0'))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   divisible(0', s(z0)) -> true
   divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
   div(z0, z1, 0') -> divisible(z0, z1)
   div(0', z0, s(z1)) -> false
   div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
   a -> b
   a -> c

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

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

(8)
Obligation:
Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LCMITER, times, TIMES, ge, GE, divisible, DIVISIBLE, plus, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
ge < LCMITER
GE < LCMITER
divisible < LCMITER
DIVISIBLE < LCMITER
plus < LCMITER
PLUS < LCMITER
times < TIMES
ge < times
plus < times
ge < TIMES
GE < TIMES
PLUS < TIMES
ge < lcmIter
divisible < lcmIter
divisible = div
DIVISIBLE = DIV
plus < lcmIter

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

(10)
Obligation:
Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
ge, LCMITER, times, TIMES, GE, divisible, DIVISIBLE, plus, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
ge < LCMITER
GE < LCMITER
divisible < LCMITER
DIVISIBLE < LCMITER
plus < LCMITER
PLUS < LCMITER
times < TIMES
ge < times
plus < times
ge < TIMES
GE < TIMES
PLUS < TIMES
ge < lcmIter
divisible < lcmIter
divisible = div
DIVISIBLE = DIV
plus < lcmIter

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s17_27(0), gen_0':s17_27(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s17_27(+(n22_27, 1)), gen_0':s17_27(+(n22_27, 1))) ->_R^Omega(0)
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) ->_IH
true

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:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
GE, LCMITER, times, TIMES, divisible, DIVISIBLE, plus, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
GE < LCMITER
divisible < LCMITER
DIVISIBLE < LCMITER
plus < LCMITER
PLUS < LCMITER
times < TIMES
plus < times
GE < TIMES
PLUS < TIMES
divisible < lcmIter
divisible = div
DIVISIBLE = DIV
plus < lcmIter

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)

Induction Base:
GE(gen_0':s17_27(0), gen_0':s17_27(0)) ->_R^Omega(1)
c15

Induction Step:
GE(gen_0':s17_27(+(n604_27, 1)), gen_0':s17_27(+(n604_27, 1))) ->_R^Omega(1)
c17(GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27))) ->_IH
c17(gen_c15:c16:c1718_27(c605_27))

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
GE, LCMITER, times, TIMES, divisible, DIVISIBLE, plus, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
GE < LCMITER
divisible < LCMITER
DIVISIBLE < LCMITER
plus < LCMITER
PLUS < LCMITER
times < TIMES
plus < times
GE < TIMES
PLUS < TIMES
divisible < lcmIter
divisible = div
DIVISIBLE = DIV
plus < lcmIter

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
plus, LCMITER, times, TIMES, divisible, DIVISIBLE, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
divisible < LCMITER
DIVISIBLE < LCMITER
plus < LCMITER
PLUS < LCMITER
times < TIMES
plus < times
PLUS < TIMES
divisible < lcmIter
divisible = div
DIVISIBLE = DIV
plus < lcmIter

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b)) -> gen_0':s17_27(+(n1485_27, b)), rt in Omega(0)

Induction Base:
plus(gen_0':s17_27(0), gen_0':s17_27(b)) ->_R^Omega(0)
gen_0':s17_27(b)

Induction Step:
plus(gen_0':s17_27(+(n1485_27, 1)), gen_0':s17_27(b)) ->_R^Omega(0)
s(plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b))) ->_IH
s(gen_0':s17_27(+(b, c1486_27)))

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:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)
plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b)) -> gen_0':s17_27(+(n1485_27, b)), rt in Omega(0)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
times, LCMITER, TIMES, divisible, DIVISIBLE, PLUS, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
divisible < LCMITER
DIVISIBLE < LCMITER
PLUS < LCMITER
times < TIMES
PLUS < TIMES
divisible < lcmIter
divisible = div
DIVISIBLE = DIV

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s17_27(n3404_27), gen_0':s17_27(b)) -> gen_c8:c919_27(n3404_27), rt in Omega(1 + n3404_27)

Induction Base:
PLUS(gen_0':s17_27(0), gen_0':s17_27(b)) ->_R^Omega(1)
c8

Induction Step:
PLUS(gen_0':s17_27(+(n3404_27, 1)), gen_0':s17_27(b)) ->_R^Omega(1)
c9(PLUS(gen_0':s17_27(n3404_27), gen_0':s17_27(b))) ->_IH
c9(gen_c8:c919_27(c3405_27))

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:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)
plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b)) -> gen_0':s17_27(+(n1485_27, b)), rt in Omega(0)
PLUS(gen_0':s17_27(n3404_27), gen_0':s17_27(b)) -> gen_c8:c919_27(n3404_27), rt in Omega(1 + n3404_27)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
TIMES, LCMITER, divisible, DIVISIBLE, DIV, lcmIter, div

They will be analysed ascendingly in the following order:
divisible < LCMITER
DIVISIBLE < LCMITER
divisible < lcmIter
divisible = div
DIVISIBLE = DIV

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DIV(gen_0':s17_27(n4879_27), gen_0':s17_27(1), gen_0':s17_27(n4879_27)) -> gen_c22:c23:c2420_27(n4879_27), rt in Omega(1 + n4879_27)

Induction Base:
DIV(gen_0':s17_27(0), gen_0':s17_27(1), gen_0':s17_27(0)) ->_R^Omega(1)
c22(DIVISIBLE(gen_0':s17_27(0), gen_0':s17_27(1))) ->_R^Omega(1)
c22(c20)

Induction Step:
DIV(gen_0':s17_27(+(n4879_27, 1)), gen_0':s17_27(1), gen_0':s17_27(+(n4879_27, 1))) ->_R^Omega(1)
c24(DIV(gen_0':s17_27(n4879_27), gen_0':s17_27(1), gen_0':s17_27(n4879_27))) ->_IH
c24(gen_c22:c23:c2420_27(c4880_27))

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

(24)
Obligation:
Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)
plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b)) -> gen_0':s17_27(+(n1485_27, b)), rt in Omega(0)
PLUS(gen_0':s17_27(n3404_27), gen_0':s17_27(b)) -> gen_c8:c919_27(n3404_27), rt in Omega(1 + n3404_27)
DIV(gen_0':s17_27(n4879_27), gen_0':s17_27(1), gen_0':s17_27(n4879_27)) -> gen_c22:c23:c2420_27(n4879_27), rt in Omega(1 + n4879_27)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
DIVISIBLE, LCMITER, divisible, lcmIter, div

They will be analysed ascendingly in the following order:
divisible < LCMITER
DIVISIBLE < LCMITER
divisible < lcmIter
divisible = div
DIVISIBLE = DIV

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
div(gen_0':s17_27(n8087_27), gen_0':s17_27(b), gen_0':s17_27(+(1, n8087_27))) -> false, rt in Omega(0)

Induction Base:
div(gen_0':s17_27(0), gen_0':s17_27(b), gen_0':s17_27(+(1, 0))) ->_R^Omega(0)
false

Induction Step:
div(gen_0':s17_27(+(n8087_27, 1)), gen_0':s17_27(b), gen_0':s17_27(+(1, +(n8087_27, 1)))) ->_R^Omega(0)
div(gen_0':s17_27(n8087_27), gen_0':s17_27(b), gen_0':s17_27(+(1, n8087_27))) ->_IH
false

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

(26)
Obligation:
Innermost TRS:
Rules:
LCM(z0, z1) -> c1(LCMITER(z0, z1, 0', times(z0, z1)), TIMES(z0, z1))
LCMITER(z0, z1, z2, z3) -> c2(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(0', z0))
LCMITER(z0, z1, z2, z3) -> c3(IF(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3), OR(ge(0', z0), ge(z2, z3)), GE(z2, z3))
IF(true, z0, z1, z2, z3) -> c4
IF(false, z0, z1, z2, z3) -> c5(IF2(divisible(z2, z1), z0, z1, z2, z3), DIVISIBLE(z2, z1))
IF2(true, z0, z1, z2, z3) -> c6
IF2(false, z0, z1, z2, z3) -> c7(LCMITER(z0, z1, plus(z0, z2), z3), PLUS(z0, z2))
PLUS(0', z0) -> c8
PLUS(s(z0), z1) -> c9(PLUS(z0, z1))
TIMES(z0, z1) -> c10(IFTIMES(ge(0', z0), z0, z1), GE(0', z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(z1, p(z0))), TIMES(z1, p(z0)), P(z0))
P(s(z0)) -> c13
P(0') -> c14
GE(z0, 0') -> c15
GE(0', s(z0)) -> c16
GE(s(z0), s(z1)) -> c17(GE(z0, z1))
OR(true, z0) -> c18
OR(false, z0) -> c19
DIVISIBLE(0', s(z0)) -> c20
DIVISIBLE(s(z0), s(z1)) -> c21(DIV(s(z0), s(z1), s(z1)))
DIV(z0, z1, 0') -> c22(DIVISIBLE(z0, z1))
DIV(0', z0, s(z1)) -> c23
DIV(s(z0), z1, s(z2)) -> c24(DIV(z0, z1, z2))
A -> c25
A -> c26
lcm(z0, z1) -> lcmIter(z0, z1, 0', times(z0, z1))
lcmIter(z0, z1, z2, z3) -> if(or(ge(0', z0), ge(z2, z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> z2
if(false, z0, z1, z2, z3) -> if2(divisible(z2, z1), z0, z1, z2, z3)
if2(true, z0, z1, z2, z3) -> z2
if2(false, z0, z1, z2, z3) -> lcmIter(z0, z1, plus(z0, z2), z3)
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> ifTimes(ge(0', z0), z0, z1)
ifTimes(true, z0, z1) -> 0'
ifTimes(false, z0, z1) -> plus(z1, times(z1, p(z0)))
p(s(z0)) -> z0
p(0') -> s(s(0'))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
divisible(0', s(z0)) -> true
divisible(s(z0), s(z1)) -> div(s(z0), s(z1), s(z1))
div(z0, z1, 0') -> divisible(z0, z1)
div(0', z0, s(z1)) -> false
div(s(z0), z1, s(z2)) -> div(z0, z1, z2)
a -> b
a -> c

Types:
LCM :: 0':s -> 0':s -> c1
c1 :: c2:c3 -> c10 -> c1
LCMITER :: 0':s -> 0':s -> 0':s -> 0':s -> c2:c3
0' :: 0':s
times :: 0':s -> 0':s -> 0':s
TIMES :: 0':s -> 0':s -> c10
c2 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
IF :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c4:c5
or :: true:false -> true:false -> true:false
ge :: 0':s -> 0':s -> true:false
OR :: true:false -> true:false -> c18:c19
GE :: 0':s -> 0':s -> c15:c16:c17
c3 :: c4:c5 -> c18:c19 -> c15:c16:c17 -> c2:c3
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c6:c7 -> c20:c21 -> c4:c5
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> c6:c7
divisible :: 0':s -> 0':s -> true:false
DIVISIBLE :: 0':s -> 0':s -> c20:c21
c6 :: c6:c7
c7 :: c2:c3 -> c8:c9 -> c6:c7
plus :: 0':s -> 0':s -> 0':s
PLUS :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
s :: 0':s -> 0':s
c9 :: c8:c9 -> c8:c9
c10 :: c11:c12 -> c15:c16:c17 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c8:c9 -> c10 -> c13:c14 -> c11:c12
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
c13 :: c13:c14
c14 :: c13:c14
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24 -> c20:c21
DIV :: 0':s -> 0':s -> 0':s -> c22:c23:c24
c22 :: c20:c21 -> c22:c23:c24
c23 :: c22:c23:c24
c24 :: c22:c23:c24 -> c22:c23:c24
A :: c25:c26
c25 :: c25:c26
c26 :: c25:c26
lcm :: 0':s -> 0':s -> 0':s
lcmIter :: 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
if2 :: true:false -> 0':s -> 0':s -> 0':s -> 0':s -> 0':s
ifTimes :: true:false -> 0':s -> 0':s -> 0':s
div :: 0':s -> 0':s -> 0':s -> true:false
a :: b:c
b :: b:c
c :: b:c
hole_c11_27 :: c1
hole_0':s2_27 :: 0':s
hole_c2:c33_27 :: c2:c3
hole_c104_27 :: c10
hole_c4:c55_27 :: c4:c5
hole_c18:c196_27 :: c18:c19
hole_c15:c16:c177_27 :: c15:c16:c17
hole_true:false8_27 :: true:false
hole_c6:c79_27 :: c6:c7
hole_c20:c2110_27 :: c20:c21
hole_c8:c911_27 :: c8:c9
hole_c11:c1212_27 :: c11:c12
hole_c13:c1413_27 :: c13:c14
hole_c22:c23:c2414_27 :: c22:c23:c24
hole_c25:c2615_27 :: c25:c26
hole_b:c16_27 :: b:c
gen_0':s17_27 :: Nat -> 0':s
gen_c15:c16:c1718_27 :: Nat -> c15:c16:c17
gen_c8:c919_27 :: Nat -> c8:c9
gen_c22:c23:c2420_27 :: Nat -> c22:c23:c24


Lemmas:
ge(gen_0':s17_27(n22_27), gen_0':s17_27(n22_27)) -> true, rt in Omega(0)
GE(gen_0':s17_27(n604_27), gen_0':s17_27(n604_27)) -> gen_c15:c16:c1718_27(n604_27), rt in Omega(1 + n604_27)
plus(gen_0':s17_27(n1485_27), gen_0':s17_27(b)) -> gen_0':s17_27(+(n1485_27, b)), rt in Omega(0)
PLUS(gen_0':s17_27(n3404_27), gen_0':s17_27(b)) -> gen_c8:c919_27(n3404_27), rt in Omega(1 + n3404_27)
DIV(gen_0':s17_27(n4879_27), gen_0':s17_27(1), gen_0':s17_27(n4879_27)) -> gen_c22:c23:c2420_27(n4879_27), rt in Omega(1 + n4879_27)
div(gen_0':s17_27(n8087_27), gen_0':s17_27(b), gen_0':s17_27(+(1, n8087_27))) -> false, rt in Omega(0)


Generator Equations:
gen_0':s17_27(0) <=> 0'
gen_0':s17_27(+(x, 1)) <=> s(gen_0':s17_27(x))
gen_c15:c16:c1718_27(0) <=> c15
gen_c15:c16:c1718_27(+(x, 1)) <=> c17(gen_c15:c16:c1718_27(x))
gen_c8:c919_27(0) <=> c8
gen_c8:c919_27(+(x, 1)) <=> c9(gen_c8:c919_27(x))
gen_c22:c23:c2420_27(0) <=> c22(c20)
gen_c22:c23:c2420_27(+(x, 1)) <=> c24(gen_c22:c23:c2420_27(x))


The following defined symbols remain to be analysed:
divisible, LCMITER, lcmIter

They will be analysed ascendingly in the following order:
divisible < LCMITER
divisible < lcmIter
divisible = div