YES
Time: 0.054456
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:
  DP:
   {                               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())}
  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()))}
  EDG:
   {(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())))
    (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_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))
    (union#(edge(x, y, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(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) -> 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))
    (reach#(x, y, edge(u, v, i), h) -> eq#(x, u), eq#(s x, s y) -> eq#(x, y))
    (if_reach_2#(false(), x, y, edge(u, v, i), h) -> union#(i, h), union#(edge(x, y, i), h) -> union#(i, h))
    (if_reach_1#(true(), x, y, edge(u, v, i), h) -> eq#(y, v), eq#(s x, s y) -> eq#(x, y))
    (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)))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))}
   SCCS (3):
    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 (5):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if_reach_1](x0, x1, x2, x3, x4) = 0,
       
       [if_reach_2](x0, x1, x2, x3, x4) = 0,
       
       [reach](x0, x1, x2, x3) = 0,
       
       [edge](x0, x1, x2) = x0 + 1,
       
       [eq](x0, x1) = 1,
       
       [or](x0, x1) = x0 + 1,
       
       [union](x0, x1) = x0 + x1,
       
       [s](x0) = 0,
       
       [true] = 1,
       
       [0] = 0,
       
       [false] = 1,
       
       [empty] = 1,
       
       [if_reach_1#](x0, x1, x2, x3, x4) = x0 + x1 + x2,
       
       [if_reach_2#](x0, x1, x2, x3, x4) = x0 + x1 + 1,
       
       [reach#](x0, x1, x2, x3) = x0 + x1 + 1
      Strict:
       if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())
       2 + 0x + 0y + 1h + 1i + 0u + 0v >= 2 + 0y + 1h + 1i + 0v
       if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, h)
       2 + 0x + 0y + 1h + 1i + 0u + 0v >= 1 + 0x + 0y + 1h + 1i
       if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))
       2 + 0x + 0y + 1h + 1i + 0u + 0v >= 2 + 0x + 0y + 1h + 1i + 0u + 0v
       if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h)
       2 + 0x + 0y + 1h + 1i + 0u + 0v >= 2 + 0x + 0y + 1h + 1i + 0u + 0v
       reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h)
       2 + 0x + 0y + 1h + 1i + 0u + 0v >= 2 + 0x + 0y + 1h + 1i + 0u + 0v
      Weak:
       
     EDG:
      {(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_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) -> 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 (1):
       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#(v, y, union(i, h), empty())}
       SCC (4):
        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#(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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [if_reach_1](x0, x1, x2, x3, x4) = 0,
          
          [if_reach_2](x0, x1, x2, x3, x4) = x0,
          
          [reach](x0, x1, x2, x3) = 1,
          
          [edge](x0, x1, x2) = x0 + x1 + 1,
          
          [eq](x0, x1) = 0,
          
          [or](x0, x1) = x0 + 1,
          
          [union](x0, x1) = x0 + x1,
          
          [s](x0) = 0,
          
          [true] = 1,
          
          [0] = 0,
          
          [false] = 0,
          
          [empty] = 0,
          
          [if_reach_1#](x0, x1, x2, x3, x4) = x0 + x1 + 1,
          
          [if_reach_2#](x0, x1, x2, x3, x4) = x0 + x1 + 1,
          
          [reach#](x0, x1, x2, x3) = x0 + x1 + 1
         Strict:
          if_reach_2#(false(), x, y, edge(u, v, i), h) -> reach#(v, y, union(i, h), empty())
          2 + 0x + 0y + 1h + 1i + 1u + 0v >= 1 + 0y + 1h + 1i + 0v
          if_reach_1#(false(), x, y, edge(u, v, i), h) -> reach#(x, y, i, edge(u, v, h))
          2 + 0x + 0y + 1h + 1i + 1u + 0v >= 2 + 0x + 0y + 1h + 1i + 1u + 0v
          if_reach_1#(true(), x, y, edge(u, v, i), h) -> if_reach_2#(eq(y, v), x, y, edge(u, v, i), h)
          2 + 0x + 0y + 1h + 1i + 1u + 0v >= 2 + 0x + 0y + 1h + 1i + 1u + 0v
          reach#(x, y, edge(u, v, i), h) -> if_reach_1#(eq(x, u), x, y, edge(u, v, i), h)
          2 + 0x + 0y + 1h + 1i + 1u + 0v >= 2 + 0x + 0y + 1h + 1i + 1u + 0v
         Weak:
          
        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 (1):
          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 (2):
           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 (0):
              
              Qed
   SCC (1):
    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 (1):
    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#) = 1
     Strict:
      {}
     Qed