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

  Signature: 0       :: b
             app     :: c -> c -> c
             cons    :: b -> c -> c
             false   :: a
             filter  :: (b -> a) -> c -> c
             filter2 :: a -> (b -> a) -> b -> c -> c
             map     :: (b -> b) -> c -> c
             minus   :: b -> b -> b
             nil     :: c
             plus    :: b -> b -> b
             quot    :: b -> b -> b
             s       :: b -> b
             sum     :: c -> c
             true    :: a

  Rules: minus(X, 0) -> X
         minus(s(Y), s(U)) -> minus(Y, U)
         minus(minus(V, W), P) -> minus(V, plus(W, P))
         quot(0, s(X1)) -> 0
         quot(s(Y1), s(U1)) -> s(quot(minus(Y1, U1), s(U1)))
         plus(0, V1) -> V1
         plus(s(W1), P1) -> s(plus(W1, P1))
         app(nil, X2) -> X2
         app(Y2, nil) -> Y2
         app(cons(W2, V2), U2) -> cons(W2, app(V2, U2))
         sum(cons(P2, nil)) -> cons(P2, nil)
         sum(cons(Y3, cons(U3, X3))) -> sum(cons(plus(Y3, U3), X3))
         sum(app(W3, cons(P3, cons(X4, V3)))) -> sum(app(W3, sum(cons(P3, cons(X4, V3)))))
         map(Z4, nil) -> nil
         map(G4, cons(V4, W4)) -> cons(G4(V4), map(G4, W4))
         filter(J4, nil) -> nil
         filter(F5, cons(Y5, U5)) -> filter2(F5(Y5), F5, Y5, U5)
         filter2(true, H5, W5, P5) -> cons(W5, filter(H5, P5))
         filter2(false, F6, Y6, U6) -> filter(F6, U6)

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)  minus#(s(Y), s(U)) => minus#(Y, U)
      (2)  minus#(minus(V, W), P) => plus#(W, P)
      (3)  minus#(minus(V, W), P) => minus#(V, plus(W, P))
      (4)  quot#(s(Y1), s(U1)) => minus#(Y1, U1)
      (5)  quot#(s(Y1), s(U1)) => quot#(minus(Y1, U1), s(U1))
      (6)  plus#(s(W1), P1) => plus#(W1, P1)
      (7)  app#(cons(W2, V2), U2) => app#(V2, U2)
      (8)  sum#(cons(Y3, cons(U3, X3))) => plus#(Y3, U3)
      (9)  sum#(cons(Y3, cons(U3, X3))) => sum#(cons(plus(Y3, U3), X3))
      (10) sum#(app(W3, cons(P3, cons(X4, V3)))) => sum#(cons(P3, cons(X4, V3)))
      (11) sum#(app(W3, cons(P3, cons(X4, V3)))) => app#(W3, sum(cons(P3, cons(X4, V3))))
      (12) sum#(app(W3, cons(P3, cons(X4, V3)))) => sum#(app(W3, sum(cons(P3, cons(X4, V3)))))
      (13) map#(G4, cons(V4, W4)) => map#(G4, W4)
      (14) filter#(F5, cons(Y5, U5)) => filter2#(F5(Y5), F5, Y5, U5)
      (15) filter2#(true, H5, W5, P5) => filter#(H5, P5)
      (16) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

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

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) plus#(s(W1), P1) => plus#(W1, P1)

  P3. (1) minus#(s(Y), s(U)) => minus#(Y, U)
      (2) minus#(minus(V, W), P) => minus#(V, plus(W, P))

  P4. (1) quot#(s(Y1), s(U1)) => quot#(minus(Y1, U1), s(U1))

  P5. (1) app#(cons(W2, V2), U2) => app#(V2, U2)

  P6. (1) sum#(cons(Y3, cons(U3, X3))) => sum#(cons(plus(Y3, U3), X3))

  P7. (1) sum#(app(W3, cons(P3, cons(X4, V3)))) => sum#(app(W3, sum(cons(P3, cons(X4, V3)))))

  P8. (1) map#(G4, cons(V4, W4)) => map#(G4, W4)

  P9. (1) filter#(F5, cons(Y5, U5)) => filter2#(F5(Y5), F5, Y5, U5)
      (2) filter2#(true, H5, W5, P5) => filter#(H5, P5)
      (3) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

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

We use the following projection function:

  nu(plus#) = 1

We thus have:

  (1) s(W1) |>| W1

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

We thus have:

  (1) s(Y)        |>| Y
  (2) minus(V, W) |>| V

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 5 usable rules (out of 19 rules in the input problem).

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

  R2. (1) minus(X, 0) -> X
      (2) minus(s(Y), s(U)) -> minus(Y, U)
      (3) minus(minus(V, W), P) -> minus(V, plus(W, P))
      (4) plus(0, V1) -> V1
      (5) plus(s(W1), P1) -> s(plus(W1, P1))

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

We use the following projection function:

  nu(app#) = 1

We thus have:

  (1) cons(W2, V2) |>| V2

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

Processor output: { }.

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

We obtain 2 usable rules (out of 19 rules in the input problem).

Processor output: { D11 = (P6, R3, i, c) }, where:

  R3. (1) plus(0, V1) -> V1
      (2) plus(s(W1), P1) -> s(plus(W1, P1))

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

We obtain 8 usable rules (out of 19 rules in the input problem).

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

  R4. (1) app(nil, X2) -> X2
      (2) app(Y2, nil) -> Y2
      (3) app(cons(W2, V2), U2) -> cons(W2, app(V2, U2))
      (4) plus(0, V1) -> V1
      (5) plus(s(W1), P1) -> s(plus(W1, P1))
      (6) sum(cons(P2, nil)) -> cons(P2, nil)
      (7) sum(cons(Y3, cons(U3, X3))) -> sum(cons(plus(Y3, U3), X3))
      (8) sum(app(W3, cons(P3, cons(X4, V3)))) -> sum(app(W3, sum(cons(P3, cons(X4, V3)))))

***** 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) cons(V4, W4) |>| W4

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) cons(Y5, U5) |>|  U5
  (2) P5           |>=| P5
  (3) U6           |>=| U6

We may remove the strictly oriented DPs.

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

  P10. (1) filter2#(true, H5, W5, P5) => filter#(H5, P5)
       (2) filter2#(false, F6, Y6, U6) => filter#(F6, U6)

***** We apply the Usable rules with respect to an argument wiltering [with HORPO] Processor on D10 = (P4, R2, i, c).

Constrained HORPO yields:

  quot#2(s1(Y1), s1(U1)) (>) quot#2(minus2(Y1, U1), s1(U1))
  minus2(X, 00) (>=) X
  minus2(s1(Y), s1(U)) (>=) minus2(Y, U)
  minus2(minus2(V, W), P) (>=) minus2(V, plus2(W, P))

We do this using the following settings:

* Disregarded arguments:

  minus2 2 
  quot#2 2 

* Precedence and permutation:

    s1      { 1 }
  > quot#2  { 1 }
  > 00      { }
  = minus2  { }   1
  = plus2   { 1 } 2

* Well-founded theory orderings:

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

Processor output: { }.

***** We apply the Usable rules with respect to an argument wiltering [with HORPO] Processor on D11 = (P6, R3, i, c).

Constrained HORPO yields:

  sum#1(cons2(Y3, cons2(U3, X3))) (>) sum#1(cons2(plus2(Y3, U3), X3))
  plus2(00, V1) (>=) V1
  plus2(s1(W1), P1) (>=) s1(plus2(W1, P1))

We do this using the following settings:

* Disregarded arguments:

  plus2 1 
  s1    1 

* Precedence and permutation:

    cons2  { 1 2 }
  > plus2  { }     2
  > s1     { }
  > 00     { }
  = sum#1  { 1 }

* Well-founded theory orderings:

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

Processor output: { }.

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