We consider universal computability of the STRS with no additional rule schemes:

  Signature: 0          :: a
             cons       :: d -> e -> e
             edge       :: a -> a -> b -> b
             empty      :: b
             eq         :: a -> a -> c
             false      :: c
             filter     :: (d -> c) -> e -> e
             filter2    :: c -> (d -> c) -> d -> e -> e
             if_reach_1 :: c -> a -> a -> b -> b -> c
             if_reach_2 :: c -> a -> a -> b -> b -> c
             map        :: (d -> d) -> e -> e
             nil        :: e
             or         :: c -> c -> c
             reach      :: a -> a -> b -> b -> c
             s          :: a -> a
             true       :: c
             union      :: b -> b -> b

  Rules: eq(0, 0) -> true
         eq(0, s(X)) -> false
         eq(s(Y), 0) -> false
         eq(s(U), s(V)) -> eq(U, V)
         or(true, W) -> true
         or(false, P) -> P
         union(empty, X1) -> X1
         union(edge(V1, W1, U1), Y1) -> edge(V1, W1, union(U1, Y1))
         reach(X2, Y2, empty, P1) -> false
         reach(X3, Y3, edge(W2, P2, V2), U2) -> if_reach_1(eq(X3, W2), X3, Y3, edge(W2, P2, V2), U2)
         if_reach_1(true, X4, Y4, edge(W3, P3, V3), U3) -> if_reach_2(eq(Y4, P3), X4, Y4, edge(W3, P3, V3), U3)
         if_reach_1(false, X5, Y5, edge(W4, P4, V4), U4) -> reach(X5, Y5, V4, edge(W4, P4, U4))
         if_reach_2(true, X6, Y6, edge(W5, P5, V5), U5) -> true
         if_reach_2(false, X7, Y7, edge(W6, P6, V6), U6) -> or(reach(X7, Y7, V6, U6), reach(P6, Y7, union(V6, U6), empty))
         map(G7, nil) -> nil
         map(H7, cons(W7, P7)) -> cons(H7(W7), map(H7, P7))
         filter(F8, nil) -> nil
         filter(Z8, cons(U8, V8)) -> filter2(Z8(U8), Z8, U8, V8)
         filter2(true, I8, P8, X9) -> cons(P8, filter(I8, X9))
         filter2(false, Z9, U9, V9) -> filter(Z9, V9)

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

We start by computing the initial DP problem D1 = (P1, R UNION R_?, i, c), where:

  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 D1 = (P1, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1:  1 
  2:  2 
  3:  1 
  4:  5 6 7 
  5:  1 
  6:  8 9 10 11 
  7:  3 4 
  8:  3 4 
  9:  2 
  10: 3 4 
  11:
  12: 12 
  13: 14 15 
  14: 13 
  15: 13 

There are 5 SCCs.

Processor output: { D2 = (P2, R UNION R_?, i, c) ; D3 = (P3, R UNION R_?, i, c) ; D4 = (P4, R UNION R_?, i, c) ; D5 = (P5, R UNION R_?, i, c) ; D6 = (P6, R UNION R_?, i, c) }, where:

  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 D2 = (P2, R UNION R_?, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D3 = (P3, R UNION R_?, i, c).

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.

Processor output: { }.

***** We apply the Usable Rules Processor on D4 = (P4, R UNION R_?, i, c).

We obtain 6 usable rules (out of 20 rules in the input problem).

Processor output: { D7 = (P4, R2, i, c) }, where:

  R2. (1) eq(0, 0) -> true
      (2) eq(0, s(X)) -> false
      (3) eq(s(Y), 0) -> false
      (4) eq(s(U), s(V)) -> eq(U, V)
      (5) union(empty, X1) -> X1
      (6) union(edge(V1, W1, U1), Y1) -> edge(V1, W1, union(U1, Y1))

***** We apply the Subterm Criterion Processor on D5 = (P5, R UNION R_?, i, c).

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(W7, P7) |>| P7

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

Processor output: { }.

***** We apply the Subterm Criterion Processor on D6 = (P6, R UNION R_?, i, c).

We use the following projection function:

  nu(filter#)  = 2
  nu(filter2#) = 4

We thus have:

  (1) cons(U8, V8) |>|  V8
  (2) X9           |>=| X9
  (3) V9           |>=| V9

We may remove the strictly oriented DPs.

Processor output: { D8 = (P7, R UNION R_?, i, c) }, where:

  P7. (1) filter2#(true, I8, P8, X9) => filter#(I8, X9)
      (2) filter2#(false, Z9, U9, V9) => filter#(Z9, V9)

***** No progress could be made on DP problem D7 = (P4, R2, i, c).