We consider termination of the STRS with no additional rule schemes: Signature: 0 :: a cons :: c -> d -> d f :: a -> a -> a -> a -> b false :: b filter :: (c -> b) -> d -> d filter2 :: b -> (c -> b) -> c -> d -> d if :: b -> b -> b -> b le :: a -> a -> b map :: (c -> c) -> d -> d minus :: a -> a -> a nil :: d perfectp :: a -> b s :: a -> a true :: b Rules: minus(0, X) -> 0 minus(s(Y), 0) -> s(Y) minus(s(U), s(V)) -> minus(U, V) le(0, W) -> true le(s(P), 0) -> false le(s(X1), s(Y1)) -> le(X1, Y1) if(true, U1, V1) -> U1 if(false, W1, P1) -> P1 perfectp(0) -> false perfectp(s(X2)) -> f(X2, s(0), s(X2), s(X2)) f(0, U2, 0, Y2) -> true f(0, W2, s(P2), V2) -> false f(s(Y3), 0, U3, X3) -> f(Y3, X3, minus(U3, s(Y3)), X3) f(s(W3), s(P3), X4, V3) -> if(le(W3, P3), f(s(W3), minus(P3, W3), X4, V3), f(W3, V3, 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, i, c), where: P1. (1) minus#(s(U), s(V)) => minus#(U, V) (2) le#(s(X1), s(Y1)) => le#(X1, Y1) (3) perfectp#(s(X2)) => f#(X2, s(0), s(X2), s(X2)) (4) f#(s(Y3), 0, U3, X3) => minus#(U3, s(Y3)) (5) f#(s(Y3), 0, U3, X3) => f#(Y3, X3, minus(U3, s(Y3)), X3) (6) f#(s(W3), s(P3), X4, V3) => le#(W3, P3) (7) f#(s(W3), s(P3), X4, V3) => minus#(P3, W3) (8) f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3) (9) f#(s(W3), s(P3), X4, V3) => f#(W3, V3, X4, V3) (10) f#(s(W3), s(P3), X4, V3) => if#(le(W3, P3), f(s(W3), minus(P3, W3), X4, V3), f(W3, V3, X4, V3)) (11) map#(G4, cons(V4, W4)) => map#(G4, W4) (12) filter#(F5, cons(Y5, U5)) => filter2#(F5(Y5), F5, Y5, U5) (13) filter2#(true, H5, W5, P5) => filter#(H5, P5) (14) filter2#(false, F6, Y6, U6) => filter#(F6, U6) ***** We apply the Graph Processor on D1 = (P1, R, i, c). We compute a graph approximation with the following edges: 1: 1 2: 2 3: 6 7 8 9 10 4: 1 5: 4 5 6 7 8 9 10 6: 2 7: 1 8: 4 5 6 7 8 9 10 9: 4 5 6 7 8 9 10 10: 11: 11 12: 13 14 13: 12 14: 12 There are 5 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) }, where: P2. (1) minus#(s(U), s(V)) => minus#(U, V) P3. (1) le#(s(X1), s(Y1)) => le#(X1, Y1) P4. (1) f#(s(Y3), 0, U3, X3) => f#(Y3, X3, minus(U3, s(Y3)), X3) (2) f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3) (3) f#(s(W3), s(P3), X4, V3) => f#(W3, V3, X4, V3) P5. (1) map#(G4, cons(V4, W4)) => map#(G4, W4) P6. (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, i, c). We use the following projection function: nu(minus#) = 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, 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, i, c). We use the following projection function: nu(f#) = 1 We thus have: (1) s(Y3) |>| Y3 (2) s(W3) |>=| s(W3) (3) s(W3) |>| W3 We may remove the strictly oriented DPs. Processor output: { D7 = (P7, R, i, c) }, where: P7. (1) f#(s(W3), s(P3), X4, V3) => f#(s(W3), minus(P3, W3), X4, V3) ***** We apply the Subterm Criterion Processor on D5 = (P5, 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 D6 = (P6, 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: { D8 = (P8, R, i, c) }, where: P8. (1) filter2#(true, H5, W5, P5) => filter#(H5, P5) (2) filter2#(false, F6, Y6, U6) => filter#(F6, U6) ***** We apply the Usable Rules Processor on D7 = (P7, R, i, c). We obtain 3 usable rules (out of 20 rules in the input problem). Processor output: { D9 = (P7, R2, i, c) }, where: R2. (1) minus(0, X) -> 0 (2) minus(s(Y), 0) -> s(Y) (3) minus(s(U), s(V)) -> minus(U, V) ***** We apply the Graph Processor on D8 = (P8, R, i, c). We compute a graph approximation with the following edges: 1: 2: As there are no SCCs, this DP problem is removed. Processor output: { }. ***** We apply the Usable rules with respect to HORPO Processor on D9 = (P7, R2, i, c). Constrained HORPO yields: f#4(s1(W3), s1(P3), X4, V3) (>) f#4(s1(W3), minus2(P3, W3), X4, V3) minus2(00, X) (>=) 00 minus2(s1(Y), 00) (>=) s1(Y) minus2(s1(U), s1(V)) (>=) minus2(U, V) We do this using the following settings: * Disregarded arguments: f#4 4 minus2 2 * Precedence and permutation: 00 { } = s1 { 1 } > f#4 { 1 3 } _ _ 2 = minus2 { } 1 * Well-founded theory orderings: [>]_{Bool} = {(true,false)} [>]_{Int} = {(x,y) | x < 1000 /\ x < y } Processor output: { }.