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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 15.4 s]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 9 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 300 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 93 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), 53 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 27 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 124 ms]
        (26) typed CpxTrs


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

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


The TRS R consists of the following rules:

   COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
   COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0), p(z0), z1), GR(add(z0, z1), 0), ADD(z0, z1))
   COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0), p(z0), z1), P(z0))
   COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
   COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0), p(z0), z1), GR(add(z0, z1), 0), ADD(z0, z1))
   COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0), p(z0), z1), P(z0))
   COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0), z0, p(z1)), GR(add(z0, z1), 0), ADD(z0, z1))
   COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0), z0, p(z1)), P(z1))
   GR(0, z0) -> c8
   GR(s(z0), 0) -> c9
   GR(s(z0), s(z1)) -> c10(GR(z0, z1))
   ADD(0, z0) -> c11
   ADD(s(z0), z1) -> c12(ADD(z0, z1))
   EQ(0, 0) -> c13
   EQ(0, s(z0)) -> c14
   EQ(s(z0), 0) -> c15
   EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
   P(0) -> c17
   P(s(z0)) -> c18

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

   cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
   cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0), p(z0), z1)
   cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
   cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0), p(z0), z1)
   cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0), z0, p(z1))
   gr(0, z0) -> false
   gr(s(z0), 0) -> true
   gr(s(z0), s(z1)) -> gr(z0, z1)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   p(0) -> 0
   p(s(z0)) -> z0

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:

   COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
   COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0), p(z0), z1), GR(add(z0, z1), 0), ADD(z0, z1))
   COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0), p(z0), z1), P(z0))
   COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
   COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0), p(z0), z1), GR(add(z0, z1), 0), ADD(z0, z1))
   COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0), p(z0), z1), P(z0))
   COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0), z0, p(z1)), GR(add(z0, z1), 0), ADD(z0, z1))
   COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0), z0, p(z1)), P(z1))
   GR(0, z0) -> c8
   GR(s(z0), 0) -> c9
   GR(s(z0), s(z1)) -> c10(GR(z0, z1))
   ADD(0, z0) -> c11
   ADD(s(z0), z1) -> c12(ADD(z0, z1))
   EQ(0, 0) -> c13
   EQ(0, s(z0)) -> c14
   EQ(s(z0), 0) -> c15
   EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
   P(0) -> c17
   P(s(z0)) -> c18

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

   cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
   cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0), p(z0), z1)
   cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
   cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0), p(z0), z1)
   cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0), z0, p(z1))
   gr(0, z0) -> false
   gr(s(z0), 0) -> true
   gr(s(z0), s(z1)) -> gr(z0, z1)
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   p(0) -> 0
   p(s(z0)) -> z0

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:

   COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
   COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0, z1))
   COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
   COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
   COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0, z1))
   COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
   COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0, z1))
   COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
   GR(0', z0) -> c8
   GR(s(z0), 0') -> c9
   GR(s(z0), s(z1)) -> c10(GR(z0, z1))
   ADD(0', z0) -> c11
   ADD(s(z0), z1) -> c12(ADD(z0, z1))
   EQ(0', 0') -> c13
   EQ(0', s(z0)) -> c14
   EQ(s(z0), 0') -> c15
   EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
   P(0') -> c17
   P(s(z0)) -> c18

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

   cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
   cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
   cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
   cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
   cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
   gr(0', z0) -> false
   gr(s(z0), 0') -> true
   gr(s(z0), s(z1)) -> gr(z0, z1)
   add(0', z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   p(0') -> 0'
   p(s(z0)) -> z0

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
ADD/1

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

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

   COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
   COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
   COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
   COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
   COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
   COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
   COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
   COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
   GR(0', z0) -> c8
   GR(s(z0), 0') -> c9
   GR(s(z0), s(z1)) -> c10(GR(z0, z1))
   ADD(0') -> c11
   ADD(s(z0)) -> c12(ADD(z0))
   EQ(0', 0') -> c13
   EQ(0', s(z0)) -> c14
   EQ(s(z0), 0') -> c15
   EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
   P(0') -> c17
   P(s(z0)) -> c18

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

   cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
   cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
   cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
   cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
   cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
   gr(0', z0) -> false
   gr(s(z0), 0') -> true
   gr(s(z0), s(z1)) -> gr(z0, z1)
   add(0', z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   p(0') -> 0'
   p(s(z0)) -> z0

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

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

(8)
Obligation:
Innermost TRS:
Rules:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
COND1, COND2, gr, GR, add, ADD, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
gr < COND1
GR < COND1
COND1 = COND3
gr < COND2
GR < COND2
add < COND2
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
gr < COND3
gr < cond1
gr < cond2
gr < cond3
GR < COND3
add < COND3
add < cond2
add < cond3
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(10)
Obligation:
Innermost TRS:
Rules:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
gr, COND1, COND2, GR, add, ADD, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
gr < COND1
GR < COND1
COND1 = COND3
gr < COND2
GR < COND2
add < COND2
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
gr < COND3
gr < cond1
gr < cond2
gr < cond3
GR < COND3
add < COND3
add < cond2
add < cond3
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)

Induction Base:
gr(gen_0':s11_19(0), gen_0':s11_19(0)) ->_R^Omega(0)
false

Induction Step:
gr(gen_0':s11_19(+(n16_19, 1)), gen_0':s11_19(+(n16_19, 1))) ->_R^Omega(0)
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) ->_IH
false

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

(12)
Obligation:
Innermost TRS:
Rules:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
GR, COND1, COND2, add, ADD, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
GR < COND1
COND1 = COND3
GR < COND2
add < COND2
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
GR < COND3
add < COND3
add < cond2
add < cond3
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)

Induction Base:
GR(gen_0':s11_19(0), gen_0':s11_19(0)) ->_R^Omega(1)
c8

Induction Step:
GR(gen_0':s11_19(+(n449_19, 1)), gen_0':s11_19(+(n449_19, 1))) ->_R^Omega(1)
c10(GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19))) ->_IH
c10(gen_c8:c9:c1012_19(c450_19))

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:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
GR, COND1, COND2, add, ADD, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
GR < COND1
COND1 = COND3
GR < COND2
add < COND2
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
GR < COND3
add < COND3
add < cond2
add < cond3
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
add, COND1, COND2, ADD, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
COND1 = COND3
add < COND2
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
add < COND3
add < cond2
add < cond3
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

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

Induction Base:
add(gen_0':s11_19(0), gen_0':s11_19(b)) ->_R^Omega(0)
gen_0':s11_19(b)

Induction Step:
add(gen_0':s11_19(+(n1165_19, 1)), gen_0':s11_19(b)) ->_R^Omega(0)
s(add(gen_0':s11_19(n1165_19), gen_0':s11_19(b))) ->_IH
s(gen_0':s11_19(+(b, c1166_19)))

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:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)
add(gen_0':s11_19(n1165_19), gen_0':s11_19(b)) -> gen_0':s11_19(+(n1165_19, b)), rt in Omega(0)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
ADD, COND1, COND2, COND3, eq, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
COND1 = COND3
ADD < COND2
COND2 = COND3
eq < COND2
EQ < COND2
ADD < COND3
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD(gen_0':s11_19(n2496_19)) -> gen_c11:c1213_19(n2496_19), rt in Omega(1 + n2496_19)

Induction Base:
ADD(gen_0':s11_19(0)) ->_R^Omega(1)
c11

Induction Step:
ADD(gen_0':s11_19(+(n2496_19, 1))) ->_R^Omega(1)
c12(ADD(gen_0':s11_19(n2496_19))) ->_IH
c12(gen_c11:c1213_19(c2497_19))

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:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)
add(gen_0':s11_19(n1165_19), gen_0':s11_19(b)) -> gen_0':s11_19(+(n1165_19, b)), rt in Omega(0)
ADD(gen_0':s11_19(n2496_19)) -> gen_c11:c1213_19(n2496_19), rt in Omega(1 + n2496_19)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
eq, COND1, COND2, COND3, EQ, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
COND1 = COND3
COND2 = COND3
eq < COND2
EQ < COND2
eq < cond2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s11_19(n2900_19), gen_0':s11_19(n2900_19)) -> true, rt in Omega(0)

Induction Base:
eq(gen_0':s11_19(0), gen_0':s11_19(0)) ->_R^Omega(0)
true

Induction Step:
eq(gen_0':s11_19(+(n2900_19, 1)), gen_0':s11_19(+(n2900_19, 1))) ->_R^Omega(0)
eq(gen_0':s11_19(n2900_19), gen_0':s11_19(n2900_19)) ->_IH
true

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:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)
add(gen_0':s11_19(n1165_19), gen_0':s11_19(b)) -> gen_0':s11_19(+(n1165_19, b)), rt in Omega(0)
ADD(gen_0':s11_19(n2496_19)) -> gen_c11:c1213_19(n2496_19), rt in Omega(1 + n2496_19)
eq(gen_0':s11_19(n2900_19), gen_0':s11_19(n2900_19)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
EQ, COND1, COND2, COND3, cond1, cond2, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
COND1 = COND3
COND2 = COND3
EQ < COND2
cond1 = cond2
cond1 = cond3
cond2 = cond3

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s11_19(n3569_19), gen_0':s11_19(n3569_19)) -> gen_c13:c14:c15:c1614_19(n3569_19), rt in Omega(1 + n3569_19)

Induction Base:
EQ(gen_0':s11_19(0), gen_0':s11_19(0)) ->_R^Omega(1)
c13

Induction Step:
EQ(gen_0':s11_19(+(n3569_19, 1)), gen_0':s11_19(+(n3569_19, 1))) ->_R^Omega(1)
c16(EQ(gen_0':s11_19(n3569_19), gen_0':s11_19(n3569_19))) ->_IH
c16(gen_c13:c14:c15:c1614_19(c3570_19))

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

(26)
Obligation:
Innermost TRS:
Rules:
COND1(true, z0, z1) -> c(COND2(gr(z0, z1), z0, z1), GR(z0, z1))
COND2(true, z0, z1) -> c1(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND2(true, z0, z1) -> c2(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND2(false, z0, z1) -> c3(COND3(eq(z0, z1), z0, z1), EQ(z0, z1))
COND3(true, z0, z1) -> c4(COND1(gr(add(z0, z1), 0'), p(z0), z1), GR(add(z0, z1), 0'), ADD(z0))
COND3(true, z0, z1) -> c5(COND1(gr(add(z0, z1), 0'), p(z0), z1), P(z0))
COND3(false, z0, z1) -> c6(COND1(gr(add(z0, z1), 0'), z0, p(z1)), GR(add(z0, z1), 0'), ADD(z0))
COND3(false, z0, z1) -> c7(COND1(gr(add(z0, z1), 0'), z0, p(z1)), P(z1))
GR(0', z0) -> c8
GR(s(z0), 0') -> c9
GR(s(z0), s(z1)) -> c10(GR(z0, z1))
ADD(0') -> c11
ADD(s(z0)) -> c12(ADD(z0))
EQ(0', 0') -> c13
EQ(0', s(z0)) -> c14
EQ(s(z0), 0') -> c15
EQ(s(z0), s(z1)) -> c16(EQ(z0, z1))
P(0') -> c17
P(s(z0)) -> c18
cond1(true, z0, z1) -> cond2(gr(z0, z1), z0, z1)
cond2(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond2(false, z0, z1) -> cond3(eq(z0, z1), z0, z1)
cond3(true, z0, z1) -> cond1(gr(add(z0, z1), 0'), p(z0), z1)
cond3(false, z0, z1) -> cond1(gr(add(z0, z1), 0'), z0, p(z1))
gr(0', z0) -> false
gr(s(z0), 0') -> true
gr(s(z0), s(z1)) -> gr(z0, z1)
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
p(0') -> 0'
p(s(z0)) -> z0

Types:
COND1 :: true:false -> 0':s -> 0':s -> c
true :: true:false
c :: c1:c2:c3 -> c8:c9:c10 -> c
COND2 :: true:false -> 0':s -> 0':s -> c1:c2:c3
gr :: 0':s -> 0':s -> true:false
GR :: 0':s -> 0':s -> c8:c9:c10
c1 :: c -> c8:c9:c10 -> c11:c12 -> c1:c2:c3
add :: 0':s -> 0':s -> 0':s
0' :: 0':s
p :: 0':s -> 0':s
ADD :: 0':s -> c11:c12
c2 :: c -> c17:c18 -> c1:c2:c3
P :: 0':s -> c17:c18
false :: true:false
c3 :: c4:c5:c6:c7 -> c13:c14:c15:c16 -> c1:c2:c3
COND3 :: true:false -> 0':s -> 0':s -> c4:c5:c6:c7
eq :: 0':s -> 0':s -> true:false
EQ :: 0':s -> 0':s -> c13:c14:c15:c16
c4 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c5 :: c -> c17:c18 -> c4:c5:c6:c7
c6 :: c -> c8:c9:c10 -> c11:c12 -> c4:c5:c6:c7
c7 :: c -> c17:c18 -> c4:c5:c6:c7
c8 :: c8:c9:c10
s :: 0':s -> 0':s
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
c11 :: c11:c12
c12 :: c11:c12 -> c11:c12
c13 :: c13:c14:c15:c16
c14 :: c13:c14:c15:c16
c15 :: c13:c14:c15:c16
c16 :: c13:c14:c15:c16 -> c13:c14:c15:c16
c17 :: c17:c18
c18 :: c17:c18
cond1 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond2 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
cond3 :: true:false -> 0':s -> 0':s -> cond1:cond2:cond3
hole_c1_19 :: c
hole_true:false2_19 :: true:false
hole_0':s3_19 :: 0':s
hole_c1:c2:c34_19 :: c1:c2:c3
hole_c8:c9:c105_19 :: c8:c9:c10
hole_c11:c126_19 :: c11:c12
hole_c17:c187_19 :: c17:c18
hole_c4:c5:c6:c78_19 :: c4:c5:c6:c7
hole_c13:c14:c15:c169_19 :: c13:c14:c15:c16
hole_cond1:cond2:cond310_19 :: cond1:cond2:cond3
gen_0':s11_19 :: Nat -> 0':s
gen_c8:c9:c1012_19 :: Nat -> c8:c9:c10
gen_c11:c1213_19 :: Nat -> c11:c12
gen_c13:c14:c15:c1614_19 :: Nat -> c13:c14:c15:c16


Lemmas:
gr(gen_0':s11_19(n16_19), gen_0':s11_19(n16_19)) -> false, rt in Omega(0)
GR(gen_0':s11_19(n449_19), gen_0':s11_19(n449_19)) -> gen_c8:c9:c1012_19(n449_19), rt in Omega(1 + n449_19)
add(gen_0':s11_19(n1165_19), gen_0':s11_19(b)) -> gen_0':s11_19(+(n1165_19, b)), rt in Omega(0)
ADD(gen_0':s11_19(n2496_19)) -> gen_c11:c1213_19(n2496_19), rt in Omega(1 + n2496_19)
eq(gen_0':s11_19(n2900_19), gen_0':s11_19(n2900_19)) -> true, rt in Omega(0)
EQ(gen_0':s11_19(n3569_19), gen_0':s11_19(n3569_19)) -> gen_c13:c14:c15:c1614_19(n3569_19), rt in Omega(1 + n3569_19)


Generator Equations:
gen_0':s11_19(0) <=> 0'
gen_0':s11_19(+(x, 1)) <=> s(gen_0':s11_19(x))
gen_c8:c9:c1012_19(0) <=> c8
gen_c8:c9:c1012_19(+(x, 1)) <=> c10(gen_c8:c9:c1012_19(x))
gen_c11:c1213_19(0) <=> c11
gen_c11:c1213_19(+(x, 1)) <=> c12(gen_c11:c1213_19(x))
gen_c13:c14:c15:c1614_19(0) <=> c13
gen_c13:c14:c15:c1614_19(+(x, 1)) <=> c16(gen_c13:c14:c15:c1614_19(x))


The following defined symbols remain to be analysed:
cond2, COND1, COND2, COND3, cond1, cond3

They will be analysed ascendingly in the following order:
COND1 = COND2
COND1 = COND3
COND2 = COND3
cond1 = cond2
cond1 = cond3
cond2 = cond3