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

  Signature: 0          :: b
             add        :: b -> c -> c
             app        :: c -> c -> c
             eq         :: b -> b -> a
             false      :: a
             filter     :: (b -> a) -> c -> c
             filter2    :: a -> (b -> a) -> b -> c -> c
             if_min     :: a -> c -> b
             if_minsort :: a -> c -> c -> c
             if_rm      :: a -> b -> c -> c
             le         :: b -> b -> a
             map        :: (b -> b) -> c -> c
             min        :: c -> b
             minsort    :: c -> c -> c
             nil        :: c
             rm         :: b -> c -> c
             s          :: b -> b
             true       :: a

  Rules: eq(0, 0) -> true
         eq(0, s(X)) -> false
         eq(s(Y), 0) -> false
         eq(s(U), s(V)) -> eq(U, V)
         le(0, W) -> true
         le(s(P), 0) -> false
         le(s(X1), s(Y1)) -> le(X1, Y1)
         app(nil, U1) -> U1
         app(add(V1, W1), P1) -> add(V1, app(W1, P1))
         min(add(X2, nil)) -> X2
         min(add(U2, add(Y2, V2))) -> if_min(le(U2, Y2), add(U2, add(Y2, V2)))
         if_min(true, add(P2, add(W2, X3))) -> min(add(P2, X3))
         if_min(false, add(U3, add(Y3, V3))) -> min(add(Y3, V3))
         rm(W3, nil) -> nil
         rm(X4, add(P3, Y4)) -> if_rm(eq(X4, P3), X4, add(P3, Y4))
         if_rm(true, V4, add(U4, W4)) -> rm(V4, W4)
         if_rm(false, X5, add(P4, Y5)) -> add(P4, rm(X5, Y5))
         minsort(nil, nil) -> nil
         minsort(add(U5, V5), W5) -> if_minsort(eq(U5, min(add(U5, V5))), add(U5, V5), W5)
         if_minsort(true, add(P5, X6), Y6) -> add(P5, minsort(app(rm(P5, X6), Y6), nil))
         if_minsort(false, add(U6, V6), W6) -> minsort(V6, add(U6, W6))
         map(J6, nil) -> nil
         map(F7, add(Y7, U7)) -> add(F7(Y7), map(F7, U7))
         filter(H7, nil) -> nil
         filter(I7, add(P7, X8)) -> filter2(I7(P7), I7, P7, X8)
         filter2(true, Z8, U8, V8) -> add(U8, filter(Z8, V8))
         filter2(false, I8, P8, X9) -> filter(I8, X9)

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)  le#(s(X1), s(Y1)) => le#(X1, Y1)
      (3)  app#(add(V1, W1), P1) => app#(W1, P1)
      (4)  min#(add(U2, add(Y2, V2))) => le#(U2, Y2)
      (5)  min#(add(U2, add(Y2, V2))) => if_min#(le(U2, Y2), add(U2, add(Y2, V2)))
      (6)  if_min#(true, add(P2, add(W2, X3))) => min#(add(P2, X3))
      (7)  if_min#(false, add(U3, add(Y3, V3))) => min#(add(Y3, V3))
      (8)  rm#(X4, add(P3, Y4)) => eq#(X4, P3)
      (9)  rm#(X4, add(P3, Y4)) => if_rm#(eq(X4, P3), X4, add(P3, Y4))
      (10) if_rm#(true, V4, add(U4, W4)) => rm#(V4, W4)
      (11) if_rm#(false, X5, add(P4, Y5)) => rm#(X5, Y5)
      (12) minsort#(add(U5, V5), W5) => min#(add(U5, V5))
      (13) minsort#(add(U5, V5), W5) => eq#(U5, min(add(U5, V5)))
      (14) minsort#(add(U5, V5), W5) => if_minsort#(eq(U5, min(add(U5, V5))), add(U5, V5), W5)
      (15) if_minsort#(true, add(P5, X6), Y6) => rm#(P5, X6)
      (16) if_minsort#(true, add(P5, X6), Y6) => app#(rm(P5, X6), Y6)
      (17) if_minsort#(true, add(P5, X6), Y6) => minsort#(app(rm(P5, X6), Y6), nil)
      (18) if_minsort#(false, add(U6, V6), W6) => minsort#(V6, add(U6, W6))
      (19) map#(F7, add(Y7, U7)) => map#(F7, U7)
      (20) filter#(I7, add(P7, X8)) => filter2#(I7(P7), I7, P7, X8)
      (21) filter2#(true, Z8, U8, V8) => filter#(Z8, V8)
      (22) filter2#(false, I8, P8, X9) => filter#(I8, X9)

***** 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:  3 
  4:  2 
  5:  6 7 
  6:  4 5 
  7:  4 5 
  8:  1 
  9:  10 11 
  10: 8 9 
  11: 8 9 
  12: 4 5 
  13: 1 
  14: 15 16 17 18 
  15: 8 9 
  16: 3 
  17: 12 13 14 
  18: 12 13 14 
  19: 19 
  20: 21 22 
  21: 20 
  22: 20 

There are 8 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) ; D7 = (P7, R UNION R_?, i, c) ; D8 = (P8, R UNION R_?, i, c) ; D9 = (P9, R UNION R_?, i, c) }, where:

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

  P3. (1) le#(s(X1), s(Y1)) => le#(X1, Y1)

  P4. (1) app#(add(V1, W1), P1) => app#(W1, P1)

  P5. (1) min#(add(U2, add(Y2, V2))) => if_min#(le(U2, Y2), add(U2, add(Y2, V2)))
      (2) if_min#(true, add(P2, add(W2, X3))) => min#(add(P2, X3))
      (3) if_min#(false, add(U3, add(Y3, V3))) => min#(add(Y3, V3))

  P6. (1) rm#(X4, add(P3, Y4)) => if_rm#(eq(X4, P3), X4, add(P3, Y4))
      (2) if_rm#(true, V4, add(U4, W4)) => rm#(V4, W4)
      (3) if_rm#(false, X5, add(P4, Y5)) => rm#(X5, Y5)

  P7. (1) minsort#(add(U5, V5), W5) => if_minsort#(eq(U5, min(add(U5, V5))), add(U5, V5), W5)
      (2) if_minsort#(true, add(P5, X6), Y6) => minsort#(app(rm(P5, X6), Y6), nil)
      (3) if_minsort#(false, add(U6, V6), W6) => minsort#(V6, add(U6, W6))

  P8. (1) map#(F7, add(Y7, U7)) => map#(F7, U7)

  P9. (1) filter#(I7, add(P7, X8)) => filter2#(I7(P7), I7, P7, X8)
      (2) filter2#(true, Z8, U8, V8) => filter#(Z8, V8)
      (3) filter2#(false, I8, P8, X9) => filter#(I8, X9)

***** 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(le#) = 1

We thus have:

  (1) s(X1) |>| X1

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

Processor output: { }.

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

We use the following projection function:

  nu(app#) = 1

We thus have:

  (1) add(V1, W1) |>| W1

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

Processor output: { }.

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

We obtain 3 usable rules (out of 27 rules in the input problem).

Processor output: { D10 = (P5, R2, i, c) }, where:

  R2. (1) le(0, W) -> true
      (2) le(s(P), 0) -> false
      (3) le(s(X1), s(Y1)) -> le(X1, Y1)

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

We use the following projection function:

  nu(if_rm#) = 3
  nu(rm#)    = 2

We thus have:

  (1) add(P3, Y4) |>=| add(P3, Y4)
  (2) add(U4, W4) |>|  W4
  (3) add(P4, Y5) |>|  Y5

We may remove the strictly oriented DPs.

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

  P10. (1) rm#(X4, add(P3, Y4)) => if_rm#(eq(X4, P3), X4, add(P3, Y4))

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

We obtain 17 usable rules (out of 27 rules in the input problem).

Processor output: { D12 = (P7, R3, i, c) }, where:

  R3. (1)  app(nil, U1) -> U1
      (2)  app(add(V1, W1), P1) -> add(V1, app(W1, P1))
      (3)  eq(0, 0) -> true
      (4)  eq(0, s(X)) -> false
      (5)  eq(s(Y), 0) -> false
      (6)  eq(s(U), s(V)) -> eq(U, V)
      (7)  if_min(true, add(P2, add(W2, X3))) -> min(add(P2, X3))
      (8)  if_min(false, add(U3, add(Y3, V3))) -> min(add(Y3, V3))
      (9)  if_rm(true, V4, add(U4, W4)) -> rm(V4, W4)
      (10) if_rm(false, X5, add(P4, Y5)) -> add(P4, rm(X5, Y5))
      (11) le(0, W) -> true
      (12) le(s(P), 0) -> false
      (13) le(s(X1), s(Y1)) -> le(X1, Y1)
      (14) min(add(X2, nil)) -> X2
      (15) min(add(U2, add(Y2, V2))) -> if_min(le(U2, Y2), add(U2, add(Y2, V2)))
      (16) rm(W3, nil) -> nil
      (17) rm(X4, add(P3, Y4)) -> if_rm(eq(X4, P3), X4, add(P3, Y4))

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

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) add(Y7, U7) |>| U7

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

Processor output: { }.

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

We use the following projection function:

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

We thus have:

  (1) add(P7, X8) |>|  X8
  (2) V8          |>=| V8
  (3) X9          |>=| X9

We may remove the strictly oriented DPs.

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

  P11. (1) filter2#(true, Z8, U8, V8) => filter#(Z8, V8)
       (2) filter2#(false, I8, P8, X9) => filter#(I8, X9)

***** We apply the Reduction Pair [with HORPO] Processor on D10 = (P5, R2, i, c).

Constrained HORPO yields:

  min#(add(U2, add(Y2, V2))) (>=) if_min#(le(U2, Y2), add(U2, add(Y2, V2)))
  if_min#(true, add(P2, add(W2, X3))) (>) min#(add(P2, X3))
  if_min#(false, add(U3, add(Y3, V3))) (>) min#(add(Y3, V3))
  le(0, W) (>=) true
  le(s(P), 0) (>=) false
  le(s(X1), s(Y1)) (>=) le(X1, Y1)

We do this using the following settings:

* Disregarded arguments:

  if_min# 1 
  le      1 

* Precedence and permutation:

    0        { }
  = false    { }
  > add      { 1 } 2
  = s        { 1 }
  > if_min#  { 2 }
  = min#     { 1 }
  > le       { 2 }
  = true     { }

* Well-founded theory orderings:

  [>]_{Bool} = {(true,false)}
  [>]_{Int}  = {(x,y) | x < 1000 /\ x < y }

Processor output: { D14 = (P12, R2, i, c) }, where:

  P12. (1) min#(add(U2, add(Y2, V2))) => if_min#(le(U2, Y2), add(U2, add(Y2, V2)))

***** We apply the Graph Processor on D11 = (P10, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1:

As there are no SCCs, this DP problem is removed.

Processor output: { }.

***** No progress could be made on DP problem D12 = (P7, R3, i, c).