WORST_CASE(?,O(n^2)) * Step 1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {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) = [4] p(Cons) = [1] x2 + [0] p(False) = [0] p(Nil) = [0] p(S) = [1] p(True) = [0] p(and) = [4] x1 + [4] x2 + [0] p(domatch) = [0] p(domatch[Ite]) = [4] x1 + [0] p(eqNatList) = [2] p(eqNatList[Ite]) = [2] x1 + [2] p(notEmpty) = [3] p(prefix) = [0] p(strmatch) = [0] Following rules are strictly oriented: eqNatList(Cons(x,xs),Nil()) = [2] > [0] = False() eqNatList(Nil(),Cons(y,ys)) = [2] > [0] = False() eqNatList(Nil(),Nil()) = [2] > [0] = True() notEmpty(Cons(x,xs)) = [3] > [0] = True() notEmpty(Nil()) = [3] > [0] = False() Following rules are (at-least) weakly oriented: !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() domatch(patcs,Cons(x,xs),n) = [0] >= [0] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) = [0] >= [0] = Nil() domatch(Nil(),Nil(),n) = [0] >= [0] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [0] >= [0] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [0] >= [0] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [2] >= [2] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList[Ite](False(),y,ys,x,xs) = [2] >= [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [2] >= [2] = eqNatList(xs,ys) 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() strmatch(patstr,str) = [0] >= [0] = domatch(patstr,str,Nil()) * Step 2: WeightGap 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) 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(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() - 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [3] p(0) = [0] p(Cons) = [1] x2 + [1] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [1] p(and) = [1] x1 + [1] x2 + [0] p(domatch) = [3] x2 + [2] x3 + [0] p(domatch[Ite]) = [1] x1 + [3] x3 + [1] p(eqNatList) = [3] x1 + [6] x2 + [1] p(eqNatList[Ite]) = [1] x1 + [6] x3 + [3] x5 + [4] p(notEmpty) = [2] x1 + [0] p(prefix) = [0] p(strmatch) = [2] x1 + [4] x2 + [1] Following rules are strictly oriented: eqNatList(Cons(x,xs),Cons(y,ys)) = [3] xs + [6] ys + [10] > [3] xs + [6] ys + [7] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) strmatch(patstr,str) = [2] patstr + [4] str + [1] > [3] str + [0] = domatch(patstr,str,Nil()) Following rules are (at-least) weakly oriented: !EQ(0(),0()) = [3] >= [1] = True() !EQ(0(),S(y)) = [3] >= [0] = False() !EQ(S(x),0()) = [3] >= [0] = False() !EQ(S(x),S(y)) = [3] >= [3] = !EQ(x,y) and(False(),False()) = [0] >= [0] = False() and(False(),True()) = [1] >= [0] = False() and(True(),False()) = [1] >= [0] = False() and(True(),True()) = [2] >= [1] = True() domatch(patcs,Cons(x,xs),n) = [2] n + [3] xs + [3] >= [3] xs + [4] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) = [2] n + [0] >= [0] = Nil() domatch(Nil(),Nil(),n) = [2] n + [0] >= [1] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [3] xs + [4] >= [3] xs + [4] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [3] xs + [5] >= [3] xs + [5] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Nil()) = [3] xs + [4] >= [0] = False() eqNatList(Nil(),Cons(y,ys)) = [6] ys + [7] >= [0] = False() eqNatList(Nil(),Nil()) = [1] >= [1] = True() eqNatList[Ite](False(),y,ys,x,xs) = [3] xs + [6] ys + [4] >= [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [3] xs + [6] ys + [5] >= [3] xs + [6] ys + [1] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [2] xs + [2] >= [1] = True() notEmpty(Nil()) = [0] >= [0] = False() prefix(Cons(x,xs),Nil()) = [0] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [0] >= [3] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [0] >= [1] = True() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap 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()) prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) -> True() - 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(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() 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} / {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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [3] p(0) = [4] p(Cons) = [1] x2 + [4] p(False) = [3] p(Nil) = [2] p(S) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [6] p(domatch) = [0] p(domatch[Ite]) = [1] x1 + [4] p(eqNatList) = [1] x2 + [2] p(eqNatList[Ite]) = [1] x1 + [1] x3 + [2] p(notEmpty) = [3] x1 + [0] p(prefix) = [2] p(strmatch) = [4] x1 + [2] x2 + [0] Following rules are strictly oriented: prefix(Nil(),cs) = [2] > [0] = True() Following rules are (at-least) weakly oriented: !EQ(0(),0()) = [3] >= [0] = True() !EQ(0(),S(y)) = [3] >= [3] = False() !EQ(S(x),0()) = [3] >= [3] = False() !EQ(S(x),S(y)) = [3] >= [3] = !EQ(x,y) and(False(),False()) = [12] >= [3] = False() and(False(),True()) = [9] >= [3] = False() and(True(),False()) = [9] >= [3] = False() and(True(),True()) = [6] >= [0] = True() domatch(patcs,Cons(x,xs),n) = [0] >= [6] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) = [0] >= [2] = Nil() domatch(Nil(),Nil(),n) = [0] >= [6] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [7] >= [0] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [4] >= [4] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [1] ys + [6] >= [1] ys + [5] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) = [4] >= [3] = False() eqNatList(Nil(),Cons(y,ys)) = [1] ys + [6] >= [3] = False() eqNatList(Nil(),Nil()) = [4] >= [0] = True() eqNatList[Ite](False(),y,ys,x,xs) = [1] ys + [5] >= [3] = False() eqNatList[Ite](True(),y,ys,x,xs) = [1] ys + [2] >= [1] ys + [2] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [3] xs + [12] >= [0] = True() notEmpty(Nil()) = [6] >= [3] = False() prefix(Cons(x,xs),Nil()) = [2] >= [3] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [2] >= [11] = and(!EQ(x',x),prefix(xs',xs)) strmatch(patstr,str) = [4] patstr + [2] str + [0] >= [0] = domatch(patstr,str,Nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: NaturalMI 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()) prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),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() 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(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} / {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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {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] x2 + [0] p(False) = [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(True) = [0] p(and) = [4] x1 + [4] x2 + [0] p(domatch) = [2] p(domatch[Ite]) = [4] x1 + [2] p(eqNatList) = [4] x1 + [1] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [1] x3 + [4] x5 + [0] p(notEmpty) = [4] x1 + [0] p(prefix) = [0] p(strmatch) = [4] x1 + [4] x2 + [2] Following rules are strictly oriented: domatch(Cons(x,xs),Nil(),n) = [2] > [0] = Nil() domatch(Nil(),Nil(),n) = [2] > [0] = Cons(n,Nil()) Following rules are (at-least) weakly oriented: !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() domatch(patcs,Cons(x,xs),n) = [2] >= [2] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch[Ite](False(),patcs,Cons(x,xs),n) = [2] >= [2] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [2] >= [2] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [4] xs + [1] ys + [0] >= [4] xs + [1] ys + [0] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) = [4] xs + [0] >= [0] = False() eqNatList(Nil(),Cons(y,ys)) = [1] ys + [0] >= [0] = False() eqNatList(Nil(),Nil()) = [0] >= [0] = True() eqNatList[Ite](False(),y,ys,x,xs) = [4] xs + [1] ys + [0] >= [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [4] xs + [1] ys + [0] >= [4] xs + [1] ys + [0] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [4] xs + [0] >= [0] = True() notEmpty(Nil()) = [0] >= [0] = False() 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() strmatch(patstr,str) = [4] patstr + [4] str + [2] >= [2] = domatch(patstr,str,Nil()) * Step 5: WeightGap 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) prefix(Cons(x,xs),Nil()) -> False() prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),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() 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(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} / {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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(!EQ) = [0] p(0) = [4] p(Cons) = [1] x2 + [0] p(False) = [0] p(Nil) = [2] p(S) = [0] p(True) = [0] p(and) = [1] x1 + [1] x2 + [4] p(domatch) = [1] x3 + [4] p(domatch[Ite]) = [1] x1 + [6] p(eqNatList) = [1] x2 + [0] p(eqNatList[Ite]) = [1] x1 + [1] x3 + [0] p(notEmpty) = [4] x1 + [4] p(prefix) = [2] p(strmatch) = [1] x1 + [1] x2 + [7] Following rules are strictly oriented: prefix(Cons(x,xs),Nil()) = [2] > [0] = False() Following rules are (at-least) weakly oriented: !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()) = [4] >= [0] = False() and(False(),True()) = [4] >= [0] = False() and(True(),False()) = [4] >= [0] = False() and(True(),True()) = [4] >= [0] = True() domatch(patcs,Cons(x,xs),n) = [1] n + [4] >= [8] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) = [1] n + [4] >= [2] = Nil() domatch(Nil(),Nil(),n) = [1] n + [4] >= [2] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [6] >= [6] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [6] >= [6] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [1] ys + [0] >= [1] ys + [0] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) = [2] >= [0] = False() eqNatList(Nil(),Cons(y,ys)) = [1] ys + [0] >= [0] = False() eqNatList(Nil(),Nil()) = [2] >= [0] = True() eqNatList[Ite](False(),y,ys,x,xs) = [1] ys + [0] >= [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [1] ys + [0] >= [1] ys + [0] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [4] xs + [4] >= [0] = True() notEmpty(Nil()) = [12] >= [0] = False() prefix(Cons(x',xs'),Cons(x,xs)) = [2] >= [6] = and(!EQ(x',x),prefix(xs',xs)) prefix(Nil(),cs) = [2] >= [0] = True() strmatch(patstr,str) = [1] patstr + [1] str + [7] >= [6] = domatch(patstr,str,Nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: NaturalMI 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) prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),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() 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(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} / {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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {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] x2 + [4] p(False) = [0] p(Nil) = [2] p(S) = [4] p(True) = [0] p(and) = [4] x1 + [4] x2 + [0] p(domatch) = [2] x2 + [3] p(domatch[Ite]) = [4] x1 + [2] x3 + [0] p(eqNatList) = [3] p(eqNatList[Ite]) = [4] x1 + [3] p(notEmpty) = [2] p(prefix) = [0] p(strmatch) = [2] x2 + [4] Following rules are strictly oriented: domatch(patcs,Cons(x,xs),n) = [2] xs + [11] > [2] xs + [8] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) Following rules are (at-least) weakly oriented: !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() domatch(Cons(x,xs),Nil(),n) = [7] >= [2] = Nil() domatch(Nil(),Nil(),n) = [7] >= [6] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [2] xs + [8] >= [2] xs + [3] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [2] xs + [8] >= [2] xs + [7] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [3] >= [3] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) = [3] >= [0] = False() eqNatList(Nil(),Cons(y,ys)) = [3] >= [0] = False() eqNatList(Nil(),Nil()) = [3] >= [0] = True() eqNatList[Ite](False(),y,ys,x,xs) = [3] >= [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [3] >= [3] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [2] >= [0] = True() notEmpty(Nil()) = [2] >= [0] = False() 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() strmatch(patstr,str) = [2] str + [4] >= [2] str + [3] = domatch(patstr,str,Nil()) * Step 7: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),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() 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(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} / {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: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(and) = {1,2}, uargs(domatch[Ite]) = {1}, uargs(eqNatList[Ite]) = {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] [2] p(0) = [0] [4] p(Cons) = [1 1] x2 + [0] [0 1] [4] p(False) = [0] [0] p(Nil) = [0] [4] p(S) = [0 1] x1 + [0] [0 1] [0] p(True) = [0] [1] p(and) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] p(domatch) = [4 2] x2 + [4] [0 1] [4] p(domatch[Ite]) = [1 4] x1 + [4 1] x3 + [0] [0 1] [0 1] [3] p(eqNatList) = [5 2] x1 + [0 0] x2 + [3] [0 0] [0 1] [1] p(eqNatList[Ite]) = [2 1] x1 + [0 0] x3 + [5 2] x5 + [2] [0 0] [0 1] [0 0] [5] p(notEmpty) = [0 0] x1 + [0] [1 1] [0] p(prefix) = [0 1] x2 + [0] [0 0] [1] p(strmatch) = [0 0] x1 + [4 3] x2 + [4] [0 4] [1 1] [4] Following rules are strictly oriented: prefix(Cons(x',xs'),Cons(x,xs)) = [0 1] xs + [4] [0 0] [1] > [0 1] xs + [0] [0 0] [1] = and(!EQ(x',x),prefix(xs',xs)) Following rules are (at-least) weakly oriented: !EQ(0(),0()) = [0] [2] >= [0] [1] = True() !EQ(0(),S(y)) = [0] [2] >= [0] [0] = False() !EQ(S(x),0()) = [0] [2] >= [0] [0] = False() !EQ(S(x),S(y)) = [0] [2] >= [0] [2] = !EQ(x,y) and(False(),False()) = [0] [0] >= [0] [0] = False() and(False(),True()) = [0] [1] >= [0] [0] = False() and(True(),False()) = [0] [0] >= [0] [0] = False() and(True(),True()) = [0] [1] >= [0] [1] = True() domatch(patcs,Cons(x,xs),n) = [4 6] xs + [12] [0 1] [8] >= [4 6] xs + [12] [0 1] [8] = domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n) domatch(Cons(x,xs),Nil(),n) = [12] [8] >= [0] [4] = Nil() domatch(Nil(),Nil(),n) = [12] [8] >= [4] [8] = Cons(n,Nil()) domatch[Ite](False(),patcs,Cons(x,xs),n) = [4 5] xs + [4] [0 1] [7] >= [4 2] xs + [4] [0 1] [4] = domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))) domatch[Ite](True(),patcs,Cons(x,xs),n) = [4 5] xs + [8] [0 1] [8] >= [4 3] xs + [8] [0 1] [8] = Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))) eqNatList(Cons(x,xs),Cons(y,ys)) = [5 7] xs + [0 0] ys + [11] [0 0] [0 1] [5] >= [5 2] xs + [0 0] ys + [4] [0 0] [0 1] [5] = eqNatList[Ite](!EQ(x,y),y,ys,x,xs) eqNatList(Cons(x,xs),Nil()) = [5 7] xs + [11] [0 0] [5] >= [0] [0] = False() eqNatList(Nil(),Cons(y,ys)) = [0 0] ys + [11] [0 1] [5] >= [0] [0] = False() eqNatList(Nil(),Nil()) = [11] [5] >= [0] [1] = True() eqNatList[Ite](False(),y,ys,x,xs) = [5 2] xs + [0 0] ys + [2] [0 0] [0 1] [5] >= [0] [0] = False() eqNatList[Ite](True(),y,ys,x,xs) = [5 2] xs + [0 0] ys + [3] [0 0] [0 1] [5] >= [5 2] xs + [0 0] ys + [3] [0 0] [0 1] [1] = eqNatList(xs,ys) notEmpty(Cons(x,xs)) = [0 0] xs + [0] [1 2] [4] >= [0] [1] = True() notEmpty(Nil()) = [0] [4] >= [0] [0] = False() prefix(Cons(x,xs),Nil()) = [4] [1] >= [0] [0] = False() prefix(Nil(),cs) = [0 1] cs + [0] [0 0] [1] >= [0] [1] = True() strmatch(patstr,str) = [0 0] patstr + [4 3] str + [4] [0 4] [1 1] [4] >= [4 2] str + [4] [0 1] [4] = domatch(patstr,str,Nil()) * Step 8: 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() 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} / {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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))