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

  Signature: :       :: a -> a -> a
             C       :: a
             cons    :: c -> d -> d
             false   :: b
             filter  :: (c -> b) -> d -> d
             filter2 :: b -> (c -> b) -> c -> d -> d
             map     :: (c -> c) -> d -> d
             nil     :: d
             true    :: b

  Rules: :(:(:(:(C, Y), U), V), X) -> :(:(Y, V), :(:(:(Y, U), V), X))
         map(I, nil) -> nil
         map(J, cons(X1, Y1)) -> cons(J(X1), map(J, Y1))
         filter(G1, nil) -> nil
         filter(H1, cons(W1, P1)) -> filter2(H1(W1), H1, W1, P1)
         filter2(true, F2, Y2, U2) -> cons(Y2, filter(F2, U2))
         filter2(false, H2, W2, P2) -> filter(H2, P2)

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) :#(:(:(:(C, Y), U), V), X) => :#(Y, V)
      (2) :#(:(:(:(C, Y), U), V), X) => :#(Y, U)
      (3) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, U), V)
      (4) :#(:(:(:(C, Y), U), V), X) => :#(:(:(Y, U), V), X)
      (5) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, V), :(:(:(Y, U), V), X))
      (6) map#(J, cons(X1, Y1)) => map#(J, Y1)
      (7) filter#(H1, cons(W1, P1)) => filter2#(H1(W1), H1, W1, P1)
      (8) filter2#(true, F2, Y2, U2) => filter#(F2, U2)
      (9) filter2#(false, H2, W2, P2) => filter#(H2, P2)

***** 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 3 4 5 
  2: 1 2 3 4 5 
  3: 1 2 3 4 5 
  4: 1 2 3 4 5 
  5: 1 2 3 4 5 
  6: 6 
  7: 8 9 
  8: 7 
  9: 7 

There are 3 SCCs.

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

  P2. (1) :#(:(:(:(C, Y), U), V), X) => :#(Y, V)
      (2) :#(:(:(:(C, Y), U), V), X) => :#(Y, U)
      (3) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, U), V)
      (4) :#(:(:(:(C, Y), U), V), X) => :#(:(:(Y, U), V), X)
      (5) :#(:(:(:(C, Y), U), V), X) => :#(:(Y, V), :(:(:(Y, U), V), X))

  P3. (1) map#(J, cons(X1, Y1)) => map#(J, Y1)

  P4. (1) filter#(H1, cons(W1, P1)) => filter2#(H1(W1), H1, W1, P1)
      (2) filter2#(true, F2, Y2, U2) => filter#(F2, U2)
      (3) filter2#(false, H2, W2, P2) => filter#(H2, P2)

***** No progress could be made on DP problem D2 = (P2, R UNION R_?, i, c).