We consider universal computability of the STRS with no additional rule schemes: Signature: 0 :: b cons :: b -> 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_replace :: a -> b -> b -> c -> c le :: b -> b -> a map :: (b -> b) -> c -> c min :: c -> b nil :: c replace :: b -> b -> c -> c s :: b -> b sort :: c -> c true :: a Rules: eq(0, 0) -> true eq(0, s(X)) -> false eq(s(Y), 0) -> false eq(s(V), s(U)) -> eq(V, U) le(0, W) -> true le(s(P), 0) -> false le(s(Y1), s(X1)) -> le(Y1, X1) min(cons(0, nil)) -> 0 min(cons(s(U1), nil)) -> s(U1) min(cons(W1, cons(V1, P1))) -> if_min(le(W1, V1), cons(W1, cons(V1, P1))) if_min(true, cons(Y2, cons(X2, U2))) -> min(cons(Y2, U2)) if_min(false, cons(W2, cons(V2, P2))) -> min(cons(V2, P2)) replace(Y3, X3, nil) -> nil replace(W3, V3, cons(U3, P3)) -> if_replace(eq(W3, U3), W3, V3, cons(U3, P3)) if_replace(true, U4, Y4, cons(X4, V4)) -> cons(Y4, V4) if_replace(false, X5, P4, cons(W4, Y5)) -> cons(W4, replace(X5, P4, Y5)) sort(nil) -> nil sort(cons(U5, V5)) -> cons(min(cons(U5, V5)), sort(replace(min(cons(U5, V5)), U5, V5))) map(I5, nil) -> nil map(J5, cons(X6, Y6)) -> cons(J5(X6), map(J5, Y6)) filter(G6, nil) -> nil filter(H6, cons(W6, P6)) -> filter2(H6(W6), H6, W6, P6) filter2(true, F7, Y7, U7) -> cons(Y7, filter(F7, U7)) filter2(false, H7, W7, P7) -> filter(H7, P7) 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(V), s(U)) => eq#(V, U) (2) le#(s(Y1), s(X1)) => le#(Y1, X1) (3) min#(cons(W1, cons(V1, P1))) => le#(W1, V1) (4) min#(cons(W1, cons(V1, P1))) => if_min#(le(W1, V1), cons(W1, cons(V1, P1))) (5) if_min#(true, cons(Y2, cons(X2, U2))) => min#(cons(Y2, U2)) (6) if_min#(false, cons(W2, cons(V2, P2))) => min#(cons(V2, P2)) (7) replace#(W3, V3, cons(U3, P3)) => eq#(W3, U3) (8) replace#(W3, V3, cons(U3, P3)) => if_replace#(eq(W3, U3), W3, V3, cons(U3, P3)) (9) if_replace#(false, X5, P4, cons(W4, Y5)) => replace#(X5, P4, Y5) (10) sort#(cons(U5, V5)) => min#(cons(U5, V5)) (11) sort#(cons(U5, V5)) => min#(cons(U5, V5)) (12) sort#(cons(U5, V5)) => replace#(min(cons(U5, V5)), U5, V5) (13) sort#(cons(U5, V5)) => sort#(replace(min(cons(U5, V5)), U5, V5)) (14) map#(J5, cons(X6, Y6)) => map#(J5, Y6) (15) filter#(H6, cons(W6, P6)) => filter2#(H6(W6), H6, W6, P6) (16) filter2#(true, F7, Y7, U7) => filter#(F7, U7) (17) filter2#(false, H7, W7, P7) => filter#(H7, P7) ***** 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: 2 4: 5 6 5: 3 4 6: 3 4 7: 1 8: 9 9: 7 8 10: 3 4 11: 3 4 12: 7 8 13: 10 11 12 13 14: 14 15: 16 17 16: 15 17: 15 There are 7 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) }, where: P2. (1) eq#(s(V), s(U)) => eq#(V, U) P3. (1) le#(s(Y1), s(X1)) => le#(Y1, X1) P4. (1) min#(cons(W1, cons(V1, P1))) => if_min#(le(W1, V1), cons(W1, cons(V1, P1))) (2) if_min#(true, cons(Y2, cons(X2, U2))) => min#(cons(Y2, U2)) (3) if_min#(false, cons(W2, cons(V2, P2))) => min#(cons(V2, P2)) P5. (1) replace#(W3, V3, cons(U3, P3)) => if_replace#(eq(W3, U3), W3, V3, cons(U3, P3)) (2) if_replace#(false, X5, P4, cons(W4, Y5)) => replace#(X5, P4, Y5) P6. (1) sort#(cons(U5, V5)) => sort#(replace(min(cons(U5, V5)), U5, V5)) P7. (1) map#(J5, cons(X6, Y6)) => map#(J5, Y6) P8. (1) filter#(H6, cons(W6, P6)) => filter2#(H6(W6), H6, W6, P6) (2) filter2#(true, F7, Y7, U7) => filter#(F7, U7) (3) filter2#(false, H7, W7, P7) => filter#(H7, P7) ***** 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(V) |>| V 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(Y1) |>| Y1 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 3 usable rules (out of 24 rules in the input problem). Processor output: { D9 = (P4, R2, i, c) }, where: R2. (1) le(0, W) -> true (2) le(s(P), 0) -> false (3) le(s(Y1), s(X1)) -> le(Y1, X1) ***** We apply the Subterm Criterion Processor on D5 = (P5, R UNION R_?, i, c). We use the following projection function: nu(if_replace#) = 4 nu(replace#) = 3 We thus have: (1) cons(U3, P3) |>=| cons(U3, P3) (2) cons(W4, Y5) |>| Y5 We may remove the strictly oriented DPs. Processor output: { D10 = (P9, R UNION R_?, i, c) }, where: P9. (1) replace#(W3, V3, cons(U3, P3)) => if_replace#(eq(W3, U3), W3, V3, cons(U3, P3)) ***** We apply the Usable Rules Processor on D6 = (P6, R UNION R_?, i, c). We obtain 16 usable rules (out of 24 rules in the input problem). Processor output: { D11 = (P6, R3, i, c) }, where: R3. (1) eq(0, 0) -> true (2) eq(0, s(X)) -> false (3) eq(s(Y), 0) -> false (4) eq(s(V), s(U)) -> eq(V, U) (5) if_min(true, cons(Y2, cons(X2, U2))) -> min(cons(Y2, U2)) (6) if_min(false, cons(W2, cons(V2, P2))) -> min(cons(V2, P2)) (7) if_replace(true, U4, Y4, cons(X4, V4)) -> cons(Y4, V4) (8) if_replace(false, X5, P4, cons(W4, Y5)) -> cons(W4, replace(X5, P4, Y5)) (9) le(0, W) -> true (10) le(s(P), 0) -> false (11) le(s(Y1), s(X1)) -> le(Y1, X1) (12) min(cons(0, nil)) -> 0 (13) min(cons(s(U1), nil)) -> s(U1) (14) min(cons(W1, cons(V1, P1))) -> if_min(le(W1, V1), cons(W1, cons(V1, P1))) (15) replace(Y3, X3, nil) -> nil (16) replace(W3, V3, cons(U3, P3)) -> if_replace(eq(W3, U3), W3, V3, cons(U3, P3)) ***** We apply the Subterm Criterion Processor on D7 = (P7, R UNION R_?, i, c). We use the following projection function: nu(map#) = 2 We thus have: (1) cons(X6, Y6) |>| Y6 All DPs are strictly oriented, and may be removed. Hence, this DP problem is finite. Processor output: { }. ***** We apply the Subterm Criterion Processor on D8 = (P8, R UNION R_?, i, c). We use the following projection function: nu(filter#) = 2 nu(filter2#) = 4 We thus have: (1) cons(W6, P6) |>| P6 (2) U7 |>=| U7 (3) P7 |>=| P7 We may remove the strictly oriented DPs. Processor output: { D12 = (P10, R UNION R_?, i, c) }, where: P10. (1) filter2#(true, F7, Y7, U7) => filter#(F7, U7) (2) filter2#(false, H7, W7, P7) => filter#(H7, P7) ***** We apply the Usable rules with respect to HORPO Processor on D9 = (P4, R2, i, c). Constrained HORPO yields: min#1(cons2(W1, cons2(V1, P1))) (>) if_min#2(le2(W1, V1), cons2(W1, cons2(V1, P1))) if_min#2(true0, cons2(Y2, cons2(X2, U2))) (>) min#1(cons2(Y2, U2)) if_min#2(false0, cons2(W2, cons2(V2, P2))) (>) min#1(cons2(V2, P2)) le2(00, W) (>=) true0 le2(s1(P), 00) (>=) false0 le2(s1(Y1), s1(X1)) (>=) le2(Y1, X1) We do this using the following settings: * Disregarded arguments: le2 2 * Precedence and permutation: 00 { } = false0 { } = s1 { 1 } = true0 { } > cons2 { 1 2 } > min#1 { 1 } > if_min#2 { 2 } 1 > le2 { } 1 * Well-founded theory orderings: [>]_{Bool} = {(true,false)} [>]_{Int} = {(x,y) | x < 1000 /\ x < y } Processor output: { }. ***** We apply the Graph Processor on D10 = (P9, 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 D11 = (P6, R3, i, c).