MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1} / {__/2,a/0,and/2,e/0 ,i/0,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____,a__and,a__isList,a__isNeList,a__isNePal,a__isPal ,a__isQid,mark} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a____#(X,nil()) -> c_1(mark#(X)) a____#(X1,X2) -> c_2() a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(X1,X2) -> c_5() a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(X) -> c_8() a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isList#(nil()) -> c_10() a__isNeList#(V) -> c_11(a__isQid#(V)) a__isNeList#(X) -> c_12() a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(V) -> c_15(a__isQid#(V)) a__isNePal#(X) -> c_16() a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) a__isPal#(V) -> c_18(a__isNePal#(V)) a__isPal#(X) -> c_19() a__isPal#(nil()) -> c_20() a__isQid#(X) -> c_21() a__isQid#(a()) -> c_22() a__isQid#(e()) -> c_23() a__isQid#(i()) -> c_24() a__isQid#(o()) -> c_25() a__isQid#(u()) -> c_26() mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(a()) -> c_28() mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(e()) -> c_30() mark#(i()) -> c_31() mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) mark#(isQid(X)) -> c_36(a__isQid#(X)) mark#(nil()) -> c_37() mark#(o()) -> c_38() mark#(tt()) -> c_39() mark#(u()) -> c_40() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(X1,X2) -> c_2() a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(X1,X2) -> c_5() a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(X) -> c_8() a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isList#(nil()) -> c_10() a__isNeList#(V) -> c_11(a__isQid#(V)) a__isNeList#(X) -> c_12() a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(V) -> c_15(a__isQid#(V)) a__isNePal#(X) -> c_16() a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) a__isPal#(V) -> c_18(a__isNePal#(V)) a__isPal#(X) -> c_19() a__isPal#(nil()) -> c_20() a__isQid#(X) -> c_21() a__isQid#(a()) -> c_22() a__isQid#(e()) -> c_23() a__isQid#(i()) -> c_24() a__isQid#(o()) -> c_25() a__isQid#(u()) -> c_26() mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(a()) -> c_28() mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(e()) -> c_30() mark#(i()) -> c_31() mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) mark#(isQid(X)) -> c_36(a__isQid#(X)) mark#(nil()) -> c_37() mark#(o()) -> c_38() mark#(tt()) -> c_39() mark#(u()) -> c_40() - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,5,8,10,12,16,19,20,21,22,23,24,25,26,28,30,31,37,38,39,40} by application of Pre({2,5,8,10,12,16,19,20,21,22,23,24,25,26,28,30,31,37,38,39,40}) = {1,3,4,6,7,9,11,13,14,15,17,18,27,29 ,32,33,34,35,36}. Here rules are labelled as follows: 1: a____#(X,nil()) -> c_1(mark#(X)) 2: a____#(X1,X2) -> c_2() 3: a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) 4: a____#(nil(),X) -> c_4(mark#(X)) 5: a__and#(X1,X2) -> c_5() 6: a__and#(tt(),X) -> c_6(mark#(X)) 7: a__isList#(V) -> c_7(a__isNeList#(V)) 8: a__isList#(X) -> c_8() 9: a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) 10: a__isList#(nil()) -> c_10() 11: a__isNeList#(V) -> c_11(a__isQid#(V)) 12: a__isNeList#(X) -> c_12() 13: a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) 14: a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) 15: a__isNePal#(V) -> c_15(a__isQid#(V)) 16: a__isNePal#(X) -> c_16() 17: a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) 18: a__isPal#(V) -> c_18(a__isNePal#(V)) 19: a__isPal#(X) -> c_19() 20: a__isPal#(nil()) -> c_20() 21: a__isQid#(X) -> c_21() 22: a__isQid#(a()) -> c_22() 23: a__isQid#(e()) -> c_23() 24: a__isQid#(i()) -> c_24() 25: a__isQid#(o()) -> c_25() 26: a__isQid#(u()) -> c_26() 27: mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 28: mark#(a()) -> c_28() 29: mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) 30: mark#(e()) -> c_30() 31: mark#(i()) -> c_31() 32: mark#(isList(X)) -> c_32(a__isList#(X)) 33: mark#(isNeList(X)) -> c_33(a__isNeList#(X)) 34: mark#(isNePal(X)) -> c_34(a__isNePal#(X)) 35: mark#(isPal(X)) -> c_35(a__isPal#(X)) 36: mark#(isQid(X)) -> c_36(a__isQid#(X)) 37: mark#(nil()) -> c_37() 38: mark#(o()) -> c_38() 39: mark#(tt()) -> c_39() 40: mark#(u()) -> c_40() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(V) -> c_11(a__isQid#(V)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(V) -> c_15(a__isQid#(V)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) mark#(isQid(X)) -> c_36(a__isQid#(X)) - Weak DPs: a____#(X1,X2) -> c_2() a__and#(X1,X2) -> c_5() a__isList#(X) -> c_8() a__isList#(nil()) -> c_10() a__isNeList#(X) -> c_12() a__isNePal#(X) -> c_16() a__isPal#(X) -> c_19() a__isPal#(nil()) -> c_20() a__isQid#(X) -> c_21() a__isQid#(a()) -> c_22() a__isQid#(e()) -> c_23() a__isQid#(i()) -> c_24() a__isQid#(o()) -> c_25() a__isQid#(u()) -> c_26() mark#(a()) -> c_28() mark#(e()) -> c_30() mark#(i()) -> c_31() mark#(nil()) -> c_37() mark#(o()) -> c_38() mark#(tt()) -> c_39() mark#(u()) -> c_40() - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {7,10,19} by application of Pre({7,10,19}) = {1,2,3,4,5,9,12,13,14,16,17}. Here rules are labelled as follows: 1: a____#(X,nil()) -> c_1(mark#(X)) 2: a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) 3: a____#(nil(),X) -> c_4(mark#(X)) 4: a__and#(tt(),X) -> c_6(mark#(X)) 5: a__isList#(V) -> c_7(a__isNeList#(V)) 6: a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) 7: a__isNeList#(V) -> c_11(a__isQid#(V)) 8: a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) 9: a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) 10: a__isNePal#(V) -> c_15(a__isQid#(V)) 11: a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) 12: a__isPal#(V) -> c_18(a__isNePal#(V)) 13: mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 14: mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) 15: mark#(isList(X)) -> c_32(a__isList#(X)) 16: mark#(isNeList(X)) -> c_33(a__isNeList#(X)) 17: mark#(isNePal(X)) -> c_34(a__isNePal#(X)) 18: mark#(isPal(X)) -> c_35(a__isPal#(X)) 19: mark#(isQid(X)) -> c_36(a__isQid#(X)) 20: a____#(X1,X2) -> c_2() 21: a__and#(X1,X2) -> c_5() 22: a__isList#(X) -> c_8() 23: a__isList#(nil()) -> c_10() 24: a__isNeList#(X) -> c_12() 25: a__isNePal#(X) -> c_16() 26: a__isPal#(X) -> c_19() 27: a__isPal#(nil()) -> c_20() 28: a__isQid#(X) -> c_21() 29: a__isQid#(a()) -> c_22() 30: a__isQid#(e()) -> c_23() 31: a__isQid#(i()) -> c_24() 32: a__isQid#(o()) -> c_25() 33: a__isQid#(u()) -> c_26() 34: mark#(a()) -> c_28() 35: mark#(e()) -> c_30() 36: mark#(i()) -> c_31() 37: mark#(nil()) -> c_37() 38: mark#(o()) -> c_38() 39: mark#(tt()) -> c_39() 40: mark#(u()) -> c_40() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) - Weak DPs: a____#(X1,X2) -> c_2() a__and#(X1,X2) -> c_5() a__isList#(X) -> c_8() a__isList#(nil()) -> c_10() a__isNeList#(V) -> c_11(a__isQid#(V)) a__isNeList#(X) -> c_12() a__isNePal#(V) -> c_15(a__isQid#(V)) a__isNePal#(X) -> c_16() a__isPal#(X) -> c_19() a__isPal#(nil()) -> c_20() a__isQid#(X) -> c_21() a__isQid#(a()) -> c_22() a__isQid#(e()) -> c_23() a__isQid#(i()) -> c_24() a__isQid#(o()) -> c_25() a__isQid#(u()) -> c_26() mark#(a()) -> c_28() mark#(e()) -> c_30() mark#(i()) -> c_31() mark#(isQid(X)) -> c_36(a__isQid#(X)) mark#(nil()) -> c_37() mark#(o()) -> c_38() mark#(tt()) -> c_39() mark#(u()) -> c_40() - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a____#(X,nil()) -> c_1(mark#(X)) -->_1 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 mark#(u()) -> c_40():40 -->_1 mark#(tt()) -> c_39():39 -->_1 mark#(o()) -> c_38():38 -->_1 mark#(nil()) -> c_37():37 -->_1 mark#(i()) -> c_31():35 -->_1 mark#(e()) -> c_30():34 -->_1 mark#(a()) -> c_28():33 2:S:a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) -->_5 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_4 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_2 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_5 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_4 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_5 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_4 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_5 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_4 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_5 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_4 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_5 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_4 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_5 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_4 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_3 a____#(nil(),X) -> c_4(mark#(X)):3 -->_1 a____#(nil(),X) -> c_4(mark#(X)):3 -->_5 mark#(u()) -> c_40():40 -->_4 mark#(u()) -> c_40():40 -->_2 mark#(u()) -> c_40():40 -->_5 mark#(tt()) -> c_39():39 -->_4 mark#(tt()) -> c_39():39 -->_2 mark#(tt()) -> c_39():39 -->_5 mark#(o()) -> c_38():38 -->_4 mark#(o()) -> c_38():38 -->_2 mark#(o()) -> c_38():38 -->_5 mark#(nil()) -> c_37():37 -->_4 mark#(nil()) -> c_37():37 -->_2 mark#(nil()) -> c_37():37 -->_5 mark#(i()) -> c_31():35 -->_4 mark#(i()) -> c_31():35 -->_2 mark#(i()) -> c_31():35 -->_5 mark#(e()) -> c_30():34 -->_4 mark#(e()) -> c_30():34 -->_2 mark#(e()) -> c_30():34 -->_5 mark#(a()) -> c_28():33 -->_4 mark#(a()) -> c_28():33 -->_2 mark#(a()) -> c_28():33 -->_3 a____#(X1,X2) -> c_2():17 -->_1 a____#(X1,X2) -> c_2():17 -->_3 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_1 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_3 a____#(X,nil()) -> c_1(mark#(X)):1 -->_1 a____#(X,nil()) -> c_1(mark#(X)):1 3:S:a____#(nil(),X) -> c_4(mark#(X)) -->_1 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 mark#(u()) -> c_40():40 -->_1 mark#(tt()) -> c_39():39 -->_1 mark#(o()) -> c_38():38 -->_1 mark#(nil()) -> c_37():37 -->_1 mark#(i()) -> c_31():35 -->_1 mark#(e()) -> c_30():34 -->_1 mark#(a()) -> c_28():33 4:S:a__and#(tt(),X) -> c_6(mark#(X)) -->_1 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 mark#(u()) -> c_40():40 -->_1 mark#(tt()) -> c_39():39 -->_1 mark#(o()) -> c_38():38 -->_1 mark#(nil()) -> c_37():37 -->_1 mark#(i()) -> c_31():35 -->_1 mark#(e()) -> c_30():34 -->_1 mark#(a()) -> c_28():33 5:S:a__isList#(V) -> c_7(a__isNeList#(V)) -->_1 a__isNeList#(V) -> c_11(a__isQid#(V)):21 -->_1 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_1 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 -->_1 a__isNeList#(X) -> c_12():22 6:S:a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) -->_2 a__isList#(nil()) -> c_10():20 -->_2 a__isList#(X) -> c_8():19 -->_1 a__and#(X1,X2) -> c_5():18 -->_2 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_2 a__isList#(V) -> c_7(a__isNeList#(V)):5 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 7:S:a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) -->_2 a__isList#(nil()) -> c_10():20 -->_2 a__isList#(X) -> c_8():19 -->_1 a__and#(X1,X2) -> c_5():18 -->_2 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_2 a__isList#(V) -> c_7(a__isNeList#(V)):5 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 8:S:a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) -->_2 a__isNeList#(V) -> c_11(a__isQid#(V)):21 -->_2 a__isNeList#(X) -> c_12():22 -->_1 a__and#(X1,X2) -> c_5():18 -->_2 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_2 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 9:S:a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) -->_2 a__isQid#(u()) -> c_26():32 -->_2 a__isQid#(o()) -> c_25():31 -->_2 a__isQid#(i()) -> c_24():30 -->_2 a__isQid#(e()) -> c_23():29 -->_2 a__isQid#(a()) -> c_22():28 -->_2 a__isQid#(X) -> c_21():27 -->_1 a__and#(X1,X2) -> c_5():18 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 10:S:a__isPal#(V) -> c_18(a__isNePal#(V)) -->_1 a__isNePal#(V) -> c_15(a__isQid#(V)):23 -->_1 a__isNePal#(X) -> c_16():24 -->_1 a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)):9 11:S:mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_2 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_3 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_3 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_3 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_3 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_3 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_3 mark#(u()) -> c_40():40 -->_2 mark#(u()) -> c_40():40 -->_3 mark#(tt()) -> c_39():39 -->_2 mark#(tt()) -> c_39():39 -->_3 mark#(o()) -> c_38():38 -->_2 mark#(o()) -> c_38():38 -->_3 mark#(nil()) -> c_37():37 -->_2 mark#(nil()) -> c_37():37 -->_3 mark#(i()) -> c_31():35 -->_2 mark#(i()) -> c_31():35 -->_3 mark#(e()) -> c_30():34 -->_2 mark#(e()) -> c_30():34 -->_3 mark#(a()) -> c_28():33 -->_2 mark#(a()) -> c_28():33 -->_1 a____#(X1,X2) -> c_2():17 -->_3 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 a____#(nil(),X) -> c_4(mark#(X)):3 -->_1 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_1 a____#(X,nil()) -> c_1(mark#(X)):1 12:S:mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) -->_2 mark#(isQid(X)) -> c_36(a__isQid#(X)):36 -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(u()) -> c_40():40 -->_2 mark#(tt()) -> c_39():39 -->_2 mark#(o()) -> c_38():38 -->_2 mark#(nil()) -> c_37():37 -->_2 mark#(i()) -> c_31():35 -->_2 mark#(e()) -> c_30():34 -->_2 mark#(a()) -> c_28():33 -->_1 a__and#(X1,X2) -> c_5():18 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 13:S:mark#(isList(X)) -> c_32(a__isList#(X)) -->_1 a__isList#(nil()) -> c_10():20 -->_1 a__isList#(X) -> c_8():19 -->_1 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_1 a__isList#(V) -> c_7(a__isNeList#(V)):5 14:S:mark#(isNeList(X)) -> c_33(a__isNeList#(X)) -->_1 a__isNeList#(V) -> c_11(a__isQid#(V)):21 -->_1 a__isNeList#(X) -> c_12():22 -->_1 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_1 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 15:S:mark#(isNePal(X)) -> c_34(a__isNePal#(X)) -->_1 a__isNePal#(V) -> c_15(a__isQid#(V)):23 -->_1 a__isNePal#(X) -> c_16():24 -->_1 a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)):9 16:S:mark#(isPal(X)) -> c_35(a__isPal#(X)) -->_1 a__isPal#(nil()) -> c_20():26 -->_1 a__isPal#(X) -> c_19():25 -->_1 a__isPal#(V) -> c_18(a__isNePal#(V)):10 17:W:a____#(X1,X2) -> c_2() 18:W:a__and#(X1,X2) -> c_5() 19:W:a__isList#(X) -> c_8() 20:W:a__isList#(nil()) -> c_10() 21:W:a__isNeList#(V) -> c_11(a__isQid#(V)) -->_1 a__isQid#(u()) -> c_26():32 -->_1 a__isQid#(o()) -> c_25():31 -->_1 a__isQid#(i()) -> c_24():30 -->_1 a__isQid#(e()) -> c_23():29 -->_1 a__isQid#(a()) -> c_22():28 -->_1 a__isQid#(X) -> c_21():27 22:W:a__isNeList#(X) -> c_12() 23:W:a__isNePal#(V) -> c_15(a__isQid#(V)) -->_1 a__isQid#(u()) -> c_26():32 -->_1 a__isQid#(o()) -> c_25():31 -->_1 a__isQid#(i()) -> c_24():30 -->_1 a__isQid#(e()) -> c_23():29 -->_1 a__isQid#(a()) -> c_22():28 -->_1 a__isQid#(X) -> c_21():27 24:W:a__isNePal#(X) -> c_16() 25:W:a__isPal#(X) -> c_19() 26:W:a__isPal#(nil()) -> c_20() 27:W:a__isQid#(X) -> c_21() 28:W:a__isQid#(a()) -> c_22() 29:W:a__isQid#(e()) -> c_23() 30:W:a__isQid#(i()) -> c_24() 31:W:a__isQid#(o()) -> c_25() 32:W:a__isQid#(u()) -> c_26() 33:W:mark#(a()) -> c_28() 34:W:mark#(e()) -> c_30() 35:W:mark#(i()) -> c_31() 36:W:mark#(isQid(X)) -> c_36(a__isQid#(X)) -->_1 a__isQid#(u()) -> c_26():32 -->_1 a__isQid#(o()) -> c_25():31 -->_1 a__isQid#(i()) -> c_24():30 -->_1 a__isQid#(e()) -> c_23():29 -->_1 a__isQid#(a()) -> c_22():28 -->_1 a__isQid#(X) -> c_21():27 37:W:mark#(nil()) -> c_37() 38:W:mark#(o()) -> c_38() 39:W:mark#(tt()) -> c_39() 40:W:mark#(u()) -> c_40() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: a____#(X1,X2) -> c_2() 33: mark#(a()) -> c_28() 34: mark#(e()) -> c_30() 35: mark#(i()) -> c_31() 37: mark#(nil()) -> c_37() 38: mark#(o()) -> c_38() 39: mark#(tt()) -> c_39() 40: mark#(u()) -> c_40() 19: a__isList#(X) -> c_8() 20: a__isList#(nil()) -> c_10() 22: a__isNeList#(X) -> c_12() 21: a__isNeList#(V) -> c_11(a__isQid#(V)) 18: a__and#(X1,X2) -> c_5() 24: a__isNePal#(X) -> c_16() 23: a__isNePal#(V) -> c_15(a__isQid#(V)) 25: a__isPal#(X) -> c_19() 26: a__isPal#(nil()) -> c_20() 36: mark#(isQid(X)) -> c_36(a__isQid#(X)) 27: a__isQid#(X) -> c_21() 28: a__isQid#(a()) -> c_22() 29: a__isQid#(e()) -> c_23() 30: a__isQid#(i()) -> c_24() 31: a__isQid#(o()) -> c_25() 32: a__isQid#(u()) -> c_26() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/2,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a____#(X,nil()) -> c_1(mark#(X)) -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 2:S:a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) -->_5 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_4 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_5 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_4 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_5 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_4 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_5 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_4 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_5 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_4 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_5 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_4 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_3 a____#(nil(),X) -> c_4(mark#(X)):3 -->_1 a____#(nil(),X) -> c_4(mark#(X)):3 -->_3 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_1 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_3 a____#(X,nil()) -> c_1(mark#(X)):1 -->_1 a____#(X,nil()) -> c_1(mark#(X)):1 3:S:a____#(nil(),X) -> c_4(mark#(X)) -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 4:S:a__and#(tt(),X) -> c_6(mark#(X)) -->_1 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_1 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_1 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_1 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_1 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_1 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 5:S:a__isList#(V) -> c_7(a__isNeList#(V)) -->_1 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_1 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 6:S:a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) -->_2 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_2 a__isList#(V) -> c_7(a__isNeList#(V)):5 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 7:S:a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) -->_2 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_2 a__isList#(V) -> c_7(a__isNeList#(V)):5 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 8:S:a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) -->_2 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_2 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 9:S:a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)) -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 10:S:a__isPal#(V) -> c_18(a__isNePal#(V)) -->_1 a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)):9 11:S:mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_3 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_3 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_3 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_3 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_3 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 a____#(nil(),X) -> c_4(mark#(X)):3 -->_1 a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)):2 -->_1 a____#(X,nil()) -> c_1(mark#(X)):1 12:S:mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) -->_2 mark#(isPal(X)) -> c_35(a__isPal#(X)):16 -->_2 mark#(isNePal(X)) -> c_34(a__isNePal#(X)):15 -->_2 mark#(isNeList(X)) -> c_33(a__isNeList#(X)):14 -->_2 mark#(isList(X)) -> c_32(a__isList#(X)):13 -->_2 mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)):12 -->_2 mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):11 -->_1 a__and#(tt(),X) -> c_6(mark#(X)):4 13:S:mark#(isList(X)) -> c_32(a__isList#(X)) -->_1 a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)):6 -->_1 a__isList#(V) -> c_7(a__isNeList#(V)):5 14:S:mark#(isNeList(X)) -> c_33(a__isNeList#(X)) -->_1 a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)):8 -->_1 a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)):7 15:S:mark#(isNePal(X)) -> c_34(a__isNePal#(X)) -->_1 a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P)),a__isQid#(I)):9 16:S:mark#(isPal(X)) -> c_35(a__isPal#(X)) -->_1 a__isPal#(V) -> c_18(a__isNePal#(V)):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P))) * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P))) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(a____) = {1,2}, uargs(a__and) = {1}, uargs(a____#) = {1,2}, uargs(a__and#) = {1}, uargs(c_1) = {1}, uargs(c_3) = {1,2,3,4,5}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_9) = {1,2}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_27) = {1,2,3}, uargs(c_29) = {1,2}, uargs(c_32) = {1}, uargs(c_33) = {1}, uargs(c_34) = {1}, uargs(c_35) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(__) = [0] p(a) = [0] p(a____) = [1] x1 + [1] x2 + [0] p(a__and) = [1] x1 + [0] p(a__isList) = [0] p(a__isNeList) = [0] p(a__isNePal) = [0] p(a__isPal) = [0] p(a__isQid) = [0] p(and) = [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [0] p(isNePal) = [0] p(isPal) = [0] p(isQid) = [0] p(mark) = [0] p(nil) = [0] p(o) = [0] p(tt) = [0] p(u) = [0] p(a____#) = [1] x1 + [1] x2 + [3] p(a__and#) = [1] x1 + [3] p(a__isList#) = [0] p(a__isNeList#) = [7] p(a__isNePal#) = [0] p(a__isPal#) = [0] p(a__isQid#) = [0] p(mark#) = [1] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] x2 + [3] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_28) = [0] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] x1 + [0] p(c_33) = [1] x1 + [0] p(c_34) = [1] x1 + [0] p(c_35) = [1] x1 + [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] Following rules are strictly oriented: a____#(X,nil()) = [1] X + [3] > [1] = c_1(mark#(X)) a____#(nil(),X) = [1] X + [3] > [1] = c_4(mark#(X)) a__and#(tt(),X) = [3] > [1] = c_6(mark#(X)) a__isNeList#(__(V1,V2)) = [7] > [6] = c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) mark#(isList(X)) = [1] > [0] = c_32(a__isList#(X)) mark#(isNePal(X)) = [1] > [0] = c_34(a__isNePal#(X)) mark#(isPal(X)) = [1] > [0] = c_35(a__isPal#(X)) Following rules are (at-least) weakly oriented: a____#(__(X,Y),Z) = [1] Z + [3] >= [9] = c_3(a____#(mark(X),a____(mark(Y),mark(Z))),mark#(X),a____#(mark(Y),mark(Z)),mark#(Y),mark#(Z)) a__isList#(V) = [0] >= [7] = c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) = [0] >= [3] = c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) = [7] >= [10] = c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) = [0] >= [3] = c_17(a__and#(a__isQid(I),isPal(P))) a__isPal#(V) = [0] >= [0] = c_18(a__isNePal#(V)) mark#(__(X1,X2)) = [1] >= [5] = c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) = [1] >= [4] = c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isNeList(X)) = [1] >= [7] = c_33(a__isNeList#(X)) a____(X,nil()) = [1] X + [0] >= [0] = mark(X) a____(X1,X2) = [1] X1 + [1] X2 + [0] >= [0] = __(X1,X2) a____(__(X,Y),Z) = [1] Z + [0] >= [0] = a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) = [1] X + [0] >= [0] = mark(X) a__and(X1,X2) = [1] X1 + [0] >= [0] = and(X1,X2) a__and(tt(),X) = [0] >= [0] = mark(X) a__isList(V) = [0] >= [0] = a__isNeList(V) a__isList(X) = [0] >= [0] = isList(X) a__isList(__(V1,V2)) = [0] >= [0] = a__and(a__isList(V1),isList(V2)) a__isList(nil()) = [0] >= [0] = tt() a__isNeList(V) = [0] >= [0] = a__isQid(V) a__isNeList(X) = [0] >= [0] = isNeList(X) a__isNeList(__(V1,V2)) = [0] >= [0] = a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) = [0] >= [0] = a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) = [0] >= [0] = a__isQid(V) a__isNePal(X) = [0] >= [0] = isNePal(X) a__isNePal(__(I,__(P,I))) = [0] >= [0] = a__and(a__isQid(I),isPal(P)) a__isPal(V) = [0] >= [0] = a__isNePal(V) a__isPal(X) = [0] >= [0] = isPal(X) a__isPal(nil()) = [0] >= [0] = tt() a__isQid(X) = [0] >= [0] = isQid(X) a__isQid(a()) = [0] >= [0] = tt() a__isQid(e()) = [0] >= [0] = tt() a__isQid(i()) = [0] >= [0] = tt() a__isQid(o()) = [0] >= [0] = tt() a__isQid(u()) = [0] >= [0] = tt() mark(__(X1,X2)) = [0] >= [0] = a____(mark(X1),mark(X2)) mark(a()) = [0] >= [0] = a() mark(and(X1,X2)) = [0] >= [0] = a__and(mark(X1),X2) mark(e()) = [0] >= [0] = e() mark(i()) = [0] >= [0] = i() mark(isList(X)) = [0] >= [0] = a__isList(X) mark(isNeList(X)) = [0] >= [0] = a__isNeList(X) mark(isNePal(X)) = [0] >= [0] = a__isNePal(X) mark(isPal(X)) = [0] >= [0] = a__isPal(X) mark(isQid(X)) = [0] >= [0] = a__isQid(X) mark(nil()) = [0] >= [0] = nil() mark(o()) = [0] >= [0] = o() mark(tt()) = [0] >= [0] = tt() mark(u()) = [0] >= [0] = u() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P))) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) - Weak DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(a____) = {1,2}, uargs(a__and) = {1}, uargs(a____#) = {1,2}, uargs(a__and#) = {1}, uargs(c_1) = {1}, uargs(c_3) = {1,2,3,4,5}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_9) = {1,2}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_27) = {1,2,3}, uargs(c_29) = {1,2}, uargs(c_32) = {1}, uargs(c_33) = {1}, uargs(c_34) = {1}, uargs(c_35) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(__) = [0] p(a) = [0] p(a____) = [1] x1 + [1] x2 + [0] p(a__and) = [1] x1 + [0] p(a__isList) = [0] p(a__isNeList) = [0] p(a__isNePal) = [0] p(a__isPal) = [0] p(a__isQid) = [0] p(and) = [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [0] p(isNePal) = [0] p(isPal) = [0] p(isQid) = [0] p(mark) = [0] p(nil) = [0] p(o) = [0] p(tt) = [0] p(u) = [0] p(a____#) = [1] x1 + [1] x2 + [5] p(a__and#) = [1] x1 + [4] p(a__isList#) = [0] p(a__isNeList#) = [4] p(a__isNePal#) = [0] p(a__isPal#) = [1] p(a__isQid#) = [0] p(mark#) = [1] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [3] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [3] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [1] x2 + [1] x3 + [6] p(c_28) = [0] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [2] p(c_31) = [0] p(c_32) = [1] x1 + [1] p(c_33) = [1] x1 + [0] p(c_34) = [1] x1 + [0] p(c_35) = [1] x1 + [0] p(c_36) = [1] x1 + [4] p(c_37) = [0] p(c_38) = [1] p(c_39) = [0] p(c_40) = [1] Following rules are strictly oriented: a__isPal#(V) = [1] > [0] = c_18(a__isNePal#(V)) Following rules are (at-least) weakly oriented: a____#(X,nil()) = [1] X + [5] >= [1] = c_1(mark#(X)) a____#(__(X,Y),Z) = [1] Z + [5] >= [13] = c_3(a____#(mark(X),a____(mark(Y),mark(Z))),mark#(X),a____#(mark(Y),mark(Z)),mark#(Y),mark#(Z)) a____#(nil(),X) = [1] X + [5] >= [1] = c_4(mark#(X)) a__and#(tt(),X) = [4] >= [1] = c_6(mark#(X)) a__isList#(V) = [0] >= [7] = c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) = [0] >= [7] = c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) = [4] >= [4] = c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) = [4] >= [8] = c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) = [0] >= [4] = c_17(a__and#(a__isQid(I),isPal(P))) mark#(__(X1,X2)) = [1] >= [13] = c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) = [1] >= [5] = c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isList(X)) = [1] >= [1] = c_32(a__isList#(X)) mark#(isNeList(X)) = [1] >= [4] = c_33(a__isNeList#(X)) mark#(isNePal(X)) = [1] >= [0] = c_34(a__isNePal#(X)) mark#(isPal(X)) = [1] >= [1] = c_35(a__isPal#(X)) a____(X,nil()) = [1] X + [0] >= [0] = mark(X) a____(X1,X2) = [1] X1 + [1] X2 + [0] >= [0] = __(X1,X2) a____(__(X,Y),Z) = [1] Z + [0] >= [0] = a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) = [1] X + [0] >= [0] = mark(X) a__and(X1,X2) = [1] X1 + [0] >= [0] = and(X1,X2) a__and(tt(),X) = [0] >= [0] = mark(X) a__isList(V) = [0] >= [0] = a__isNeList(V) a__isList(X) = [0] >= [0] = isList(X) a__isList(__(V1,V2)) = [0] >= [0] = a__and(a__isList(V1),isList(V2)) a__isList(nil()) = [0] >= [0] = tt() a__isNeList(V) = [0] >= [0] = a__isQid(V) a__isNeList(X) = [0] >= [0] = isNeList(X) a__isNeList(__(V1,V2)) = [0] >= [0] = a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) = [0] >= [0] = a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) = [0] >= [0] = a__isQid(V) a__isNePal(X) = [0] >= [0] = isNePal(X) a__isNePal(__(I,__(P,I))) = [0] >= [0] = a__and(a__isQid(I),isPal(P)) a__isPal(V) = [0] >= [0] = a__isNePal(V) a__isPal(X) = [0] >= [0] = isPal(X) a__isPal(nil()) = [0] >= [0] = tt() a__isQid(X) = [0] >= [0] = isQid(X) a__isQid(a()) = [0] >= [0] = tt() a__isQid(e()) = [0] >= [0] = tt() a__isQid(i()) = [0] >= [0] = tt() a__isQid(o()) = [0] >= [0] = tt() a__isQid(u()) = [0] >= [0] = tt() mark(__(X1,X2)) = [0] >= [0] = a____(mark(X1),mark(X2)) mark(a()) = [0] >= [0] = a() mark(and(X1,X2)) = [0] >= [0] = a__and(mark(X1),X2) mark(e()) = [0] >= [0] = e() mark(i()) = [0] >= [0] = i() mark(isList(X)) = [0] >= [0] = a__isList(X) mark(isNeList(X)) = [0] >= [0] = a__isNeList(X) mark(isNePal(X)) = [0] >= [0] = a__isNePal(X) mark(isPal(X)) = [0] >= [0] = a__isPal(X) mark(isQid(X)) = [0] >= [0] = a__isQid(X) mark(nil()) = [0] >= [0] = nil() mark(o()) = [0] >= [0] = o() mark(tt()) = [0] >= [0] = tt() mark(u()) = [0] >= [0] = u() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: a____#(__(X,Y),Z) -> c_3(a____#(mark(X),a____(mark(Y),mark(Z))) ,mark#(X) ,a____#(mark(Y),mark(Z)) ,mark#(Y) ,mark#(Z)) a__isList#(V) -> c_7(a__isNeList#(V)) a__isList#(__(V1,V2)) -> c_9(a__and#(a__isList(V1),isList(V2)),a__isList#(V1)) a__isNeList#(__(V1,V2)) -> c_14(a__and#(a__isNeList(V1),isList(V2)),a__isNeList#(V1)) a__isNePal#(__(I,__(P,I))) -> c_17(a__and#(a__isQid(I),isPal(P))) mark#(__(X1,X2)) -> c_27(a____#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(and(X1,X2)) -> c_29(a__and#(mark(X1),X2),mark#(X1)) mark#(isNeList(X)) -> c_33(a__isNeList#(X)) - Weak DPs: a____#(X,nil()) -> c_1(mark#(X)) a____#(nil(),X) -> c_4(mark#(X)) a__and#(tt(),X) -> c_6(mark#(X)) a__isNeList#(__(V1,V2)) -> c_13(a__and#(a__isList(V1),isNeList(V2)),a__isList#(V1)) a__isPal#(V) -> c_18(a__isNePal#(V)) mark#(isList(X)) -> c_32(a__isList#(X)) mark#(isNePal(X)) -> c_34(a__isNePal#(X)) mark#(isPal(X)) -> c_35(a__isPal#(X)) - Weak TRS: a____(X,nil()) -> mark(X) a____(X1,X2) -> __(X1,X2) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(nil(),X) -> mark(X) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1,a____#/2,a__and#/2 ,a__isList#/1,a__isNeList#/1,a__isNePal#/1,a__isPal#/1,a__isQid#/1,mark#/1} / {__/2,a/0,and/2,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0,c_1/1,c_2/0,c_3/5,c_4/1,c_5/0,c_6/1,c_7/1 ,c_8/0,c_9/2,c_10/0,c_11/1,c_12/0,c_13/2,c_14/2,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/0,c_22/0 ,c_23/0,c_24/0,c_25/0,c_26/0,c_27/3,c_28/0,c_29/2,c_30/0,c_31/0,c_32/1,c_33/1,c_34/1,c_35/1,c_36/1,c_37/0 ,c_38/0,c_39/0,c_40/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____#,a__and#,a__isList#,a__isNeList#,a__isNePal# ,a__isPal#,a__isQid#,mark#} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE