WORST_CASE(Omega(n^1),?)
proof of input_jmcYX861ZN.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 47 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 433 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 71 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 125 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 23 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 45 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 1716 ms]
        (28) typed CpxTrs


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

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


The TRS R consists of the following rules:

   eq(0, 0) -> true
   eq(0, s(x)) -> false
   eq(s(x), 0) -> false
   eq(s(x), s(y)) -> eq(x, y)
   or(true, y) -> true
   or(false, y) -> y
   and(true, y) -> y
   and(false, y) -> false
   size(empty) -> 0
   size(edge(x, y, i)) -> s(size(i))
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   reachable(x, y, i) -> reach(x, y, 0, i, i)
   reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
   if1(true, x, y, c, i, j) -> true
   if1(false, x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
   if2(false, x, y, c, i, j) -> false
   if2(true, x, y, c, empty, j) -> false
   if2(true, x, y, c, edge(u, v, i), j) -> or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   and(true, z0) -> z0
   and(false, z0) -> false
   size(empty) -> 0
   size(edge(z0, z1, z2)) -> s(size(z2))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   reachable(z0, z1, z2) -> reach(z0, z1, 0, z2, z2)
   reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
   if1(true, z0, z1, z2, z3, z4) -> true
   if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
   if2(false, z0, z1, z2, z3, z4) -> false
   if2(true, z0, z1, z2, empty, z3) -> false
   if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))
Tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   AND(true, z0) -> c6
   AND(false, z0) -> c7
   SIZE(empty) -> c8
   SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
   LE(0, z0) -> c10
   LE(s(z0), 0) -> c11
   LE(s(z0), s(z1)) -> c12(LE(z0, z1))
   REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0, z2, z2))
   REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
   IF1(true, z0, z1, z2, z3, z4) -> c15
   IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
   IF2(false, z0, z1, z2, z3, z4) -> c17
   IF2(true, z0, z1, z2, empty, z3) -> c18
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
S tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   AND(true, z0) -> c6
   AND(false, z0) -> c7
   SIZE(empty) -> c8
   SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
   LE(0, z0) -> c10
   LE(s(z0), 0) -> c11
   LE(s(z0), s(z1)) -> c12(LE(z0, z1))
   REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0, z2, z2))
   REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
   IF1(true, z0, z1, z2, z3, z4) -> c15
   IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
   IF2(false, z0, z1, z2, z3, z4) -> c17
   IF2(true, z0, z1, z2, empty, z3) -> c18
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, and_2, size_1, le_2, reachable_3, reach_5, if1_6, if2_6

Defined Pair Symbols:   EQ_2, OR_2, AND_2, SIZE_1, LE_2, REACHABLE_3, REACH_5, IF1_6, IF2_6

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6, c7, c8, c9_1, c10, c11, c12_1, c13_1, c14_2, c15, c16_3, c17, c18, c19_2, c20_3, c21_3


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

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

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


The TRS R consists of the following rules:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   AND(true, z0) -> c6
   AND(false, z0) -> c7
   SIZE(empty) -> c8
   SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
   LE(0, z0) -> c10
   LE(s(z0), 0) -> c11
   LE(s(z0), s(z1)) -> c12(LE(z0, z1))
   REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0, z2, z2))
   REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
   IF1(true, z0, z1, z2, z3, z4) -> c15
   IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
   IF2(false, z0, z1, z2, z3, z4) -> c17
   IF2(true, z0, z1, z2, empty, z3) -> c18
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))

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

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   and(true, z0) -> z0
   and(false, z0) -> false
   size(empty) -> 0
   size(edge(z0, z1, z2)) -> s(size(z2))
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   reachable(z0, z1, z2) -> reach(z0, z1, 0, z2, z2)
   reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
   if1(true, z0, z1, z2, z3, z4) -> true
   if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
   if2(false, z0, z1, z2, z3, z4) -> false
   if2(true, z0, z1, z2, empty, z3) -> false
   if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

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

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

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


The TRS R consists of the following rules:

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   AND(true, z0) -> c6
   AND(false, z0) -> c7
   SIZE(empty) -> c8
   SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
   LE(0', z0) -> c10
   LE(s(z0), 0') -> c11
   LE(s(z0), s(z1)) -> c12(LE(z0, z1))
   REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
   REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
   IF1(true, z0, z1, z2, z3, z4) -> c15
   IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
   IF2(false, z0, z1, z2, z3, z4) -> c17
   IF2(true, z0, z1, z2, empty, z3) -> c18
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
   IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))

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

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   and(true, z0) -> z0
   and(false, z0) -> false
   size(empty) -> 0'
   size(edge(z0, z1, z2)) -> s(size(z2))
   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
   reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
   if1(true, z0, z1, z2, z3, z4) -> true
   if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
   if2(false, z0, z1, z2, z3, z4) -> false
   if2(true, z0, z1, z2, empty, z3) -> false
   if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
EQ, SIZE, LE, REACH, eq, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
EQ < REACH
EQ < IF2
SIZE < REACH
LE < REACH
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(10)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
EQ, SIZE, LE, REACH, eq, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
EQ < REACH
EQ < IF2
SIZE < REACH
LE < REACH
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)

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

Induction Step:
EQ(gen_0':s14_22(+(n20_22, 1)), gen_0':s14_22(+(n20_22, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22))) ->_IH
c3(gen_c:c1:c2:c313_22(c21_22))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
EQ, SIZE, LE, REACH, eq, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
EQ < REACH
EQ < IF2
SIZE < REACH
LE < REACH
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
SIZE, LE, REACH, eq, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
SIZE < REACH
LE < REACH
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)

Induction Base:
SIZE(gen_empty:edge16_22(0)) ->_R^Omega(1)
c8

Induction Step:
SIZE(gen_empty:edge16_22(+(n1053_22, 1))) ->_R^Omega(1)
c9(SIZE(gen_empty:edge16_22(n1053_22))) ->_IH
c9(gen_c8:c915_22(c1054_22))

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

(18)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
LE, REACH, eq, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
LE < REACH
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)

Induction Base:
LE(gen_0':s14_22(0), gen_0':s14_22(0)) ->_R^Omega(1)
c10

Induction Step:
LE(gen_0':s14_22(+(n1517_22, 1)), gen_0':s14_22(+(n1517_22, 1))) ->_R^Omega(1)
c12(LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22))) ->_IH
c12(gen_c10:c11:c1217_22(c1518_22))

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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
eq, REACH, IF2, le, size, if2, reach

They will be analysed ascendingly in the following order:
eq < REACH
REACH = IF2
le < REACH
size < REACH
eq < IF2
eq < if2
eq < reach
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s14_22(n2399_22), gen_0':s14_22(n2399_22)) -> true, rt in Omega(0)

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

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

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

(22)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)
eq(gen_0':s14_22(n2399_22), gen_0':s14_22(n2399_22)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
le, REACH, IF2, size, if2, reach

They will be analysed ascendingly in the following order:
REACH = IF2
le < REACH
size < REACH
if2 < IF2
reach < IF2
le < reach
size < reach
if2 = reach

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s14_22(n3100_22), gen_0':s14_22(n3100_22)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s14_22(0), gen_0':s14_22(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s14_22(+(n3100_22, 1)), gen_0':s14_22(+(n3100_22, 1))) ->_R^Omega(0)
le(gen_0':s14_22(n3100_22), gen_0':s14_22(n3100_22)) ->_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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)
eq(gen_0':s14_22(n2399_22), gen_0':s14_22(n2399_22)) -> true, rt in Omega(0)
le(gen_0':s14_22(n3100_22), gen_0':s14_22(n3100_22)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
size, REACH, IF2, if2, reach

They will be analysed ascendingly in the following order:
REACH = IF2
size < REACH
if2 < IF2
reach < IF2
size < reach
if2 = reach

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
size(gen_empty:edge16_22(n3595_22)) -> gen_0':s14_22(n3595_22), rt in Omega(0)

Induction Base:
size(gen_empty:edge16_22(0)) ->_R^Omega(0)
0'

Induction Step:
size(gen_empty:edge16_22(+(n3595_22, 1))) ->_R^Omega(0)
s(size(gen_empty:edge16_22(n3595_22))) ->_IH
s(gen_0':s14_22(c3596_22))

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:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)
eq(gen_0':s14_22(n2399_22), gen_0':s14_22(n2399_22)) -> true, rt in Omega(0)
le(gen_0':s14_22(n3100_22), gen_0':s14_22(n3100_22)) -> true, rt in Omega(0)
size(gen_empty:edge16_22(n3595_22)) -> gen_0':s14_22(n3595_22), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
reach, REACH, IF2, if2

They will be analysed ascendingly in the following order:
REACH = IF2
if2 < IF2
reach < IF2
if2 = reach

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
if2(true, gen_0':s14_22(0), gen_0':s14_22(0), gen_0':s14_22(c), gen_empty:edge16_22(n4400_22), gen_empty:edge16_22(e)) -> *19_22, rt in Omega(0)

Induction Base:
if2(true, gen_0':s14_22(0), gen_0':s14_22(0), gen_0':s14_22(c), gen_empty:edge16_22(0), gen_empty:edge16_22(e))

Induction Step:
if2(true, gen_0':s14_22(0), gen_0':s14_22(0), gen_0':s14_22(c), gen_empty:edge16_22(+(n4400_22, 1)), gen_empty:edge16_22(e)) ->_R^Omega(0)
or(if2(true, gen_0':s14_22(0), gen_0':s14_22(0), gen_0':s14_22(c), gen_empty:edge16_22(n4400_22), gen_empty:edge16_22(e)), and(eq(gen_0':s14_22(0), 0'), reach(0', gen_0':s14_22(0), s(gen_0':s14_22(c)), gen_empty:edge16_22(e), gen_empty:edge16_22(e)))) ->_IH
or(*19_22, and(eq(gen_0':s14_22(0), 0'), reach(0', gen_0':s14_22(0), s(gen_0':s14_22(c)), gen_empty:edge16_22(e), gen_empty:edge16_22(e)))) ->_L^Omega(0)
or(*19_22, and(true, reach(0', gen_0':s14_22(0), s(gen_0':s14_22(c)), gen_empty:edge16_22(e), gen_empty:edge16_22(e)))) ->_R^Omega(0)
or(*19_22, and(true, if1(eq(0', gen_0':s14_22(0)), 0', gen_0':s14_22(0), s(gen_0':s14_22(c)), gen_empty:edge16_22(e), gen_empty:edge16_22(e)))) ->_L^Omega(0)
or(*19_22, and(true, if1(true, 0', gen_0':s14_22(0), s(gen_0':s14_22(c)), gen_empty:edge16_22(e), gen_empty:edge16_22(e)))) ->_R^Omega(0)
or(*19_22, and(true, true)) ->_R^Omega(0)
or(*19_22, true)

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

(28)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
AND(true, z0) -> c6
AND(false, z0) -> c7
SIZE(empty) -> c8
SIZE(edge(z0, z1, z2)) -> c9(SIZE(z2))
LE(0', z0) -> c10
LE(s(z0), 0') -> c11
LE(s(z0), s(z1)) -> c12(LE(z0, z1))
REACHABLE(z0, z1, z2) -> c13(REACH(z0, z1, 0', z2, z2))
REACH(z0, z1, z2, z3, z4) -> c14(IF1(eq(z0, z1), z0, z1, z2, z3, z4), EQ(z0, z1))
IF1(true, z0, z1, z2, z3, z4) -> c15
IF1(false, z0, z1, z2, z3, z4) -> c16(IF2(le(z2, size(z4)), z0, z1, z2, z3, z4), LE(z2, size(z4)), SIZE(z4))
IF2(false, z0, z1, z2, z3, z4) -> c17
IF2(true, z0, z1, z2, empty, z3) -> c18
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c19(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), IF2(true, z0, z1, z2, z5, z6))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c20(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), EQ(z0, z3))
IF2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> c21(OR(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6))), AND(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)), REACH(z4, z1, s(z2), z6, z6))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
and(true, z0) -> z0
and(false, z0) -> false
size(empty) -> 0'
size(edge(z0, z1, z2)) -> s(size(z2))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
reachable(z0, z1, z2) -> reach(z0, z1, 0', z2, z2)
reach(z0, z1, z2, z3, z4) -> if1(eq(z0, z1), z0, z1, z2, z3, z4)
if1(true, z0, z1, z2, z3, z4) -> true
if1(false, z0, z1, z2, z3, z4) -> if2(le(z2, size(z4)), z0, z1, z2, z3, z4)
if2(false, z0, z1, z2, z3, z4) -> false
if2(true, z0, z1, z2, empty, z3) -> false
if2(true, z0, z1, z2, edge(z3, z4, z5), z6) -> or(if2(true, z0, z1, z2, z5, z6), and(eq(z0, z3), reach(z4, z1, s(z2), z6, z6)))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
AND :: true:false -> true:false -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
SIZE :: empty:edge -> c8:c9
empty :: empty:edge
c8 :: c8:c9
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c9 :: c8:c9 -> c8:c9
LE :: 0':s -> 0':s -> c10:c11:c12
c10 :: c10:c11:c12
c11 :: c10:c11:c12
c12 :: c10:c11:c12 -> c10:c11:c12
REACHABLE :: 0':s -> 0':s -> empty:edge -> c13
c13 :: c14 -> c13
REACH :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c14
c14 :: c15:c16 -> c:c1:c2:c3 -> c14
IF1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c15:c16
eq :: 0':s -> 0':s -> true:false
c15 :: c15:c16
c16 :: c17:c18:c19:c20:c21 -> c10:c11:c12 -> c8:c9 -> c15:c16
IF2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> c17:c18:c19:c20:c21
le :: 0':s -> 0':s -> true:false
size :: empty:edge -> 0':s
c17 :: c17:c18:c19:c20:c21
c18 :: c17:c18:c19:c20:c21
c19 :: c4:c5 -> c17:c18:c19:c20:c21 -> c17:c18:c19:c20:c21
if2 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
and :: true:false -> true:false -> true:false
reach :: 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
c20 :: c4:c5 -> c6:c7 -> c:c1:c2:c3 -> c17:c18:c19:c20:c21
c21 :: c4:c5 -> c6:c7 -> c14 -> c17:c18:c19:c20:c21
or :: true:false -> true:false -> true:false
reachable :: 0':s -> 0':s -> empty:edge -> true:false
if1 :: true:false -> 0':s -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_22 :: c:c1:c2:c3
hole_0':s2_22 :: 0':s
hole_c4:c53_22 :: c4:c5
hole_true:false4_22 :: true:false
hole_c6:c75_22 :: c6:c7
hole_c8:c96_22 :: c8:c9
hole_empty:edge7_22 :: empty:edge
hole_c10:c11:c128_22 :: c10:c11:c12
hole_c139_22 :: c13
hole_c1410_22 :: c14
hole_c15:c1611_22 :: c15:c16
hole_c17:c18:c19:c20:c2112_22 :: c17:c18:c19:c20:c21
gen_c:c1:c2:c313_22 :: Nat -> c:c1:c2:c3
gen_0':s14_22 :: Nat -> 0':s
gen_c8:c915_22 :: Nat -> c8:c9
gen_empty:edge16_22 :: Nat -> empty:edge
gen_c10:c11:c1217_22 :: Nat -> c10:c11:c12
gen_c17:c18:c19:c20:c2118_22 :: Nat -> c17:c18:c19:c20:c21


Lemmas:
EQ(gen_0':s14_22(n20_22), gen_0':s14_22(n20_22)) -> gen_c:c1:c2:c313_22(n20_22), rt in Omega(1 + n20_22)
SIZE(gen_empty:edge16_22(n1053_22)) -> gen_c8:c915_22(n1053_22), rt in Omega(1 + n1053_22)
LE(gen_0':s14_22(n1517_22), gen_0':s14_22(n1517_22)) -> gen_c10:c11:c1217_22(n1517_22), rt in Omega(1 + n1517_22)
eq(gen_0':s14_22(n2399_22), gen_0':s14_22(n2399_22)) -> true, rt in Omega(0)
le(gen_0':s14_22(n3100_22), gen_0':s14_22(n3100_22)) -> true, rt in Omega(0)
size(gen_empty:edge16_22(n3595_22)) -> gen_0':s14_22(n3595_22), rt in Omega(0)
if2(true, gen_0':s14_22(0), gen_0':s14_22(0), gen_0':s14_22(c), gen_empty:edge16_22(n4400_22), gen_empty:edge16_22(e)) -> *19_22, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c313_22(0) <=> c
gen_c:c1:c2:c313_22(+(x, 1)) <=> c3(gen_c:c1:c2:c313_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c8:c915_22(0) <=> c8
gen_c8:c915_22(+(x, 1)) <=> c9(gen_c8:c915_22(x))
gen_empty:edge16_22(0) <=> empty
gen_empty:edge16_22(+(x, 1)) <=> edge(0', 0', gen_empty:edge16_22(x))
gen_c10:c11:c1217_22(0) <=> c10
gen_c10:c11:c1217_22(+(x, 1)) <=> c12(gen_c10:c11:c1217_22(x))
gen_c17:c18:c19:c20:c2118_22(0) <=> c17
gen_c17:c18:c19:c20:c2118_22(+(x, 1)) <=> c19(c4, gen_c17:c18:c19:c20:c2118_22(x))


The following defined symbols remain to be analysed:
reach, REACH, IF2

They will be analysed ascendingly in the following order:
REACH = IF2
if2 < IF2
reach < IF2
if2 = reach