YES
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)),
                      reach(x, y, empty(), h) -> false(),
                reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
   if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
  if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
   if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
  if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
 DP:
  Strict:
   {                             eq#(s(x), s(y)) -> eq#(x, y),
                        union#(edge(x, y, i), h) -> union#(i, h),
                  reach#(x, y, edge(u, v, i), h) -> eq#(x, u),
                  reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
     if_reach_1#(true(), x, y, edge(u, v, i), h) -> eq#(y, v),
     if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h),
    if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> or#(reach(x, y, i, h), reach(v, y, union(i, h), empty())),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
    if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
  Weak:
  {                               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)),
                       reach(x, y, empty(), h) -> false(),
                 reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
    if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
   if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
    if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
   if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
  EDG:
   {(if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))
    (reach#(x, y, edge(u, v, i), h) -> eq#(x, u), eq#(s(x), s(y)) -> eq#(x, y))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h), if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h), if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h), if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h), if_reach_2#(false(), x, y, edge(u, v, i), h) -> or#(reach(x, y, i, h), reach(v, y, union(i, h), empty())))
    (eq#(s(x), s(y)) -> eq#(x, y), eq#(s(x), s(y)) -> eq#(x, y))
    (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
    (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> eq#(y, v), eq#(s(x), s(y)) -> eq#(x, y))
    (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
    (if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty()), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
    (if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)), reach#(x, y, edge(u, v, i), h) -> eq#(x, u))
    (if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
    (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h), if_reach_1#(true(), x, y, edge(u, v, i), h) -> eq#(y, v))
    (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h), if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h))
    (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h), if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)))
    (union#(edge(x, y, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))}
   SCCS:
    Scc:
     {              reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
       if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h),
      if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)),
      if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
      if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
    Scc:
     {union#(edge(x, y, i), h) -> union#(i, h)}
    Scc:
     {eq#(s(x), s(y)) -> eq#(x, y)}
    SCC:
     Strict:
      {              reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
        if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h),
       if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)),
       if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h),
       if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())}
     Weak:
     {                               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)),
                          reach(x, y, empty(), h) -> false(),
                    reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
       if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
      if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
       if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
      if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
     POLY:
      Argument Filtering:
       pi(if_reach_2#) = [3,4], pi(if_reach_2) = [], pi(if_reach_1#) = [3,4], pi(if_reach_1) = [], pi(reach#) = [2,3], pi(reach) = [], pi(edge) = [2], pi(empty) = [], pi(union) = [0,1], pi(or) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [if_reach_2#](x0, x1) = x0 + x1,
       [if_reach_1#](x0, x1) = x0 + x1,
       [reach#](x0, x1) = x0 + x1,
       [edge](x0) = x0 + 1,
       [union](x0, x1) = x0 + x1,
       [empty] = 0
      Strict:
       {              reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
         if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h),
        if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))}
      Weak:
       {                               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)),
                            reach(x, y, empty(), h) -> false(),
                      reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
         if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
        if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
         if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
        if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
      EDG:
       {(if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)), reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h))
        (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h), if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h))
        (reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h), if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h)))}
       SCCS:
        Scc:
         {              reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
          if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))}
        SCC:
         Strict:
          {              reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h),
           if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))}
         Weak:
         {                               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)),
                              reach(x, y, empty(), h) -> false(),
                        reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
           if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
          if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
           if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
          if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
         SPSC:
          Simple Projection:
           pi(if_reach_1#) = 3, pi(reach#) = 2
          Strict:
           {reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h)}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {union#(edge(x, y, i), h) -> union#(i, h)}
     Weak:
     {                               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)),
                          reach(x, y, empty(), h) -> false(),
                    reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
       if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
      if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
       if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
      if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
     SPSC:
      Simple Projection:
       pi(union#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {eq#(s(x), s(y)) -> eq#(x, y)}
     Weak:
     {                               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)),
                          reach(x, y, empty(), h) -> false(),
                    reach(x, y, edge(u, v, i), h) -> if_reach_1(eq(x, u), x, y, edge(u, v, i), h),
       if_reach_1(true(), x, y, edge(u, v, i), h) -> if_reach_2(eq(y, v), x, y, edge(u, v, i), h),
      if_reach_1(false(), x, y, edge(u, v, i), h) -> reach(x, y, i, edge(u, v, h)),
       if_reach_2(true(), x, y, edge(u, v, i), h) -> true(),
      if_reach_2(false(), x, y, edge(u, v, i), h) -> or(reach(x, y, i, h), reach(v, y, union(i, h), empty()))}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {}
      Qed