YES We show the termination of the TRS R: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) active(__(X,nil())) -> mark(X) active(__(nil(),X)) -> mark(X) active(and(tt(),X)) -> mark(X) active(isList(V)) -> mark(isNeList(V)) active(isList(nil())) -> mark(tt()) active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) active(isNeList(V)) -> mark(isQid(V)) active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) active(isNePal(V)) -> mark(isQid(V)) active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) active(isPal(V)) -> mark(isNePal(V)) active(isPal(nil())) -> mark(tt()) active(isQid(a())) -> mark(tt()) active(isQid(e())) -> mark(tt()) active(isQid(i())) -> mark(tt()) active(isQid(o())) -> mark(tt()) active(isQid(u())) -> mark(tt()) active(__(X1,X2)) -> __(active(X1),X2) active(__(X1,X2)) -> __(X1,active(X2)) active(and(X1,X2)) -> and(active(X1),X2) __(mark(X1),X2) -> mark(__(X1,X2)) __(X1,mark(X2)) -> mark(__(X1,X2)) and(mark(X1),X2) -> mark(and(X1,X2)) proper(__(X1,X2)) -> __(proper(X1),proper(X2)) proper(nil()) -> ok(nil()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(isList(X)) -> isList(proper(X)) proper(isNeList(X)) -> isNeList(proper(X)) proper(isQid(X)) -> isQid(proper(X)) proper(isNePal(X)) -> isNePal(proper(X)) proper(isPal(X)) -> isPal(proper(X)) proper(a()) -> ok(a()) proper(e()) -> ok(e()) proper(i()) -> ok(i()) proper(o()) -> ok(o()) proper(u()) -> ok(u()) __(ok(X1),ok(X2)) -> ok(__(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) isList(ok(X)) -> ok(isList(X)) isNeList(ok(X)) -> ok(isNeList(X)) isQid(ok(X)) -> ok(isQid(X)) isNePal(ok(X)) -> ok(isNePal(X)) isPal(ok(X)) -> ok(isPal(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z)) p2: active#(__(__(X,Y),Z)) -> __#(Y,Z) p3: active#(isList(V)) -> isNeList#(V) p4: active#(isList(__(V1,V2))) -> and#(isList(V1),isList(V2)) p5: active#(isList(__(V1,V2))) -> isList#(V1) p6: active#(isList(__(V1,V2))) -> isList#(V2) p7: active#(isNeList(V)) -> isQid#(V) p8: active#(isNeList(__(V1,V2))) -> and#(isList(V1),isNeList(V2)) p9: active#(isNeList(__(V1,V2))) -> isList#(V1) p10: active#(isNeList(__(V1,V2))) -> isNeList#(V2) p11: active#(isNeList(__(V1,V2))) -> and#(isNeList(V1),isList(V2)) p12: active#(isNeList(__(V1,V2))) -> isNeList#(V1) p13: active#(isNeList(__(V1,V2))) -> isList#(V2) p14: active#(isNePal(V)) -> isQid#(V) p15: active#(isNePal(__(I,__(P,I)))) -> and#(isQid(I),isPal(P)) p16: active#(isNePal(__(I,__(P,I)))) -> isQid#(I) p17: active#(isNePal(__(I,__(P,I)))) -> isPal#(P) p18: active#(isPal(V)) -> isNePal#(V) p19: active#(__(X1,X2)) -> __#(active(X1),X2) p20: active#(__(X1,X2)) -> active#(X1) p21: active#(__(X1,X2)) -> __#(X1,active(X2)) p22: active#(__(X1,X2)) -> active#(X2) p23: active#(and(X1,X2)) -> and#(active(X1),X2) p24: active#(and(X1,X2)) -> active#(X1) p25: __#(mark(X1),X2) -> __#(X1,X2) p26: __#(X1,mark(X2)) -> __#(X1,X2) p27: and#(mark(X1),X2) -> and#(X1,X2) p28: proper#(__(X1,X2)) -> __#(proper(X1),proper(X2)) p29: proper#(__(X1,X2)) -> proper#(X1) p30: proper#(__(X1,X2)) -> proper#(X2) p31: proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) p32: proper#(and(X1,X2)) -> proper#(X1) p33: proper#(and(X1,X2)) -> proper#(X2) p34: proper#(isList(X)) -> isList#(proper(X)) p35: proper#(isList(X)) -> proper#(X) p36: proper#(isNeList(X)) -> isNeList#(proper(X)) p37: proper#(isNeList(X)) -> proper#(X) p38: proper#(isQid(X)) -> isQid#(proper(X)) p39: proper#(isQid(X)) -> proper#(X) p40: proper#(isNePal(X)) -> isNePal#(proper(X)) p41: proper#(isNePal(X)) -> proper#(X) p42: proper#(isPal(X)) -> isPal#(proper(X)) p43: proper#(isPal(X)) -> proper#(X) p44: __#(ok(X1),ok(X2)) -> __#(X1,X2) p45: and#(ok(X1),ok(X2)) -> and#(X1,X2) p46: isList#(ok(X)) -> isList#(X) p47: isNeList#(ok(X)) -> isNeList#(X) p48: isQid#(ok(X)) -> isQid#(X) p49: isNePal#(ok(X)) -> isNePal#(X) p50: isPal#(ok(X)) -> isPal#(X) p51: top#(mark(X)) -> top#(proper(X)) p52: top#(mark(X)) -> proper#(X) p53: top#(ok(X)) -> top#(active(X)) p54: top#(ok(X)) -> active#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The estimated dependency graph contains the following SCCs: {p51, p53} {p20, p22, p24} {p29, p30, p32, p33, p35, p37, p39, p41, p43} {p25, p26, p44} {p47} {p27, p45} {p46} {p48} {p50} {p49} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: top#(ok(X)) -> top#(active(X)) p2: top#(mark(X)) -> top#(proper(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) 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, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46 Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: top#_A(x1) = ((0,0,0),(1,0,0),(0,1,0)) x1 ok_A(x1) = x1 + (0,0,1) active_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (0,0,1) mark_A(x1) = ((1,0,0),(0,1,0),(0,1,0)) x1 + (0,4,30) proper_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (0,0,1) ___A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(0,1,0),(1,1,1)) x2 + (6,1,1) and_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,0)) x1 + ((1,0,0),(0,0,0),(1,1,0)) x2 + (1,4,31) isList_A(x1) = ((1,0,0),(1,1,0),(1,0,1)) x1 + (4,6,10) isNeList_A(x1) = ((1,0,0),(0,0,0),(1,0,0)) x1 + (3,1,2) isQid_A(x1) = (2,1,31) isNePal_A(x1) = ((1,0,0),(0,0,0),(1,0,0)) x1 + (3,4,2) isPal_A(x1) = x1 + (4,9,2) nil_A() = (1,1,1) tt_A() = (1,6,0) a_A() = (1,1,1) e_A() = (0,1,1) i_A() = (1,1,1) o_A() = (1,1,1) u_A() = (1,1,0) The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: top#(ok(X)) -> top#(active(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: top#(ok(X)) -> top#(active(X)) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) 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, r22, r23, r24, r25, r40, r41, r42, r43, r44, r45, r46 Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: top#_A(x1) = ((1,0,0),(0,1,0),(0,1,1)) x1 ok_A(x1) = x1 + (0,2,1) active_A(x1) = ((1,0,0),(0,1,0),(0,1,1)) x1 + (0,1,1) ___A(x1,x2) = ((1,0,0),(0,1,0),(0,1,0)) x1 + (2,8,1) mark_A(x1) = (2,3,9) and_A(x1,x2) = x1 + x2 + (1,1,1) isList_A(x1) = x1 + (3,2,2) isNeList_A(x1) = ((1,0,0),(0,1,0),(1,1,0)) x1 + (2,3,6) isQid_A(x1) = x1 + (1,0,6) isNePal_A(x1) = ((1,0,0),(0,1,0),(1,0,1)) x1 + (3,1,0) isPal_A(x1) = x1 + (3,0,5) nil_A() = (1,3,1) tt_A() = (1,2,1) a_A() = (1,3,1) e_A() = (1,3,1) i_A() = (2,0,1) o_A() = (1,2,1) u_A() = (1,3,1) The next rules are strictly ordered: p1 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: active#(and(X1,X2)) -> active#(X1) p2: active#(__(X1,X2)) -> active#(X2) p3: active#(__(X1,X2)) -> active#(X1) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: active#_A(x1) = ((1,0,0),(0,0,0),(1,1,0)) x1 and_A(x1,x2) = ((1,0,0),(0,0,0),(1,1,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1) ___A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1) 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: proper#(isPal(X)) -> proper#(X) p2: proper#(isNePal(X)) -> proper#(X) p3: proper#(isQid(X)) -> proper#(X) p4: proper#(isNeList(X)) -> proper#(X) p5: proper#(isList(X)) -> proper#(X) p6: proper#(and(X1,X2)) -> proper#(X2) p7: proper#(and(X1,X2)) -> proper#(X1) p8: proper#(__(X1,X2)) -> proper#(X2) p9: proper#(__(X1,X2)) -> proper#(X1) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: proper#_A(x1) = ((0,0,0),(1,0,0),(1,1,0)) x1 isPal_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) isNePal_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) isQid_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) isNeList_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) isList_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) and_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1) ___A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(0,1,0),(1,1,1)) x2 + (1,1,1) The next rules are strictly ordered: p1, p2, p3, p4, p5, p6, p7, p8, p9 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: __#(mark(X1),X2) -> __#(X1,X2) p2: __#(ok(X1),ok(X2)) -> __#(X1,X2) p3: __#(X1,mark(X2)) -> __#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: __#_A(x1,x2) = ((1,0,0),(1,1,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) ok_A(x1) = ((1,0,0),(1,1,0),(1,1,0)) x1 + (1,1,1) 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#(ok(X)) -> isNeList#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: isNeList#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) The next rules are strictly ordered: p1 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, r46, r47, r48 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: and#(mark(X1),X2) -> and#(X1,X2) p2: and#(ok(X1),ok(X2)) -> and#(X1,X2) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: and#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,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, r46, r47, r48 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: isList#(ok(X)) -> isList#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: isList#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) The next rules are strictly ordered: p1 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, r46, r47, r48 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: isQid#(ok(X)) -> isQid#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: isQid#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) The next rules are strictly ordered: p1 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, r46, r47, r48 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: isPal#(ok(X)) -> isPal#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: isPal#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) The next rules are strictly ordered: p1 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, r46, r47, r48 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: isNePal#(ok(X)) -> isNePal#(X) and R consists of: r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) r2: active(__(X,nil())) -> mark(X) r3: active(__(nil(),X)) -> mark(X) r4: active(and(tt(),X)) -> mark(X) r5: active(isList(V)) -> mark(isNeList(V)) r6: active(isList(nil())) -> mark(tt()) r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) r8: active(isNeList(V)) -> mark(isQid(V)) r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) r11: active(isNePal(V)) -> mark(isQid(V)) r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) r13: active(isPal(V)) -> mark(isNePal(V)) r14: active(isPal(nil())) -> mark(tt()) r15: active(isQid(a())) -> mark(tt()) r16: active(isQid(e())) -> mark(tt()) r17: active(isQid(i())) -> mark(tt()) r18: active(isQid(o())) -> mark(tt()) r19: active(isQid(u())) -> mark(tt()) r20: active(__(X1,X2)) -> __(active(X1),X2) r21: active(__(X1,X2)) -> __(X1,active(X2)) r22: active(and(X1,X2)) -> and(active(X1),X2) r23: __(mark(X1),X2) -> mark(__(X1,X2)) r24: __(X1,mark(X2)) -> mark(__(X1,X2)) r25: and(mark(X1),X2) -> mark(and(X1,X2)) r26: proper(__(X1,X2)) -> __(proper(X1),proper(X2)) r27: proper(nil()) -> ok(nil()) r28: proper(and(X1,X2)) -> and(proper(X1),proper(X2)) r29: proper(tt()) -> ok(tt()) r30: proper(isList(X)) -> isList(proper(X)) r31: proper(isNeList(X)) -> isNeList(proper(X)) r32: proper(isQid(X)) -> isQid(proper(X)) r33: proper(isNePal(X)) -> isNePal(proper(X)) r34: proper(isPal(X)) -> isPal(proper(X)) r35: proper(a()) -> ok(a()) r36: proper(e()) -> ok(e()) r37: proper(i()) -> ok(i()) r38: proper(o()) -> ok(o()) r39: proper(u()) -> ok(u()) r40: __(ok(X1),ok(X2)) -> ok(__(X1,X2)) r41: and(ok(X1),ok(X2)) -> ok(and(X1,X2)) r42: isList(ok(X)) -> ok(isList(X)) r43: isNeList(ok(X)) -> ok(isNeList(X)) r44: isQid(ok(X)) -> ok(isQid(X)) r45: isNePal(ok(X)) -> ok(isNePal(X)) r46: isPal(ok(X)) -> ok(isPal(X)) r47: top(mark(X)) -> top(proper(X)) r48: top(ok(X)) -> top(active(X)) The set of usable rules consists of (no rules) Take the monotone reduction pair: matrix interpretations: carrier: N^3 order: lexicographic order interpretations: isNePal#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1) The next rules are strictly ordered: p1 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, r46, r47, r48 We remove them from the problem. Then no dependency pair remains.