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), 2287 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) typed CpxTrs
(7) OrderProof [LOWER BOUND(ID), 27 ms]
(8) typed CpxTrs
(9) RewriteLemmaProof [LOWER BOUND(ID), 250 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 132 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 99.6 s]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 60 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 128 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 121 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 71 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (28) 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:

   PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
   PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
   IFPLUS(true, z0, z1) -> c3(P(z1))
   IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c5(TIMESITER(0, z0, z1, 0))
   TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   IFTIMES(true, z0, z1, z2, z3) -> c7
   IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
   IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
   ISZERO(0) -> c10
   ISZERO(s(0)) -> c11
   ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
   INC(0) -> c13
   INC(s(z0)) -> c14(INC(z0))
   INC(z0) -> c15
   P(0) -> c16
   P(s(z0)) -> c17
   P(s(s(z0))) -> c18(P(s(z0)))
   GE(z0, 0) -> c19
   GE(0, s(z0)) -> c20
   GE(s(z0), s(z1)) -> c21(GE(z0, z1))
   F0(0, z0, z1) -> c22(F1(z1, z0, z1))
   F0(z0, z1, z2) -> c23
   F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
   F1(z0, z1, z2) -> c25
   F2(z0, 1, z1) -> c26(F0(z0, z1, z1))

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

   plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
   ifPlus(true, z0, z1) -> p(z1)
   ifPlus(false, z0, z1) -> plus(p(z0), z1)
   times(z0, z1) -> timesIter(0, z0, z1, 0)
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z3
   ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   inc(0) -> s(0)
   inc(s(z0)) -> s(inc(z0))
   inc(z0) -> s(z0)
   p(0) -> 0
   p(s(z0)) -> z0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   f0(0, z0, z1) -> f1(z1, z0, z1)
   f0(z0, z1, z2) -> d
   f1(z0, z1, z2) -> f2(z0, z1, z2)
   f1(z0, z1, z2) -> c
   f2(z0, 1, z1) -> f0(z0, z1, z1)

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

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

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


The TRS R consists of the following rules:

   PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
   PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
   IFPLUS(true, z0, z1) -> c3(P(z1))
   IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c5(TIMESITER(0, z0, z1, 0))
   TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   IFTIMES(true, z0, z1, z2, z3) -> c7
   IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
   IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
   ISZERO(0) -> c10
   ISZERO(s(0)) -> c11
   ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
   INC(0) -> c13
   INC(s(z0)) -> c14(INC(z0))
   INC(z0) -> c15
   P(0) -> c16
   P(s(z0)) -> c17
   P(s(s(z0))) -> c18(P(s(z0)))
   GE(z0, 0) -> c19
   GE(0, s(z0)) -> c20
   GE(s(z0), s(z1)) -> c21(GE(z0, z1))
   F0(0, z0, z1) -> c22(F1(z1, z0, z1))
   F0(z0, z1, z2) -> c23
   F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
   F1(z0, z1, z2) -> c25
   F2(z0, 1, z1) -> c26(F0(z0, z1, z1))

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

   plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
   ifPlus(true, z0, z1) -> p(z1)
   ifPlus(false, z0, z1) -> plus(p(z0), z1)
   times(z0, z1) -> timesIter(0, z0, z1, 0)
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z3
   ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   inc(0) -> s(0)
   inc(s(z0)) -> s(inc(z0))
   inc(z0) -> s(z0)
   p(0) -> 0
   p(s(z0)) -> z0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   f0(0, z0, z1) -> f1(z1, z0, z1)
   f0(z0, z1, z2) -> d
   f1(z0, z1, z2) -> f2(z0, z1, z2)
   f1(z0, z1, z2) -> c
   f2(z0, 1, z1) -> f0(z0, z1, z1)

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

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

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


The TRS R consists of the following rules:

   PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
   PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
   IFPLUS(true, z0, z1) -> c3(P(z1))
   IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
   TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
   IFTIMES(true, z0, z1, z2, z3) -> c7
   IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
   IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
   ISZERO(0') -> c10
   ISZERO(s(0')) -> c11
   ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
   INC(0') -> c13
   INC(s(z0)) -> c14(INC(z0))
   INC(z0) -> c15
   P(0') -> c16
   P(s(z0)) -> c17
   P(s(s(z0))) -> c18(P(s(z0)))
   GE(z0, 0') -> c19
   GE(0', s(z0)) -> c20
   GE(s(z0), s(z1)) -> c21(GE(z0, z1))
   F0(0', z0, z1) -> c22(F1(z1, z0, z1))
   F0(z0, z1, z2) -> c23
   F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
   F1(z0, z1, z2) -> c25
   F2(z0, 1', z1) -> c26(F0(z0, z1, z1))

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

   plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
   ifPlus(true, z0, z1) -> p(z1)
   ifPlus(false, z0, z1) -> plus(p(z0), z1)
   times(z0, z1) -> timesIter(0', z0, z1, 0')
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z3
   ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
   isZero(0') -> true
   isZero(s(0')) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   inc(0') -> s(0')
   inc(s(z0)) -> s(inc(z0))
   inc(z0) -> s(z0)
   p(0') -> 0'
   p(s(z0)) -> z0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   f0(0', z0, z1) -> f1(z1, z0, z1)
   f0(z0, z1, z2) -> d
   f1(z0, z1, z2) -> f2(z0, z1, z2)
   f1(z0, z1, z2) -> c
   f2(z0, 1', z1) -> f0(z0, z1, z1)

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

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

(6)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21

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

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS, isZero, inc, ISZERO, INC, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
isZero < PLUS
inc < PLUS
ISZERO < PLUS
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
isZero < plus
inc < TIMESITER
inc < plus
inc < timesIter
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(8)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
isZero, PLUS, inc, ISZERO, INC, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
isZero < PLUS
inc < PLUS
ISZERO < PLUS
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
isZero < plus
inc < TIMESITER
inc < plus
inc < timesIter
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)

Induction Base:
isZero(gen_0':s:1'16_27(+(1, 0))) ->_R^Omega(0)
false

Induction Step:
isZero(gen_0':s:1'16_27(+(1, +(n22_27, 1)))) ->_R^Omega(0)
isZero(s(gen_0':s:1'16_27(n22_27))) ->_IH
false

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

(10)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
inc, PLUS, ISZERO, INC, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
inc < PLUS
ISZERO < PLUS
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
inc < TIMESITER
inc < plus
inc < timesIter
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)

Induction Base:
inc(gen_0':s:1'16_27(0)) ->_R^Omega(0)
s(0')

Induction Step:
inc(gen_0':s:1'16_27(+(n296_27, 1))) ->_R^Omega(0)
s(inc(gen_0':s:1'16_27(n296_27))) ->_IH
s(gen_0':s:1'16_27(+(1, c297_27)))

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:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
ISZERO, PLUS, INC, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
ISZERO < PLUS
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)

Induction Base:
ISZERO(gen_0':s:1'16_27(+(2, 0)))

Induction Step:
ISZERO(gen_0':s:1'16_27(+(2, +(n1222_27, 1)))) ->_R^Omega(1)
c12(ISZERO(s(gen_0':s:1'16_27(+(1, n1222_27))))) ->_IH
c12(*21_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:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
ISZERO, PLUS, INC, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
ISZERO < PLUS
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
INC, PLUS, P, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
INC < PLUS
P < PLUS
p < PLUS
PLUS < TIMESITER
INC < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)

Induction Base:
INC(gen_0':s:1'16_27(0)) ->_R^Omega(1)
c13

Induction Step:
INC(gen_0':s:1'16_27(+(n74164_27, 1))) ->_R^Omega(1)
c14(INC(gen_0':s:1'16_27(n74164_27))) ->_IH
c14(gen_c13:c14:c1518_27(c74165_27))

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

(20)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
P, PLUS, p, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
P < PLUS
p < PLUS
PLUS < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s:1'16_27(+(2, n74758_27))) -> *21_27, rt in Omega(n74758_27)

Induction Base:
P(gen_0':s:1'16_27(+(2, 0)))

Induction Step:
P(gen_0':s:1'16_27(+(2, +(n74758_27, 1)))) ->_R^Omega(1)
c18(P(s(gen_0':s:1'16_27(+(1, n74758_27))))) ->_IH
c18(*21_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:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)
P(gen_0':s:1'16_27(+(2, n74758_27))) -> *21_27, rt in Omega(n74758_27)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
p, PLUS, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
p < PLUS
PLUS < TIMESITER
p < plus
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s:1'16_27(+(2, n75532_27))) -> *21_27, rt in Omega(0)

Induction Base:
p(gen_0':s:1'16_27(+(2, 0)))

Induction Step:
p(gen_0':s:1'16_27(+(2, +(n75532_27, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s:1'16_27(+(1, n75532_27))))) ->_IH
s(*21_27)

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:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)
P(gen_0':s:1'16_27(+(2, n74758_27))) -> *21_27, rt in Omega(n74758_27)
p(gen_0':s:1'16_27(+(2, n75532_27))) -> *21_27, rt in Omega(0)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
PLUS, TIMESITER, ge, GE, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
PLUS < TIMESITER
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s:1'16_27(n77658_27), gen_0':s:1'16_27(n77658_27)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s:1'16_27(0), gen_0':s:1'16_27(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s:1'16_27(+(n77658_27, 1)), gen_0':s:1'16_27(+(n77658_27, 1))) ->_R^Omega(0)
ge(gen_0':s:1'16_27(n77658_27), gen_0':s:1'16_27(n77658_27)) ->_IH
true

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:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)
P(gen_0':s:1'16_27(+(2, n74758_27))) -> *21_27, rt in Omega(n74758_27)
p(gen_0':s:1'16_27(+(2, n75532_27))) -> *21_27, rt in Omega(0)
ge(gen_0':s:1'16_27(n77658_27), gen_0':s:1'16_27(n77658_27)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
GE, TIMESITER, plus, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
GE < TIMESITER
plus < TIMESITER
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s:1'16_27(n78430_27), gen_0':s:1'16_27(n78430_27)) -> gen_c19:c20:c2120_27(n78430_27), rt in Omega(1 + n78430_27)

Induction Base:
GE(gen_0':s:1'16_27(0), gen_0':s:1'16_27(0)) ->_R^Omega(1)
c19

Induction Step:
GE(gen_0':s:1'16_27(+(n78430_27, 1)), gen_0':s:1'16_27(+(n78430_27, 1))) ->_R^Omega(1)
c21(GE(gen_0':s:1'16_27(n78430_27), gen_0':s:1'16_27(n78430_27))) ->_IH
c21(gen_c19:c20:c2120_27(c78431_27))

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

(28)
Obligation:
Innermost TRS:
Rules:
PLUS(z0, z1) -> c1(IFPLUS(isZero(z0), z0, inc(z1)), ISZERO(z0))
PLUS(z0, z1) -> c2(IFPLUS(isZero(z0), z0, inc(z1)), INC(z1))
IFPLUS(true, z0, z1) -> c3(P(z1))
IFPLUS(false, z0, z1) -> c4(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c5(TIMESITER(0', z0, z1, 0'))
TIMESITER(z0, z1, z2, z3) -> c6(IFTIMES(ge(z0, z1), z0, z1, z2, z3), GE(z0, z1))
IFTIMES(true, z0, z1, z2, z3) -> c7
IFTIMES(false, z0, z1, z2, z3) -> c8(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), INC(z0))
IFTIMES(false, z0, z1, z2, z3) -> c9(TIMESITER(inc(z0), z1, z2, plus(z3, z2)), PLUS(z3, z2))
ISZERO(0') -> c10
ISZERO(s(0')) -> c11
ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
INC(0') -> c13
INC(s(z0)) -> c14(INC(z0))
INC(z0) -> c15
P(0') -> c16
P(s(z0)) -> c17
P(s(s(z0))) -> c18(P(s(z0)))
GE(z0, 0') -> c19
GE(0', s(z0)) -> c20
GE(s(z0), s(z1)) -> c21(GE(z0, z1))
F0(0', z0, z1) -> c22(F1(z1, z0, z1))
F0(z0, z1, z2) -> c23
F1(z0, z1, z2) -> c24(F2(z0, z1, z2))
F1(z0, z1, z2) -> c25
F2(z0, 1', z1) -> c26(F0(z0, z1, z1))
plus(z0, z1) -> ifPlus(isZero(z0), z0, inc(z1))
ifPlus(true, z0, z1) -> p(z1)
ifPlus(false, z0, z1) -> plus(p(z0), z1)
times(z0, z1) -> timesIter(0', z0, z1, 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z0, z1), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z3
ifTimes(false, z0, z1, z2, z3) -> timesIter(inc(z0), z1, z2, plus(z3, z2))
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
inc(0') -> s(0')
inc(s(z0)) -> s(inc(z0))
inc(z0) -> s(z0)
p(0') -> 0'
p(s(z0)) -> z0
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
f0(0', z0, z1) -> f1(z1, z0, z1)
f0(z0, z1, z2) -> d
f1(z0, z1, z2) -> f2(z0, z1, z2)
f1(z0, z1, z2) -> c
f2(z0, 1', z1) -> f0(z0, z1, z1)

Types:
PLUS :: 0':s:1' -> 0':s:1' -> c1:c2
c1 :: c3:c4 -> c10:c11:c12 -> c1:c2
IFPLUS :: true:false -> 0':s:1' -> 0':s:1' -> c3:c4
isZero :: 0':s:1' -> true:false
inc :: 0':s:1' -> 0':s:1'
ISZERO :: 0':s:1' -> c10:c11:c12
c2 :: c3:c4 -> c13:c14:c15 -> c1:c2
INC :: 0':s:1' -> c13:c14:c15
true :: true:false
c3 :: c16:c17:c18 -> c3:c4
P :: 0':s:1' -> c16:c17:c18
false :: true:false
c4 :: c1:c2 -> c16:c17:c18 -> c3:c4
p :: 0':s:1' -> 0':s:1'
TIMES :: 0':s:1' -> 0':s:1' -> c5
c5 :: c6 -> c5
TIMESITER :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c6
0' :: 0':s:1'
c6 :: c7:c8:c9 -> c19:c20:c21 -> c6
IFTIMES :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> c7:c8:c9
ge :: 0':s:1' -> 0':s:1' -> true:false
GE :: 0':s:1' -> 0':s:1' -> c19:c20:c21
c7 :: c7:c8:c9
c8 :: c6 -> c13:c14:c15 -> c7:c8:c9
plus :: 0':s:1' -> 0':s:1' -> 0':s:1'
c9 :: c6 -> c1:c2 -> c7:c8:c9
c10 :: c10:c11:c12
s :: 0':s:1' -> 0':s:1'
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
c13 :: c13:c14:c15
c14 :: c13:c14:c15 -> c13:c14:c15
c15 :: c13:c14:c15
c16 :: c16:c17:c18
c17 :: c16:c17:c18
c18 :: c16:c17:c18 -> c16:c17:c18
c19 :: c19:c20:c21
c20 :: c19:c20:c21
c21 :: c19:c20:c21 -> c19:c20:c21
F0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c22:c23
c22 :: c24:c25 -> c22:c23
F1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c24:c25
c23 :: c22:c23
c24 :: c26 -> c24:c25
F2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> c26
c25 :: c24:c25
1' :: 0':s:1'
c26 :: c22:c23 -> c26
ifPlus :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1'
times :: 0':s:1' -> 0':s:1' -> 0':s:1'
timesIter :: 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
ifTimes :: true:false -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1' -> 0':s:1'
f0 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
f1 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
d :: d:c
f2 :: 0':s:1' -> 0':s:1' -> 0':s:1' -> d:c
c :: d:c
hole_c1:c21_27 :: c1:c2
hole_0':s:1'2_27 :: 0':s:1'
hole_c3:c43_27 :: c3:c4
hole_c10:c11:c124_27 :: c10:c11:c12
hole_true:false5_27 :: true:false
hole_c13:c14:c156_27 :: c13:c14:c15
hole_c16:c17:c187_27 :: c16:c17:c18
hole_c58_27 :: c5
hole_c69_27 :: c6
hole_c7:c8:c910_27 :: c7:c8:c9
hole_c19:c20:c2111_27 :: c19:c20:c21
hole_c22:c2312_27 :: c22:c23
hole_c24:c2513_27 :: c24:c25
hole_c2614_27 :: c26
hole_d:c15_27 :: d:c
gen_0':s:1'16_27 :: Nat -> 0':s:1'
gen_c10:c11:c1217_27 :: Nat -> c10:c11:c12
gen_c13:c14:c1518_27 :: Nat -> c13:c14:c15
gen_c16:c17:c1819_27 :: Nat -> c16:c17:c18
gen_c19:c20:c2120_27 :: Nat -> c19:c20:c21


Lemmas:
isZero(gen_0':s:1'16_27(+(1, n22_27))) -> false, rt in Omega(0)
inc(gen_0':s:1'16_27(n296_27)) -> gen_0':s:1'16_27(+(1, n296_27)), rt in Omega(0)
ISZERO(gen_0':s:1'16_27(+(2, n1222_27))) -> *21_27, rt in Omega(n1222_27)
INC(gen_0':s:1'16_27(n74164_27)) -> gen_c13:c14:c1518_27(n74164_27), rt in Omega(1 + n74164_27)
P(gen_0':s:1'16_27(+(2, n74758_27))) -> *21_27, rt in Omega(n74758_27)
p(gen_0':s:1'16_27(+(2, n75532_27))) -> *21_27, rt in Omega(0)
ge(gen_0':s:1'16_27(n77658_27), gen_0':s:1'16_27(n77658_27)) -> true, rt in Omega(0)
GE(gen_0':s:1'16_27(n78430_27), gen_0':s:1'16_27(n78430_27)) -> gen_c19:c20:c2120_27(n78430_27), rt in Omega(1 + n78430_27)


Generator Equations:
gen_0':s:1'16_27(0) <=> 0'
gen_0':s:1'16_27(+(x, 1)) <=> s(gen_0':s:1'16_27(x))
gen_c10:c11:c1217_27(0) <=> c10
gen_c10:c11:c1217_27(+(x, 1)) <=> c12(gen_c10:c11:c1217_27(x))
gen_c13:c14:c1518_27(0) <=> c13
gen_c13:c14:c1518_27(+(x, 1)) <=> c14(gen_c13:c14:c1518_27(x))
gen_c16:c17:c1819_27(0) <=> c16
gen_c16:c17:c1819_27(+(x, 1)) <=> c18(gen_c16:c17:c1819_27(x))
gen_c19:c20:c2120_27(0) <=> c19
gen_c19:c20:c2120_27(+(x, 1)) <=> c21(gen_c19:c20:c2120_27(x))


The following defined symbols remain to be analysed:
plus, TIMESITER, F0, F1, F2, timesIter, f0, f1, f2

They will be analysed ascendingly in the following order:
plus < TIMESITER
plus < timesIter
F0 = F1
F0 = F2
F1 = F2
f0 = f1
f0 = f2
f1 = f2