We consider termination 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, f, 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, f, 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, f, c) ; D3 = (P3, R, f, c) ; D4 = (P4, R, f, c) ; D5 = (P5, R, f, c) ; D6 = (P6, R, f, c) ; D7 = (P7, R, f, c) ; D8 = (P8, R, f, c) ; D9 = (P9, R, f, 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, f, 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, f, 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: { }.

***** No progress could be made on DP problem D4 = (P4, R, f, c).