YES We show the termination of the TRS R: a(a(divides(),|0|()),a(s(),y)) -> true() a(a(divides(),a(s(),x)),a(s(),y)) -> a(a(a(div2(),x),a(s(),y)),y) a(a(a(div2(),x),y),|0|()) -> a(a(divides(),x),y) a(a(a(div2(),|0|()),y),a(s(),z)) -> false() a(a(a(div2(),a(s(),x)),y),a(s(),z)) -> a(a(a(div2(),x),y),z) a(a(filter(),f),nil()) -> nil() a(a(filter(),f),a(a(cons(),x),xs)) -> a(a(a(if(),a(f,x)),x),a(a(filter(),f),xs)) a(a(a(if(),true()),x),xs) -> a(a(cons(),x),xs) a(a(a(if(),false()),x),xs) -> xs a(a(not(),f),x) -> a(not2(),a(f,x)) a(not2(),true()) -> false() a(not2(),false()) -> true() a(sieve(),nil()) -> nil() a(sieve(),a(a(cons(),x),xs)) -> a(a(cons(),x),a(sieve(),a(a(filter(),a(not(),a(divides(),x))),xs))) Instead we prove termination of the uncurried system: a(cons_0(),y) -> cons_1(y) a(cons_1(x1),y) -> cons_2(x1,y) a(div2_0(),y) -> div2_1(y) a(div2_1(x1),y) -> div2_2(x1,y) a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) a(divides_0(),y) -> divides_1(y) a(divides_1(x1),y) -> divides_2(x1,y) a(filter_0(),y) -> filter_1(y) a(filter_1(x1),y) -> filter_2(x1,y) a(if_0(),y) -> if_1(y) a(if_1(x1),y) -> if_2(x1,y) a(if_2(x1,x2),y) -> if_3(x1,x2,y) a(not_0(),y) -> not_1(y) a(not_1(x1),y) -> not_2(x1,y) a(not2_0(),y) -> not2_1(y) a(s_0(),y) -> s_1(y) a(sieve_0(),y) -> sieve_1(y) divides_2(|0|_0(),s_1(y)) -> true_0() divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) div2_3(x,y,|0|_0()) -> divides_2(x,y) div2_3(|0|_0(),y,s_1(z)) -> false_0() div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) filter_2(f,nil_0()) -> nil_0() filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) if_3(true_0(),x,xs) -> cons_2(x,xs) if_3(false_0(),x,xs) -> xs not_2(f,x) -> not2_1(a(f,x)) not2_1(true_0()) -> false_0() not2_1(false_0()) -> true_0() sieve_1(nil_0()) -> nil_0() sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: a#(div2_2(x1,x2),y) -> div2_3#(x1,x2,y) p2: a#(divides_1(x1),y) -> divides_2#(x1,y) p3: a#(filter_1(x1),y) -> filter_2#(x1,y) p4: a#(if_2(x1,x2),y) -> if_3#(x1,x2,y) p5: a#(not_1(x1),y) -> not_2#(x1,y) p6: a#(not2_0(),y) -> not2_1#(y) p7: a#(sieve_0(),y) -> sieve_1#(y) p8: divides_2#(s_1(x),s_1(y)) -> div2_3#(x,s_1(y),y) p9: div2_3#(x,y,|0|_0()) -> divides_2#(x,y) p10: div2_3#(s_1(x),y,s_1(z)) -> div2_3#(x,y,z) p11: filter_2#(f,cons_2(x,xs)) -> if_3#(a(f,x),x,filter_2(f,xs)) p12: filter_2#(f,cons_2(x,xs)) -> a#(f,x) p13: filter_2#(f,cons_2(x,xs)) -> filter_2#(f,xs) p14: not_2#(f,x) -> not2_1#(a(f,x)) p15: not_2#(f,x) -> a#(f,x) p16: sieve_1#(cons_2(x,xs)) -> sieve_1#(filter_2(not_1(divides_1(x)),xs)) p17: sieve_1#(cons_2(x,xs)) -> filter_2#(not_1(divides_1(x)),xs) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The estimated dependency graph contains the following SCCs: {p3, p5, p7, p12, p13, p15, p16, p17} {p8, p9, p10} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not_2#(f,x) -> a#(f,x) p2: a#(sieve_0(),y) -> sieve_1#(y) p3: sieve_1#(cons_2(x,xs)) -> filter_2#(not_1(divides_1(x)),xs) p4: filter_2#(f,cons_2(x,xs)) -> filter_2#(f,xs) p5: filter_2#(f,cons_2(x,xs)) -> a#(f,x) p6: a#(not_1(x1),y) -> not_2#(x1,y) p7: a#(filter_1(x1),y) -> filter_2#(x1,y) p8: sieve_1#(cons_2(x,xs)) -> sieve_1#(filter_2(not_1(divides_1(x)),xs)) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The set of usable rules consists of r18, r23, r26, r30 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: not_2#_A(x1,x2) = x1 a#_A(x1,x2) = x1 sieve_0_A() = 4 sieve_1#_A(x1) = 4 cons_2_A(x1,x2) = x1 + x2 filter_2#_A(x1,x2) = x1 not_1_A(x1) = x1 + 2 divides_1_A(x1) = 2 filter_1_A(x1) = x1 + 2 filter_2_A(x1,x2) = x1 + x2 + 2 divides_2_A(x1,x2) = x1 + x2 + 4 |0|_0_A() = 1 s_1_A(x1) = x1 + 2 true_0_A() = 4 nil_0_A() = 1 if_3_A(x1,x2,x3) = x2 + x3 + 2 false_0_A() = 5 sieve_1_A(x1) = x1 + 2 not_2#!_A(x1,x2) = 7 a#!_A(x1,x2) = 6 sieve_0!_A() = 10 sieve_1#!_A(x1) = 10 cons_2!_A(x1,x2) = 5 filter_2#!_A(x1,x2) = 6 not_1!_A(x1) = 9 divides_1!_A(x1) = 9 filter_1!_A(x1) = 7 filter_2!_A(x1,x2) = 2 divides_2!_A(x1,x2) = x1 + 10 |0|_0!_A() = 7 s_1!_A(x1) = 9 true_0!_A() = 6 nil_0!_A() = 3 if_3!_A(x1,x2,x3) = 1 false_0!_A() = 0 sieve_1!_A(x1) = 4 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: not_2#_A(x1,x2) = x1 a#_A(x1,x2) = x1 sieve_0_A() = 7 sieve_1#_A(x1) = 7 cons_2_A(x1,x2) = x1 + x2 filter_2#_A(x1,x2) = x1 not_1_A(x1) = x1 + 5 divides_1_A(x1) = 2 filter_1_A(x1) = x1 + 2 filter_2_A(x1,x2) = x1 + x2 + 2 divides_2_A(x1,x2) = x1 + x2 + 4 |0|_0_A() = 1 s_1_A(x1) = x1 + 2 true_0_A() = 4 nil_0_A() = 1 if_3_A(x1,x2,x3) = x2 + x3 false_0_A() = 5 sieve_1_A(x1) = x1 + 2 not_2#!_A(x1,x2) = 1 a#!_A(x1,x2) = 0 sieve_0!_A() = 14 sieve_1#!_A(x1) = 14 cons_2!_A(x1,x2) = x2 + 5 filter_2#!_A(x1,x2) = 6 not_1!_A(x1) = x1 + 2 divides_1!_A(x1) = 13 filter_1!_A(x1) = 7 filter_2!_A(x1,x2) = x1 + x2 + 8 divides_2!_A(x1,x2) = x1 + 12 |0|_0!_A() = 7 s_1!_A(x1) = 7 true_0!_A() = 6 nil_0!_A() = 10 if_3!_A(x1,x2,x3) = x1 + 3 false_0!_A() = 0 sieve_1!_A(x1) = 3 partial status: pi(not_2#) = [1] pi(a#) = [1] pi(sieve_0) = [] pi(sieve_1#) = [] pi(cons_2) = [1, 2] pi(filter_2#) = [1] pi(not_1) = [1] pi(divides_1) = [] pi(filter_1) = [1] pi(filter_2) = [2] pi(divides_2) = [1, 2] pi(|0|_0) = [] pi(s_1) = [1] pi(true_0) = [] pi(nil_0) = [] pi(if_3) = [2, 3] pi(false_0) = [] pi(sieve_1) = [] The following rules are removed: p1, p2, p3, p5, p6, p7 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: filter_2#(f,cons_2(x,xs)) -> filter_2#(f,xs) p2: sieve_1#(cons_2(x,xs)) -> sieve_1#(filter_2(not_1(divides_1(x)),xs)) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The estimated dependency graph contains the following SCCs: {p1} {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: filter_2#(f,cons_2(x,xs)) -> filter_2#(f,xs) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: filter_2#_A(x1,x2) = 0 cons_2_A(x1,x2) = x1 + 7 filter_2#!_A(x1,x2) = 0 cons_2!_A(x1,x2) = x1 + x2 + 2 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: filter_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = x2 + 11 filter_2#!_A(x1,x2) = 0 cons_2!_A(x1,x2) = x1 + 19 partial status: pi(filter_2#) = [2] pi(cons_2) = [2] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: sieve_1#(cons_2(x,xs)) -> sieve_1#(filter_2(not_1(divides_1(x)),xs)) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The set of usable rules consists of r1, r2, r3, r6, r8, r10, r11, r12, r13, r15, r16, r21, r23, r24, r25, r26, r28, r29, r30 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: sieve_1#_A(x1) = 0 cons_2_A(x1,x2) = x2 + 4 filter_2_A(x1,x2) = x2 + 1 not_1_A(x1) = 10 divides_1_A(x1) = x1 + 3 a_A(x1,x2) = x2 + 10 cons_0_A() = 1 cons_1_A(x1) = 7 div2_0_A() = 2 div2_1_A(x1) = 3 divides_0_A() = 4 filter_0_A() = 1 filter_1_A(x1) = 8 if_0_A() = 1 if_1_A(x1) = 1 if_2_A(x1,x2) = 8 if_3_A(x1,x2,x3) = x3 + 4 not_0_A() = 5 not2_0_A() = 9 not2_1_A(x1) = 1 s_0_A() = 9 s_1_A(x1) = x1 + 1 div2_3_A(x1,x2,x3) = x2 + x3 |0|_0_A() = 1 false_0_A() = 1 nil_0_A() = 1 true_0_A() = 1 sieve_1_A(x1) = 1 sieve_1#!_A(x1) = x1 + 4 cons_2!_A(x1,x2) = 6 filter_2!_A(x1,x2) = x2 + 7 not_1!_A(x1) = 4 divides_1!_A(x1) = 3 a!_A(x1,x2) = x1 + x2 cons_0!_A() = 1 cons_1!_A(x1) = 0 div2_0!_A() = 0 div2_1!_A(x1) = 1 divides_0!_A() = 3 filter_0!_A() = 1 filter_1!_A(x1) = 0 if_0!_A() = 1 if_1!_A(x1) = 0 if_2!_A(x1,x2) = 0 if_3!_A(x1,x2,x3) = 7 not_0!_A() = 0 not2_0!_A() = 0 not2_1!_A(x1) = 8 s_0!_A() = 0 s_1!_A(x1) = x1 + 8 div2_3!_A(x1,x2,x3) = x3 + 7 |0|_0!_A() = 1 false_0!_A() = 0 nil_0!_A() = 0 true_0!_A() = 7 sieve_1!_A(x1) = x1 + 1 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: sieve_1#_A(x1) = 0 cons_2_A(x1,x2) = 0 filter_2_A(x1,x2) = x1 not_1_A(x1) = 3 divides_1_A(x1) = x1 + 1 a_A(x1,x2) = x2 + 3 cons_0_A() = 1 cons_1_A(x1) = 1 div2_0_A() = 1 div2_1_A(x1) = 1 divides_0_A() = 1 filter_0_A() = 1 filter_1_A(x1) = 1 if_0_A() = 1 if_1_A(x1) = 1 if_2_A(x1,x2) = 3 if_3_A(x1,x2,x3) = x3 not_0_A() = 1 not2_0_A() = 1 not2_1_A(x1) = 1 s_0_A() = 1 s_1_A(x1) = x1 + 3 div2_3_A(x1,x2,x3) = 1 |0|_0_A() = 0 false_0_A() = 1 nil_0_A() = 0 true_0_A() = 1 sieve_1_A(x1) = x1 sieve_1#!_A(x1) = x1 + 3 cons_2!_A(x1,x2) = 7 filter_2!_A(x1,x2) = x1 + 6 not_1!_A(x1) = 2 divides_1!_A(x1) = 6 a!_A(x1,x2) = x2 + 9 cons_0!_A() = 11 cons_1!_A(x1) = 10 div2_0!_A() = 9 div2_1!_A(x1) = 8 divides_0!_A() = 6 filter_0!_A() = 0 filter_1!_A(x1) = 7 if_0!_A() = 0 if_1!_A(x1) = 1 if_2!_A(x1,x2) = 1 if_3!_A(x1,x2,x3) = x2 + 8 not_0!_A() = 0 not2_0!_A() = 0 not2_1!_A(x1) = 10 s_0!_A() = 0 s_1!_A(x1) = x1 + 1 div2_3!_A(x1,x2,x3) = x3 |0|_0!_A() = 4 false_0!_A() = 2 nil_0!_A() = 0 true_0!_A() = 3 sieve_1!_A(x1) = 8 partial status: pi(sieve_1#) = [] pi(cons_2) = [2] pi(filter_2) = [] pi(not_1) = [] pi(divides_1) = [] pi(a) = [2] pi(cons_0) = [] pi(cons_1) = [] pi(div2_0) = [] pi(div2_1) = [] pi(divides_0) = [] pi(filter_0) = [] pi(filter_1) = [] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] pi(if_3) = [3] pi(not_0) = [] pi(not2_0) = [] pi(not2_1) = [1] pi(s_0) = [] pi(s_1) = [] pi(div2_3) = [] pi(|0|_0) = [] pi(false_0) = [] pi(nil_0) = [] pi(true_0) = [] pi(sieve_1) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div2_3#(x,y,|0|_0()) -> divides_2#(x,y) p2: divides_2#(s_1(x),s_1(y)) -> div2_3#(x,s_1(y),y) p3: div2_3#(s_1(x),y,s_1(z)) -> div2_3#(x,y,z) and R consists of: r1: a(cons_0(),y) -> cons_1(y) r2: a(cons_1(x1),y) -> cons_2(x1,y) r3: a(div2_0(),y) -> div2_1(y) r4: a(div2_1(x1),y) -> div2_2(x1,y) r5: a(div2_2(x1,x2),y) -> div2_3(x1,x2,y) r6: a(divides_0(),y) -> divides_1(y) r7: a(divides_1(x1),y) -> divides_2(x1,y) r8: a(filter_0(),y) -> filter_1(y) r9: a(filter_1(x1),y) -> filter_2(x1,y) r10: a(if_0(),y) -> if_1(y) r11: a(if_1(x1),y) -> if_2(x1,y) r12: a(if_2(x1,x2),y) -> if_3(x1,x2,y) r13: a(not_0(),y) -> not_1(y) r14: a(not_1(x1),y) -> not_2(x1,y) r15: a(not2_0(),y) -> not2_1(y) r16: a(s_0(),y) -> s_1(y) r17: a(sieve_0(),y) -> sieve_1(y) r18: divides_2(|0|_0(),s_1(y)) -> true_0() r19: divides_2(s_1(x),s_1(y)) -> div2_3(x,s_1(y),y) r20: div2_3(x,y,|0|_0()) -> divides_2(x,y) r21: div2_3(|0|_0(),y,s_1(z)) -> false_0() r22: div2_3(s_1(x),y,s_1(z)) -> div2_3(x,y,z) r23: filter_2(f,nil_0()) -> nil_0() r24: filter_2(f,cons_2(x,xs)) -> if_3(a(f,x),x,filter_2(f,xs)) r25: if_3(true_0(),x,xs) -> cons_2(x,xs) r26: if_3(false_0(),x,xs) -> xs r27: not_2(f,x) -> not2_1(a(f,x)) r28: not2_1(true_0()) -> false_0() r29: not2_1(false_0()) -> true_0() r30: sieve_1(nil_0()) -> nil_0() r31: sieve_1(cons_2(x,xs)) -> cons_2(x,sieve_1(filter_2(not_1(divides_1(x)),xs))) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: div2_3#_A(x1,x2,x3) = 0 |0|_0_A() = 1 divides_2#_A(x1,x2) = 0 s_1_A(x1) = 2 div2_3#!_A(x1,x2,x3) = x2 + 1 |0|_0!_A() = 9 divides_2#!_A(x1,x2) = x2 s_1!_A(x1) = x1 + 7 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: div2_3#_A(x1,x2,x3) = 0 |0|_0_A() = 1 divides_2#_A(x1,x2) = 0 s_1_A(x1) = x1 + 2 div2_3#!_A(x1,x2,x3) = x1 + x3 + 6 |0|_0!_A() = 11 divides_2#!_A(x1,x2) = x1 + 6 s_1!_A(x1) = 7 partial status: pi(div2_3#) = [1] pi(|0|_0) = [] pi(divides_2#) = [1] pi(s_1) = [1] The following rules are removed: p1, p2, p3 Then no dependency pair remains.