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
  , 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(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)))
  , if2(false(), x, y, c, i, j) -> false() }
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()
  , and^#(true(), y) -> c_7()
  , and^#(false(), y) -> c_8()
  , size^#(empty()) -> c_9()
  , size^#(edge(x, y, i)) -> c_10(size^#(i))
  , le^#(0(), y) -> c_11()
  , le^#(s(x), 0()) -> c_12()
  , le^#(s(x), s(y)) -> c_13(le^#(x, y))
  , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_15(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(true(), x, y, c, i, j) -> c_16()
  , if1^#(false(), x, y, c, i, j) ->
    c_17(if2^#(le(c, size(j)), x, y, c, i, j),
         le^#(c, size(j)),
         size^#(j))
  , if2^#(true(), x, y, c, empty(), j) -> c_18()
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_19(or^#(if2(true(), x, y, c, i, j),
              and(eq(x, u), reach(v, y, s(c), j, j))),
         if2^#(true(), x, y, c, i, j),
         and^#(eq(x, u), reach(v, y, s(c), j, j)),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j))
  , if2^#(false(), x, y, c, i, j) -> c_20() }

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()
  , and^#(true(), y) -> c_7()
  , and^#(false(), y) -> c_8()
  , size^#(empty()) -> c_9()
  , size^#(edge(x, y, i)) -> c_10(size^#(i))
  , le^#(0(), y) -> c_11()
  , le^#(s(x), 0()) -> c_12()
  , le^#(s(x), s(y)) -> c_13(le^#(x, y))
  , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_15(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(true(), x, y, c, i, j) -> c_16()
  , if1^#(false(), x, y, c, i, j) ->
    c_17(if2^#(le(c, size(j)), x, y, c, i, j),
         le^#(c, size(j)),
         size^#(j))
  , if2^#(true(), x, y, c, empty(), j) -> c_18()
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_19(or^#(if2(true(), x, y, c, i, j),
              and(eq(x, u), reach(v, y, s(c), j, j))),
         if2^#(true(), x, y, c, i, j),
         and^#(eq(x, u), reach(v, y, s(c), j, j)),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j))
  , if2^#(false(), x, y, c, i, j) -> c_20() }
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
  , 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(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)))
  , if2(false(), x, y, c, i, j) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,3,5,6,7,8,9,11,12,16,18,20} by applications of
Pre({1,2,3,5,6,7,8,9,11,12,16,18,20}) = {4,10,13,15,17,19}. 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: and^#(true(), y) -> c_7()
    , 8: and^#(false(), y) -> c_8()
    , 9: size^#(empty()) -> c_9()
    , 10: size^#(edge(x, y, i)) -> c_10(size^#(i))
    , 11: le^#(0(), y) -> c_11()
    , 12: le^#(s(x), 0()) -> c_12()
    , 13: le^#(s(x), s(y)) -> c_13(le^#(x, y))
    , 14: reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
    , 15: reach^#(x, y, c, i, j) ->
          c_15(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
    , 16: if1^#(true(), x, y, c, i, j) -> c_16()
    , 17: if1^#(false(), x, y, c, i, j) ->
          c_17(if2^#(le(c, size(j)), x, y, c, i, j),
               le^#(c, size(j)),
               size^#(j))
    , 18: if2^#(true(), x, y, c, empty(), j) -> c_18()
    , 19: if2^#(true(), x, y, c, edge(u, v, i), j) ->
          c_19(or^#(if2(true(), x, y, c, i, j),
                    and(eq(x, u), reach(v, y, s(c), j, j))),
               if2^#(true(), x, y, c, i, j),
               and^#(eq(x, u), reach(v, y, s(c), j, j)),
               eq^#(x, u),
               reach^#(v, y, s(c), j, j))
    , 20: if2^#(false(), x, y, c, i, j) -> c_20() }

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))
  , size^#(edge(x, y, i)) -> c_10(size^#(i))
  , le^#(s(x), s(y)) -> c_13(le^#(x, y))
  , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_15(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(false(), x, y, c, i, j) ->
    c_17(if2^#(le(c, size(j)), x, y, c, i, j),
         le^#(c, size(j)),
         size^#(j))
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_19(or^#(if2(true(), x, y, c, i, j),
              and(eq(x, u), reach(v, y, s(c), j, j))),
         if2^#(true(), x, y, c, i, j),
         and^#(eq(x, u), reach(v, y, s(c), j, j)),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j)) }
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()
  , and^#(true(), y) -> c_7()
  , and^#(false(), y) -> c_8()
  , size^#(empty()) -> c_9()
  , le^#(0(), y) -> c_11()
  , le^#(s(x), 0()) -> c_12()
  , if1^#(true(), x, y, c, i, j) -> c_16()
  , if2^#(true(), x, y, c, empty(), j) -> c_18()
  , if2^#(false(), x, y, c, i, j) -> c_20() }
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
  , 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(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)))
  , if2(false(), x, y, c, i, j) -> false() }
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()
, and^#(true(), y) -> c_7()
, and^#(false(), y) -> c_8()
, size^#(empty()) -> c_9()
, le^#(0(), y) -> c_11()
, le^#(s(x), 0()) -> c_12()
, if1^#(true(), x, y, c, i, j) -> c_16()
, if2^#(true(), x, y, c, empty(), j) -> c_18()
, if2^#(false(), x, y, c, i, j) -> c_20() }

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))
  , size^#(edge(x, y, i)) -> c_10(size^#(i))
  , le^#(s(x), s(y)) -> c_13(le^#(x, y))
  , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_15(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(false(), x, y, c, i, j) ->
    c_17(if2^#(le(c, size(j)), x, y, c, i, j),
         le^#(c, size(j)),
         size^#(j))
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_19(or^#(if2(true(), x, y, c, i, j),
              and(eq(x, u), reach(v, y, s(c), j, j))),
         if2^#(true(), x, y, c, i, j),
         and^#(eq(x, u), reach(v, y, s(c), j, j)),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j)) }
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
  , 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(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)))
  , if2(false(), x, y, c, i, j) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_19(or^#(if2(true(), x, y, c, i, j),
              and(eq(x, u), reach(v, y, s(c), j, j))),
         if2^#(true(), x, y, c, i, j),
         and^#(eq(x, u), reach(v, y, s(c), j, j)),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j)) }

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))
  , size^#(edge(x, y, i)) -> c_2(size^#(i))
  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , reachable^#(x, y, i) -> c_4(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(false(), x, y, c, i, j) ->
    c_6(if2^#(le(c, size(j)), x, y, c, i, j),
        le^#(c, size(j)),
        size^#(j))
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_7(if2^#(true(), x, y, c, i, j),
        eq^#(x, u),
        reach^#(v, y, s(c), j, j)) }
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
  , 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(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)))
  , if2(false(), x, y, c, i, j) -> false() }
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)
    , 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) }

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))
  , size^#(edge(x, y, i)) -> c_2(size^#(i))
  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , reachable^#(x, y, i) -> c_4(reach^#(x, y, 0(), i, i))
  , reach^#(x, y, c, i, j) ->
    c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(false(), x, y, c, i, j) ->
    c_6(if2^#(le(c, size(j)), x, y, c, i, j),
        le^#(c, size(j)),
        size^#(j))
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_7(if2^#(true(), x, y, c, i, j),
        eq^#(x, u),
        reach^#(v, y, s(c), j, j)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(x)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
     -->_1 eq^#(s(x), s(y)) -> c_1(eq^#(x, y)) :1
  
  2: size^#(edge(x, y, i)) -> c_2(size^#(i))
     -->_1 size^#(edge(x, y, i)) -> c_2(size^#(i)) :2
  
  3: le^#(s(x), s(y)) -> c_3(le^#(x, y))
     -->_1 le^#(s(x), s(y)) -> c_3(le^#(x, y)) :3
  
  4: reachable^#(x, y, i) -> c_4(reach^#(x, y, 0(), i, i))
     -->_1 reach^#(x, y, c, i, j) ->
           c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y)) :5
  
  5: reach^#(x, y, c, i, j) ->
     c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
     -->_1 if1^#(false(), x, y, c, i, j) ->
           c_6(if2^#(le(c, size(j)), x, y, c, i, j),
               le^#(c, size(j)),
               size^#(j)) :6
     -->_2 eq^#(s(x), s(y)) -> c_1(eq^#(x, y)) :1
  
  6: if1^#(false(), x, y, c, i, j) ->
     c_6(if2^#(le(c, size(j)), x, y, c, i, j),
         le^#(c, size(j)),
         size^#(j))
     -->_1 if2^#(true(), x, y, c, edge(u, v, i), j) ->
           c_7(if2^#(true(), x, y, c, i, j),
               eq^#(x, u),
               reach^#(v, y, s(c), j, j)) :7
     -->_2 le^#(s(x), s(y)) -> c_3(le^#(x, y)) :3
     -->_3 size^#(edge(x, y, i)) -> c_2(size^#(i)) :2
  
  7: if2^#(true(), x, y, c, edge(u, v, i), j) ->
     c_7(if2^#(true(), x, y, c, i, j),
         eq^#(x, u),
         reach^#(v, y, s(c), j, j))
     -->_1 if2^#(true(), x, y, c, edge(u, v, i), j) ->
           c_7(if2^#(true(), x, y, c, i, j),
               eq^#(x, u),
               reach^#(v, y, s(c), j, j)) :7
     -->_3 reach^#(x, y, c, i, j) ->
           c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y)) :5
     -->_2 eq^#(s(x), s(y)) -> c_1(eq^#(x, y)) :1
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { reachable^#(x, y, i) -> c_4(reach^#(x, y, 0(), 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))
  , size^#(edge(x, y, i)) -> c_2(size^#(i))
  , le^#(s(x), s(y)) -> c_3(le^#(x, y))
  , reach^#(x, y, c, i, j) ->
    c_5(if1^#(eq(x, y), x, y, c, i, j), eq^#(x, y))
  , if1^#(false(), x, y, c, i, j) ->
    c_6(if2^#(le(c, size(j)), x, y, c, i, j),
        le^#(c, size(j)),
        size^#(j))
  , if2^#(true(), x, y, c, edge(u, v, i), j) ->
    c_7(if2^#(true(), x, y, c, i, j),
        eq^#(x, u),
        reach^#(v, y, s(c), j, j)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(x)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..