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: 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),!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: 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() !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#(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),!EQ#(x,y)) eqNatList#(Cons(x,xs),Nil()) -> c_5() eqNatList#(Nil(),Cons(y,ys)) -> c_6() eqNatList#(Nil(),Nil()) -> c_7() 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#(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())) * Step 3: 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() 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/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 4: 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() 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/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 5: 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() 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/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 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: Decompose 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - 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() 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#(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/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} Problem (S) - Strict DPs: 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: 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[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) 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} ** Step 7.a:1: 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() 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#(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/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#(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:W: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:W:eqNatList#(Cons(x,xs),Nil()) -> c_5() 6:W:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7:W: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 10:W: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 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 11:W: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 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2 -->_1 domatch#(Nil(),Nil(),n) -> c_3():3 12:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):4 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6 -->_1 eqNatList#(Nil(),Nil()) -> c_7():7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) 12: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) 5: eqNatList#(Cons(x,xs),Nil()) -> c_5() 6: eqNatList#(Nil(),Cons(y,ys)) -> c_6() 7: eqNatList#(Nil(),Nil()) -> c_7() ** Step 7.a:2: PredecessorEstimationCP 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() 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())))) - 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 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() Consider the set of all dependency pairs 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() 8: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) 10: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 11: domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1,2,3} These cover all (indirect) predecessors of dependency pairs {1,2,3,10,11} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 7.a:2.a:1: NaturalMI 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#(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[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())))) - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_11) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1} Following symbols are considered usable: {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [3] x2 + [5] p(0) = [1] p(Cons) = [1] x2 + [2] p(False) = [0] p(Nil) = [0] p(S) = [6] p(True) = [0] p(and) = [4] x1 + [8] p(domatch) = [4] p(domatch[Ite]) = [8] x1 + [1] x2 + [1] x3 + [1] x4 + [1] p(eqNatList) = [1] x1 + [2] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [1] x2 + [2] x4 + [0] p(notEmpty) = [1] x1 + [1] p(prefix) = [0] p(strmatch) = [1] x1 + [2] x2 + [8] p(!EQ#) = [1] x2 + [2] p(and#) = [4] x1 + [2] x2 + [2] p(domatch#) = [8] x1 + [4] x2 + [12] p(domatch[Ite]#) = [8] x2 + [4] x3 + [4] p(eqNatList#) = [1] x1 + [1] x2 + [0] p(eqNatList[Ite]#) = [2] x2 + [1] x3 + [1] x4 + [0] p(notEmpty#) = [0] p(prefix#) = [0] p(strmatch#) = [8] x1 + [1] x2 + [0] p(c_1) = [1] x1 + [8] x2 + [2] p(c_2) = [4] p(c_3) = [11] p(c_4) = [8] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [1] p(c_9) = [0] p(c_10) = [2] p(c_11) = [4] x1 + [0] p(c_12) = [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [4] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [1] p(c_22) = [1] x1 + [0] p(c_23) = [1] x1 + [0] p(c_24) = [1] p(c_25) = [1] Following rules are strictly oriented: domatch#(patcs,Cons(x,xs),n) = [8] patcs + [4] xs + [20] > [8] patcs + [4] xs + [14] = 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) = [8] xs + [28] > [4] = c_2() domatch#(Nil(),Nil(),n) = [12] > [11] = c_3() Following rules are (at-least) weakly oriented: domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [8] patcs + [4] xs + [12] >= [8] patcs + [4] xs + [12] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [8] patcs + [4] xs + [12] >= [8] patcs + [4] xs + [12] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) prefix#(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_11(prefix#(xs',xs)) *** Step 7.a:2.a:2: Assumption WORST_CASE(?,O(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) -> 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())))) - 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.a:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak 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() 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())))) - 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: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)):1 2:W: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())))):6 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):5 -->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):1 3:W:domatch#(Cons(x,xs),Nil(),n) -> c_2() 4:W:domatch#(Nil(),Nil(),n) -> c_3() 5: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():4 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():3 -->_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 6: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():4 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():3 -->_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 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: domatch#(Cons(x,xs),Nil(),n) -> c_2() 4: domatch#(Nil(),Nil(),n) -> c_3() *** Step 7.a:2.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak 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())))) - 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) The strictly oriented rules are moved into the weak component. **** Step 7.a:2.b:2.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) - Weak 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())))) - 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: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_11) = {1}, uargs(c_22) = {1}, uargs(c_23) = {1} Following symbols are considered usable: {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [0 1] x1 + [2] [1 2] [1] p(0) = [0] [0] p(Cons) = [1 2] x2 + [1] [0 1] [1] p(False) = [1] [0] p(Nil) = [0] [0] p(S) = [1 0] x1 + [1] [0 0] [2] p(True) = [0] [2] p(and) = [2 0] x1 + [0 0] x2 + [0] [0 1] [0 1] [0] p(domatch) = [0 0] x2 + [0] [0 1] [0] p(domatch[Ite]) = [0 0] x1 + [0 0] x4 + [2] [0 2] [1 2] [0] p(eqNatList) = [2 2] x2 + [0] [2 0] [0] p(eqNatList[Ite]) = [1 0] x5 + [1] [1 2] [0] p(notEmpty) = [0 2] x1 + [0] [2 0] [0] p(prefix) = [0 3] x1 + [2] [2 2] [0] p(strmatch) = [1 2] x1 + [2 0] x2 + [0] [2 0] [2 0] [0] p(!EQ#) = [2 2] x2 + [1] [1 1] [0] p(and#) = [2] [2] p(domatch#) = [2 0] x1 + [1 1] x2 + [1] [0 0] [0 1] [0] p(domatch[Ite]#) = [2 0] x2 + [1 0] x3 + [0 0] x4 + [0] [1 0] [0 0] [0 1] [0] p(eqNatList#) = [1 0] x2 + [0] [0 1] [0] p(eqNatList[Ite]#) = [0 0] x2 + [1 0] x3 + [0 2] x4 + [0] [2 0] [2 0] [0 0] [1] p(notEmpty#) = [0 0] x1 + [0] [0 2] [0] p(prefix#) = [0 0] x1 + [0 1] x2 + [0] [0 1] [0 0] [1] p(strmatch#) = [0 0] x1 + [0 2] x2 + [0] [0 1] [1 0] [0] p(c_1) = [1 0] x1 + [1 0] x2 + [0] [0 0] [1 0] [0] p(c_2) = [0] [0] p(c_3) = [1] [2] p(c_4) = [1] [0] p(c_5) = [0] [1] p(c_6) = [1] [2] p(c_7) = [1] [0] p(c_8) = [2] [2] p(c_9) = [0] [0] p(c_10) = [0] [0] p(c_11) = [1 0] x1 + [0] [0 1] [0] p(c_12) = [1] [0] p(c_13) = [2] [2] p(c_14) = [0] [2] p(c_15) = [0] [1] p(c_16) = [2] [0] p(c_17) = [0] [0] p(c_18) = [0] [1] p(c_19) = [0] [2] p(c_20) = [1] [0] p(c_21) = [2] [0] p(c_22) = [1 0] x1 + [0] [0 0] [0] p(c_23) = [1 1] x1 + [0] [0 0] [0] p(c_24) = [2] [2] p(c_25) = [0 0] x1 + [0] [2 0] [0] Following rules are strictly oriented: prefix#(Cons(x',xs'),Cons(x,xs)) = [0 1] xs + [0 0] xs' + [1] [0 0] [0 1] [2] > [0 1] xs + [0 0] xs' + [0] [0 0] [0 1] [1] = c_11(prefix#(xs',xs)) Following rules are (at-least) weakly oriented: domatch#(patcs,Cons(x,xs),n) = [2 0] patcs + [1 3] xs + [3] [0 0] [0 1] [1] >= [2 0] patcs + [1 3] xs + [2] [0 0] [0 1] [1] = 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) = [0 0] n + [2 0] patcs + [1 2] xs + [1] [0 1] [1 0] [0 0] [0] >= [2 0] patcs + [1 1] xs + [1] [0 0] [0 0] [0] = c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [0 0] n + [2 0] patcs + [1 2] xs + [1] [0 1] [1 0] [0 0] [0] >= [2 0] patcs + [1 2] xs + [1] [0 0] [0 0] [0] = c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) **** Step 7.a:2.b:2.a:2: Assumption 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) ,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())))) 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 7.a:2.b:2.b:1: RemoveWeakSuffixes 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) ,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())))) 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W: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 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):4 -->_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:W: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:W: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:W: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)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 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))) 3: domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 2: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 4: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) **** Step 7.a:2.b:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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). ** Step 7.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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: 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[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1: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)):10 2:S:eqNatList#(Cons(x,xs),Nil()) -> c_5() 3:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 4:S:eqNatList#(Nil(),Nil()) -> c_7() 5:W: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 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):11 -->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):9 -->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):8 6:W:domatch#(Cons(x,xs),Nil(),n) -> c_2() 7:W:domatch#(Nil(),Nil(),n) -> c_3() 8: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():7 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():6 -->_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))):5 9: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():7 -->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():6 -->_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))):5 10:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():4 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():3 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():2 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):1 11:W: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)):11 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: 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))) 9: domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 8: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))) 6: domatch#(Cons(x,xs),Nil(),n) -> c_2() 7: domatch#(Nil(),Nil(),n) -> c_3() 11: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)) ** Step 7.b:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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: 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) 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)) ** Step 7.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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) - 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: eqNatList#(Cons(x,xs),Nil()) -> c_5() 3: eqNatList#(Nil(),Cons(y,ys)) -> c_6() 4: eqNatList#(Nil(),Nil()) -> c_7() The strictly oriented rules are moved into the weak component. *** Step 7.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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) - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_25) = {1} Following symbols are considered usable: {!EQ,!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [1] x1 + [3] x2 + [0] p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [0] p(False) = [1] p(Nil) = [0] p(S) = [1] x1 + [1] p(True) = [0] p(and) = [1] p(domatch) = [0] p(domatch[Ite]) = [1] x3 + [2] p(eqNatList) = [2] x1 + [1] x2 + [2] p(eqNatList[Ite]) = [2] x2 + [1] x4 + [1] p(notEmpty) = [4] p(prefix) = [2] x2 + [0] p(strmatch) = [1] x1 + [8] x2 + [0] p(!EQ#) = [1] x1 + [1] p(and#) = [2] x1 + [1] p(domatch#) = [1] x1 + [2] x2 + [1] x3 + [1] p(domatch[Ite]#) = [2] x1 + [1] x4 + [1] p(eqNatList#) = [8] x1 + [14] x2 + [2] p(eqNatList[Ite]#) = [4] x1 + [2] x2 + [14] x3 + [2] x4 + [8] x5 + [2] p(notEmpty#) = [0] p(prefix#) = [1] x2 + [1] p(strmatch#) = [1] p(c_1) = [1] x2 + [1] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [0] p(c_7) = [1] p(c_8) = [4] p(c_9) = [0] p(c_10) = [4] p(c_11) = [1] x1 + [1] p(c_12) = [0] p(c_13) = [4] x1 + [8] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] p(c_18) = [1] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] p(c_22) = [4] x1 + [1] p(c_23) = [1] p(c_24) = [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: eqNatList#(Cons(x,xs),Nil()) = [8] x + [8] xs + [2] > [1] = c_5() eqNatList#(Nil(),Cons(y,ys)) = [14] y + [14] ys + [2] > [0] = c_6() eqNatList#(Nil(),Nil()) = [2] > [1] = c_7() Following rules are (at-least) weakly oriented: eqNatList#(Cons(x,xs),Cons(y,ys)) = [8] x + [8] xs + [14] y + [14] ys + [2] >= [6] x + [8] xs + [14] y + [14] ys + [2] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) eqNatList[Ite]#(True(),y,ys,x,xs) = [2] x + [8] xs + [2] y + [14] ys + [2] >= [8] xs + [14] ys + [2] = c_25(eqNatList#(xs,ys)) !EQ(0(),0()) = [0] >= [0] = True() !EQ(0(),S(y)) = [3] y + [3] >= [1] = False() !EQ(S(x),0()) = [1] x + [1] >= [1] = False() !EQ(S(x),S(y)) = [1] x + [3] y + [4] >= [1] x + [3] y + [0] = !EQ(x,y) *** Step 7.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: 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) - 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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) - 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: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)):5 2:W:eqNatList#(Cons(x,xs),Nil()) -> c_5() 3:W:eqNatList#(Nil(),Cons(y,ys)) -> c_6() 4:W:eqNatList#(Nil(),Nil()) -> c_7() 5:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Nil(),Nil()) -> c_7():4 -->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():3 -->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():2 -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: eqNatList#(Cons(x,xs),Nil()) -> c_5() 3: eqNatList#(Nil(),Cons(y,ys)) -> c_6() 4: eqNatList#(Nil(),Nil()) -> c_7() *** Step 7.b:3.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) - 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) - 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) Consider the set of all dependency pairs 1: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) 5: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,5} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 7.b:3.b:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) - 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) - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_25) = {1} Following symbols are considered usable: {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [10] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [0] p(domatch) = [0] p(domatch[Ite]) = [0] p(eqNatList) = [1] x2 + [0] p(eqNatList[Ite]) = [1] x4 + [4] p(notEmpty) = [8] p(prefix) = [1] p(strmatch) = [1] x2 + [8] p(!EQ#) = [0] p(and#) = [2] x2 + [0] p(domatch#) = [0] p(domatch[Ite]#) = [4] x1 + [1] x2 + [8] p(eqNatList#) = [2] x1 + [4] p(eqNatList[Ite]#) = [2] x5 + [4] p(notEmpty#) = [2] x1 + [1] p(prefix#) = [2] x1 + [0] p(strmatch#) = [2] x1 + [1] p(c_1) = [1] x2 + [2] p(c_2) = [1] p(c_3) = [2] p(c_4) = [1] x1 + [12] p(c_5) = [2] p(c_6) = [0] p(c_7) = [1] p(c_8) = [1] p(c_9) = [0] p(c_10) = [0] p(c_11) = [4] x1 + [1] p(c_12) = [1] p(c_13) = [8] p(c_14) = [1] p(c_15) = [0] p(c_16) = [1] p(c_17) = [1] x1 + [2] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] p(c_21) = [2] p(c_22) = [1] p(c_23) = [8] p(c_24) = [0] p(c_25) = [1] x1 + [0] Following rules are strictly oriented: eqNatList#(Cons(x,xs),Cons(y,ys)) = [2] x + [2] xs + [24] > [2] xs + [16] = c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) Following rules are (at-least) weakly oriented: eqNatList[Ite]#(True(),y,ys,x,xs) = [2] xs + [4] >= [2] xs + [4] = c_25(eqNatList#(xs,ys)) **** Step 7.b:3.b:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) 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) - 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 7.b:3.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) 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) - 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:W: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)):2 2:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) -->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)) 2: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)) **** Step 7.b:3.b:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) - 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))