MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { 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
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i
  , reach(x, y, i, h) ->
    if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
  , if1(true(), b1, b2, b3, x, y, i, h) -> true()
  , if1(false(), b1, b2, b3, x, y, i, h) ->
    if2(b1, b2, b3, x, y, i, h)
  , if2(true(), b2, b3, x, y, i, h) -> false()
  , if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
  , if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h)
  , if3(false(), b3, x, y, i, h) ->
    reach(x, y, rest(i), edge(from(i), to(i), h))
  , if4(true(), x, y, i, h) -> true()
  , if4(false(), x, y, i, h) ->
    or(reach(x, y, rest(i), h),
       reach(to(i), y, union(rest(i), h), empty())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(x)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , or^#(true(), y) -> c_5()
  , or^#(false(), y) -> c_6()
  , union^#(empty(), h) -> c_7()
  , union^#(edge(x, y, i), h) -> c_8(union^#(i, h))
  , isEmpty^#(empty()) -> c_9()
  , isEmpty^#(edge(x, y, i)) -> c_10()
  , from^#(edge(x, y, i)) -> c_11()
  , to^#(edge(x, y, i)) -> c_12()
  , rest^#(empty()) -> c_13()
  , rest^#(edge(x, y, i)) -> c_14()
  , reach^#(x, y, i, h) ->
    c_15(if1^#(eq(x, y),
               isEmpty(i),
               eq(x, from(i)),
               eq(y, to(i)),
               x,
               y,
               i,
               h),
         eq^#(x, y),
         isEmpty^#(i),
         eq^#(x, from(i)),
         from^#(i),
         eq^#(y, to(i)),
         to^#(i))
  , if1^#(true(), b1, b2, b3, x, y, i, h) -> c_16()
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_17(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(true(), b2, b3, x, y, i, h) -> c_18()
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_19(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_20(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
         rest^#(i),
         from^#(i),
         to^#(i))
  , if4^#(true(), x, y, i, h) -> c_22()
  , if4^#(false(), x, y, i, h) ->
    c_23(or^#(reach(x, y, rest(i), h),
              reach(to(i), y, union(rest(i), h), empty())),
         reach^#(x, y, rest(i), h),
         rest^#(i),
         reach^#(to(i), y, union(rest(i), h), empty()),
         to^#(i),
         union^#(rest(i), h),
         rest^#(i)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(x)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , or^#(true(), y) -> c_5()
  , or^#(false(), y) -> c_6()
  , union^#(empty(), h) -> c_7()
  , union^#(edge(x, y, i), h) -> c_8(union^#(i, h))
  , isEmpty^#(empty()) -> c_9()
  , isEmpty^#(edge(x, y, i)) -> c_10()
  , from^#(edge(x, y, i)) -> c_11()
  , to^#(edge(x, y, i)) -> c_12()
  , rest^#(empty()) -> c_13()
  , rest^#(edge(x, y, i)) -> c_14()
  , reach^#(x, y, i, h) ->
    c_15(if1^#(eq(x, y),
               isEmpty(i),
               eq(x, from(i)),
               eq(y, to(i)),
               x,
               y,
               i,
               h),
         eq^#(x, y),
         isEmpty^#(i),
         eq^#(x, from(i)),
         from^#(i),
         eq^#(y, to(i)),
         to^#(i))
  , if1^#(true(), b1, b2, b3, x, y, i, h) -> c_16()
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_17(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(true(), b2, b3, x, y, i, h) -> c_18()
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_19(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_20(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
         rest^#(i),
         from^#(i),
         to^#(i))
  , if4^#(true(), x, y, i, h) -> c_22()
  , if4^#(false(), x, y, i, h) ->
    c_23(or^#(reach(x, y, rest(i), h),
              reach(to(i), y, union(rest(i), h), empty())),
         reach^#(x, y, rest(i), h),
         rest^#(i),
         reach^#(to(i), y, union(rest(i), h), empty()),
         to^#(i),
         union^#(rest(i), h),
         rest^#(i)) }
Weak Trs:
  { 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
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i
  , reach(x, y, i, h) ->
    if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
  , if1(true(), b1, b2, b3, x, y, i, h) -> true()
  , if1(false(), b1, b2, b3, x, y, i, h) ->
    if2(b1, b2, b3, x, y, i, h)
  , if2(true(), b2, b3, x, y, i, h) -> false()
  , if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
  , if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h)
  , if3(false(), b3, x, y, i, h) ->
    reach(x, y, rest(i), edge(from(i), to(i), h))
  , if4(true(), x, y, i, h) -> true()
  , if4(false(), x, y, i, h) ->
    or(reach(x, y, rest(i), h),
       reach(to(i), y, union(rest(i), h), empty())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,3,5,6,7,9,10,11,12,13,14,16,18,22} by applications of
Pre({1,2,3,5,6,7,9,10,11,12,13,14,16,18,22}) =
{4,8,15,17,20,21,23}. Here rules are labeled as follows:

  DPs:
    { 1: eq^#(0(), 0()) -> c_1()
    , 2: eq^#(0(), s(x)) -> c_2()
    , 3: eq^#(s(x), 0()) -> c_3()
    , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
    , 5: or^#(true(), y) -> c_5()
    , 6: or^#(false(), y) -> c_6()
    , 7: union^#(empty(), h) -> c_7()
    , 8: union^#(edge(x, y, i), h) -> c_8(union^#(i, h))
    , 9: isEmpty^#(empty()) -> c_9()
    , 10: isEmpty^#(edge(x, y, i)) -> c_10()
    , 11: from^#(edge(x, y, i)) -> c_11()
    , 12: to^#(edge(x, y, i)) -> c_12()
    , 13: rest^#(empty()) -> c_13()
    , 14: rest^#(edge(x, y, i)) -> c_14()
    , 15: reach^#(x, y, i, h) ->
          c_15(if1^#(eq(x, y),
                     isEmpty(i),
                     eq(x, from(i)),
                     eq(y, to(i)),
                     x,
                     y,
                     i,
                     h),
               eq^#(x, y),
               isEmpty^#(i),
               eq^#(x, from(i)),
               from^#(i),
               eq^#(y, to(i)),
               to^#(i))
    , 16: if1^#(true(), b1, b2, b3, x, y, i, h) -> c_16()
    , 17: if1^#(false(), b1, b2, b3, x, y, i, h) ->
          c_17(if2^#(b1, b2, b3, x, y, i, h))
    , 18: if2^#(true(), b2, b3, x, y, i, h) -> c_18()
    , 19: if2^#(false(), b2, b3, x, y, i, h) ->
          c_19(if3^#(b2, b3, x, y, i, h))
    , 20: if3^#(true(), b3, x, y, i, h) -> c_20(if4^#(b3, x, y, i, h))
    , 21: if3^#(false(), b3, x, y, i, h) ->
          c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
               rest^#(i),
               from^#(i),
               to^#(i))
    , 22: if4^#(true(), x, y, i, h) -> c_22()
    , 23: if4^#(false(), x, y, i, h) ->
          c_23(or^#(reach(x, y, rest(i), h),
                    reach(to(i), y, union(rest(i), h), empty())),
               reach^#(x, y, rest(i), h),
               rest^#(i),
               reach^#(to(i), y, union(rest(i), h), empty()),
               to^#(i),
               union^#(rest(i), h),
               rest^#(i)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , union^#(edge(x, y, i), h) -> c_8(union^#(i, h))
  , reach^#(x, y, i, h) ->
    c_15(if1^#(eq(x, y),
               isEmpty(i),
               eq(x, from(i)),
               eq(y, to(i)),
               x,
               y,
               i,
               h),
         eq^#(x, y),
         isEmpty^#(i),
         eq^#(x, from(i)),
         from^#(i),
         eq^#(y, to(i)),
         to^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_17(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_19(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_20(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
         rest^#(i),
         from^#(i),
         to^#(i))
  , if4^#(false(), x, y, i, h) ->
    c_23(or^#(reach(x, y, rest(i), h),
              reach(to(i), y, union(rest(i), h), empty())),
         reach^#(x, y, rest(i), h),
         rest^#(i),
         reach^#(to(i), y, union(rest(i), h), empty()),
         to^#(i),
         union^#(rest(i), h),
         rest^#(i)) }
Weak DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(x)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , or^#(true(), y) -> c_5()
  , or^#(false(), y) -> c_6()
  , union^#(empty(), h) -> c_7()
  , isEmpty^#(empty()) -> c_9()
  , isEmpty^#(edge(x, y, i)) -> c_10()
  , from^#(edge(x, y, i)) -> c_11()
  , to^#(edge(x, y, i)) -> c_12()
  , rest^#(empty()) -> c_13()
  , rest^#(edge(x, y, i)) -> c_14()
  , if1^#(true(), b1, b2, b3, x, y, i, h) -> c_16()
  , if2^#(true(), b2, b3, x, y, i, h) -> c_18()
  , if4^#(true(), x, y, i, h) -> c_22() }
Weak Trs:
  { 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
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i
  , reach(x, y, i, h) ->
    if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
  , if1(true(), b1, b2, b3, x, y, i, h) -> true()
  , if1(false(), b1, b2, b3, x, y, i, h) ->
    if2(b1, b2, b3, x, y, i, h)
  , if2(true(), b2, b3, x, y, i, h) -> false()
  , if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
  , if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h)
  , if3(false(), b3, x, y, i, h) ->
    reach(x, y, rest(i), edge(from(i), to(i), h))
  , if4(true(), x, y, i, h) -> true()
  , if4(false(), x, y, i, h) ->
    or(reach(x, y, rest(i), h),
       reach(to(i), y, union(rest(i), h), empty())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(x)) -> c_2()
, eq^#(s(x), 0()) -> c_3()
, or^#(true(), y) -> c_5()
, or^#(false(), y) -> c_6()
, union^#(empty(), h) -> c_7()
, isEmpty^#(empty()) -> c_9()
, isEmpty^#(edge(x, y, i)) -> c_10()
, from^#(edge(x, y, i)) -> c_11()
, to^#(edge(x, y, i)) -> c_12()
, rest^#(empty()) -> c_13()
, rest^#(edge(x, y, i)) -> c_14()
, if1^#(true(), b1, b2, b3, x, y, i, h) -> c_16()
, if2^#(true(), b2, b3, x, y, i, h) -> c_18()
, if4^#(true(), x, y, i, h) -> c_22() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , union^#(edge(x, y, i), h) -> c_8(union^#(i, h))
  , reach^#(x, y, i, h) ->
    c_15(if1^#(eq(x, y),
               isEmpty(i),
               eq(x, from(i)),
               eq(y, to(i)),
               x,
               y,
               i,
               h),
         eq^#(x, y),
         isEmpty^#(i),
         eq^#(x, from(i)),
         from^#(i),
         eq^#(y, to(i)),
         to^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_17(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_19(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_20(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
         rest^#(i),
         from^#(i),
         to^#(i))
  , if4^#(false(), x, y, i, h) ->
    c_23(or^#(reach(x, y, rest(i), h),
              reach(to(i), y, union(rest(i), h), empty())),
         reach^#(x, y, rest(i), h),
         rest^#(i),
         reach^#(to(i), y, union(rest(i), h), empty()),
         to^#(i),
         union^#(rest(i), h),
         rest^#(i)) }
Weak Trs:
  { 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
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i
  , reach(x, y, i, h) ->
    if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
  , if1(true(), b1, b2, b3, x, y, i, h) -> true()
  , if1(false(), b1, b2, b3, x, y, i, h) ->
    if2(b1, b2, b3, x, y, i, h)
  , if2(true(), b2, b3, x, y, i, h) -> false()
  , if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
  , if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h)
  , if3(false(), b3, x, y, i, h) ->
    reach(x, y, rest(i), edge(from(i), to(i), h))
  , if4(true(), x, y, i, h) -> true()
  , if4(false(), x, y, i, h) ->
    or(reach(x, y, rest(i), h),
       reach(to(i), y, union(rest(i), h), empty())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { reach^#(x, y, i, h) ->
    c_15(if1^#(eq(x, y),
               isEmpty(i),
               eq(x, from(i)),
               eq(y, to(i)),
               x,
               y,
               i,
               h),
         eq^#(x, y),
         isEmpty^#(i),
         eq^#(x, from(i)),
         from^#(i),
         eq^#(y, to(i)),
         to^#(i))
  , if3^#(false(), b3, x, y, i, h) ->
    c_21(reach^#(x, y, rest(i), edge(from(i), to(i), h)),
         rest^#(i),
         from^#(i),
         to^#(i))
  , if4^#(false(), x, y, i, h) ->
    c_23(or^#(reach(x, y, rest(i), h),
              reach(to(i), y, union(rest(i), h), empty())),
         reach^#(x, y, rest(i), h),
         rest^#(i),
         reach^#(to(i), y, union(rest(i), h), empty()),
         to^#(i),
         union^#(rest(i), h),
         rest^#(i)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
  , union^#(edge(x, y, i), h) -> c_2(union^#(i, h))
  , reach^#(x, y, i, h) ->
    c_3(if1^#(eq(x, y),
              isEmpty(i),
              eq(x, from(i)),
              eq(y, to(i)),
              x,
              y,
              i,
              h),
        eq^#(x, y),
        eq^#(x, from(i)),
        eq^#(y, to(i)))
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_4(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_5(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_6(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_7(reach^#(x, y, rest(i), edge(from(i), to(i), h)))
  , if4^#(false(), x, y, i, h) ->
    c_8(reach^#(x, y, rest(i), h),
        reach^#(to(i), y, union(rest(i), h), empty()),
        union^#(rest(i), h)) }
Weak Trs:
  { 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
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i
  , reach(x, y, i, h) ->
    if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
  , if1(true(), b1, b2, b3, x, y, i, h) -> true()
  , if1(false(), b1, b2, b3, x, y, i, h) ->
    if2(b1, b2, b3, x, y, i, h)
  , if2(true(), b2, b3, x, y, i, h) -> false()
  , if2(false(), b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
  , if3(true(), b3, x, y, i, h) -> if4(b3, x, y, i, h)
  , if3(false(), b3, x, y, i, h) ->
    reach(x, y, rest(i), edge(from(i), to(i), h))
  , if4(true(), x, y, i, h) -> true()
  , if4(false(), x, y, i, h) ->
    or(reach(x, y, rest(i), h),
       reach(to(i), y, union(rest(i), h), empty())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { eq(0(), 0()) -> true()
    , eq(0(), s(x)) -> false()
    , eq(s(x), 0()) -> false()
    , eq(s(x), s(y)) -> eq(x, y)
    , union(empty(), h) -> h
    , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
    , isEmpty(empty()) -> true()
    , isEmpty(edge(x, y, i)) -> false()
    , from(edge(x, y, i)) -> x
    , to(edge(x, y, i)) -> y
    , rest(empty()) -> empty()
    , rest(edge(x, y, i)) -> i }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
  , union^#(edge(x, y, i), h) -> c_2(union^#(i, h))
  , reach^#(x, y, i, h) ->
    c_3(if1^#(eq(x, y),
              isEmpty(i),
              eq(x, from(i)),
              eq(y, to(i)),
              x,
              y,
              i,
              h),
        eq^#(x, y),
        eq^#(x, from(i)),
        eq^#(y, to(i)))
  , if1^#(false(), b1, b2, b3, x, y, i, h) ->
    c_4(if2^#(b1, b2, b3, x, y, i, h))
  , if2^#(false(), b2, b3, x, y, i, h) ->
    c_5(if3^#(b2, b3, x, y, i, h))
  , if3^#(true(), b3, x, y, i, h) -> c_6(if4^#(b3, x, y, i, h))
  , if3^#(false(), b3, x, y, i, h) ->
    c_7(reach^#(x, y, rest(i), edge(from(i), to(i), h)))
  , if4^#(false(), x, y, i, h) ->
    c_8(reach^#(x, y, rest(i), h),
        reach^#(to(i), y, union(rest(i), h), empty()),
        union^#(rest(i), h)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(x)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , union(empty(), h) -> h
  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
  , isEmpty(empty()) -> true()
  , isEmpty(edge(x, y, i)) -> false()
  , from(edge(x, y, i)) -> x
  , to(edge(x, y, i)) -> y
  , rest(empty()) -> empty()
  , rest(edge(x, y, i)) -> i }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..