YES We show the termination of the TRS R: app(app(mapt(),f),app(leaf(),x)) -> app(leaf(),app(f,x)) app(app(mapt(),f),app(node(),xs)) -> app(node(),app(app(maptlist(),f),xs)) app(app(maptlist(),f),nil()) -> nil() app(app(maptlist(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(app(mapt(),f),x)),app(app(maptlist(),f),xs)) Instead we prove termination of the uncurried system: app(cons_0(),y) -> cons_1(y) app(cons_1(x1),y) -> cons_2(x1,y) app(leaf_0(),y) -> leaf_1(y) app(mapt_0(),y) -> mapt_1(y) app(mapt_1(x1),y) -> mapt_2(x1,y) app(maptlist_0(),y) -> maptlist_1(y) app(maptlist_1(x1),y) -> maptlist_2(x1,y) app(node_0(),y) -> node_1(y) mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) maptlist_2(f,nil_0()) -> nil_0() maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) p3: mapt_2#(f,leaf_1(x)) -> app#(f,x) p4: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p5: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p6: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(mapt_1(x1),y) -> mapt_2#(x1,y) p2: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p4: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p5: mapt_2#(f,leaf_1(x)) -> app#(f,x) p6: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12 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: app#_A(0,0) = 0 app#_A(0,1) = 0 app#_A(1,0) = 0 app#_A(1,1) = 0 mapt_1_A(0) = 1 mapt_1_A(1) = 1 mapt_2#_A(0,0) = 0 mapt_2#_A(0,1) = 0 mapt_2#_A(1,0) = 0 mapt_2#_A(1,1) = 0 node_1_A(0) = 0 node_1_A(1) = 0 maptlist_2#_A(0,0) = 0 maptlist_2#_A(0,1) = 0 maptlist_2#_A(1,0) = 0 maptlist_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 0 cons_2_A(1,0) = 0 cons_2_A(1,1) = 0 leaf_1_A(0) = 0 leaf_1_A(1) = 0 maptlist_1_A(0) = 1 maptlist_1_A(1) = 1 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 leaf_0_A = 1 mapt_0_A = 0 mapt_2_A(0,0) = 0 mapt_2_A(0,1) = 0 mapt_2_A(1,0) = 0 mapt_2_A(1,1) = 0 maptlist_0_A = 0 maptlist_2_A(0,0) = 0 maptlist_2_A(0,1) = 0 maptlist_2_A(1,0) = 0 maptlist_2_A(1,1) = 0 node_0_A = 1 nil_0_A = 0 app#!_A(0,0) = 0 app#!_A(0,1) = 0 app#!_A(1,0) = 0 app#!_A(1,1) = 0 mapt_1!_A(0) = 0 mapt_1!_A(1) = 1 mapt_2#!_A(0,0) = 0 mapt_2#!_A(0,1) = 0 mapt_2#!_A(1,0) = 0 mapt_2#!_A(1,1) = 0 node_1!_A(0) = 0 node_1!_A(1) = 1 maptlist_2#!_A(0,0) = 0 maptlist_2#!_A(0,1) = 0 maptlist_2#!_A(1,0) = 0 maptlist_2#!_A(1,1) = 0 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 maptlist_1!_A(0) = 0 maptlist_1!_A(1) = 1 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 0 app!_A(1,1) = 1 cons_0!_A = 1 cons_1!_A(0) = 0 cons_1!_A(1) = 0 leaf_0!_A = 1 mapt_0!_A = 1 mapt_2!_A(0,0) = 0 mapt_2!_A(0,1) = 0 mapt_2!_A(1,0) = 0 mapt_2!_A(1,1) = 1 maptlist_0!_A = 1 maptlist_2!_A(0,0) = 0 maptlist_2!_A(0,1) = 0 maptlist_2!_A(1,0) = 0 maptlist_2!_A(1,1) = 0 node_0!_A = 0 nil_0!_A = 0 partial status: pi(app#) = [1] pi(mapt_1) = [1] pi(mapt_2#) = [1] pi(node_1) = [] pi(maptlist_2#) = [1] pi(cons_2) = [2] pi(leaf_1) = [] pi(maptlist_1) = [1] pi(app) = [2] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(mapt_0) = [] pi(mapt_2) = [] pi(maptlist_0) = [] pi(maptlist_2) = [2] pi(node_0) = [] pi(nil_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p4: mapt_2#(f,leaf_1(x)) -> app#(f,x) p5: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p3: mapt_2#(f,leaf_1(x)) -> app#(f,x) p4: app#(maptlist_1(x1),y) -> maptlist_2#(x1,y) p5: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12 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: mapt_2#_A(0,0) = 0 mapt_2#_A(0,1) = 0 mapt_2#_A(1,0) = 0 mapt_2#_A(1,1) = 0 node_1_A(0) = 0 node_1_A(1) = 0 maptlist_2#_A(0,0) = 0 maptlist_2#_A(0,1) = 0 maptlist_2#_A(1,0) = 0 maptlist_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 0 cons_2_A(1,0) = 0 cons_2_A(1,1) = 0 leaf_1_A(0) = 0 leaf_1_A(1) = 0 app#_A(0,0) = 0 app#_A(0,1) = 0 app#_A(1,0) = 0 app#_A(1,1) = 0 maptlist_1_A(0) = 1 maptlist_1_A(1) = 1 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 leaf_0_A = 1 mapt_0_A = 0 mapt_1_A(0) = 1 mapt_1_A(1) = 1 mapt_2_A(0,0) = 0 mapt_2_A(0,1) = 0 mapt_2_A(1,0) = 0 mapt_2_A(1,1) = 0 maptlist_0_A = 0 maptlist_2_A(0,0) = 0 maptlist_2_A(0,1) = 0 maptlist_2_A(1,0) = 0 maptlist_2_A(1,1) = 0 node_0_A = 1 nil_0_A = 0 mapt_2#!_A(0,0) = 1 mapt_2#!_A(0,1) = 0 mapt_2#!_A(1,0) = 1 mapt_2#!_A(1,1) = 1 node_1!_A(0) = 0 node_1!_A(1) = 0 maptlist_2#!_A(0,0) = 1 maptlist_2#!_A(0,1) = 1 maptlist_2#!_A(1,0) = 1 maptlist_2#!_A(1,1) = 1 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 app#!_A(0,0) = 0 app#!_A(0,1) = 1 app#!_A(1,0) = 1 app#!_A(1,1) = 0 maptlist_1!_A(0) = 1 maptlist_1!_A(1) = 1 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 cons_0!_A = 1 cons_1!_A(0) = 0 cons_1!_A(1) = 0 leaf_0!_A = 1 mapt_0!_A = 1 mapt_1!_A(0) = 0 mapt_1!_A(1) = 0 mapt_2!_A(0,0) = 1 mapt_2!_A(0,1) = 1 mapt_2!_A(1,0) = 0 mapt_2!_A(1,1) = 0 maptlist_0!_A = 1 maptlist_2!_A(0,0) = 0 maptlist_2!_A(0,1) = 0 maptlist_2!_A(1,0) = 0 maptlist_2!_A(1,1) = 0 node_0!_A = 1 nil_0!_A = 0 partial status: pi(mapt_2#) = [1] pi(node_1) = [] pi(maptlist_2#) = [1] pi(cons_2) = [] pi(leaf_1) = [] pi(app#) = [1] pi(maptlist_1) = [1] pi(app) = [2] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(mapt_0) = [] pi(mapt_1) = [] pi(mapt_2) = [2] pi(maptlist_0) = [] pi(maptlist_2) = [] pi(node_0) = [] pi(nil_0) = [] The following rules are removed: p4 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) p3: mapt_2#(f,leaf_1(x)) -> app#(f,x) p4: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1, p2, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: mapt_2#(f,node_1(xs)) -> maptlist_2#(f,xs) p2: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) p3: maptlist_2#(f,cons_2(x,xs)) -> mapt_2#(f,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12 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: mapt_2#_A(0,0) = 0 mapt_2#_A(0,1) = 0 mapt_2#_A(1,0) = 0 mapt_2#_A(1,1) = 0 node_1_A(0) = 0 node_1_A(1) = 0 maptlist_2#_A(0,0) = 0 maptlist_2#_A(0,1) = 0 maptlist_2#_A(1,0) = 0 maptlist_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 0 cons_2_A(1,0) = 0 cons_2_A(1,1) = 0 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 leaf_0_A = 1 leaf_1_A(0) = 0 leaf_1_A(1) = 0 mapt_0_A = 0 mapt_1_A(0) = 1 mapt_1_A(1) = 1 mapt_2_A(0,0) = 0 mapt_2_A(0,1) = 0 mapt_2_A(1,0) = 0 mapt_2_A(1,1) = 0 maptlist_0_A = 0 maptlist_1_A(0) = 1 maptlist_1_A(1) = 1 maptlist_2_A(0,0) = 0 maptlist_2_A(0,1) = 0 maptlist_2_A(1,0) = 0 maptlist_2_A(1,1) = 0 node_0_A = 1 nil_0_A = 0 mapt_2#!_A(0,0) = 0 mapt_2#!_A(0,1) = 0 mapt_2#!_A(1,0) = 0 mapt_2#!_A(1,1) = 0 node_1!_A(0) = 0 node_1!_A(1) = 0 maptlist_2#!_A(0,0) = 0 maptlist_2#!_A(0,1) = 0 maptlist_2#!_A(1,0) = 0 maptlist_2#!_A(1,1) = 0 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 1 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 cons_0!_A = 0 cons_1!_A(0) = 0 cons_1!_A(1) = 0 leaf_0!_A = 1 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 mapt_0!_A = 1 mapt_1!_A(0) = 0 mapt_1!_A(1) = 0 mapt_2!_A(0,0) = 0 mapt_2!_A(0,1) = 0 mapt_2!_A(1,0) = 0 mapt_2!_A(1,1) = 0 maptlist_0!_A = 0 maptlist_1!_A(0) = 0 maptlist_1!_A(1) = 0 maptlist_2!_A(0,0) = 0 maptlist_2!_A(0,1) = 0 maptlist_2!_A(1,0) = 0 maptlist_2!_A(1,1) = 0 node_0!_A = 0 nil_0!_A = 1 partial status: pi(mapt_2#) = [2] pi(node_1) = [1] pi(maptlist_2#) = [2] pi(cons_2) = [1, 2] pi(app) = [1, 2] pi(cons_0) = [] pi(cons_1) = [1] pi(leaf_0) = [] pi(leaf_1) = [] pi(mapt_0) = [] pi(mapt_1) = [] pi(mapt_2) = [2] pi(maptlist_0) = [] pi(maptlist_1) = [] pi(maptlist_2) = [2] pi(node_0) = [] pi(nil_0) = [] The following rules are removed: p1, p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: maptlist_2#(f,cons_2(x,xs)) -> maptlist_2#(f,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(leaf_0(),y) -> leaf_1(y) r4: app(mapt_0(),y) -> mapt_1(y) r5: app(mapt_1(x1),y) -> mapt_2(x1,y) r6: app(maptlist_0(),y) -> maptlist_1(y) r7: app(maptlist_1(x1),y) -> maptlist_2(x1,y) r8: app(node_0(),y) -> node_1(y) r9: mapt_2(f,leaf_1(x)) -> leaf_1(app(f,x)) r10: mapt_2(f,node_1(xs)) -> node_1(maptlist_2(f,xs)) r11: maptlist_2(f,nil_0()) -> nil_0() r12: maptlist_2(f,cons_2(x,xs)) -> cons_2(mapt_2(f,x),maptlist_2(f,xs)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12 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: maptlist_2#_A(0,0) = 0 maptlist_2#_A(0,1) = 0 maptlist_2#_A(1,0) = 0 maptlist_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 0 cons_2_A(1,0) = 0 cons_2_A(1,1) = 0 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 leaf_0_A = 1 leaf_1_A(0) = 0 leaf_1_A(1) = 0 mapt_0_A = 0 mapt_1_A(0) = 1 mapt_1_A(1) = 1 mapt_2_A(0,0) = 0 mapt_2_A(0,1) = 0 mapt_2_A(1,0) = 0 mapt_2_A(1,1) = 0 maptlist_0_A = 0 maptlist_1_A(0) = 1 maptlist_1_A(1) = 1 maptlist_2_A(0,0) = 0 maptlist_2_A(0,1) = 0 maptlist_2_A(1,0) = 0 maptlist_2_A(1,1) = 0 node_0_A = 1 node_1_A(0) = 0 node_1_A(1) = 0 nil_0_A = 0 maptlist_2#!_A(0,0) = 0 maptlist_2#!_A(0,1) = 0 maptlist_2#!_A(1,0) = 0 maptlist_2#!_A(1,1) = 0 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 1 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 1 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 0 app!_A(1,1) = 1 cons_0!_A = 1 cons_1!_A(0) = 1 cons_1!_A(1) = 1 leaf_0!_A = 1 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 mapt_0!_A = 0 mapt_1!_A(0) = 0 mapt_1!_A(1) = 0 mapt_2!_A(0,0) = 0 mapt_2!_A(0,1) = 0 mapt_2!_A(1,0) = 0 mapt_2!_A(1,1) = 0 maptlist_0!_A = 1 maptlist_1!_A(0) = 0 maptlist_1!_A(1) = 0 maptlist_2!_A(0,0) = 0 maptlist_2!_A(0,1) = 1 maptlist_2!_A(1,0) = 0 maptlist_2!_A(1,1) = 1 node_0!_A = 1 node_1!_A(0) = 0 node_1!_A(1) = 0 nil_0!_A = 0 partial status: pi(maptlist_2#) = [2] pi(cons_2) = [2] pi(app) = [2] pi(cons_0) = [] pi(cons_1) = [] pi(leaf_0) = [] pi(leaf_1) = [] pi(mapt_0) = [] pi(mapt_1) = [1] pi(mapt_2) = [] pi(maptlist_0) = [] pi(maptlist_1) = [1] pi(maptlist_2) = [2] pi(node_0) = [] pi(node_1) = [] pi(nil_0) = [] The following rules are removed: p1 Then no dependency pair remains.