The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  P1. (1)  eq#(s(U), s(V)) => eq#(U, V)
      (2)  union#(edge(V1, W1, U1), Y1) => union#(U1, Y1)
      (3)  reach#(X3, Y3, edge(W2, P2, V2), U2) => eq#(X3, W2)
      (4)  reach#(X3, Y3, edge(W2, P2, V2), U2) => if_reach_1#(eq(X3, W2), X3, Y3, edge(W2, P2, V2), U2)
      (5)  if_reach_1#(true, X4, Y4, edge(W3, P3, V3), U3) => eq#(Y4, P3)
      (6)  if_reach_1#(true, X4, Y4, edge(W3, P3, V3), U3) => if_reach_2#(eq(Y4, P3), X4, Y4, edge(W3, P3, V3), U3)
      (7)  if_reach_1#(false, X5, Y5, edge(W4, P4, V4), U4) => reach#(X5, Y5, V4, edge(W4, P4, U4))
      (8)  if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => reach#(X7, Y7, V6, U6)
      (9)  if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => union#(V6, U6)
      (10) if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => reach#(P6, Y7, union(V6, U6), empty)
      (11) if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => or#(reach(X7, Y7, V6, U6), reach(P6, Y7, union(V6, U6), empty))
      (12) map#(H7, cons(W7, P7)) => map#(H7, P7)
      (13) filter#(Z8, cons(U8, V8)) => filter2#(Z8(U8), Z8, U8, V8)
      (14) filter2#(true, I8, P8, X9) => filter#(I8, X9)
      (15) filter2#(false, Z9, U9, V9) => filter#(Z9, V9)

***** We apply the Graph Processor on P1.

Considering the 5 SCCs, this DP problem is split into the following new problems.

  P2. (1) eq#(s(U), s(V)) => eq#(U, V)

  P3. (1) union#(edge(V1, W1, U1), Y1) => union#(U1, Y1)

  P4. (1) reach#(X3, Y3, edge(W2, P2, V2), U2) => if_reach_1#(eq(X3, W2), X3, Y3, edge(W2, P2, V2), U2)
      (2) if_reach_1#(true, X4, Y4, edge(W3, P3, V3), U3) => if_reach_2#(eq(Y4, P3), X4, Y4, edge(W3, P3, V3), U3)
      (3) if_reach_1#(false, X5, Y5, edge(W4, P4, V4), U4) => reach#(X5, Y5, V4, edge(W4, P4, U4))
      (4) if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => reach#(X7, Y7, V6, U6)
      (5) if_reach_2#(false, X7, Y7, edge(W6, P6, V6), U6) => reach#(P6, Y7, union(V6, U6), empty)

  P5. (1) map#(H7, cons(W7, P7)) => map#(H7, P7)

  P6. (1) filter#(Z8, cons(U8, V8)) => filter2#(Z8(U8), Z8, U8, V8)
      (2) filter2#(true, I8, P8, X9) => filter#(I8, X9)
      (3) filter2#(false, Z9, U9, V9) => filter#(Z9, V9)

***** We apply the Subterm Criterion Processor on P2.

We use the following projection function:

  nu(eq#) = 1

We thus have:

  (1) s(U) |>| U

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Subterm Criterion Processor on P3.

We use the following projection function:

  nu(union#) = 1

We thus have:

  (1) edge(V1, W1, U1) |>| U1

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** No progress could be made on DP problem P4.