YES We show the termination of the TRS R: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt(),P) -> U72(isPal(activate(P))) U72(tt()) -> tt() U81(tt()) -> tt() isList(V) -> U11(isNeList(activate(V))) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__o()) -> o() activate(n__u()) -> u() activate(X) -> X -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) p2: __#(__(X,Y),Z) -> __#(Y,Z) p3: U21#(tt(),V2) -> U22#(isList(activate(V2))) p4: U21#(tt(),V2) -> isList#(activate(V2)) p5: U21#(tt(),V2) -> activate#(V2) p6: U41#(tt(),V2) -> U42#(isNeList(activate(V2))) p7: U41#(tt(),V2) -> isNeList#(activate(V2)) p8: U41#(tt(),V2) -> activate#(V2) p9: U51#(tt(),V2) -> U52#(isList(activate(V2))) p10: U51#(tt(),V2) -> isList#(activate(V2)) p11: U51#(tt(),V2) -> activate#(V2) p12: U71#(tt(),P) -> U72#(isPal(activate(P))) p13: U71#(tt(),P) -> isPal#(activate(P)) p14: U71#(tt(),P) -> activate#(P) p15: isList#(V) -> U11#(isNeList(activate(V))) p16: isList#(V) -> isNeList#(activate(V)) p17: isList#(V) -> activate#(V) p18: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p19: isList#(n____(V1,V2)) -> isList#(activate(V1)) p20: isList#(n____(V1,V2)) -> activate#(V1) p21: isList#(n____(V1,V2)) -> activate#(V2) p22: isNeList#(V) -> U31#(isQid(activate(V))) p23: isNeList#(V) -> isQid#(activate(V)) p24: isNeList#(V) -> activate#(V) p25: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p26: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p27: isNeList#(n____(V1,V2)) -> activate#(V1) p28: isNeList#(n____(V1,V2)) -> activate#(V2) p29: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p30: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p31: isNeList#(n____(V1,V2)) -> activate#(V1) p32: isNeList#(n____(V1,V2)) -> activate#(V2) p33: isNePal#(V) -> U61#(isQid(activate(V))) p34: isNePal#(V) -> isQid#(activate(V)) p35: isNePal#(V) -> activate#(V) p36: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) p37: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I)) p38: isNePal#(n____(I,n____(P,I))) -> activate#(I) p39: isNePal#(n____(I,n____(P,I))) -> activate#(P) p40: isPal#(V) -> U81#(isNePal(activate(V))) p41: isPal#(V) -> isNePal#(activate(V)) p42: isPal#(V) -> activate#(V) p43: activate#(n__nil()) -> nil#() p44: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2)) p45: activate#(n____(X1,X2)) -> activate#(X1) p46: activate#(n____(X1,X2)) -> activate#(X2) p47: activate#(n__a()) -> a#() p48: activate#(n__e()) -> e#() p49: activate#(n__i()) -> i#() p50: activate#(n__o()) -> o#() p51: activate#(n__u()) -> u#() and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The estimated dependency graph contains the following SCCs: {p13, p36, p41} {p4, p7, p10, p16, p18, p19, p25, p26, p29, p30} {p45, p46} {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isPal#(V) -> isNePal#(activate(V)) p2: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) p3: U71#(tt(),P) -> isPal#(activate(P)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isPal#_A(x1) = ((0,1),(0,0)) x1 + (3,0) isNePal#_A(x1) = ((0,1),(0,0)) x1 + (2,0) activate_A(x1) = ((1,1),(0,1)) x1 n_____A(x1,x2) = x1 + x2 + (1,0) U71#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 isQid_A(x1) = ((0,1),(0,0)) x1 + (1,1) tt_A() = (4,0) ___A(x1,x2) = x1 + x2 + (1,0) nil_A() = (2,2) n__nil_A() = (1,2) a_A() = (2,4) n__a_A() = (1,4) e_A() = (2,4) n__e_A() = (1,4) i_A() = (2,4) n__i_A() = (1,4) o_A() = (2,4) n__o_A() = (1,4) u_A() = (2,4) n__u_A() = (1,4) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isPal#_A(x1) = (1,0) isNePal#_A(x1) = (2,1) activate_A(x1) = ((1,1),(1,1)) x1 n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (0,1) U71#_A(x1,x2) = x1 + (0,1) isQid_A(x1) = (1,1) tt_A() = (2,2) ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (0,1) nil_A() = (0,1) n__nil_A() = (1,2) a_A() = (1,1) n__a_A() = (0,2) e_A() = (0,0) n__e_A() = (1,1) i_A() = (1,0) n__i_A() = (1,0) o_A() = (0,3) n__o_A() = (1,1) u_A() = (2,2) n__u_A() = (1,0) The next rules are strictly ordered: p1, p2, p3 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) p2: U51#(tt(),V2) -> isList#(activate(V2)) p3: isList#(n____(V1,V2)) -> isList#(activate(V1)) p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) p5: U21#(tt(),V2) -> isList#(activate(V2)) p6: isList#(V) -> isNeList#(activate(V)) p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) p8: isNeList#(n____(V1,V2)) -> isList#(activate(V1)) p9: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p10: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = ((0,1),(0,0)) x1 n_____A(x1,x2) = x1 + x2 + (1,3) U51#_A(x1,x2) = ((0,1),(0,0)) x2 + (1,0) isNeList_A(x1) = x1 + (6,1) activate_A(x1) = ((1,1),(0,1)) x1 + (1,0) tt_A() = (0,1) isList#_A(x1) = ((0,1),(0,0)) x1 + (1,0) U21#_A(x1,x2) = ((0,1),(0,0)) x2 + (2,0) isList_A(x1) = (3,1) U41#_A(x1,x2) = x1 + ((0,1),(0,0)) x2 U22_A(x1) = (1,1) U42_A(x1) = (1,1) U52_A(x1) = x1 + (1,1) ___A(x1,x2) = x1 + x2 + (2,3) nil_A() = (2,1) U11_A(x1) = (1,1) U21_A(x1,x2) = x1 + (2,0) U31_A(x1) = (1,1) U41_A(x1,x2) = (2,1) U51_A(x1,x2) = (5,1) isQid_A(x1) = (1,1) n__a_A() = (1,1) n__e_A() = (1,1) n__i_A() = (1,1) n__o_A() = (1,1) n__u_A() = (1,1) n__nil_A() = (1,1) a_A() = (2,1) e_A() = (2,1) i_A() = (2,1) o_A() = (2,1) u_A() = (2,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = (11,2) n_____A(x1,x2) = ((0,1),(1,1)) x1 + ((0,1),(1,0)) x2 + (1,0) U51#_A(x1,x2) = (11,1) isNeList_A(x1) = (1,1) activate_A(x1) = (1,2) tt_A() = (7,4) isList#_A(x1) = (1,1) U21#_A(x1,x2) = (0,0) isList_A(x1) = (10,1) U41#_A(x1,x2) = ((1,1),(0,1)) x1 + (0,1) U22_A(x1) = (12,3) U42_A(x1) = (3,3) U52_A(x1) = ((0,1),(0,1)) x1 + (2,2) ___A(x1,x2) = ((0,0),(1,0)) x2 + (0,1) nil_A() = (0,3) U11_A(x1) = (0,3) U21_A(x1,x2) = (11,2) U31_A(x1) = (2,2) U41_A(x1,x2) = (2,2) U51_A(x1,x2) = (2,2) isQid_A(x1) = (8,1) n__a_A() = (1,1) n__e_A() = (1,1) n__i_A() = (1,1) n__o_A() = (1,1) n__u_A() = (1,1) n__nil_A() = (1,0) a_A() = (2,3) e_A() = (2,3) i_A() = (2,3) o_A() = (2,3) u_A() = (2,3) The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p2: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) p2: U41#(tt(),V2) -> isNeList#(activate(V2)) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = x1 n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (4,1) U41#_A(x1,x2) = ((0,1),(0,0)) x1 + x2 isList_A(x1) = ((1,1),(1,0)) x1 + (3,1) activate_A(x1) = ((1,0),(1,1)) x1 + (0,1) tt_A() = (1,1) U42_A(x1) = (2,1) U52_A(x1) = (2,1) U22_A(x1) = (2,1) U31_A(x1) = (2,1) U41_A(x1,x2) = ((0,1),(0,0)) x1 + (2,1) isNeList_A(x1) = ((0,1),(0,1)) x1 + (3,1) U51_A(x1,x2) = (3,1) isQid_A(x1) = ((0,1),(0,1)) x1 + (2,1) n__a_A() = (1,1) n__e_A() = (1,0) n__i_A() = (1,0) n__o_A() = (1,1) n__u_A() = (1,0) ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (4,1) nil_A() = (1,1) U11_A(x1) = (2,1) U21_A(x1,x2) = x1 + ((0,1),(0,0)) x2 + (2,1) n__nil_A() = (1,1) a_A() = (1,1) e_A() = (1,0) i_A() = (1,0) o_A() = (1,1) u_A() = (1,0) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: isNeList#_A(x1) = ((0,1),(0,0)) x1 + (4,2) n_____A(x1,x2) = x1 + (1,0) U41#_A(x1,x2) = ((1,1),(1,1)) x2 isList_A(x1) = ((0,0),(1,0)) x1 + (1,0) activate_A(x1) = x1 + (2,1) tt_A() = (6,4) U42_A(x1) = (3,3) U52_A(x1) = (5,3) U22_A(x1) = (5,3) U31_A(x1) = (2,2) U41_A(x1,x2) = (2,2) isNeList_A(x1) = (1,1) U51_A(x1,x2) = (0,2) isQid_A(x1) = (7,1) n__a_A() = (1,1) n__e_A() = (1,1) n__i_A() = (1,1) n__o_A() = (1,1) n__u_A() = (1,1) ___A(x1,x2) = x1 + (2,0) nil_A() = (1,1) U11_A(x1) = (2,1) U21_A(x1,x2) = ((0,1),(0,0)) x1 + (0,2) n__nil_A() = (0,0) a_A() = (2,2) e_A() = (2,2) i_A() = (2,2) o_A() = (2,2) u_A() = (2,2) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: activate#(n____(X1,X2)) -> activate#(X2) p2: activate#(n____(X1,X2)) -> activate#(X1) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: activate#_A(x1) = ((1,1),(1,1)) x1 n_____A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: activate#_A(x1) = ((1,1),(1,0)) x1 n_____A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2 + (1,1) The next rules are strictly ordered: p1, p2 r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) p2: __#(__(X,Y),Z) -> __#(Y,Z) and R consists of: r1: __(__(X,Y),Z) -> __(X,__(Y,Z)) r2: __(X,nil()) -> X r3: __(nil(),X) -> X r4: U11(tt()) -> tt() r5: U21(tt(),V2) -> U22(isList(activate(V2))) r6: U22(tt()) -> tt() r7: U31(tt()) -> tt() r8: U41(tt(),V2) -> U42(isNeList(activate(V2))) r9: U42(tt()) -> tt() r10: U51(tt(),V2) -> U52(isList(activate(V2))) r11: U52(tt()) -> tt() r12: U61(tt()) -> tt() r13: U71(tt(),P) -> U72(isPal(activate(P))) r14: U72(tt()) -> tt() r15: U81(tt()) -> tt() r16: isList(V) -> U11(isNeList(activate(V))) r17: isList(n__nil()) -> tt() r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) r19: isNeList(V) -> U31(isQid(activate(V))) r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) r22: isNePal(V) -> U61(isQid(activate(V))) r23: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(P)) r24: isPal(V) -> U81(isNePal(activate(V))) r25: isPal(n__nil()) -> tt() r26: isQid(n__a()) -> tt() r27: isQid(n__e()) -> tt() r28: isQid(n__i()) -> tt() r29: isQid(n__o()) -> tt() r30: isQid(n__u()) -> tt() r31: nil() -> n__nil() r32: __(X1,X2) -> n____(X1,X2) r33: a() -> n__a() r34: e() -> n__e() r35: i() -> n__i() r36: o() -> n__o() r37: u() -> n__u() r38: activate(n__nil()) -> nil() r39: activate(n____(X1,X2)) -> __(activate(X1),activate(X2)) r40: activate(n__a()) -> a() r41: activate(n__e()) -> e() r42: activate(n__i()) -> i() r43: activate(n__o()) -> o() r44: activate(n__u()) -> u() r45: activate(X) -> X The set of usable rules consists of r1, r2, r3, r32 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^2 order: standard order interpretations: __#_A(x1,x2) = ((1,1),(1,1)) x1 + x2 ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1) nil_A() = (1,1) n_____A(x1,x2) = (0,0) 2. matrix interpretations: carrier: N^2 order: standard order interpretations: __#_A(x1,x2) = ((0,1),(0,1)) x1 + ((1,0),(1,1)) x2 ___A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(0,0)) x2 + (1,2) nil_A() = (1,1) n_____A(x1,x2) = (2,3) The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains.