WORST_CASE(Omega(n^1),O(n^2))
* Step 1: Sum WORST_CASE(Omega(n^1),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:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ 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:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
prefix(y,u){y -> Cons(x,y),u -> Cons(z,u)} =
prefix(Cons(x,y),Cons(z,u)) ->^+ and(!EQ(x,z),prefix(y,u))
= C[prefix(y,u) = prefix(y,u){}]
** Step 1.b: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 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
notEmpty#(Cons(x,xs)) -> c_8()
notEmpty#(Nil()) -> c_9()
prefix#(Cons(x,xs),Nil()) -> c_10()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
prefix#(Nil(),cs) -> c_12()
strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
- Weak DPs:
!EQ#(0(),0()) -> c_14()
!EQ#(0(),S(y)) -> c_15()
!EQ#(S(x),0()) -> c_16()
!EQ#(S(x),S(y)) -> c_17(!EQ#(x,y))
and#(False(),False()) -> c_18()
and#(False(),True()) -> c_19()
and#(True(),False()) -> c_20()
and#(True(),True()) -> c_21()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch(Cons(x,xs),Nil(),n) -> Nil()
domatch(Nil(),Nil(),n) -> Cons(n,Nil())
domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs)
eqNatList(Cons(x,xs),Nil()) -> False()
eqNatList(Nil(),Cons(y,ys)) -> False()
eqNatList(Nil(),Nil()) -> True()
eqNatList[Ite](False(),y,ys,x,xs) -> False()
eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
strmatch(patstr,str) -> domatch(patstr,str,Nil())
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{8,9,10,12}
by application of
Pre({8,9,10,12}) = {1,11}.
Here rules are labelled as follows:
1: domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
2: domatch#(Cons(x,xs),Nil(),n) -> c_2()
3: domatch#(Nil(),Nil(),n) -> c_3()
4: eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
5: eqNatList#(Cons(x,xs),Nil()) -> c_5()
6: eqNatList#(Nil(),Cons(y,ys)) -> c_6()
7: eqNatList#(Nil(),Nil()) -> c_7()
8: notEmpty#(Cons(x,xs)) -> c_8()
9: notEmpty#(Nil()) -> c_9()
10: prefix#(Cons(x,xs),Nil()) -> c_10()
11: prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
12: prefix#(Nil(),cs) -> c_12()
13: strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
14: !EQ#(0(),0()) -> c_14()
15: !EQ#(0(),S(y)) -> c_15()
16: !EQ#(S(x),0()) -> c_16()
17: !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y))
18: and#(False(),False()) -> c_18()
19: and#(False(),True()) -> c_19()
20: and#(True(),False()) -> c_20()
21: and#(True(),True()) -> c_21()
22: domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
23: domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
24: eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24()
25: eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
- Weak DPs:
!EQ#(0(),0()) -> c_14()
!EQ#(0(),S(y)) -> c_15()
!EQ#(S(x),0()) -> c_16()
!EQ#(S(x),S(y)) -> c_17(!EQ#(x,y))
and#(False(),False()) -> c_18()
and#(False(),True()) -> c_19()
and#(True(),False()) -> c_20()
and#(True(),True()) -> c_21()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
notEmpty#(Cons(x,xs)) -> c_8()
notEmpty#(Nil()) -> c_9()
prefix#(Cons(x,xs),Nil()) -> c_10()
prefix#(Nil(),cs) -> c_12()
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch(Cons(x,xs),Nil(),n) -> Nil()
domatch(Nil(),Nil(),n) -> Cons(n,Nil())
domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs)
eqNatList(Cons(x,xs),Nil()) -> False()
eqNatList(Nil(),Cons(y,ys)) -> False()
eqNatList(Nil(),Nil()) -> True()
eqNatList[Ite](False(),y,ys,x,xs) -> False()
eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
strmatch(patstr,str) -> domatch(patstr,str,Nil())
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
-->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):19
-->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):18
-->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8
-->_2 prefix#(Nil(),cs) -> c_12():25
2:S:domatch#(Cons(x,xs),Nil(),n) -> c_2()
3:S:domatch#(Nil(),Nil(),n) -> c_3()
4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
-->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):21
-->_2 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13
-->_1 eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24():20
-->_2 !EQ#(S(x),0()) -> c_16():12
-->_2 !EQ#(0(),S(y)) -> c_15():11
-->_2 !EQ#(0(),0()) -> c_14():10
5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5()
6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6()
7:S:eqNatList#(Nil(),Nil()) -> c_7()
8:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
-->_2 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13
-->_3 prefix#(Nil(),cs) -> c_12():25
-->_3 prefix#(Cons(x,xs),Nil()) -> c_10():24
-->_1 and#(True(),True()) -> c_21():17
-->_1 and#(True(),False()) -> c_20():16
-->_1 and#(False(),True()) -> c_19():15
-->_1 and#(False(),False()) -> c_18():14
-->_2 !EQ#(S(x),0()) -> c_16():12
-->_2 !EQ#(0(),S(y)) -> c_15():11
-->_2 !EQ#(0(),0()) -> c_14():10
-->_3 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8
9:S:strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
10:W:!EQ#(0(),0()) -> c_14()
11:W:!EQ#(0(),S(y)) -> c_15()
12:W:!EQ#(S(x),0()) -> c_16()
13:W:!EQ#(S(x),S(y)) -> c_17(!EQ#(x,y))
-->_1 !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y)):13
-->_1 !EQ#(S(x),0()) -> c_16():12
-->_1 !EQ#(0(),S(y)) -> c_15():11
-->_1 !EQ#(0(),0()) -> c_14():10
14:W:and#(False(),False()) -> c_18()
15:W:and#(False(),True()) -> c_19()
16:W:and#(True(),False()) -> c_20()
17:W:and#(True(),True()) -> c_21()
18:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
19:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
20:W:eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24()
21:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
-->_1 eqNatList#(Nil(),Nil()) -> c_7():7
-->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6
-->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5
-->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)):4
22:W:notEmpty#(Cons(x,xs)) -> c_8()
23:W:notEmpty#(Nil()) -> c_9()
24:W:prefix#(Cons(x,xs),Nil()) -> c_10()
25:W:prefix#(Nil(),cs) -> c_12()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
23: notEmpty#(Nil()) -> c_9()
22: notEmpty#(Cons(x,xs)) -> c_8()
20: eqNatList[Ite]#(False(),y,ys,x,xs) -> c_24()
14: and#(False(),False()) -> c_18()
15: and#(False(),True()) -> c_19()
16: and#(True(),False()) -> c_20()
17: and#(True(),True()) -> c_21()
24: prefix#(Cons(x,xs),Nil()) -> c_10()
25: prefix#(Nil(),cs) -> c_12()
13: !EQ#(S(x),S(y)) -> c_17(!EQ#(x,y))
10: !EQ#(0(),0()) -> c_14()
11: !EQ#(0(),S(y)) -> c_15()
12: !EQ#(S(x),0()) -> c_16()
** Step 1.b:4: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
- Weak DPs:
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch(Cons(x,xs),Nil(),n) -> Nil()
domatch(Nil(),Nil(),n) -> Cons(n,Nil())
domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs)
eqNatList(Cons(x,xs),Nil()) -> False()
eqNatList(Nil(),Cons(y,ys)) -> False()
eqNatList(Nil(),Nil()) -> True()
eqNatList[Ite](False(),y,ys,x,xs) -> False()
eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
strmatch(patstr,str) -> domatch(patstr,str,Nil())
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/3,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
-->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):19
-->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):18
-->_2 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs)):8
2:S:domatch#(Cons(x,xs),Nil(),n) -> c_2()
3:S:domatch#(Nil(),Nil(),n) -> c_3()
4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y))
-->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):21
5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5()
6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6()
7:S:eqNatList#(Nil(),Nil()) -> c_7()
8:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs)),!EQ#(x',x),prefix#(xs',xs))
-->_3 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(and#(!EQ(x',x),prefix(xs',xs))
,!EQ#(x',x)
,prefix#(xs',xs)):8
9:S:strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
18:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
19:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(Nil(),Nil(),n) -> c_3():3
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():2
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
21:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
-->_1 eqNatList#(Nil(),Nil()) -> c_7():7
-->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6
-->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5
-->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs),!EQ#(x,y)):4
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
** Step 1.b:5: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
- Weak DPs:
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
domatch(patcs,Cons(x,xs),n) -> domatch[Ite](prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch(Cons(x,xs),Nil(),n) -> Nil()
domatch(Nil(),Nil(),n) -> Cons(n,Nil())
domatch[Ite](False(),patcs,Cons(x,xs),n) -> domatch(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite](True(),patcs,Cons(x,xs),n) -> Cons(n,domatch(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite](!EQ(x,y),y,ys,x,xs)
eqNatList(Cons(x,xs),Nil()) -> False()
eqNatList(Nil(),Cons(y,ys)) -> False()
eqNatList(Nil(),Nil()) -> True()
eqNatList[Ite](False(),y,ys,x,xs) -> False()
eqNatList[Ite](True(),y,ys,x,xs) -> eqNatList(xs,ys)
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
strmatch(patstr,str) -> domatch(patstr,str,Nil())
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
strmatch#(patstr,str) -> c_13(domatch#(patstr,str,Nil()))
** Step 1.b: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 1.b:7: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
- Weak DPs:
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
and a lower component
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
Further, following extension rules are added to the lower component.
domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)
eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys)
*** Step 1.b:7.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
- Weak DPs:
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs)))
-->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):3
-->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))):2
2:S:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
3:S:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
-->_1 domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
,prefix#(patcs,Cons(x,xs))):1
4:S:eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
-->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys)):8
5:S:eqNatList#(Cons(x,xs),Nil()) -> c_5()
6:S:eqNatList#(Nil(),Cons(y,ys)) -> c_6()
7:S:eqNatList#(Nil(),Nil()) -> c_7()
8:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
-->_1 eqNatList#(Nil(),Nil()) -> c_7():7
-->_1 eqNatList#(Nil(),Cons(y,ys)) -> c_6():6
-->_1 eqNatList#(Cons(x,xs),Nil()) -> c_5():5
-->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)):4
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
*** Step 1.b:7.a:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
- Weak DPs:
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(and) = {1,2},
uargs(domatch[Ite]#) = {1},
uargs(eqNatList[Ite]#) = {1},
uargs(c_1) = {1},
uargs(c_4) = {1},
uargs(c_22) = {1},
uargs(c_23) = {1},
uargs(c_25) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(!EQ) = [0]
p(0) = [0]
p(Cons) = [2]
p(False) = [0]
p(Nil) = [0]
p(S) = [1] x1 + [0]
p(True) = [0]
p(and) = [1] x1 + [1] x2 + [0]
p(domatch) = [0]
p(domatch[Ite]) = [0]
p(eqNatList) = [0]
p(eqNatList[Ite]) = [0]
p(notEmpty) = [0]
p(prefix) = [5]
p(strmatch) = [0]
p(!EQ#) = [0]
p(and#) = [0]
p(domatch#) = [0]
p(domatch[Ite]#) = [1] x1 + [1] x3 + [0]
p(eqNatList#) = [1]
p(eqNatList[Ite]#) = [1] x1 + [2]
p(notEmpty#) = [0]
p(prefix#) = [0]
p(strmatch#) = [0]
p(c_1) = [1] x1 + [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [1] x1 + [0]
p(c_23) = [1] x1 + [0]
p(c_24) = [0]
p(c_25) = [1] x1 + [1]
Following rules are strictly oriented:
domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [2]
> [0]
= c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [2]
> [0]
= c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Nil()) = [1]
> [0]
= c_5()
eqNatList#(Nil(),Cons(y,ys)) = [1]
> [0]
= c_6()
eqNatList#(Nil(),Nil()) = [1]
> [0]
= c_7()
Following rules are (at-least) weakly oriented:
domatch#(patcs,Cons(x,xs),n) = [0]
>= [7]
= c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
eqNatList#(Cons(x,xs),Cons(y,ys)) = [1]
>= [2]
= c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList[Ite]#(True(),y,ys,x,xs) = [2]
>= [2]
= c_25(eqNatList#(xs,ys))
!EQ(0(),0()) = [0]
>= [0]
= True()
!EQ(0(),S(y)) = [0]
>= [0]
= False()
!EQ(S(x),0()) = [0]
>= [0]
= False()
!EQ(S(x),S(y)) = [0]
>= [0]
= !EQ(x,y)
and(False(),False()) = [0]
>= [0]
= False()
and(False(),True()) = [0]
>= [0]
= False()
and(True(),False()) = [0]
>= [0]
= False()
and(True(),True()) = [0]
>= [0]
= True()
prefix(Cons(x,xs),Nil()) = [5]
>= [0]
= False()
prefix(Cons(x',xs'),Cons(x,xs)) = [5]
>= [5]
= and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) = [5]
>= [0]
= True()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:7.a:3: NaturalPI 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))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,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),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(c_1) = {1},
uargs(c_4) = {1},
uargs(c_22) = {1},
uargs(c_23) = {1},
uargs(c_25) = {1}
Following symbols are considered usable:
{!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#}
TcT has computed the following interpretation:
p(!EQ) = 2
p(0) = 0
p(Cons) = 4 + x1 + x2
p(False) = 0
p(Nil) = 0
p(S) = 0
p(True) = 0
p(and) = 2 + 2*x1 + 4*x2
p(domatch) = 2 + 2*x2 + x3
p(domatch[Ite]) = x2
p(eqNatList) = 1
p(eqNatList[Ite]) = x2
p(notEmpty) = 4*x1
p(prefix) = 1
p(strmatch) = 4*x2
p(!EQ#) = 1
p(and#) = 1 + 4*x2
p(domatch#) = 2
p(domatch[Ite]#) = 2
p(eqNatList#) = 3*x1
p(eqNatList[Ite]#) = 1 + 3*x5
p(notEmpty#) = 2 + 4*x1
p(prefix#) = x1
p(strmatch#) = 1
p(c_1) = x1
p(c_2) = 1
p(c_3) = 0
p(c_4) = 6 + x1
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = 0
p(c_9) = 1
p(c_10) = 0
p(c_11) = 1 + x1
p(c_12) = 0
p(c_13) = 0
p(c_14) = 1
p(c_15) = 0
p(c_16) = 0
p(c_17) = 2
p(c_18) = 1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 1
p(c_22) = x1
p(c_23) = x1
p(c_24) = 0
p(c_25) = x1
Following rules are strictly oriented:
eqNatList#(Cons(x,xs),Cons(y,ys)) = 12 + 3*x + 3*xs
> 7 + 3*xs
= c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
Following rules are (at-least) weakly oriented:
domatch#(patcs,Cons(x,xs),n) = 2
>= 2
= c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) = 2
>= 2
= c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) = 2
>= 2
= c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Nil()) = 12 + 3*x + 3*xs
>= 0
= c_5()
eqNatList#(Nil(),Cons(y,ys)) = 0
>= 0
= c_6()
eqNatList#(Nil(),Nil()) = 0
>= 0
= c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) = 1 + 3*xs
>= 3*xs
= c_25(eqNatList#(xs,ys))
*** Step 1.b:7.a:4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
- 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/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(and) = {1,2},
uargs(domatch[Ite]#) = {1},
uargs(eqNatList[Ite]#) = {1},
uargs(c_1) = {1},
uargs(c_4) = {1},
uargs(c_22) = {1},
uargs(c_23) = {1},
uargs(c_25) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(!EQ) = [0]
p(0) = [0]
p(Cons) = [1] x2 + [2]
p(False) = [0]
p(Nil) = [4]
p(S) = [1] x1 + [0]
p(True) = [0]
p(and) = [1] x1 + [1] x2 + [0]
p(domatch) = [0]
p(domatch[Ite]) = [0]
p(eqNatList) = [1] x2 + [0]
p(eqNatList[Ite]) = [1] x2 + [2] x4 + [2] x5 + [0]
p(notEmpty) = [2] x1 + [2]
p(prefix) = [0]
p(strmatch) = [4]
p(!EQ#) = [0]
p(and#) = [4] x1 + [4] x2 + [0]
p(domatch#) = [1] x2 + [1]
p(domatch[Ite]#) = [1] x1 + [1] x3 + [0]
p(eqNatList#) = [1] x2 + [0]
p(eqNatList[Ite]#) = [1] x1 + [1] x3 + [2]
p(notEmpty#) = [4] x1 + [1]
p(prefix#) = [1] x1 + [1] x2 + [2]
p(strmatch#) = [1] x1 + [2]
p(c_1) = [1] x1 + [0]
p(c_2) = [0]
p(c_3) = [1]
p(c_4) = [1] x1 + [0]
p(c_5) = [1]
p(c_6) = [2]
p(c_7) = [0]
p(c_8) = [1]
p(c_9) = [0]
p(c_10) = [1]
p(c_11) = [0]
p(c_12) = [1]
p(c_13) = [2]
p(c_14) = [0]
p(c_15) = [1]
p(c_16) = [0]
p(c_17) = [1] x1 + [0]
p(c_18) = [1]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [1]
p(c_22) = [1] x1 + [0]
p(c_23) = [1] x1 + [1]
p(c_24) = [0]
p(c_25) = [1] x1 + [2]
Following rules are strictly oriented:
domatch#(patcs,Cons(x,xs),n) = [1] xs + [3]
> [1] xs + [2]
= c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
Following rules are (at-least) weakly oriented:
domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] xs + [2]
>= [1] xs + [1]
= c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] xs + [2]
>= [1] xs + [2]
= c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) = [1] ys + [2]
>= [1] ys + [2]
= c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) = [4]
>= [1]
= c_5()
eqNatList#(Nil(),Cons(y,ys)) = [1] ys + [2]
>= [2]
= c_6()
eqNatList#(Nil(),Nil()) = [4]
>= [0]
= c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) = [1] ys + [2]
>= [1] ys + [2]
= c_25(eqNatList#(xs,ys))
!EQ(0(),0()) = [0]
>= [0]
= True()
!EQ(0(),S(y)) = [0]
>= [0]
= False()
!EQ(S(x),0()) = [0]
>= [0]
= False()
!EQ(S(x),S(y)) = [0]
>= [0]
= !EQ(x,y)
and(False(),False()) = [0]
>= [0]
= False()
and(False(),True()) = [0]
>= [0]
= False()
and(True(),False()) = [0]
>= [0]
= False()
and(True(),True()) = [0]
>= [0]
= True()
prefix(Cons(x,xs),Nil()) = [0]
>= [0]
= False()
prefix(Cons(x',xs'),Cons(x,xs)) = [0]
>= [0]
= and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) = [0]
>= [0]
= True()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:7.a:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
domatch#(patcs,Cons(x,xs),n) -> c_1(domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> c_22(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> c_23(domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> c_4(eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs))
eqNatList#(Cons(x,xs),Nil()) -> c_5()
eqNatList#(Nil(),Cons(y,ys)) -> c_6()
eqNatList#(Nil(),Nil()) -> c_7()
eqNatList[Ite]#(True(),y,ys,x,xs) -> c_25(eqNatList#(xs,ys))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 1.b:7.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
- Weak DPs:
domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)
eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys)
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:domatch#(Cons(x,xs),Nil(),n) -> c_2()
2:S:domatch#(Nil(),Nil(),n) -> c_3()
3:S:prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
-->_1 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):3
4:W:domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
-->_1 domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))):7
-->_1 domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil()))):6
5:W:domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
-->_1 prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs)):3
6:W:domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
-->_1 domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)):5
-->_1 domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n):4
-->_1 domatch#(Nil(),Nil(),n) -> c_3():2
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():1
7:W:domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
-->_1 domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs)):5
-->_1 domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n):4
-->_1 domatch#(Nil(),Nil(),n) -> c_3():2
-->_1 domatch#(Cons(x,xs),Nil(),n) -> c_2():1
8:W:eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)
-->_1 eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys):9
9:W:eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys)
-->_1 eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
8: eqNatList#(Cons(x,xs),Cons(y,ys)) -> eqNatList[Ite]#(!EQ(x,y),y,ys,x,xs)
9: eqNatList[Ite]#(True(),y,ys,x,xs) -> eqNatList#(xs,ys)
*** Step 1.b:7.b:2: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
- Weak DPs:
domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
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(c_11) = {1}
Following symbols are considered usable:
{!EQ,and,prefix,!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) = [0]
p(False) = [0]
p(Nil) = [0]
p(S) = [0]
p(True) = [0]
p(and) = [0]
p(domatch) = [0]
p(domatch[Ite]) = [1]
p(eqNatList) = [0]
p(eqNatList[Ite]) = [0]
p(notEmpty) = [0]
p(prefix) = [0]
p(strmatch) = [0]
p(!EQ#) = [0]
p(and#) = [0]
p(domatch#) = [11]
p(domatch[Ite]#) = [11]
p(eqNatList#) = [0]
p(eqNatList[Ite]#) = [0]
p(notEmpty#) = [0]
p(prefix#) = [11]
p(strmatch#) = [0]
p(c_1) = [0]
p(c_2) = [10]
p(c_3) = [11]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [0]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [0]
Following rules are strictly oriented:
domatch#(Cons(x,xs),Nil(),n) = [11]
> [10]
= c_2()
Following rules are (at-least) weakly oriented:
domatch#(patcs,Cons(x,xs),n) = [11]
>= [11]
= domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) = [11]
>= [11]
= prefix#(patcs,Cons(x,xs))
domatch#(Nil(),Nil(),n) = [11]
>= [11]
= c_3()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [11]
>= [11]
= domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [11]
>= [11]
= domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
prefix#(Cons(x',xs'),Cons(x,xs)) = [11]
>= [11]
= c_11(prefix#(xs',xs))
!EQ(0(),0()) = [0]
>= [0]
= True()
!EQ(0(),S(y)) = [0]
>= [0]
= False()
!EQ(S(x),0()) = [0]
>= [0]
= False()
!EQ(S(x),S(y)) = [0]
>= [0]
= !EQ(x,y)
and(False(),False()) = [0]
>= [0]
= False()
and(False(),True()) = [0]
>= [0]
= False()
and(True(),False()) = [0]
>= [0]
= False()
and(True(),True()) = [0]
>= [0]
= True()
prefix(Cons(x,xs),Nil()) = [0]
>= [0]
= False()
prefix(Cons(x',xs'),Cons(x,xs)) = [0]
>= [0]
= and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) = [0]
>= [0]
= True()
*** Step 1.b:7.b:3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
domatch#(Nil(),Nil(),n) -> c_3()
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
- Weak DPs:
domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(and) = {1,2},
uargs(domatch[Ite]#) = {1},
uargs(c_11) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(!EQ) = [0]
p(0) = [1]
p(Cons) = [1] x1 + [1] x2 + [1]
p(False) = [0]
p(Nil) = [0]
p(S) = [2]
p(True) = [0]
p(and) = [1] x1 + [1] x2 + [0]
p(domatch) = [1]
p(domatch[Ite]) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [4]
p(eqNatList) = [1] x1 + [1] x2 + [0]
p(eqNatList[Ite]) = [4] x3 + [1] x5 + [1]
p(notEmpty) = [1] x1 + [1]
p(prefix) = [0]
p(strmatch) = [4] x1 + [1] x2 + [1]
p(!EQ#) = [4] x1 + [4] x2 + [1]
p(and#) = [2] x1 + [2] x2 + [0]
p(domatch#) = [3] x1 + [2] x2 + [1] x3 + [2]
p(domatch[Ite]#) = [1] x1 + [3] x2 + [2] x3 + [1] x4 + [2]
p(eqNatList#) = [4] x2 + [0]
p(eqNatList[Ite]#) = [4] x1 + [1] x2 + [1] x3 + [1] x5 + [1]
p(notEmpty#) = [1] x1 + [1]
p(prefix#) = [3] x1 + [2] x2 + [2]
p(strmatch#) = [4] x1 + [1]
p(c_1) = [1] x1 + [0]
p(c_2) = [5]
p(c_3) = [0]
p(c_4) = [1]
p(c_5) = [0]
p(c_6) = [4]
p(c_7) = [2]
p(c_8) = [1]
p(c_9) = [1]
p(c_10) = [1]
p(c_11) = [1] x1 + [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [0]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [0]
Following rules are strictly oriented:
domatch#(Nil(),Nil(),n) = [1] n + [2]
> [0]
= c_3()
prefix#(Cons(x',xs'),Cons(x,xs)) = [2] x + [3] x' + [2] xs + [3] xs' + [7]
> [2] xs + [3] xs' + [2]
= c_11(prefix#(xs',xs))
Following rules are (at-least) weakly oriented:
domatch#(patcs,Cons(x,xs),n) = [1] n + [3] patcs + [2] x + [2] xs + [4]
>= [1] n + [3] patcs + [2] x + [2] xs + [4]
= domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) = [1] n + [3] patcs + [2] x + [2] xs + [4]
>= [3] patcs + [2] x + [2] xs + [4]
= prefix#(patcs,Cons(x,xs))
domatch#(Cons(x,xs),Nil(),n) = [1] n + [3] x + [3] xs + [5]
>= [5]
= c_2()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) = [1] n + [3] patcs + [2] x + [2] xs + [4]
>= [1] n + [3] patcs + [2] xs + [4]
= domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) = [1] n + [3] patcs + [2] x + [2] xs + [4]
>= [1] n + [3] patcs + [2] xs + [4]
= domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
!EQ(0(),0()) = [0]
>= [0]
= True()
!EQ(0(),S(y)) = [0]
>= [0]
= False()
!EQ(S(x),0()) = [0]
>= [0]
= False()
!EQ(S(x),S(y)) = [0]
>= [0]
= !EQ(x,y)
and(False(),False()) = [0]
>= [0]
= False()
and(False(),True()) = [0]
>= [0]
= False()
and(True(),False()) = [0]
>= [0]
= False()
and(True(),True()) = [0]
>= [0]
= True()
prefix(Cons(x,xs),Nil()) = [0]
>= [0]
= False()
prefix(Cons(x',xs'),Cons(x,xs)) = [0]
>= [0]
= and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) = [0]
>= [0]
= True()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:7.b:4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
domatch#(patcs,Cons(x,xs),n) -> domatch[Ite]#(prefix(patcs,Cons(x,xs)),patcs,Cons(x,xs),n)
domatch#(patcs,Cons(x,xs),n) -> prefix#(patcs,Cons(x,xs))
domatch#(Cons(x,xs),Nil(),n) -> c_2()
domatch#(Nil(),Nil(),n) -> c_3()
domatch[Ite]#(False(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
domatch[Ite]#(True(),patcs,Cons(x,xs),n) -> domatch#(patcs,xs,Cons(n,Cons(Nil(),Nil())))
prefix#(Cons(x',xs'),Cons(x,xs)) -> c_11(prefix#(xs',xs))
- Weak TRS:
!EQ(0(),0()) -> True()
!EQ(0(),S(y)) -> False()
!EQ(S(x),0()) -> False()
!EQ(S(x),S(y)) -> !EQ(x,y)
and(False(),False()) -> False()
and(False(),True()) -> False()
and(True(),False()) -> False()
and(True(),True()) -> True()
prefix(Cons(x,xs),Nil()) -> False()
prefix(Cons(x',xs'),Cons(x,xs)) -> and(!EQ(x',x),prefix(xs',xs))
prefix(Nil(),cs) -> True()
- Signature:
{!EQ/2,and/2,domatch/3,domatch[Ite]/4,eqNatList/2,eqNatList[Ite]/5,notEmpty/1,prefix/2,strmatch/2,!EQ#/2
,and#/2,domatch#/3,domatch[Ite]#/4,eqNatList#/2,eqNatList[Ite]#/5,notEmpty#/1,prefix#/2,strmatch#/2} / {0/0
,Cons/2,False/0,Nil/0,S/1,True/0,c_1/2,c_2/0,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0
,c_13/1,c_14/0,c_15/0,c_16/0,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0,c_25/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {!EQ#,and#,domatch#,domatch[Ite]#,eqNatList#
,eqNatList[Ite]#,notEmpty#,prefix#,strmatch#} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^2))