We consider termination of the STRS with no additional rule schemes:

  Signature: 0         :: b
             add       :: b -> c -> c
             app       :: c -> c -> c
             false     :: a
             filter    :: (b -> a) -> c -> c
             filter2   :: a -> (b -> a) -> b -> c -> c
             high      :: b -> c -> c
             if_high   :: a -> b -> c -> c
             if_low    :: a -> b -> c -> c
             le        :: b -> b -> a
             low       :: b -> c -> c
             map       :: (b -> b) -> c -> c
             minus     :: b -> b -> b
             nil       :: c
             quicksort :: c -> c
             quot      :: b -> b -> b
             s         :: b -> b
             true      :: a

  Rules: minus(X, 0) -> X
         minus(s(Y), s(U)) -> minus(Y, U)
         quot(0, s(V)) -> 0
         quot(s(W), s(P)) -> s(quot(minus(W, P), s(P)))
         le(0, X1) -> true
         le(s(Y1), 0) -> false
         le(s(U1), s(V1)) -> le(U1, V1)
         app(nil, W1) -> W1
         app(add(P1, X2), Y2) -> add(P1, app(X2, Y2))
         low(U2, nil) -> nil
         low(W2, add(V2, P2)) -> if_low(le(V2, W2), W2, add(V2, P2))
         if_low(true, Y3, add(X3, U3)) -> add(X3, low(Y3, U3))
         if_low(false, W3, add(V3, P3)) -> low(W3, P3)
         high(X4, nil) -> nil
         high(U4, add(Y4, V4)) -> if_high(le(Y4, U4), U4, add(Y4, V4))
         if_high(true, P4, add(W4, X5)) -> high(P4, X5)
         if_high(false, U5, add(Y5, V5)) -> add(Y5, high(U5, V5))
         quicksort(nil) -> nil
         quicksort(add(W5, P5)) -> app(quicksort(low(W5, P5)), add(W5, quicksort(high(W5, P5))))
         map(F6, nil) -> nil
         map(Z6, add(U6, V6)) -> add(Z6(U6), map(Z6, V6))
         filter(I6, nil) -> nil
         filter(J6, add(X7, Y7)) -> filter2(J6(X7), J6, X7, Y7)
         filter2(true, G7, V7, W7) -> add(V7, filter(G7, W7))
         filter2(false, J7, X8, Y8) -> filter(J7, Y8)

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, i, c), where:

  P1. (1)  minus#(s(Y), s(U)) => minus#(Y, U)
      (2)  quot#(s(W), s(P)) => minus#(W, P)
      (3)  quot#(s(W), s(P)) => quot#(minus(W, P), s(P))
      (4)  le#(s(U1), s(V1)) => le#(U1, V1)
      (5)  app#(add(P1, X2), Y2) => app#(X2, Y2)
      (6)  low#(W2, add(V2, P2)) => le#(V2, W2)
      (7)  low#(W2, add(V2, P2)) => if_low#(le(V2, W2), W2, add(V2, P2))
      (8)  if_low#(true, Y3, add(X3, U3)) => low#(Y3, U3)
      (9)  if_low#(false, W3, add(V3, P3)) => low#(W3, P3)
      (10) high#(U4, add(Y4, V4)) => le#(Y4, U4)
      (11) high#(U4, add(Y4, V4)) => if_high#(le(Y4, U4), U4, add(Y4, V4))
      (12) if_high#(true, P4, add(W4, X5)) => high#(P4, X5)
      (13) if_high#(false, U5, add(Y5, V5)) => high#(U5, V5)
      (14) quicksort#(add(W5, P5)) => low#(W5, P5)
      (15) quicksort#(add(W5, P5)) => quicksort#(low(W5, P5))
      (16) quicksort#(add(W5, P5)) => high#(W5, P5)
      (17) quicksort#(add(W5, P5)) => quicksort#(high(W5, P5))
      (18) quicksort#(add(W5, P5)) => app#(quicksort(low(W5, P5)), add(W5, quicksort(high(W5, P5))))
      (19) map#(Z6, add(U6, V6)) => map#(Z6, V6)
      (20) filter#(J6, add(X7, Y7)) => filter2#(J6(X7), J6, X7, Y7)
      (21) filter2#(true, G7, V7, W7) => filter#(G7, W7)
      (22) filter2#(false, J7, X8, Y8) => filter#(J7, Y8)

***** We apply the Graph Processor on D1 = (P1, R, i, c).

We compute a graph approximation with the following edges:

  1:  1 
  2:  1 
  3:  2 3 
  4:  4 
  5:  5 
  6:  4 
  7:  8 9 
  8:  6 7 
  9:  6 7 
  10: 4 
  11: 12 13 
  12: 10 11 
  13: 10 11 
  14: 6 7 
  15: 14 15 16 17 18 
  16: 10 11 
  17: 14 15 16 17 18 
  18: 5 
  19: 19 
  20: 21 22 
  21: 20 
  22: 20 

There are 9 SCCs.

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) ; D5 = (P5, R, i, c) ; D6 = (P6, R, i, c) ; D7 = (P7, R, i, c) ; D8 = (P8, R, i, c) ; D9 = (P9, R, i, c) ; D10 = (P10, R, i, c) }, where:

  P2. (1) minus#(s(Y), s(U)) => minus#(Y, U)

  P3. (1) quot#(s(W), s(P)) => quot#(minus(W, P), s(P))

  P4. (1) le#(s(U1), s(V1)) => le#(U1, V1)

  P5. (1) app#(add(P1, X2), Y2) => app#(X2, Y2)

  P6. (1) low#(W2, add(V2, P2)) => if_low#(le(V2, W2), W2, add(V2, P2))
      (2) if_low#(true, Y3, add(X3, U3)) => low#(Y3, U3)
      (3) if_low#(false, W3, add(V3, P3)) => low#(W3, P3)

  P7. (1) high#(U4, add(Y4, V4)) => if_high#(le(Y4, U4), U4, add(Y4, V4))
      (2) if_high#(true, P4, add(W4, X5)) => high#(P4, X5)
      (3) if_high#(false, U5, add(Y5, V5)) => high#(U5, V5)

  P8. (1) quicksort#(add(W5, P5)) => quicksort#(low(W5, P5))
      (2) quicksort#(add(W5, P5)) => quicksort#(high(W5, P5))

  P9. (1) map#(Z6, add(U6, V6)) => map#(Z6, V6)

  P10. (1) filter#(J6, add(X7, Y7)) => filter2#(J6(X7), J6, X7, Y7)
       (2) filter2#(true, G7, V7, W7) => filter#(G7, W7)
       (3) filter2#(false, J7, X8, Y8) => filter#(J7, Y8)

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

We use the following projection function:

  nu(minus#) = 1

We thus have:

  (1) s(Y) |>| Y

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

Processor output: { }.

***** We apply the Usable Rules Processor on D3 = (P3, R, i, c).

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

Processor output: { D11 = (P3, R2, i, c) }, where:

  R2. (1) minus(X, 0) -> X
      (2) minus(s(Y), s(U)) -> minus(Y, U)

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

We use the following projection function:

  nu(le#) = 1

We thus have:

  (1) s(U1) |>| U1

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

Processor output: { }.

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

We use the following projection function:

  nu(app#) = 1

We thus have:

  (1) add(P1, X2) |>| X2

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, i, c).

We use the following projection function:

  nu(if_low#) = 3
  nu(low#)    = 2

We thus have:

  (1) add(V2, P2) |>=| add(V2, P2)
  (2) add(X3, U3) |>|  U3
  (3) add(V3, P3) |>|  P3

We may remove the strictly oriented DPs.

Processor output: { D12 = (P11, R, i, c) }, where:

  P11. (1) low#(W2, add(V2, P2)) => if_low#(le(V2, W2), W2, add(V2, P2))

***** We apply the Subterm Criterion Processor on D7 = (P7, R, i, c).

We use the following projection function:

  nu(high#)    = 2
  nu(if_high#) = 3

We thus have:

  (1) add(Y4, V4) |>=| add(Y4, V4)
  (2) add(W4, X5) |>|  X5
  (3) add(Y5, V5) |>|  V5

We may remove the strictly oriented DPs.

Processor output: { D13 = (P12, R, i, c) }, where:

  P12. (1) high#(U4, add(Y4, V4)) => if_high#(le(Y4, U4), U4, add(Y4, V4))

***** We apply the Usable Rules Processor on D8 = (P8, R, i, c).

We obtain 11 usable rules (out of 25 rules in the input problem).

Processor output: { D14 = (P8, R3, i, c) }, where:

  R3. (1)  high(X4, nil) -> nil
      (2)  high(U4, add(Y4, V4)) -> if_high(le(Y4, U4), U4, add(Y4, V4))
      (3)  if_high(true, P4, add(W4, X5)) -> high(P4, X5)
      (4)  if_high(false, U5, add(Y5, V5)) -> add(Y5, high(U5, V5))
      (5)  if_low(true, Y3, add(X3, U3)) -> add(X3, low(Y3, U3))
      (6)  if_low(false, W3, add(V3, P3)) -> low(W3, P3)
      (7)  le(0, X1) -> true
      (8)  le(s(Y1), 0) -> false
      (9)  le(s(U1), s(V1)) -> le(U1, V1)
      (10) low(U2, nil) -> nil
      (11) low(W2, add(V2, P2)) -> if_low(le(V2, W2), W2, add(V2, P2))

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

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) add(U6, V6) |>| V6

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

Processor output: { }.

***** We apply the Subterm Criterion Processor on D10 = (P10, R, i, c).

We use the following projection function:

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

We thus have:

  (1) add(X7, Y7) |>|  Y7
  (2) W7          |>=| W7
  (3) Y8          |>=| Y8

We may remove the strictly oriented DPs.

Processor output: { D15 = (P13, R, i, c) }, where:

  P13. (1) filter2#(true, G7, V7, W7) => filter#(G7, W7)
       (2) filter2#(false, J7, X8, Y8) => filter#(J7, Y8)

***** We apply the Usable rules with respect to HORPO Processor on D11 = (P3, R2, i, c).

Constrained HORPO yields:

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

We do this using the following settings:

* Disregarded arguments:

  minus2 2 

* Precedence and permutation:

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

* Well-founded theory orderings:

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

Processor output: { }.

***** We apply the Graph Processor on D12 = (P11, 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: { }.

***** We apply the Graph Processor on D13 = (P12, 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 D14 = (P8, R3, i, c).