WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) -> Nil() domatch(Nil(),Nil(),n) -> Cons(n,Nil()) eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) -> False() eqNatList(Nil(),Cons(y,ys)) -> False() eqNatList(Nil(),Nil()) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() strmatch(patstr,str) -> domatch(patstr,str,Nil()) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite](False(),y,ys,x,xs) -> False() eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys) - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,and,domatch,domatch[Ite],eqNatList,eqNatList[Ite] ,notEmpty,prefix,strmatch} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() prefix#(Cons(x,xs),Nil()) -> c_10() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) prefix#(Nil(),cs) -> c_12() strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) Weak DPs !EQ#(0(),0()) -> c_14() !EQ#(0(),S(y)) -> c_15() !EQ#(S(x),0()) -> c_16() !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() prefix#(Cons(x,xs),Nil()) -> c_10() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) prefix#(Nil(),cs) -> c_12() strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) - Weak DPs: !EQ#(0(),0()) -> c_14() !EQ#(0(),S(y)) -> c_15() !EQ#(S(x),0()) -> c_16() !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) -> Nil() domatch(Nil(),Nil(),n) -> Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) -> False() eqNatList(Nil(),Cons(y,ys)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),y,ys,x,xs) -> False() eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() strmatch(patstr,str) -> domatch(patstr,str,Nil()) - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {8,9,10,12} by application of Pre({8,9,10,12}) = {1,11}. Here rules are labelled as follows: 1: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) 2: domatch#(Cons(x,xs),Nil(),n) -> c_2() 3: domatch#(Nil(),Nil(),n) -> c_3() 4: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) 5: eqNatList#(Cons(x,xs),Nil()) -> c_5() 6: eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7: eqNatList#(Nil(),Nil()) -> c_7() 8: notEmpty#(Cons(x,xs)) -> c_8() 9: notEmpty#(Nil()) -> c_9() 10: prefix#(Cons(x,xs),Nil()) -> c_10() 11: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) 12: prefix#(Nil(),cs) -> c_12() 13: strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) 14: !EQ#(0(),0()) -> c_14() 15: !EQ#(0(),S(y)) -> c_15() 16: !EQ#(S(x),0()) -> c_16() 17: !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) 18: and#(False(),False()) -> c_18() 19: and#(False(),True()) -> c_19() 20: and#(True(),False()) -> c_20() 21: and#(True(),True()) -> c_21() 22: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 23: domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 24: eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() 25: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) - Weak DPs: !EQ#(0(),0()) -> c_14() !EQ#(0(),S(y)) -> c_15() !EQ#(S(x),0()) -> c_16() !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() prefix#(Cons(x,xs),Nil()) -> c_10() prefix#(Nil(),cs) -> c_12() - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) -> Nil() domatch(Nil(),Nil(),n) -> Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) -> False() eqNatList(Nil(),Cons(y,ys)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),y,ys,x,xs) -> False() eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() strmatch(patstr,str) -> domatch(patstr,str,Nil()) - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):19 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):18 -->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8 -->_2 prefix#(Nil(),cs) -> c_12():25 2:S:domatch#(Cons(x,xs),Nil(),n) -> c_2() 3:S:domatch#(Nil(),Nil(),n) -> c_3() 4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) -->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):21 -->_2 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13 -->_1 eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24():20 -->_2 !EQ#(S(x),0()) -> c_16():12 -->_2 !EQ#(0(),S(y)) -> c_15():11 -->_2 !EQ#(0(),0()) -> c_14():10 5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5() 6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7:S:eqNatList#(Nil(),Nil()) -> c_7() 8:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) -->_2 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13 -->_3 prefix#(Nil(),cs) -> c_12():25 -->_3 prefix#(Cons(x,xs),Nil()) -> c_10():24 -->_1 and#(True(),True()) -> c_21():17 -->_1 and#(True(),False()) -> c_20():16 -->_1 and#(False(),True()) -> c_19():15 -->_1 and#(False(),False()) -> c_18():14 -->_2 !EQ#(S(x),0()) -> c_16():12 -->_2 !EQ#(0(),S(y)) -> c_15():11 -->_2 !EQ#(0(),0()) -> c_14():10 -->_3 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8 9:S:strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 10:W:!EQ#(0(),0()) -> c_14() 11:W:!EQ#(0(),S(y)) -> c_15() 12:W:!EQ#(S(x),0()) -> c_16() 13:W:!EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) -->_1 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13 -->_1 !EQ#(S(x),0()) -> c_16():12 -->_1 !EQ#(0(),S(y)) -> c_15():11 -->_1 !EQ#(0(),0()) -> c_14():10 14:W:and#(False(),False()) -> c_18() 15:W:and#(False(),True()) -> c_19() 16:W:and#(True(),False()) -> c_20() 17:W:and#(True(),True()) -> c_21() 18:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 19:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 20:W:eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() 21:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():7 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)):4 22:W:notEmpty#(Cons(x,xs)) -> c_8() 23:W:notEmpty#(Nil()) -> c_9() 24:W:prefix#(Cons(x,xs),Nil()) -> c_10() 25:W:prefix#(Nil(),cs) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 23: notEmpty#(Nil()) -> c_9() 22: notEmpty#(Cons(x,xs)) -> c_8() 20: eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24() 14: and#(False(),False()) -> c_18() 15: and#(False(),True()) -> c_19() 16: and#(True(),False()) -> c_20() 17: and#(True(),True()) -> c_21() 24: prefix#(Cons(x,xs),Nil()) -> c_10() 25: prefix#(Nil(),cs) -> c_12() 13: !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)) 10: !EQ#(0(),0()) -> c_14() 11: !EQ#(0(),S(y)) -> c_15() 12: !EQ#(S(x),0()) -> c_16() * Step 4: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) - Weak DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) -> Nil() domatch(Nil(),Nil(),n) -> Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) -> False() eqNatList(Nil(),Cons(y,ys)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),y,ys,x,xs) -> False() eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() strmatch(patstr,str) -> domatch(patstr,str,Nil()) - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):19 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):18 -->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8 2:S:domatch#(Cons(x,xs),Nil(),n) -> c_2() 3:S:domatch#(Nil(),Nil(),n) -> c_3() 4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)) -->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):21 5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5() 6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7:S:eqNatList#(Nil(),Nil()) -> c_7() 8:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)) -->_3 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)) ,!EQ#(x',x) ,prefix#(xs',xs)):8 9:S:strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 18:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 19:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 21:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():7 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) - Weak DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) -> Nil() domatch(Nil(),Nil(),n) -> Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) -> False() eqNatList(Nil(),Cons(y,ys)) -> False() eqNatList(Nil(),Nil()) -> True() eqNatList[Ite](False(),y,ys,x,xs) -> False() eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() strmatch(patstr,str) -> domatch(patstr,str,Nil()) - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) * Step 6: RemoveHeads WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) - Weak DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):11 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):10 -->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):8 2:S:domatch#(Cons(x,xs),Nil(),n) -> c_2() 3:S:domatch#(Nil(),Nil(),n) -> c_3() 4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) -->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):12 5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5() 6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7:S:eqNatList#(Nil(),Nil()) -> c_7() 8:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) -->_1 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):8 9:S:strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 10:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 11:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 12:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():7 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(9,strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil())))] * Step 7: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) and a lower component domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) Further, following extension rules are added to the lower component. domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs) eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() - Weak DPs: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))) -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):3 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):2 2:S:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 3:S:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) -->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) ,prefix#(patcs,Cons(x,xs))):1 4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) -->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):8 5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5() 6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7:S:eqNatList#(Nil(),Nil()) -> c_7() 8:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():7 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) ** Step 7.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() - Weak DPs: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(eqNatList[Ite]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [1] x2 + [1] p(False) = [0] p(Nil) = [3] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [1] x2 + [0] p(!EQ#) = [2] x2 + [0] p(and#) = [1] x1 + [2] p(domatch#) = [2] x3 + [0] p(domatch[Ite]#) = [1] x1 + [1] x4 + [2] p(eqNatList#) = [3] x2 + [3] p(eqNatList[Ite]#) = [1] x1 + [3] x3 + [3] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [5] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [2] p(c_15) = [0] p(c_16) = [4] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [2] p(c_24) = [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: eqNatList#(Cons(x,xs),Nil()) = [12] > [0] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [3] ys + [6] > [0] = c_6() eqNatList#(Nil(),Nil()) = [12] > [0] = c_7() Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [2] n + [0] >= [1] n + [2] = c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] n + [2] >= [10] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] n + [2] >= [12] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) = [3] ys + [6] >= [3] ys + [8] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList[Ite]#(True(),y,ys,x,xs) = [3] ys + [3] >= [3] ys + [3] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) - Weak DPs: eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(eqNatList[Ite]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [0] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [0] p(!EQ#) = [1] x2 + [0] p(and#) = [2] x1 + [2] x2 + [0] p(domatch#) = [4] x3 + [3] p(domatch[Ite]#) = [1] x1 + [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [1] x1 + [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: domatch#(patcs,Cons(x,xs),n) = [4] n + [3] > [0] = c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) Following rules are (at-least) weakly oriented: domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [0] >= [3] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [0] >= [3] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) = [0] >= [0] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) = [0] >= [0] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [0] >= [0] = c_6() eqNatList#(Nil(),Nil()) = [0] >= [0] = c_7() eqNatList[Ite]#(True(),y,ys,x,xs) = [0] >= [0] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(eqNatList[Ite]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [2] p(Cons) = [1] x2 + [4] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [2] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [1] x2 + [1] p(domatch[Ite]) = [1] x2 + [1] x3 + [4] p(eqNatList) = [2] x1 + [1] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [4] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [1] x1 + [0] p(!EQ#) = [1] x1 + [1] x2 + [0] p(and#) = [1] x1 + [4] p(domatch#) = [1] x2 + [1] p(domatch[Ite]#) = [1] x1 + [1] x3 + [0] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [1] x1 + [2] p(notEmpty#) = [0] p(prefix#) = [4] x2 + [0] p(strmatch#) = [1] x1 + [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [7] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [1] p(c_11) = [1] x1 + [4] p(c_12) = [0] p(c_13) = [4] x1 + [0] p(c_14) = [1] p(c_15) = [1] p(c_16) = [0] p(c_17) = [2] x1 + [1] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [6] p(c_23) = [1] x1 + [2] p(c_24) = [1] p(c_25) = [1] x1 + [2] Following rules are strictly oriented: domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] xs + [4] > [1] xs + [3] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [1] xs + [5] >= [1] xs + [4] = c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] xs + [4] >= [1] xs + [7] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) = [0] >= [9] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) = [0] >= [0] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [0] >= [0] = c_6() eqNatList#(Nil(),Nil()) = [0] >= [0] = c_7() eqNatList[Ite]#(True(),y,ys,x,xs) = [2] >= [2] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(eqNatList[Ite]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [1] x2 + [2] p(False) = [0] p(Nil) = [6] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [4] x1 + [2] x2 + [2] x3 + [1] p(domatch[Ite]) = [4] x1 + [4] x2 + [0] p(eqNatList) = [1] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(notEmpty) = [1] x1 + [0] p(prefix) = [1] p(strmatch) = [4] p(!EQ#) = [0] p(and#) = [0] p(domatch#) = [1] x2 + [6] p(domatch[Ite]#) = [1] x1 + [1] x3 + [4] p(eqNatList#) = [1] x2 + [5] p(eqNatList[Ite]#) = [1] x1 + [1] x3 + [5] p(notEmpty#) = [2] x1 + [1] p(prefix#) = [1] x2 + [0] p(strmatch#) = [1] x2 + [2] p(c_1) = [1] x1 + [1] p(c_2) = [0] p(c_3) = [2] p(c_4) = [1] x1 + [1] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [2] p(c_9) = [4] p(c_10) = [1] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [4] p(c_18) = [0] p(c_19) = [2] p(c_20) = [1] p(c_21) = [4] p(c_22) = [1] x1 + [6] p(c_23) = [1] x1 + [0] p(c_24) = [1] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: eqNatList#(Cons(x,xs),Cons(y,ys)) = [1] ys + [7] > [1] ys + [6] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [1] xs + [8] >= [1] xs + [8] = c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] xs + [6] >= [1] xs + [12] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] xs + [6] >= [1] xs + [6] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Nil()) = [11] >= [0] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [1] ys + [7] >= [0] = c_6() eqNatList#(Nil(),Nil()) = [11] >= [0] = c_7() eqNatList[Ite]#(True(),y,ys,x,xs) = [1] ys + [5] >= [1] ys + [5] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [1] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [1] >= [1] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [1] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:6: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(eqNatList[Ite]#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [1] x2 + [1] p(False) = [0] p(Nil) = [0] p(S) = [4] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [0] p(!EQ#) = [0] p(and#) = [1] x1 + [1] x2 + [4] p(domatch#) = [2] x2 + [6] p(domatch[Ite]#) = [1] x1 + [2] x3 + [5] p(eqNatList#) = [7] x1 + [1] p(eqNatList[Ite]#) = [1] x1 + [7] x5 + [2] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [5] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [2] xs + [7] > [2] xs + [6] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [2] xs + [8] >= [2] xs + [7] = c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [2] xs + [7] >= [2] xs + [6] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) = [7] xs + [8] >= [7] xs + [7] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) = [7] xs + [8] >= [1] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [1] >= [1] = c_6() eqNatList#(Nil(),Nil()) = [1] >= [1] = c_7() eqNatList[Ite]#(True(),y,ys,x,xs) = [7] xs + [2] >= [7] xs + [1] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs) eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:domatch#(Cons(x,xs),Nil(),n) -> c_2() 2:S:domatch#(Nil(),Nil(),n) -> c_3() 3:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) -->_1 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):3 4:W:domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))):7 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))):6 5:W:domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) -->_1 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):3 6:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) -->_1 domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)):5 -->_1 domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n):4 -->_1 domatch#(Nil(),Nil(),n) -> c_3():2 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():1 7:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) -->_1 domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)):5 -->_1 domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n):4 -->_1 domatch#(Nil(),Nil(),n) -> c_3():2 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():1 8:W:eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs) -->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys):9 9:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys) -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs):8 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs) 9: eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys) ** Step 7.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(c_11) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [0] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [0] p(prefix) = [0] p(strmatch) = [0] p(!EQ#) = [0] p(and#) = [0] p(domatch#) = [4] p(domatch[Ite]#) = [1] x1 + [4] p(eqNatList#) = [0] p(eqNatList[Ite]#) = [1] x1 + [1] x2 + [1] x4 + [1] x5 + [0] p(notEmpty#) = [2] p(prefix#) = [1] p(strmatch#) = [4] x1 + [1] x2 + [1] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [4] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [4] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] p(c_15) = [0] p(c_16) = [2] p(c_17) = [2] x1 + [4] p(c_18) = [0] p(c_19) = [1] p(c_20) = [2] p(c_21) = [1] p(c_22) = [4] x1 + [0] p(c_23) = [1] p(c_24) = [2] p(c_25) = [2] x1 + [4] Following rules are strictly oriented: domatch#(Cons(x,xs),Nil(),n) = [4] > [0] = c_2() domatch#(Nil(),Nil(),n) = [4] > [0] = c_3() Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [4] >= [4] = domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) = [4] >= [1] = prefix#(patcs,Cons(x,xs)) domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [4] >= [4] = domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [4] >= [4] = domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) prefix#(Cons(x',xs'),Cons(x,xs)) = [1] >= [5] = c_11(prefix#(xs',xs)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, 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: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(domatch[Ite]#) = {1}, uargs(c_11) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [5] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [0] p(eqNatList[Ite]) = [0] p(notEmpty) = [4] x1 + [0] p(prefix) = [0] p(strmatch) = [1] x1 + [1] x2 + [4] p(!EQ#) = [1] x2 + [0] p(and#) = [1] x1 + [2] x2 + [2] p(domatch#) = [1] x1 + [0] p(domatch[Ite]#) = [1] x1 + [1] x2 + [0] p(eqNatList#) = [1] x1 + [0] p(eqNatList[Ite]#) = [1] x3 + [1] x4 + [1] p(notEmpty#) = [0] p(prefix#) = [1] x1 + [0] p(strmatch#) = [1] x2 + [0] p(c_1) = [1] x1 + [1] p(c_2) = [5] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [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] Following rules are strictly oriented: prefix#(Cons(x',xs'),Cons(x,xs)) = [1] x' + [1] xs' + [5] > [1] xs' + [0] = c_11(prefix#(xs',xs)) Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [1] patcs + [0] >= [1] patcs + [0] = domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) = [1] patcs + [0] >= [1] patcs + [0] = prefix#(patcs,Cons(x,xs)) domatch#(Cons(x,xs),Nil(),n) = [1] x + [1] xs + [5] >= [5] = c_2() domatch#(Nil(),Nil(),n) = [0] >= [0] = c_3() domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] patcs + [0] >= [1] patcs + [0] = domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] patcs + [0] >= [1] patcs + [0] = domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [0] >= [0] = False() !EQ(S(x),0()) = [0] >= [0] = False() !EQ(S(x),S(y)) = [0] >= [0] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [0] >= [0] = False() and(True(),False()) = [0] >= [0] = False() and(True(),True()) = [0] >= [0] = True() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [0] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)) domatch#(Cons(x,xs),Nil(),n) -> c_2() domatch#(Nil(),Nil(),n) -> c_3() domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))) prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - Signature: {!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2 ,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList# ,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))