YES We show the termination of the TRS R: app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y) app(app(lt(),|0|()),app(s(),y)) -> true() app(app(lt(),y),|0|()) -> false() app(app(eq(),x),x) -> true() app(app(eq(),app(s(),x)),|0|()) -> false() app(app(eq(),|0|()),app(s(),x)) -> false() app(app(member(),w),null()) -> false() app(app(member(),w),app(app(app(fork(),x),y),z)) -> app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z))) Instead we prove termination of the uncurried system: app(eq_0(),y) -> eq_1(y) app(eq_1(x1),y) -> eq_2(x1,y) app(fork_0(),y) -> fork_1(y) app(fork_1(x1),y) -> fork_2(x1,y) app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) app(if_0(),y) -> if_1(y) app(if_1(x1),y) -> if_2(x1,y) app(if_2(x1,x2),y) -> if_3(x1,x2,y) app(lt_0(),y) -> lt_1(y) app(lt_1(x1),y) -> lt_2(x1,y) app(member_0(),y) -> member_1(y) app(member_1(x1),y) -> member_2(x1,y) app(s_0(),y) -> s_1(y) lt_2(s_1(x),s_1(y)) -> lt_2(x,y) lt_2(|0|_0(),s_1(y)) -> true_0() lt_2(y,|0|_0()) -> false_0() eq_2(x,x) -> true_0() eq_2(s_1(x),|0|_0()) -> false_0() eq_2(|0|_0(),s_1(x)) -> false_0() member_2(w,null_0()) -> false_0() member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(eq_1(x1),y) -> eq_2#(x1,y) p2: app#(lt_1(x1),y) -> lt_2#(x1,y) p3: app#(member_1(x1),y) -> member_2#(x1,y) p4: lt_2#(s_1(x),s_1(y)) -> lt_2#(x,y) p5: member_2#(w,fork_3(x,y,z)) -> lt_2#(w,y) p6: member_2#(w,fork_3(x,y,z)) -> member_2#(w,x) p7: member_2#(w,fork_3(x,y,z)) -> eq_2#(w,y) p8: member_2#(w,fork_3(x,y,z)) -> member_2#(w,z) and R consists of: r1: app(eq_0(),y) -> eq_1(y) r2: app(eq_1(x1),y) -> eq_2(x1,y) r3: app(fork_0(),y) -> fork_1(y) r4: app(fork_1(x1),y) -> fork_2(x1,y) r5: app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) r6: app(if_0(),y) -> if_1(y) r7: app(if_1(x1),y) -> if_2(x1,y) r8: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r9: app(lt_0(),y) -> lt_1(y) r10: app(lt_1(x1),y) -> lt_2(x1,y) r11: app(member_0(),y) -> member_1(y) r12: app(member_1(x1),y) -> member_2(x1,y) r13: app(s_0(),y) -> s_1(y) r14: lt_2(s_1(x),s_1(y)) -> lt_2(x,y) r15: lt_2(|0|_0(),s_1(y)) -> true_0() r16: lt_2(y,|0|_0()) -> false_0() r17: eq_2(x,x) -> true_0() r18: eq_2(s_1(x),|0|_0()) -> false_0() r19: eq_2(|0|_0(),s_1(x)) -> false_0() r20: member_2(w,null_0()) -> false_0() r21: member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) The estimated dependency graph contains the following SCCs: {p6, p8} {p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: member_2#(w,fork_3(x,y,z)) -> member_2#(w,z) p2: member_2#(w,fork_3(x,y,z)) -> member_2#(w,x) and R consists of: r1: app(eq_0(),y) -> eq_1(y) r2: app(eq_1(x1),y) -> eq_2(x1,y) r3: app(fork_0(),y) -> fork_1(y) r4: app(fork_1(x1),y) -> fork_2(x1,y) r5: app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) r6: app(if_0(),y) -> if_1(y) r7: app(if_1(x1),y) -> if_2(x1,y) r8: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r9: app(lt_0(),y) -> lt_1(y) r10: app(lt_1(x1),y) -> lt_2(x1,y) r11: app(member_0(),y) -> member_1(y) r12: app(member_1(x1),y) -> member_2(x1,y) r13: app(s_0(),y) -> s_1(y) r14: lt_2(s_1(x),s_1(y)) -> lt_2(x,y) r15: lt_2(|0|_0(),s_1(y)) -> true_0() r16: lt_2(y,|0|_0()) -> false_0() r17: eq_2(x,x) -> true_0() r18: eq_2(s_1(x),|0|_0()) -> false_0() r19: eq_2(|0|_0(),s_1(x)) -> false_0() r20: member_2(w,null_0()) -> false_0() r21: member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: member_2#_A(0,0) = 0 member_2#_A(0,1) = 0 member_2#_A(1,0) = 0 member_2#_A(1,1) = 0 fork_3_A(0,0,0) = 0 fork_3_A(0,0,1) = 0 fork_3_A(0,1,0) = 0 fork_3_A(0,1,1) = 0 fork_3_A(1,0,0) = 0 fork_3_A(1,0,1) = 0 fork_3_A(1,1,0) = 0 fork_3_A(1,1,1) = 0 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 eq_0_A = 0 eq_1_A(0) = 1 eq_1_A(1) = 1 eq_2_A(0,0) = 0 eq_2_A(0,1) = 0 eq_2_A(1,0) = 0 eq_2_A(1,1) = 0 fork_0_A = 1 fork_1_A(0) = 0 fork_1_A(1) = 0 fork_2_A(0,0) = 1 fork_2_A(0,1) = 1 fork_2_A(1,0) = 1 fork_2_A(1,1) = 1 if_0_A = 1 if_1_A(0) = 0 if_1_A(1) = 0 if_2_A(0,0) = 1 if_2_A(0,1) = 1 if_2_A(1,0) = 1 if_2_A(1,1) = 1 if_3_A(0,0,0) = 0 if_3_A(0,0,1) = 0 if_3_A(0,1,0) = 0 if_3_A(0,1,1) = 0 if_3_A(1,0,0) = 0 if_3_A(1,0,1) = 0 if_3_A(1,1,0) = 0 if_3_A(1,1,1) = 0 lt_0_A = 0 lt_1_A(0) = 1 lt_1_A(1) = 1 lt_2_A(0,0) = 0 lt_2_A(0,1) = 0 lt_2_A(1,0) = 0 lt_2_A(1,1) = 0 member_0_A = 0 member_1_A(0) = 1 member_1_A(1) = 1 member_2_A(0,0) = 0 member_2_A(0,1) = 0 member_2_A(1,0) = 0 member_2_A(1,1) = 0 s_0_A = 0 s_1_A(0) = 1 s_1_A(1) = 1 |0|_0_A = 0 true_0_A = 0 false_0_A = 0 null_0_A = 1 member_2#!_A(0,0) = 1 member_2#!_A(0,1) = 1 member_2#!_A(1,0) = 1 member_2#!_A(1,1) = 0 fork_3!_A(0,0,0) = 0 fork_3!_A(0,0,1) = 0 fork_3!_A(0,1,0) = 1 fork_3!_A(0,1,1) = 0 fork_3!_A(1,0,0) = 0 fork_3!_A(1,0,1) = 0 fork_3!_A(1,1,0) = 0 fork_3!_A(1,1,1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 eq_0!_A = 1 eq_1!_A(0) = 1 eq_1!_A(1) = 1 eq_2!_A(0,0) = 1 eq_2!_A(0,1) = 1 eq_2!_A(1,0) = 1 eq_2!_A(1,1) = 1 fork_0!_A = 0 fork_1!_A(0) = 0 fork_1!_A(1) = 0 fork_2!_A(0,0) = 1 fork_2!_A(0,1) = 1 fork_2!_A(1,0) = 1 fork_2!_A(1,1) = 1 if_0!_A = 1 if_1!_A(0) = 1 if_1!_A(1) = 1 if_2!_A(0,0) = 0 if_2!_A(0,1) = 0 if_2!_A(1,0) = 0 if_2!_A(1,1) = 0 if_3!_A(0,0,0) = 1 if_3!_A(0,0,1) = 0 if_3!_A(0,1,0) = 1 if_3!_A(0,1,1) = 1 if_3!_A(1,0,0) = 1 if_3!_A(1,0,1) = 1 if_3!_A(1,1,0) = 0 if_3!_A(1,1,1) = 0 lt_0!_A = 1 lt_1!_A(0) = 0 lt_1!_A(1) = 0 lt_2!_A(0,0) = 1 lt_2!_A(0,1) = 1 lt_2!_A(1,0) = 1 lt_2!_A(1,1) = 1 member_0!_A = 1 member_1!_A(0) = 0 member_1!_A(1) = 0 member_2!_A(0,0) = 1 member_2!_A(0,1) = 1 member_2!_A(1,0) = 1 member_2!_A(1,1) = 1 s_0!_A = 1 s_1!_A(0) = 0 s_1!_A(1) = 0 |0|_0!_A = 1 true_0!_A = 1 false_0!_A = 1 null_0!_A = 1 partial status: pi(member_2#) = [2] pi(fork_3) = [1, 2, 3] pi(app) = [1, 2] pi(eq_0) = [] pi(eq_1) = [] pi(eq_2) = [] pi(fork_0) = [] pi(fork_1) = [1] pi(fork_2) = [1, 2] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] pi(if_3) = [] pi(lt_0) = [] pi(lt_1) = [] pi(lt_2) = [] pi(member_0) = [] pi(member_1) = [1] pi(member_2) = [1, 2] pi(s_0) = [] pi(s_1) = [] pi(|0|_0) = [] pi(true_0) = [] pi(false_0) = [] pi(null_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: member_2#(w,fork_3(x,y,z)) -> member_2#(w,x) and R consists of: r1: app(eq_0(),y) -> eq_1(y) r2: app(eq_1(x1),y) -> eq_2(x1,y) r3: app(fork_0(),y) -> fork_1(y) r4: app(fork_1(x1),y) -> fork_2(x1,y) r5: app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) r6: app(if_0(),y) -> if_1(y) r7: app(if_1(x1),y) -> if_2(x1,y) r8: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r9: app(lt_0(),y) -> lt_1(y) r10: app(lt_1(x1),y) -> lt_2(x1,y) r11: app(member_0(),y) -> member_1(y) r12: app(member_1(x1),y) -> member_2(x1,y) r13: app(s_0(),y) -> s_1(y) r14: lt_2(s_1(x),s_1(y)) -> lt_2(x,y) r15: lt_2(|0|_0(),s_1(y)) -> true_0() r16: lt_2(y,|0|_0()) -> false_0() r17: eq_2(x,x) -> true_0() r18: eq_2(s_1(x),|0|_0()) -> false_0() r19: eq_2(|0|_0(),s_1(x)) -> false_0() r20: member_2(w,null_0()) -> false_0() r21: member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: member_2#(w,fork_3(x,y,z)) -> member_2#(w,x) and R consists of: r1: app(eq_0(),y) -> eq_1(y) r2: app(eq_1(x1),y) -> eq_2(x1,y) r3: app(fork_0(),y) -> fork_1(y) r4: app(fork_1(x1),y) -> fork_2(x1,y) r5: app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) r6: app(if_0(),y) -> if_1(y) r7: app(if_1(x1),y) -> if_2(x1,y) r8: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r9: app(lt_0(),y) -> lt_1(y) r10: app(lt_1(x1),y) -> lt_2(x1,y) r11: app(member_0(),y) -> member_1(y) r12: app(member_1(x1),y) -> member_2(x1,y) r13: app(s_0(),y) -> s_1(y) r14: lt_2(s_1(x),s_1(y)) -> lt_2(x,y) r15: lt_2(|0|_0(),s_1(y)) -> true_0() r16: lt_2(y,|0|_0()) -> false_0() r17: eq_2(x,x) -> true_0() r18: eq_2(s_1(x),|0|_0()) -> false_0() r19: eq_2(|0|_0(),s_1(x)) -> false_0() r20: member_2(w,null_0()) -> false_0() r21: member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: member_2#_A(0,0) = 0 member_2#_A(0,1) = 0 member_2#_A(1,0) = 0 member_2#_A(1,1) = 0 fork_3_A(0,0,0) = 0 fork_3_A(0,0,1) = 0 fork_3_A(0,1,0) = 0 fork_3_A(0,1,1) = 0 fork_3_A(1,0,0) = 0 fork_3_A(1,0,1) = 0 fork_3_A(1,1,0) = 0 fork_3_A(1,1,1) = 0 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 eq_0_A = 0 eq_1_A(0) = 1 eq_1_A(1) = 1 eq_2_A(0,0) = 0 eq_2_A(0,1) = 0 eq_2_A(1,0) = 0 eq_2_A(1,1) = 0 fork_0_A = 1 fork_1_A(0) = 0 fork_1_A(1) = 0 fork_2_A(0,0) = 1 fork_2_A(0,1) = 1 fork_2_A(1,0) = 1 fork_2_A(1,1) = 1 if_0_A = 1 if_1_A(0) = 0 if_1_A(1) = 0 if_2_A(0,0) = 1 if_2_A(0,1) = 1 if_2_A(1,0) = 1 if_2_A(1,1) = 1 if_3_A(0,0,0) = 0 if_3_A(0,0,1) = 0 if_3_A(0,1,0) = 0 if_3_A(0,1,1) = 0 if_3_A(1,0,0) = 0 if_3_A(1,0,1) = 0 if_3_A(1,1,0) = 0 if_3_A(1,1,1) = 0 lt_0_A = 0 lt_1_A(0) = 1 lt_1_A(1) = 1 lt_2_A(0,0) = 0 lt_2_A(0,1) = 0 lt_2_A(1,0) = 0 lt_2_A(1,1) = 0 member_0_A = 0 member_1_A(0) = 1 member_1_A(1) = 1 member_2_A(0,0) = 0 member_2_A(0,1) = 0 member_2_A(1,0) = 0 member_2_A(1,1) = 0 s_0_A = 1 s_1_A(0) = 0 s_1_A(1) = 0 |0|_0_A = 0 true_0_A = 0 false_0_A = 0 null_0_A = 1 member_2#!_A(0,0) = 0 member_2#!_A(0,1) = 0 member_2#!_A(1,0) = 0 member_2#!_A(1,1) = 0 fork_3!_A(0,0,0) = 0 fork_3!_A(0,0,1) = 0 fork_3!_A(0,1,0) = 0 fork_3!_A(0,1,1) = 0 fork_3!_A(1,0,0) = 0 fork_3!_A(1,0,1) = 0 fork_3!_A(1,1,0) = 0 fork_3!_A(1,1,1) = 1 app!_A(0,0) = 1 app!_A(0,1) = 0 app!_A(1,0) = 1 app!_A(1,1) = 1 eq_0!_A = 1 eq_1!_A(0) = 0 eq_1!_A(1) = 0 eq_2!_A(0,0) = 1 eq_2!_A(0,1) = 1 eq_2!_A(1,0) = 1 eq_2!_A(1,1) = 0 fork_0!_A = 0 fork_1!_A(0) = 0 fork_1!_A(1) = 0 fork_2!_A(0,0) = 0 fork_2!_A(0,1) = 0 fork_2!_A(1,0) = 0 fork_2!_A(1,1) = 0 if_0!_A = 0 if_1!_A(0) = 0 if_1!_A(1) = 0 if_2!_A(0,0) = 0 if_2!_A(0,1) = 0 if_2!_A(1,0) = 1 if_2!_A(1,1) = 0 if_3!_A(0,0,0) = 0 if_3!_A(0,0,1) = 0 if_3!_A(0,1,0) = 1 if_3!_A(0,1,1) = 0 if_3!_A(1,0,0) = 1 if_3!_A(1,0,1) = 1 if_3!_A(1,1,0) = 0 if_3!_A(1,1,1) = 0 lt_0!_A = 1 lt_1!_A(0) = 0 lt_1!_A(1) = 0 lt_2!_A(0,0) = 1 lt_2!_A(0,1) = 1 lt_2!_A(1,0) = 1 lt_2!_A(1,1) = 1 member_0!_A = 0 member_1!_A(0) = 0 member_1!_A(1) = 0 member_2!_A(0,0) = 0 member_2!_A(0,1) = 0 member_2!_A(1,0) = 0 member_2!_A(1,1) = 0 s_0!_A = 1 s_1!_A(0) = 0 s_1!_A(1) = 0 |0|_0!_A = 1 true_0!_A = 0 false_0!_A = 0 null_0!_A = 1 partial status: pi(member_2#) = [2] pi(fork_3) = [1, 3] pi(app) = [1, 2] pi(eq_0) = [] pi(eq_1) = [] pi(eq_2) = [] pi(fork_0) = [] pi(fork_1) = [1] pi(fork_2) = [1, 2] pi(if_0) = [] pi(if_1) = [1] pi(if_2) = [1, 2] pi(if_3) = [2] pi(lt_0) = [] pi(lt_1) = [] pi(lt_2) = [] pi(member_0) = [] pi(member_1) = [] pi(member_2) = [2] pi(s_0) = [] pi(s_1) = [] pi(|0|_0) = [] pi(true_0) = [] pi(false_0) = [] pi(null_0) = [] 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: lt_2#(s_1(x),s_1(y)) -> lt_2#(x,y) and R consists of: r1: app(eq_0(),y) -> eq_1(y) r2: app(eq_1(x1),y) -> eq_2(x1,y) r3: app(fork_0(),y) -> fork_1(y) r4: app(fork_1(x1),y) -> fork_2(x1,y) r5: app(fork_2(x1,x2),y) -> fork_3(x1,x2,y) r6: app(if_0(),y) -> if_1(y) r7: app(if_1(x1),y) -> if_2(x1,y) r8: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r9: app(lt_0(),y) -> lt_1(y) r10: app(lt_1(x1),y) -> lt_2(x1,y) r11: app(member_0(),y) -> member_1(y) r12: app(member_1(x1),y) -> member_2(x1,y) r13: app(s_0(),y) -> s_1(y) r14: lt_2(s_1(x),s_1(y)) -> lt_2(x,y) r15: lt_2(|0|_0(),s_1(y)) -> true_0() r16: lt_2(y,|0|_0()) -> false_0() r17: eq_2(x,x) -> true_0() r18: eq_2(s_1(x),|0|_0()) -> false_0() r19: eq_2(|0|_0(),s_1(x)) -> false_0() r20: member_2(w,null_0()) -> false_0() r21: member_2(w,fork_3(x,y,z)) -> if_3(lt_2(w,y),member_2(w,x),if_3(eq_2(w,y),true_0(),member_2(w,z))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: lt_2#_A(0,0) = 0 lt_2#_A(0,1) = 0 lt_2#_A(1,0) = 0 lt_2#_A(1,1) = 0 s_1_A(0) = 1 s_1_A(1) = 1 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 eq_0_A = 0 eq_1_A(0) = 1 eq_1_A(1) = 1 eq_2_A(0,0) = 0 eq_2_A(0,1) = 0 eq_2_A(1,0) = 0 eq_2_A(1,1) = 0 fork_0_A = 1 fork_1_A(0) = 0 fork_1_A(1) = 0 fork_2_A(0,0) = 1 fork_2_A(0,1) = 1 fork_2_A(1,0) = 1 fork_2_A(1,1) = 1 fork_3_A(0,0,0) = 0 fork_3_A(0,0,1) = 0 fork_3_A(0,1,0) = 0 fork_3_A(0,1,1) = 0 fork_3_A(1,0,0) = 0 fork_3_A(1,0,1) = 0 fork_3_A(1,1,0) = 0 fork_3_A(1,1,1) = 0 if_0_A = 1 if_1_A(0) = 0 if_1_A(1) = 0 if_2_A(0,0) = 1 if_2_A(0,1) = 1 if_2_A(1,0) = 1 if_2_A(1,1) = 1 if_3_A(0,0,0) = 0 if_3_A(0,0,1) = 0 if_3_A(0,1,0) = 0 if_3_A(0,1,1) = 0 if_3_A(1,0,0) = 0 if_3_A(1,0,1) = 0 if_3_A(1,1,0) = 0 if_3_A(1,1,1) = 0 lt_0_A = 0 lt_1_A(0) = 1 lt_1_A(1) = 1 lt_2_A(0,0) = 0 lt_2_A(0,1) = 0 lt_2_A(1,0) = 0 lt_2_A(1,1) = 0 member_0_A = 0 member_1_A(0) = 1 member_1_A(1) = 1 member_2_A(0,0) = 0 member_2_A(0,1) = 0 member_2_A(1,0) = 0 member_2_A(1,1) = 0 s_0_A = 0 |0|_0_A = 0 true_0_A = 0 false_0_A = 0 null_0_A = 0 lt_2#!_A(0,0) = 0 lt_2#!_A(0,1) = 0 lt_2#!_A(1,0) = 0 lt_2#!_A(1,1) = 0 s_1!_A(0) = 0 s_1!_A(1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 eq_0!_A = 1 eq_1!_A(0) = 1 eq_1!_A(1) = 1 eq_2!_A(0,0) = 1 eq_2!_A(0,1) = 1 eq_2!_A(1,0) = 1 eq_2!_A(1,1) = 1 fork_0!_A = 1 fork_1!_A(0) = 0 fork_1!_A(1) = 0 fork_2!_A(0,0) = 0 fork_2!_A(0,1) = 0 fork_2!_A(1,0) = 0 fork_2!_A(1,1) = 0 fork_3!_A(0,0,0) = 0 fork_3!_A(0,0,1) = 0 fork_3!_A(0,1,0) = 0 fork_3!_A(0,1,1) = 0 fork_3!_A(1,0,0) = 0 fork_3!_A(1,0,1) = 0 fork_3!_A(1,1,0) = 0 fork_3!_A(1,1,1) = 0 if_0!_A = 1 if_1!_A(0) = 0 if_1!_A(1) = 0 if_2!_A(0,0) = 0 if_2!_A(0,1) = 0 if_2!_A(1,0) = 0 if_2!_A(1,1) = 0 if_3!_A(0,0,0) = 0 if_3!_A(0,0,1) = 0 if_3!_A(0,1,0) = 0 if_3!_A(0,1,1) = 0 if_3!_A(1,0,0) = 0 if_3!_A(1,0,1) = 0 if_3!_A(1,1,0) = 0 if_3!_A(1,1,1) = 0 lt_0!_A = 0 lt_1!_A(0) = 0 lt_1!_A(1) = 0 lt_2!_A(0,0) = 0 lt_2!_A(0,1) = 0 lt_2!_A(1,0) = 0 lt_2!_A(1,1) = 0 member_0!_A = 0 member_1!_A(0) = 0 member_1!_A(1) = 0 member_2!_A(0,0) = 0 member_2!_A(0,1) = 0 member_2!_A(1,0) = 0 member_2!_A(1,1) = 0 s_0!_A = 0 |0|_0!_A = 1 true_0!_A = 0 false_0!_A = 0 null_0!_A = 1 partial status: pi(lt_2#) = [2] pi(s_1) = [1] pi(app) = [1, 2] pi(eq_0) = [] pi(eq_1) = [] pi(eq_2) = [] pi(fork_0) = [] pi(fork_1) = [] pi(fork_2) = [2] pi(fork_3) = [2] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [2] pi(if_3) = [] pi(lt_0) = [] pi(lt_1) = [1] pi(lt_2) = [1] pi(member_0) = [] pi(member_1) = [1] pi(member_2) = [1] pi(s_0) = [] pi(|0|_0) = [] pi(true_0) = [] pi(false_0) = [] pi(null_0) = [] The following rules are removed: p1 Then no dependency pair remains.