WORST_CASE(?,O(n^2))
* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
eq#3#(nil(),@x,@xs) -> c_9()
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
nub#1#(nil()) -> c_12()
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#1#(nil(),@x) -> c_15()
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
Weak DPs
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
and mark the set of starting terms.
* Step 3: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
eq#3#(nil(),@x,@xs) -> c_9()
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
nub#1#(nil()) -> c_12()
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#1#(nil(),@x) -> c_15()
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
eq#3#(nil(),@x,@xs) -> c_9()
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
nub#1#(nil()) -> c_12()
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#1#(nil(),@x) -> c_15()
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
* Step 4: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
eq#3#(nil(),@x,@xs) -> c_9()
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
nub#1#(nil()) -> c_12()
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#1#(nil(),@x) -> c_15()
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,6,7,9,12,15}
by application of
Pre({1,2,6,7,9,12,15}) = {4,5,8,10,13}.
Here rules are labelled as follows:
1: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
2: and#(@x,@y) -> c_2(#and#(@x,@y))
3: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
4: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
5: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
6: eq#2#(::(@y,@ys)) -> c_6()
7: eq#2#(nil()) -> c_7()
8: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
9: eq#3#(nil(),@x,@xs) -> c_9()
10: nub#(@l) -> c_10(nub#1#(@l))
11: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
12: nub#1#(nil()) -> c_12()
13: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
14: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
15: remove#1#(nil(),@x) -> c_15()
16: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
17: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
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: #eq#(#0(),#0()) -> c_22()
23: #eq#(#0(),#neg(@y)) -> c_23()
24: #eq#(#0(),#pos(@y)) -> c_24()
25: #eq#(#0(),#s(@y)) -> c_25()
26: #eq#(#neg(@x),#0()) -> c_26()
27: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
28: #eq#(#neg(@x),#pos(@y)) -> c_28()
29: #eq#(#pos(@x),#0()) -> c_29()
30: #eq#(#pos(@x),#neg(@y)) -> c_30()
31: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
32: #eq#(#s(@x),#0()) -> c_32()
33: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
34: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
35: #eq#(::(@x_1,@x_2),nil()) -> c_35()
36: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
37: #eq#(nil(),nil()) -> c_37()
* Step 5: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(nil(),@x,@xs) -> c_9()
nub#1#(nil()) -> c_12()
remove#1#(nil(),@x) -> c_15()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{3}
by application of
Pre({3}) = {1}.
Here rules are labelled as follows:
1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
2: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
3: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
4: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
5: nub#(@l) -> c_10(nub#1#(@l))
6: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
7: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
8: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
9: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
10: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
11: #and#(#false(),#false()) -> c_18()
12: #and#(#false(),#true()) -> c_19()
13: #and#(#true(),#false()) -> c_20()
14: #and#(#true(),#true()) -> c_21()
15: #eq#(#0(),#0()) -> c_22()
16: #eq#(#0(),#neg(@y)) -> c_23()
17: #eq#(#0(),#pos(@y)) -> c_24()
18: #eq#(#0(),#s(@y)) -> c_25()
19: #eq#(#neg(@x),#0()) -> c_26()
20: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
21: #eq#(#neg(@x),#pos(@y)) -> c_28()
22: #eq#(#pos(@x),#0()) -> c_29()
23: #eq#(#pos(@x),#neg(@y)) -> c_30()
24: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
25: #eq#(#s(@x),#0()) -> c_32()
26: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
27: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
28: #eq#(::(@x_1,@x_2),nil()) -> c_35()
29: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
30: #eq#(nil(),nil()) -> c_37()
31: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
32: and#(@x,@y) -> c_2(#and#(@x,@y))
33: eq#2#(::(@y,@ys)) -> c_6()
34: eq#2#(nil()) -> c_7()
35: eq#3#(nil(),@x,@xs) -> c_9()
36: nub#1#(nil()) -> c_12()
37: remove#1#(nil(),@x) -> c_15()
* Step 6: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#eq#(#0(),#0()) -> c_22()
#eq#(#0(),#neg(@y)) -> c_23()
#eq#(#0(),#pos(@y)) -> c_24()
#eq#(#0(),#s(@y)) -> c_25()
#eq#(#neg(@x),#0()) -> c_26()
#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_28()
#eq#(#pos(@x),#0()) -> c_29()
#eq#(#pos(@x),#neg(@y)) -> c_30()
#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_32()
#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
#eq#(::(@x_1,@x_2),nil()) -> c_35()
#eq#(nil(),::(@y_1,@y_2)) -> c_36()
#eq#(nil(),nil()) -> c_37()
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
and#(@x,@y) -> c_2(#and#(@x,@y))
eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
eq#2#(::(@y,@ys)) -> c_6()
eq#2#(nil()) -> c_7()
eq#3#(nil(),@x,@xs) -> c_9()
nub#1#(nil()) -> c_12()
remove#1#(nil(),@x) -> c_15()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
-->_1 eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)):32
-->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2
2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
-->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3
-->_1 eq#3#(nil(),@x,@xs) -> c_9():35
3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
-->_1 and#(@x,@y) -> c_2(#and#(@x,@y)):31
-->_2 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):30
-->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
4:S:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5
-->_1 nub#1#(nil()) -> c_12():36
5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
-->_1 nub#(@l) -> c_10(nub#1#(@l)):4
6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7
-->_1 remove#1#(nil(),@x) -> c_15():37
7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8
-->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
10:W:#and#(#false(),#false()) -> c_18()
11:W:#and#(#false(),#true()) -> c_19()
12:W:#and#(#true(),#false()) -> c_20()
13:W:#and#(#true(),#true()) -> c_21()
14:W:#eq#(#0(),#0()) -> c_22()
15:W:#eq#(#0(),#neg(@y)) -> c_23()
16:W:#eq#(#0(),#pos(@y)) -> c_24()
17:W:#eq#(#0(),#s(@y)) -> c_25()
18:W:#eq#(#neg(@x),#0()) -> c_26()
19:W:#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_1 #eq#(nil(),nil()) -> c_37():29
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_1 #eq#(#s(@x),#0()) -> c_32():24
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_1 #eq#(#pos(@x),#0()) -> c_29():21
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_1 #eq#(#neg(@x),#0()) -> c_26():18
-->_1 #eq#(#0(),#s(@y)) -> c_25():17
-->_1 #eq#(#0(),#pos(@y)) -> c_24():16
-->_1 #eq#(#0(),#neg(@y)) -> c_23():15
-->_1 #eq#(#0(),#0()) -> c_22():14
20:W:#eq#(#neg(@x),#pos(@y)) -> c_28()
21:W:#eq#(#pos(@x),#0()) -> c_29()
22:W:#eq#(#pos(@x),#neg(@y)) -> c_30()
23:W:#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_1 #eq#(nil(),nil()) -> c_37():29
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_1 #eq#(#s(@x),#0()) -> c_32():24
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_1 #eq#(#pos(@x),#0()) -> c_29():21
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_1 #eq#(#neg(@x),#0()) -> c_26():18
-->_1 #eq#(#0(),#s(@y)) -> c_25():17
-->_1 #eq#(#0(),#pos(@y)) -> c_24():16
-->_1 #eq#(#0(),#neg(@y)) -> c_23():15
-->_1 #eq#(#0(),#0()) -> c_22():14
24:W:#eq#(#s(@x),#0()) -> c_32()
25:W:#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_1 #eq#(nil(),nil()) -> c_37():29
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_1 #eq#(#s(@x),#0()) -> c_32():24
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_1 #eq#(#pos(@x),#0()) -> c_29():21
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_1 #eq#(#neg(@x),#0()) -> c_26():18
-->_1 #eq#(#0(),#s(@y)) -> c_25():17
-->_1 #eq#(#0(),#pos(@y)) -> c_24():16
-->_1 #eq#(#0(),#neg(@y)) -> c_23():15
-->_1 #eq#(#0(),#0()) -> c_22():14
26:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
-->_3 #eq#(nil(),nil()) -> c_37():29
-->_2 #eq#(nil(),nil()) -> c_37():29
-->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_3 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_2 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_3 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_2 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_3 #eq#(#s(@x),#0()) -> c_32():24
-->_2 #eq#(#s(@x),#0()) -> c_32():24
-->_3 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_2 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_3 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_2 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_3 #eq#(#pos(@x),#0()) -> c_29():21
-->_2 #eq#(#pos(@x),#0()) -> c_29():21
-->_3 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_2 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_3 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_2 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_3 #eq#(#neg(@x),#0()) -> c_26():18
-->_2 #eq#(#neg(@x),#0()) -> c_26():18
-->_3 #eq#(#0(),#s(@y)) -> c_25():17
-->_2 #eq#(#0(),#s(@y)) -> c_25():17
-->_3 #eq#(#0(),#pos(@y)) -> c_24():16
-->_2 #eq#(#0(),#pos(@y)) -> c_24():16
-->_3 #eq#(#0(),#neg(@y)) -> c_23():15
-->_2 #eq#(#0(),#neg(@y)) -> c_23():15
-->_3 #eq#(#0(),#0()) -> c_22():14
-->_2 #eq#(#0(),#0()) -> c_22():14
-->_1 #and#(#true(),#true()) -> c_21():13
-->_1 #and#(#true(),#false()) -> c_20():12
-->_1 #and#(#false(),#true()) -> c_19():11
-->_1 #and#(#false(),#false()) -> c_18():10
27:W:#eq#(::(@x_1,@x_2),nil()) -> c_35()
28:W:#eq#(nil(),::(@y_1,@y_2)) -> c_36()
29:W:#eq#(nil(),nil()) -> c_37()
30:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y))
-->_1 #eq#(nil(),nil()) -> c_37():29
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):26
-->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25
-->_1 #eq#(#s(@x),#0()) -> c_32():24
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22
-->_1 #eq#(#pos(@x),#0()) -> c_29():21
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19
-->_1 #eq#(#neg(@x),#0()) -> c_26():18
-->_1 #eq#(#0(),#s(@y)) -> c_25():17
-->_1 #eq#(#0(),#pos(@y)) -> c_24():16
-->_1 #eq#(#0(),#neg(@y)) -> c_23():15
-->_1 #eq#(#0(),#0()) -> c_22():14
31:W:and#(@x,@y) -> c_2(#and#(@x,@y))
-->_1 #and#(#true(),#true()) -> c_21():13
-->_1 #and#(#true(),#false()) -> c_20():12
-->_1 #and#(#false(),#true()) -> c_19():11
-->_1 #and#(#false(),#false()) -> c_18():10
32:W:eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
-->_1 eq#2#(nil()) -> c_7():34
-->_1 eq#2#(::(@y,@ys)) -> c_6():33
33:W:eq#2#(::(@y,@ys)) -> c_6()
34:W:eq#2#(nil()) -> c_7()
35:W:eq#3#(nil(),@x,@xs) -> c_9()
36:W:nub#1#(nil()) -> c_12()
37:W:remove#1#(nil(),@x) -> c_15()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
36: nub#1#(nil()) -> c_12()
37: remove#1#(nil(),@x) -> c_15()
35: eq#3#(nil(),@x,@xs) -> c_9()
30: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
26: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
25: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y))
23: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y))
19: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y))
14: #eq#(#0(),#0()) -> c_22()
15: #eq#(#0(),#neg(@y)) -> c_23()
16: #eq#(#0(),#pos(@y)) -> c_24()
17: #eq#(#0(),#s(@y)) -> c_25()
18: #eq#(#neg(@x),#0()) -> c_26()
20: #eq#(#neg(@x),#pos(@y)) -> c_28()
21: #eq#(#pos(@x),#0()) -> c_29()
22: #eq#(#pos(@x),#neg(@y)) -> c_30()
24: #eq#(#s(@x),#0()) -> c_32()
27: #eq#(::(@x_1,@x_2),nil()) -> c_35()
28: #eq#(nil(),::(@y_1,@y_2)) -> c_36()
29: #eq#(nil(),nil()) -> c_37()
31: and#(@x,@y) -> c_2(#and#(@x,@y))
10: #and#(#false(),#false()) -> c_18()
11: #and#(#false(),#true()) -> c_19()
12: #and#(#true(),#false()) -> c_20()
13: #and#(#true(),#true()) -> c_21()
32: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2))
33: eq#2#(::(@y,@ys)) -> c_6()
34: eq#2#(nil()) -> c_7()
* Step 7: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
-->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2
2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
-->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3
3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys))
-->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
4:S:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5
5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
-->_1 nub#(@l) -> c_10(nub#1#(@l)):4
6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7
7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8
-->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
* Step 8: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4
,#and#/2,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#
,nub#1#,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
Problem (S)
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4
,#and#/2,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#
,nub#1#,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
** Step 8.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
Consider the set of all dependency pairs
1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
2: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
3: eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
4: nub#(@l) -> c_10(nub#1#(@l))
5: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
6: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
7: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
8: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
9: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** Step 8.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_8) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1,2},
uargs(c_13) = {1},
uargs(c_14) = {1,2},
uargs(c_16) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
{remove,remove#1,remove#2,#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#,remove#,remove#1#
,remove#2#}
TcT has computed the following interpretation:
p(#0) = 1
p(#and) = 1
p(#eq) = x1 + x2^2
p(#equal) = 1 + x1*x2
p(#false) = 0
p(#neg) = 1
p(#pos) = 1 + x1
p(#s) = x1
p(#true) = 1
p(::) = 1 + x1 + x2
p(and) = 1
p(eq) = 0
p(eq#1) = 0
p(eq#2) = 0
p(eq#3) = 1 + x1 + x1^2
p(nil) = 0
p(nub) = 0
p(nub#1) = 0
p(remove) = x2
p(remove#1) = x1
p(remove#2) = 1 + x3 + x4
p(#and#) = 0
p(#eq#) = 0
p(#equal#) = 0
p(and#) = 0
p(eq#) = 1 + x1*x2
p(eq#1#) = x1*x2
p(eq#2#) = 0
p(eq#3#) = x1 + x1*x3
p(nub#) = x1^2
p(nub#1#) = x1^2
p(remove#) = x1*x2 + x2
p(remove#1#) = x1 + x1*x2
p(remove#2#) = x2*x4 + x3 + x4
p(c_1) = 0
p(c_2) = 0
p(c_3) = x1
p(c_4) = x1
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = x1
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1 + x2
p(c_12) = 0
p(c_13) = x1
p(c_14) = x1 + x2
p(c_15) = 0
p(c_16) = x1
p(c_17) = x1
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
p(c_26) = 0
p(c_27) = 0
p(c_28) = 0
p(c_29) = 0
p(c_30) = 0
p(c_31) = 0
p(c_32) = 0
p(c_33) = 0
p(c_34) = 0
p(c_35) = 0
p(c_36) = 0
p(c_37) = 0
Following rules are strictly oriented:
eq#(@l1,@l2) = 1 + @l1*@l2
> @l1*@l2
= c_3(eq#1#(@l1,@l2))
Following rules are (at-least) weakly oriented:
eq#1#(::(@x,@xs),@l2) = @l2 + @l2*@x + @l2*@xs
>= @l2 + @l2*@xs
= c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) = 1 + @xs + @xs*@y + @xs*@ys + @y + @ys
>= 1 + @xs*@ys
= c_8(eq#(@xs,@ys))
nub#(@l) = @l^2
>= @l^2
= c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) = 1 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2
>= @x*@xs + @xs + @xs^2
= c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) = @l + @l*@x
>= @l + @l*@x
= c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) = 1 + @x + @x*@y + @x*@ys + @y + @ys
>= 1 + @x*@y + @x*@ys + @y + @ys
= c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) = @x*@ys + @y + @ys
>= @x*@ys + @ys
= c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) = @x*@ys + @y + @ys
>= @x*@ys + @ys
= c_17(remove#(@x,@ys))
remove(@x,@l) = @l
>= @l
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = 1 + @y + @ys
>= 1 + @y + @ys
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = 0
>= 0
= nil()
remove#2(#false(),@x,@y,@ys) = 1 + @y + @ys
>= 1 + @y + @ys
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = 1 + @y + @ys
>= @ys
= remove(@x,@ys)
*** Step 8.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 8.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
-->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2
2:W:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
-->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)):3
3:W:eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
-->_1 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
4:W:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5
5:W:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
-->_1 nub#(@l) -> c_10(nub#1#(@l)):4
6:W:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7
7:W:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8
-->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1
8:W:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
9:W:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: nub#(@l) -> c_10(nub#1#(@l))
5: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
6: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
9: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
7: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
8: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
3: eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
2: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
*** Step 8.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 8.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak DPs:
eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):2
2:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
-->_1 nub#(@l) -> c_10(nub#1#(@l)):1
3:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):4
4:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
-->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):7
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):6
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):5
5:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
6:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
7:W:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
-->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):8
8:W:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
-->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)):9
9:W:eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
-->_1 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):7
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2))
9: eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys))
8: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs))
** Step 8.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):2
2:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
-->_1 nub#(@l) -> c_10(nub#1#(@l)):1
3:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):4
4:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y))
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):6
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):5
5:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
6:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
** Step 8.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
5: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
6: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
Consider the set of all dependency pairs
1: nub#(@l) -> c_10(nub#1#(@l))
2: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
3: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
4: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
5: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
6: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{2,5,6}
These cover all (indirect) predecessors of dependency pairs
{1,2,3,4,5,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** Step 8.b:3.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_10) = {1},
uargs(c_11) = {1,2},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_16) = {1},
uargs(c_17) = {1}
Following symbols are considered usable:
{#and,and,eq,eq#1,eq#2,eq#3,remove,remove#1,remove#2,#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#
,nub#1#,remove#,remove#1#,remove#2#}
TcT has computed the following interpretation:
p(#0) = 0
p(#and) = x2
p(#eq) = 0
p(#equal) = 0
p(#false) = 1
p(#neg) = 0
p(#pos) = 0
p(#s) = 0
p(#true) = 1
p(::) = 1 + x1 + x2
p(and) = x2
p(eq) = x2
p(eq#1) = x2
p(eq#2) = x1
p(eq#3) = x1
p(nil) = 1
p(nub) = 0
p(nub#1) = 0
p(remove) = x2
p(remove#1) = x1
p(remove#2) = 1 + x3 + x4
p(#and#) = 0
p(#eq#) = 0
p(#equal#) = 0
p(and#) = 0
p(eq#) = 0
p(eq#1#) = 0
p(eq#2#) = 0
p(eq#3#) = 0
p(nub#) = 1 + x1 + x1^2
p(nub#1#) = 1 + x1 + x1^2
p(remove#) = x1*x2 + x1^2 + x2
p(remove#1#) = x1 + x1*x2 + x2^2
p(remove#2#) = x1 + x2*x4 + x2^2 + x4
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = 0
p(c_9) = 0
p(c_10) = x1
p(c_11) = x1 + x2
p(c_12) = 0
p(c_13) = x1
p(c_14) = 1 + x1
p(c_15) = 0
p(c_16) = x1
p(c_17) = x1
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
p(c_26) = 0
p(c_27) = 0
p(c_28) = 0
p(c_29) = 0
p(c_30) = 0
p(c_31) = 0
p(c_32) = 0
p(c_33) = 0
p(c_34) = 0
p(c_35) = 0
p(c_36) = 0
p(c_37) = 0
Following rules are strictly oriented:
nub#1#(::(@x,@xs)) = 3 + 3*@x + 2*@x*@xs + @x^2 + 3*@xs + @xs^2
> 1 + @x*@xs + @x^2 + 2*@xs + @xs^2
= c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#2#(#false(),@x,@y,@ys) = 1 + @x*@ys + @x^2 + @ys
> @x*@ys + @x^2 + @ys
= c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) = 1 + @x*@ys + @x^2 + @ys
> @x*@ys + @x^2 + @ys
= c_17(remove#(@x,@ys))
Following rules are (at-least) weakly oriented:
nub#(@l) = 1 + @l + @l^2
>= 1 + @l + @l^2
= c_10(nub#1#(@l))
remove#(@x,@l) = @l + @l*@x + @x^2
>= @l + @l*@x + @x^2
= c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) = 1 + @x + @x*@y + @x*@ys + @x^2 + @y + @ys
>= 1 + @x*@ys + @x^2 + @y + @ys
= c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
#and(#false(),#false()) = 1
>= 1
= #false()
#and(#false(),#true()) = 1
>= 1
= #false()
#and(#true(),#false()) = 1
>= 1
= #false()
#and(#true(),#true()) = 1
>= 1
= #true()
and(@x,@y) = @y
>= @y
= #and(@x,@y)
eq(@l1,@l2) = @l2
>= @l2
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = @l2
>= @l2
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = @l2
>= @l2
= eq#2(@l2)
eq#2(::(@y,@ys)) = 1 + @y + @ys
>= 1
= #false()
eq#2(nil()) = 1
>= 1
= #true()
eq#3(::(@y,@ys),@x,@xs) = 1 + @y + @ys
>= @ys
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = 1
>= 1
= #false()
remove(@x,@l) = @l
>= @l
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = 1 + @y + @ys
>= 1 + @y + @ys
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = 1
>= 1
= nil()
remove#2(#false(),@x,@y,@ys) = 1 + @y + @ys
>= 1 + @y + @ys
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = 1 + @y + @ys
>= @ys
= remove(@x,@ys)
*** Step 8.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
nub#(@l) -> c_10(nub#1#(@l))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
- Weak DPs:
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 8.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
nub#(@l) -> c_10(nub#1#(@l))
nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
remove#(@x,@l) -> c_13(remove#1#(@l,@x))
remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:nub#(@l) -> c_10(nub#1#(@l))
-->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):2
2:W:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
-->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
-->_1 nub#(@l) -> c_10(nub#1#(@l)):1
3:W:remove#(@x,@l) -> c_13(remove#1#(@l,@x))
-->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)):4
4:W:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
-->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):6
-->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):5
5:W:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
6:W:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
-->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: nub#(@l) -> c_10(nub#1#(@l))
2: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs))
3: remove#(@x,@l) -> c_13(remove#1#(@l,@x))
6: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys))
4: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys))
5: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys))
*** Step 8.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2
,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2
,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0
,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0
,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0
,c_37/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#
,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))