* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
#less(@x,@y) -> #cklt(#compare(@x,@y))
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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()
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0
,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert
,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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()
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0
,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert
,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#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))
#less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
and#(@x,@y) -> c_3(#and#(@x,@y))
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#1#(nil(),@x) -> c_6()
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_8()
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
isortlist#1#(nil()) -> c_11()
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#1#(nil(),@l2) -> c_14()
leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
leq#2#(nil(),@x,@xs) -> c_16()
or#(@x,@y) -> c_17(#or#(@x,@y))
Weak DPs
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#cklt#(#EQ()) -> c_22()
#cklt#(#GT()) -> c_23()
#cklt#(#LT()) -> c_24()
#compare#(#0(),#0()) -> c_25()
#compare#(#0(),#neg(@y)) -> c_26()
#compare#(#0(),#pos(@y)) -> c_27()
#compare#(#0(),#s(@y)) -> c_28()
#compare#(#neg(@x),#0()) -> c_29()
#compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_31()
#compare#(#pos(@x),#0()) -> c_32()
#compare#(#pos(@x),#neg(@y)) -> c_33()
#compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_35()
#compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
#eq#(#0(),#0()) -> c_37()
#eq#(#0(),#neg(@y)) -> c_38()
#eq#(#0(),#pos(@y)) -> c_39()
#eq#(#0(),#s(@y)) -> c_40()
#eq#(#neg(@x),#0()) -> c_41()
#eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_43()
#eq#(#pos(@x),#0()) -> c_44()
#eq#(#pos(@x),#neg(@y)) -> c_45()
#eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_47()
#eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#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_50()
#eq#(nil(),::(@y_1,@y_2)) -> c_51()
#eq#(nil(),nil()) -> c_52()
#or#(#false(),#false()) -> c_53()
#or#(#false(),#true()) -> c_54()
#or#(#true(),#false()) -> c_55()
#or#(#true(),#true()) -> c_56()
and mark the set of starting terms.
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
#less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
and#(@x,@y) -> c_3(#and#(@x,@y))
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#1#(nil(),@x) -> c_6()
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_8()
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
isortlist#1#(nil()) -> c_11()
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#1#(nil(),@l2) -> c_14()
leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
leq#2#(nil(),@x,@xs) -> c_16()
or#(@x,@y) -> c_17(#or#(@x,@y))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#cklt#(#EQ()) -> c_22()
#cklt#(#GT()) -> c_23()
#cklt#(#LT()) -> c_24()
#compare#(#0(),#0()) -> c_25()
#compare#(#0(),#neg(@y)) -> c_26()
#compare#(#0(),#pos(@y)) -> c_27()
#compare#(#0(),#s(@y)) -> c_28()
#compare#(#neg(@x),#0()) -> c_29()
#compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_31()
#compare#(#pos(@x),#0()) -> c_32()
#compare#(#pos(@x),#neg(@y)) -> c_33()
#compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_35()
#compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
#eq#(#0(),#0()) -> c_37()
#eq#(#0(),#neg(@y)) -> c_38()
#eq#(#0(),#pos(@y)) -> c_39()
#eq#(#0(),#s(@y)) -> c_40()
#eq#(#neg(@x),#0()) -> c_41()
#eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_43()
#eq#(#pos(@x),#0()) -> c_44()
#eq#(#pos(@x),#neg(@y)) -> c_45()
#eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_47()
#eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#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_50()
#eq#(nil(),::(@y_1,@y_2)) -> c_51()
#eq#(nil(),nil()) -> c_52()
#or#(#false(),#false()) -> c_53()
#or#(#false(),#true()) -> c_54()
#or#(#true(),#false()) -> c_55()
#or#(#true(),#true()) -> c_56()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#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,3,6,8,11,14,16,17}
by application of
Pre({1,2,3,6,8,11,14,16,17}) = {4,5,9,12,13,15}.
Here rules are labelled as follows:
1: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
2: #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
3: and#(@x,@y) -> c_3(#and#(@x,@y))
4: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
5: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
6: insert#1#(nil(),@x) -> c_6()
7: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
8: insert#2#(#true(),@x,@y,@ys) -> c_8()
9: isortlist#(@l) -> c_9(isortlist#1#(@l))
10: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
11: isortlist#1#(nil()) -> c_11()
12: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
13: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
14: leq#1#(nil(),@l2) -> c_14()
15: leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
16: leq#2#(nil(),@x,@xs) -> c_16()
17: or#(@x,@y) -> c_17(#or#(@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: #cklt#(#EQ()) -> c_22()
23: #cklt#(#GT()) -> c_23()
24: #cklt#(#LT()) -> c_24()
25: #compare#(#0(),#0()) -> c_25()
26: #compare#(#0(),#neg(@y)) -> c_26()
27: #compare#(#0(),#pos(@y)) -> c_27()
28: #compare#(#0(),#s(@y)) -> c_28()
29: #compare#(#neg(@x),#0()) -> c_29()
30: #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
31: #compare#(#neg(@x),#pos(@y)) -> c_31()
32: #compare#(#pos(@x),#0()) -> c_32()
33: #compare#(#pos(@x),#neg(@y)) -> c_33()
34: #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
35: #compare#(#s(@x),#0()) -> c_35()
36: #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
37: #eq#(#0(),#0()) -> c_37()
38: #eq#(#0(),#neg(@y)) -> c_38()
39: #eq#(#0(),#pos(@y)) -> c_39()
40: #eq#(#0(),#s(@y)) -> c_40()
41: #eq#(#neg(@x),#0()) -> c_41()
42: #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
43: #eq#(#neg(@x),#pos(@y)) -> c_43()
44: #eq#(#pos(@x),#0()) -> c_44()
45: #eq#(#pos(@x),#neg(@y)) -> c_45()
46: #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
47: #eq#(#s(@x),#0()) -> c_47()
48: #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
49: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
50: #eq#(::(@x_1,@x_2),nil()) -> c_50()
51: #eq#(nil(),::(@y_1,@y_2)) -> c_51()
52: #eq#(nil(),nil()) -> c_52()
53: #or#(#false(),#false()) -> c_53()
54: #or#(#false(),#true()) -> c_54()
55: #or#(#true(),#false()) -> c_55()
56: #or#(#true(),#true()) -> c_56()
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
- Weak DPs:
#and#(#false(),#false()) -> c_18()
#and#(#false(),#true()) -> c_19()
#and#(#true(),#false()) -> c_20()
#and#(#true(),#true()) -> c_21()
#cklt#(#EQ()) -> c_22()
#cklt#(#GT()) -> c_23()
#cklt#(#LT()) -> c_24()
#compare#(#0(),#0()) -> c_25()
#compare#(#0(),#neg(@y)) -> c_26()
#compare#(#0(),#pos(@y)) -> c_27()
#compare#(#0(),#s(@y)) -> c_28()
#compare#(#neg(@x),#0()) -> c_29()
#compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_31()
#compare#(#pos(@x),#0()) -> c_32()
#compare#(#pos(@x),#neg(@y)) -> c_33()
#compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_35()
#compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
#eq#(#0(),#0()) -> c_37()
#eq#(#0(),#neg(@y)) -> c_38()
#eq#(#0(),#pos(@y)) -> c_39()
#eq#(#0(),#s(@y)) -> c_40()
#eq#(#neg(@x),#0()) -> c_41()
#eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
#eq#(#neg(@x),#pos(@y)) -> c_43()
#eq#(#pos(@x),#0()) -> c_44()
#eq#(#pos(@x),#neg(@y)) -> c_45()
#eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
#eq#(#s(@x),#0()) -> c_47()
#eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#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_50()
#eq#(nil(),::(@y_1,@y_2)) -> c_51()
#eq#(nil(),nil()) -> c_52()
#equal#(@x,@y) -> c_1(#eq#(@x,@y))
#less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
#or#(#false(),#false()) -> c_53()
#or#(#false(),#true()) -> c_54()
#or#(#true(),#false()) -> c_55()
#or#(#true(),#true()) -> c_56()
and#(@x,@y) -> c_3(#and#(@x,@y))
insert#1#(nil(),@x) -> c_6()
insert#2#(#true(),@x,@y,@ys) -> c_8()
isortlist#1#(nil()) -> c_11()
leq#1#(nil(),@l2) -> c_14()
leq#2#(nil(),@x,@xs) -> c_16()
or#(@x,@y) -> c_17(#or#(@x,@y))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
-->_1 insert#1#(nil(),@x) -> c_6():51
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_8():52
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:S:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
-->_1 isortlist#1#(nil()) -> c_11():53
5:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
6:S:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
-->_1 leq#1#(nil(),@l2) -> c_14():54
7:S:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys)):8
-->_1 leq#2#(nil(),@x,@xs) -> c_16():55
8:S:leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
-->_1 or#(@x,@y) -> c_17(#or#(@x,@y)):56
-->_3 and#(@x,@y) -> c_3(#and#(@x,@y)):50
-->_2 #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):45
-->_4 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):44
-->_5 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
9:W:#and#(#false(),#false()) -> c_18()
10:W:#and#(#false(),#true()) -> c_19()
11:W:#and#(#true(),#false()) -> c_20()
12:W:#and#(#true(),#true()) -> c_21()
13:W:#cklt#(#EQ()) -> c_22()
14:W:#cklt#(#GT()) -> c_23()
15:W:#cklt#(#LT()) -> c_24()
16:W:#compare#(#0(),#0()) -> c_25()
17:W:#compare#(#0(),#neg(@y)) -> c_26()
18:W:#compare#(#0(),#pos(@y)) -> c_27()
19:W:#compare#(#0(),#s(@y)) -> c_28()
20:W:#compare#(#neg(@x),#0()) -> c_29()
21:W:#compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
-->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25
-->_1 #compare#(#s(@x),#0()) -> c_35():26
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24
-->_1 #compare#(#pos(@x),#0()) -> c_32():23
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21
-->_1 #compare#(#neg(@x),#0()) -> c_29():20
-->_1 #compare#(#0(),#s(@y)) -> c_28():19
-->_1 #compare#(#0(),#pos(@y)) -> c_27():18
-->_1 #compare#(#0(),#neg(@y)) -> c_26():17
-->_1 #compare#(#0(),#0()) -> c_25():16
22:W:#compare#(#neg(@x),#pos(@y)) -> c_31()
23:W:#compare#(#pos(@x),#0()) -> c_32()
24:W:#compare#(#pos(@x),#neg(@y)) -> c_33()
25:W:#compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
-->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27
-->_1 #compare#(#s(@x),#0()) -> c_35():26
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24
-->_1 #compare#(#pos(@x),#0()) -> c_32():23
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21
-->_1 #compare#(#neg(@x),#0()) -> c_29():20
-->_1 #compare#(#0(),#s(@y)) -> c_28():19
-->_1 #compare#(#0(),#pos(@y)) -> c_27():18
-->_1 #compare#(#0(),#neg(@y)) -> c_26():17
-->_1 #compare#(#0(),#0()) -> c_25():16
26:W:#compare#(#s(@x),#0()) -> c_35()
27:W:#compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
-->_1 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27
-->_1 #compare#(#s(@x),#0()) -> c_35():26
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_33():24
-->_1 #compare#(#pos(@x),#0()) -> c_32():23
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_31():22
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21
-->_1 #compare#(#neg(@x),#0()) -> c_29():20
-->_1 #compare#(#0(),#s(@y)) -> c_28():19
-->_1 #compare#(#0(),#pos(@y)) -> c_27():18
-->_1 #compare#(#0(),#neg(@y)) -> c_26():17
-->_1 #compare#(#0(),#0()) -> c_25():16
28:W:#eq#(#0(),#0()) -> c_37()
29:W:#eq#(#0(),#neg(@y)) -> c_38()
30:W:#eq#(#0(),#pos(@y)) -> c_39()
31:W:#eq#(#0(),#s(@y)) -> c_40()
32:W:#eq#(#neg(@x),#0()) -> c_41()
33:W:#eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_1 #eq#(nil(),nil()) -> c_52():43
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_1 #eq#(#s(@x),#0()) -> c_47():38
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_1 #eq#(#pos(@x),#0()) -> c_44():35
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_1 #eq#(#neg(@x),#0()) -> c_41():32
-->_1 #eq#(#0(),#s(@y)) -> c_40():31
-->_1 #eq#(#0(),#pos(@y)) -> c_39():30
-->_1 #eq#(#0(),#neg(@y)) -> c_38():29
-->_1 #eq#(#0(),#0()) -> c_37():28
34:W:#eq#(#neg(@x),#pos(@y)) -> c_43()
35:W:#eq#(#pos(@x),#0()) -> c_44()
36:W:#eq#(#pos(@x),#neg(@y)) -> c_45()
37:W:#eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_1 #eq#(nil(),nil()) -> c_52():43
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_1 #eq#(#s(@x),#0()) -> c_47():38
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_1 #eq#(#pos(@x),#0()) -> c_44():35
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_1 #eq#(#neg(@x),#0()) -> c_41():32
-->_1 #eq#(#0(),#s(@y)) -> c_40():31
-->_1 #eq#(#0(),#pos(@y)) -> c_39():30
-->_1 #eq#(#0(),#neg(@y)) -> c_38():29
-->_1 #eq#(#0(),#0()) -> c_37():28
38:W:#eq#(#s(@x),#0()) -> c_47()
39:W:#eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_1 #eq#(nil(),nil()) -> c_52():43
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_1 #eq#(#s(@x),#0()) -> c_47():38
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_1 #eq#(#pos(@x),#0()) -> c_44():35
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_1 #eq#(#neg(@x),#0()) -> c_41():32
-->_1 #eq#(#0(),#s(@y)) -> c_40():31
-->_1 #eq#(#0(),#pos(@y)) -> c_39():30
-->_1 #eq#(#0(),#neg(@y)) -> c_38():29
-->_1 #eq#(#0(),#0()) -> c_37():28
40:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#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_52():43
-->_2 #eq#(nil(),nil()) -> c_52():43
-->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_3 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_2 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_3 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_2 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_3 #eq#(#s(@x),#0()) -> c_47():38
-->_2 #eq#(#s(@x),#0()) -> c_47():38
-->_3 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_2 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_3 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_2 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_3 #eq#(#pos(@x),#0()) -> c_44():35
-->_2 #eq#(#pos(@x),#0()) -> c_44():35
-->_3 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_2 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_3 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_2 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_3 #eq#(#neg(@x),#0()) -> c_41():32
-->_2 #eq#(#neg(@x),#0()) -> c_41():32
-->_3 #eq#(#0(),#s(@y)) -> c_40():31
-->_2 #eq#(#0(),#s(@y)) -> c_40():31
-->_3 #eq#(#0(),#pos(@y)) -> c_39():30
-->_2 #eq#(#0(),#pos(@y)) -> c_39():30
-->_3 #eq#(#0(),#neg(@y)) -> c_38():29
-->_2 #eq#(#0(),#neg(@y)) -> c_38():29
-->_3 #eq#(#0(),#0()) -> c_37():28
-->_2 #eq#(#0(),#0()) -> c_37():28
-->_1 #and#(#true(),#true()) -> c_21():12
-->_1 #and#(#true(),#false()) -> c_20():11
-->_1 #and#(#false(),#true()) -> c_19():10
-->_1 #and#(#false(),#false()) -> c_18():9
41:W:#eq#(::(@x_1,@x_2),nil()) -> c_50()
42:W:#eq#(nil(),::(@y_1,@y_2)) -> c_51()
43:W:#eq#(nil(),nil()) -> c_52()
44:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y))
-->_1 #eq#(nil(),nil()) -> c_52():43
-->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_51():42
-->_1 #eq#(::(@x_1,@x_2),nil()) -> c_50():41
-->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2)):40
-->_1 #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y)):39
-->_1 #eq#(#s(@x),#0()) -> c_47():38
-->_1 #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y)):37
-->_1 #eq#(#pos(@x),#neg(@y)) -> c_45():36
-->_1 #eq#(#pos(@x),#0()) -> c_44():35
-->_1 #eq#(#neg(@x),#pos(@y)) -> c_43():34
-->_1 #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y)):33
-->_1 #eq#(#neg(@x),#0()) -> c_41():32
-->_1 #eq#(#0(),#s(@y)) -> c_40():31
-->_1 #eq#(#0(),#pos(@y)) -> c_39():30
-->_1 #eq#(#0(),#neg(@y)) -> c_38():29
-->_1 #eq#(#0(),#0()) -> c_37():28
45:W:#less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
-->_2 #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y)):27
-->_2 #compare#(#s(@x),#0()) -> c_35():26
-->_2 #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y)):25
-->_2 #compare#(#pos(@x),#neg(@y)) -> c_33():24
-->_2 #compare#(#pos(@x),#0()) -> c_32():23
-->_2 #compare#(#neg(@x),#pos(@y)) -> c_31():22
-->_2 #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x)):21
-->_2 #compare#(#neg(@x),#0()) -> c_29():20
-->_2 #compare#(#0(),#s(@y)) -> c_28():19
-->_2 #compare#(#0(),#pos(@y)) -> c_27():18
-->_2 #compare#(#0(),#neg(@y)) -> c_26():17
-->_2 #compare#(#0(),#0()) -> c_25():16
-->_1 #cklt#(#LT()) -> c_24():15
-->_1 #cklt#(#GT()) -> c_23():14
-->_1 #cklt#(#EQ()) -> c_22():13
46:W:#or#(#false(),#false()) -> c_53()
47:W:#or#(#false(),#true()) -> c_54()
48:W:#or#(#true(),#false()) -> c_55()
49:W:#or#(#true(),#true()) -> c_56()
50:W:and#(@x,@y) -> c_3(#and#(@x,@y))
-->_1 #and#(#true(),#true()) -> c_21():12
-->_1 #and#(#true(),#false()) -> c_20():11
-->_1 #and#(#false(),#true()) -> c_19():10
-->_1 #and#(#false(),#false()) -> c_18():9
51:W:insert#1#(nil(),@x) -> c_6()
52:W:insert#2#(#true(),@x,@y,@ys) -> c_8()
53:W:isortlist#1#(nil()) -> c_11()
54:W:leq#1#(nil(),@l2) -> c_14()
55:W:leq#2#(nil(),@x,@xs) -> c_16()
56:W:or#(@x,@y) -> c_17(#or#(@x,@y))
-->_1 #or#(#true(),#true()) -> c_56():49
-->_1 #or#(#true(),#false()) -> c_55():48
-->_1 #or#(#false(),#true()) -> c_54():47
-->_1 #or#(#false(),#false()) -> c_53():46
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
53: isortlist#1#(nil()) -> c_11()
51: insert#1#(nil(),@x) -> c_6()
52: insert#2#(#true(),@x,@y,@ys) -> c_8()
54: leq#1#(nil(),@l2) -> c_14()
55: leq#2#(nil(),@x,@xs) -> c_16()
44: #equal#(@x,@y) -> c_1(#eq#(@x,@y))
40: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_49(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
,#eq#(@x_1,@y_1)
,#eq#(@x_2,@y_2))
39: #eq#(#s(@x),#s(@y)) -> c_48(#eq#(@x,@y))
37: #eq#(#pos(@x),#pos(@y)) -> c_46(#eq#(@x,@y))
33: #eq#(#neg(@x),#neg(@y)) -> c_42(#eq#(@x,@y))
28: #eq#(#0(),#0()) -> c_37()
29: #eq#(#0(),#neg(@y)) -> c_38()
30: #eq#(#0(),#pos(@y)) -> c_39()
31: #eq#(#0(),#s(@y)) -> c_40()
32: #eq#(#neg(@x),#0()) -> c_41()
34: #eq#(#neg(@x),#pos(@y)) -> c_43()
35: #eq#(#pos(@x),#0()) -> c_44()
36: #eq#(#pos(@x),#neg(@y)) -> c_45()
38: #eq#(#s(@x),#0()) -> c_47()
41: #eq#(::(@x_1,@x_2),nil()) -> c_50()
42: #eq#(nil(),::(@y_1,@y_2)) -> c_51()
43: #eq#(nil(),nil()) -> c_52()
45: #less#(@x,@y) -> c_2(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
13: #cklt#(#EQ()) -> c_22()
14: #cklt#(#GT()) -> c_23()
15: #cklt#(#LT()) -> c_24()
27: #compare#(#s(@x),#s(@y)) -> c_36(#compare#(@x,@y))
25: #compare#(#pos(@x),#pos(@y)) -> c_34(#compare#(@x,@y))
21: #compare#(#neg(@x),#neg(@y)) -> c_30(#compare#(@y,@x))
16: #compare#(#0(),#0()) -> c_25()
17: #compare#(#0(),#neg(@y)) -> c_26()
18: #compare#(#0(),#pos(@y)) -> c_27()
19: #compare#(#0(),#s(@y)) -> c_28()
20: #compare#(#neg(@x),#0()) -> c_29()
22: #compare#(#neg(@x),#pos(@y)) -> c_31()
23: #compare#(#pos(@x),#0()) -> c_32()
24: #compare#(#pos(@x),#neg(@y)) -> c_33()
26: #compare#(#s(@x),#0()) -> c_35()
50: and#(@x,@y) -> c_3(#and#(@x,@y))
9: #and#(#false(),#false()) -> c_18()
10: #and#(#false(),#true()) -> c_19()
11: #and#(#true(),#false()) -> c_20()
12: #and#(#true(),#true()) -> c_21()
56: or#(@x,@y) -> c_17(#or#(@x,@y))
46: #or#(#false(),#false()) -> c_53()
47: #or#(#false(),#true()) -> c_54()
48: #or#(#true(),#false()) -> c_55()
49: #or#(#true(),#true()) -> c_56()
* Step 5: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/5,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:S:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
6:S:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
7:S:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys)):8
8:S:leq#2#(::(@y,@ys),@x,@xs) -> c_15(or#(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
,#less#(@x,@y)
,and#(#equal(@x,@y),leq(@xs,@ys))
,#equal#(@x,@y)
,leq#(@xs,@ys))
-->_5 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
* Step 6: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#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:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1
,c_35/0,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3
,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
Problem (S)
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1
,c_35/0,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3
,c_50/0,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
** Step 6.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#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:
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
Consider the set of all dependency pairs
1: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
4: isortlist#(@l) -> c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@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
{6}
These cover all (indirect) predecessors of dependency pairs
{6,7,8}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** Step 6.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#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_4) = {1},
uargs(c_5) = {1,2},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1}
Following symbols are considered usable:
{#or,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal#
,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = 0
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#and) = 0
p(#cklt) = x1
p(#compare) = 1 + x2^2
p(#eq) = 1
p(#equal) = 0
p(#false) = 1
p(#less) = x2
p(#neg) = 0
p(#or) = 1
p(#pos) = 1
p(#s) = 0
p(#true) = 1
p(::) = 1 + x1 + x2
p(and) = 0
p(insert) = 1 + x1 + x2
p(insert#1) = 1 + x1 + x2
p(insert#2) = 1 + x1*x2 + x1*x4 + x1^2 + x3
p(isortlist) = x1
p(isortlist#1) = x1
p(leq) = 1
p(leq#1) = 1
p(leq#2) = 1
p(nil) = 0
p(or) = 1
p(#and#) = 0
p(#cklt#) = 0
p(#compare#) = 0
p(#eq#) = 0
p(#equal#) = 0
p(#less#) = 0
p(#or#) = 0
p(and#) = 0
p(insert#) = x1*x2 + x1^2 + x2
p(insert#1#) = x1 + x1*x2 + x2^2
p(insert#2#) = x2 + x2*x4 + x2^2 + x3 + x4
p(isortlist#) = 1 + x1^2
p(isortlist#1#) = 1 + x1^2
p(leq#) = 1 + x1*x2
p(leq#1#) = x1*x2
p(leq#2#) = x1 + x1*x3
p(or#) = 0
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = x1
p(c_5) = x1 + x2
p(c_6) = 0
p(c_7) = x1
p(c_8) = 0
p(c_9) = x1
p(c_10) = 1 + x1 + x2
p(c_11) = 0
p(c_12) = x1
p(c_13) = x1
p(c_14) = 0
p(c_15) = x1
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
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
p(c_38) = 0
p(c_39) = 0
p(c_40) = 0
p(c_41) = 0
p(c_42) = 0
p(c_43) = 0
p(c_44) = 0
p(c_45) = 0
p(c_46) = 0
p(c_47) = 0
p(c_48) = 0
p(c_49) = 0
p(c_50) = 0
p(c_51) = 0
p(c_52) = 0
p(c_53) = 0
p(c_54) = 0
p(c_55) = 0
p(c_56) = 0
Following rules are strictly oriented:
leq#(@l1,@l2) = 1 + @l1*@l2
> @l1*@l2
= c_12(leq#1#(@l1,@l2))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = @l + @l*@x + @x^2
>= @l + @l*@x + @x^2
= c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) = 1 + @x + @x*@y + @x*@ys + @x^2 + @y + @ys
>= 1 + @x + @x*@y + @x*@ys + @x^2 + @y + @ys
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) = @x + @x*@ys + @x^2 + @y + @ys
>= @x*@ys + @x^2 + @ys
= c_7(insert#(@x,@ys))
isortlist#(@l) = 1 + @l^2
>= 1 + @l^2
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = 2 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2
>= 2 + @x*@xs + @x^2 + @xs + @xs^2
= c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#1#(::(@x,@xs),@l2) = @l2 + @l2*@x + @l2*@xs
>= @l2 + @l2*@xs
= c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) = 1 + @xs + @xs*@y + @xs*@ys + @y + @ys
>= 1 + @xs*@ys
= c_15(leq#(@xs,@ys))
#or(#false(),#false()) = 1
>= 1
= #false()
#or(#false(),#true()) = 1
>= 1
= #true()
#or(#true(),#false()) = 1
>= 1
= #true()
#or(#true(),#true()) = 1
>= 1
= #true()
insert(@x,@l) = 1 + @l + @x
>= 1 + @l + @x
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = 1 + @x
>= 1 + @x
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@x,::(@y,@ys))
isortlist(@l) = @l
>= @l
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = 1 + @x + @xs
>= 1 + @x + @xs
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = 0
>= 0
= nil()
leq(@l1,@l2) = 1
>= 1
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = 1
>= 1
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = 1
>= 1
= #true()
leq#2(::(@y,@ys),@x,@xs) = 1
>= 1
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = 1
>= 1
= #false()
or(@x,@y) = 1
>= 1
= #or(@x,@y)
*** Step 6.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 6.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8
8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
-->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
*** Step 6.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
*** Step 6.a:1.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
Consider the set of all dependency pairs
1: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
4: isortlist#(@l) -> c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{2}
These cover all (indirect) predecessors of dependency pairs
{2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
**** Step 6.a:1.b:3.a:1: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2}
Following symbols are considered usable:
{insert,insert#1,insert#2,isortlist,isortlist#1,#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [1]
[1]
p(#EQ) = [3]
[1]
p(#GT) = [1]
[2]
p(#LT) = [0]
[1]
p(#and) = [0 0] x1 + [2 0] x2 + [0]
[1 1] [1 0] [2]
p(#cklt) = [0 2] x1 + [0]
[1 0] [1]
p(#compare) = [1 0] x1 + [1]
[1 1] [1]
p(#eq) = [0 2] x1 + [1 0] x2 + [2]
[0 0] [0 3] [0]
p(#equal) = [1 3] x1 + [1 0] x2 + [1]
[0 1] [3 0] [1]
p(#false) = [0]
[0]
p(#less) = [2 0] x1 + [1 1] x2 + [0]
[1 2] [1 2] [0]
p(#neg) = [1 0] x1 + [0]
[0 0] [0]
p(#or) = [0 0] x1 + [2]
[1 0] [0]
p(#pos) = [1]
[0]
p(#s) = [1 0] x1 + [0]
[0 1] [0]
p(#true) = [0]
[0]
p(::) = [1 1] x2 + [0]
[0 1] [1]
p(and) = [1 1] x1 + [2]
[1 1] [3]
p(insert) = [1 1] x2 + [0]
[0 1] [1]
p(insert#1) = [1 1] x1 + [0]
[0 1] [1]
p(insert#2) = [1 2] x4 + [1]
[0 1] [2]
p(isortlist) = [1 0] x1 + [0]
[0 1] [0]
p(isortlist#1) = [1 0] x1 + [0]
[0 1] [0]
p(leq) = [0]
[0]
p(leq#1) = [0]
[0]
p(leq#2) = [2 1] x3 + [1]
[0 0] [0]
p(nil) = [0]
[0]
p(or) = [0 3] x1 + [0 0] x2 + [3]
[2 1] [1 0] [2]
p(#and#) = [2 0] x1 + [0]
[1 0] [0]
p(#cklt#) = [0 0] x1 + [0]
[0 1] [2]
p(#compare#) = [0 0] x1 + [2 2] x2 + [1]
[0 1] [0 0] [0]
p(#eq#) = [1 0] x2 + [0]
[0 0] [1]
p(#equal#) = [0 0] x2 + [2]
[0 1] [2]
p(#less#) = [1 0] x2 + [1]
[0 0] [0]
p(#or#) = [1]
[2]
p(and#) = [1]
[0]
p(insert#) = [0 2] x2 + [0]
[1 0] [0]
p(insert#1#) = [0 2] x1 + [0 0] x2 + [0]
[2 2] [0 2] [0]
p(insert#2#) = [0 2] x4 + [0]
[0 0] [1]
p(isortlist#) = [2 0] x1 + [0]
[0 2] [0]
p(isortlist#1#) = [2 0] x1 + [0]
[1 3] [0]
p(leq#) = [0]
[1]
p(leq#1#) = [1]
[1]
p(leq#2#) = [2 1] x3 + [1]
[1 0] [1]
p(or#) = [0 1] x2 + [0]
[0 0] [1]
p(c_1) = [2]
[0]
p(c_2) = [0]
[0]
p(c_3) = [0 1] x1 + [0]
[0 0] [2]
p(c_4) = [1 0] x1 + [0]
[0 0] [0]
p(c_5) = [1 1] x1 + [0]
[1 1] [1]
p(c_6) = [1]
[1]
p(c_7) = [1 0] x1 + [0]
[0 0] [1]
p(c_8) = [2]
[1]
p(c_9) = [1 0] x1 + [0]
[0 0] [0]
p(c_10) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 2] [0]
p(c_11) = [0]
[1]
p(c_12) = [1 1] x1 + [0]
[1 0] [0]
p(c_13) = [0]
[0]
p(c_14) = [0]
[2]
p(c_15) = [0 0] x1 + [1]
[2 0] [2]
p(c_16) = [0]
[0]
p(c_17) = [2]
[0]
p(c_18) = [0]
[2]
p(c_19) = [0]
[0]
p(c_20) = [1]
[0]
p(c_21) = [2]
[1]
p(c_22) = [2]
[1]
p(c_23) = [1]
[0]
p(c_24) = [1]
[0]
p(c_25) = [0]
[2]
p(c_26) = [1]
[1]
p(c_27) = [1]
[0]
p(c_28) = [1]
[0]
p(c_29) = [1]
[2]
p(c_30) = [2 2] x1 + [1]
[0 0] [0]
p(c_31) = [1]
[2]
p(c_32) = [0]
[0]
p(c_33) = [0]
[0]
p(c_34) = [0 0] x1 + [1]
[0 2] [0]
p(c_35) = [0]
[0]
p(c_36) = [0 2] x1 + [0]
[0 0] [0]
p(c_37) = [0]
[0]
p(c_38) = [2]
[1]
p(c_39) = [2]
[0]
p(c_40) = [0]
[0]
p(c_41) = [2]
[2]
p(c_42) = [0]
[0]
p(c_43) = [2]
[0]
p(c_44) = [1]
[1]
p(c_45) = [0]
[1]
p(c_46) = [1]
[1]
p(c_47) = [0]
[2]
p(c_48) = [1 0] x1 + [2]
[0 0] [2]
p(c_49) = [0 1] x1 + [1 0] x3 + [0]
[0 2] [0 0] [0]
p(c_50) = [2]
[2]
p(c_51) = [2]
[2]
p(c_52) = [0]
[0]
p(c_53) = [1]
[1]
p(c_54) = [2]
[0]
p(c_55) = [0]
[0]
p(c_56) = [2]
[0]
Following rules are strictly oriented:
insert#1#(::(@y,@ys),@x) = [0 0] @x + [0 2] @ys + [2]
[0 2] [2 4] [2]
> [0 2] @ys + [1]
[0 2] [2]
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [0 2] @l + [0]
[1 0] [0]
>= [0 2] @l + [0]
[0 0] [0]
= c_4(insert#1#(@l,@x))
insert#2#(#false(),@x,@y,@ys) = [0 2] @ys + [0]
[0 0] [1]
>= [0 2] @ys + [0]
[0 0] [1]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [2 0] @l + [0]
[0 2] [0]
>= [2 0] @l + [0]
[0 0] [0]
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = [2 2] @xs + [0]
[1 4] [3]
>= [2 2] @xs + [0]
[1 4] [0]
= c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
insert(@x,@l) = [1 1] @l + [0]
[0 1] [1]
>= [1 1] @l + [0]
[0 1] [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [0]
[1]
>= [0]
[1]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [1 0] @l + [0]
[0 1] [0]
>= [1 0] @l + [0]
[0 1] [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [1 1] @xs + [0]
[0 1] [1]
>= [1 1] @xs + [0]
[0 1] [1]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
**** Step 6.a:1.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 6.a:1.b:3.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
- Weak DPs:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
Consider the set of all dependency pairs
1: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
4: isortlist#(@l) -> c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, 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 6.a:1.b:3.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
- Weak DPs:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2}
Following symbols are considered usable:
{insert,insert#1,insert#2,isortlist,isortlist#1,#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [0]
[3]
p(#EQ) = [0]
[0]
p(#GT) = [0]
[0]
p(#LT) = [0]
[0]
p(#and) = [0 1] x1 + [0 1] x2 + [3]
[0 0] [0 0] [0]
p(#cklt) = [0]
[0]
p(#compare) = [0 1] x1 + [0 0] x2 + [1]
[0 1] [1 0] [1]
p(#eq) = [0 0] x1 + [0 2] x2 + [0]
[3 0] [0 0] [0]
p(#equal) = [0 0] x1 + [0 0] x2 + [0]
[0 3] [1 0] [1]
p(#false) = [0]
[0]
p(#less) = [0 1] x2 + [0]
[0 0] [0]
p(#neg) = [0 1] x1 + [2]
[0 0] [2]
p(#or) = [1]
[0]
p(#pos) = [0 2] x1 + [0]
[0 1] [3]
p(#s) = [0 2] x1 + [0]
[0 0] [0]
p(#true) = [0]
[0]
p(::) = [1 1] x2 + [0]
[0 1] [1]
p(and) = [0 0] x1 + [1]
[0 1] [3]
p(insert) = [1 2] x2 + [0]
[0 1] [1]
p(insert#1) = [1 2] x1 + [0]
[0 1] [1]
p(insert#2) = [1 3] x4 + [2]
[0 1] [2]
p(isortlist) = [2 0] x1 + [0]
[0 1] [0]
p(isortlist#1) = [2 0] x1 + [0]
[0 1] [0]
p(leq) = [0]
[0]
p(leq#1) = [0]
[0]
p(leq#2) = [0]
[0]
p(nil) = [0]
[0]
p(or) = [1 1] x2 + [2]
[1 1] [0]
p(#and#) = [0 1] x2 + [2]
[1 0] [1]
p(#cklt#) = [0]
[0]
p(#compare#) = [0 0] x2 + [0]
[0 1] [0]
p(#eq#) = [0 2] x1 + [2 2] x2 + [0]
[0 0] [1 2] [0]
p(#equal#) = [0 0] x1 + [0]
[0 2] [0]
p(#less#) = [1 2] x1 + [2 1] x2 + [1]
[2 0] [0 0] [0]
p(#or#) = [1 0] x1 + [0]
[0 0] [0]
p(and#) = [0 0] x2 + [2]
[1 1] [0]
p(insert#) = [0 1] x2 + [1]
[0 0] [1]
p(insert#1#) = [0 1] x1 + [0 0] x2 + [0]
[2 3] [2 2] [1]
p(insert#2#) = [0 1] x4 + [1]
[0 1] [0]
p(isortlist#) = [1 1] x1 + [1]
[2 3] [2]
p(isortlist#1#) = [1 1] x1 + [1]
[2 3] [2]
p(leq#) = [0 0] x1 + [0 0] x2 + [0]
[2 0] [1 0] [0]
p(leq#1#) = [2 2] x1 + [2 1] x2 + [0]
[0 1] [1 1] [0]
p(leq#2#) = [0 1] x2 + [1 0] x3 + [0]
[1 1] [0 0] [0]
p(or#) = [2 2] x2 + [0]
[2 0] [0]
p(c_1) = [0]
[0]
p(c_2) = [0 0] x1 + [2]
[1 1] [1]
p(c_3) = [0]
[1]
p(c_4) = [1 0] x1 + [0]
[0 0] [1]
p(c_5) = [1 0] x1 + [0]
[2 3] [2]
p(c_6) = [0]
[0]
p(c_7) = [1 0] x1 + [0]
[0 0] [0]
p(c_8) = [1]
[1]
p(c_9) = [1 0] x1 + [0]
[2 0] [0]
p(c_10) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [1]
p(c_11) = [2]
[0]
p(c_12) = [0 2] x1 + [0]
[1 1] [0]
p(c_13) = [2 2] x1 + [0]
[0 1] [0]
p(c_14) = [1]
[0]
p(c_15) = [0 0] x1 + [0]
[1 0] [0]
p(c_16) = [0]
[0]
p(c_17) = [1 1] x1 + [2]
[2 0] [1]
p(c_18) = [0]
[0]
p(c_19) = [1]
[0]
p(c_20) = [0]
[1]
p(c_21) = [2]
[0]
p(c_22) = [0]
[0]
p(c_23) = [2]
[0]
p(c_24) = [0]
[0]
p(c_25) = [0]
[1]
p(c_26) = [0]
[1]
p(c_27) = [0]
[0]
p(c_28) = [0]
[0]
p(c_29) = [0]
[2]
p(c_30) = [0]
[1]
p(c_31) = [1]
[0]
p(c_32) = [0]
[0]
p(c_33) = [2]
[2]
p(c_34) = [1]
[0]
p(c_35) = [0]
[2]
p(c_36) = [0]
[0]
p(c_37) = [0]
[0]
p(c_38) = [0]
[2]
p(c_39) = [0]
[0]
p(c_40) = [0]
[1]
p(c_41) = [0]
[0]
p(c_42) = [0]
[0]
p(c_43) = [2]
[0]
p(c_44) = [2]
[0]
p(c_45) = [1]
[0]
p(c_46) = [2 1] x1 + [0]
[1 0] [0]
p(c_47) = [0]
[2]
p(c_48) = [0 0] x1 + [2]
[2 0] [2]
p(c_49) = [0 2] x1 + [0 0] x3 + [0]
[1 0] [1 2] [1]
p(c_50) = [2]
[0]
p(c_51) = [0]
[0]
p(c_52) = [0]
[0]
p(c_53) = [0]
[0]
p(c_54) = [0]
[2]
p(c_55) = [2]
[0]
p(c_56) = [0]
[2]
Following rules are strictly oriented:
insert#(@x,@l) = [0 1] @l + [1]
[0 0] [1]
> [0 1] @l + [0]
[0 0] [1]
= c_4(insert#1#(@l,@x))
Following rules are (at-least) weakly oriented:
insert#1#(::(@y,@ys),@x) = [0 0] @x + [0 1] @ys + [1]
[2 2] [2 5] [4]
>= [0 1] @ys + [1]
[0 5] [4]
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) = [0 1] @ys + [1]
[0 1] [0]
>= [0 1] @ys + [1]
[0 0] [0]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [1 1] @l + [1]
[2 3] [2]
>= [1 1] @l + [1]
[2 2] [2]
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = [1 2] @xs + [2]
[2 5] [5]
>= [1 2] @xs + [2]
[0 0] [2]
= c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
insert(@x,@l) = [1 2] @l + [0]
[0 1] [1]
>= [1 2] @l + [0]
[0 1] [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1 3] @ys + [2]
[0 1] [2]
>= [1 3] @ys + [2]
[0 1] [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [0]
[1]
>= [0]
[1]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1 3] @ys + [2]
[0 1] [2]
>= [1 3] @ys + [1]
[0 1] [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1 3] @ys + [2]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [2 0] @l + [0]
[0 1] [0]
>= [2 0] @l + [0]
[0 1] [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [2 2] @xs + [0]
[0 1] [1]
>= [2 2] @xs + [0]
[0 1] [1]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
***** Step 6.a:1.b:3.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 6.a:1.b:3.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)):2
2:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: isortlist#(@l) -> c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
1: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
3: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
2: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
***** Step 6.a:1.b:3.b: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()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 6.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak DPs:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):2
2:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):1
3:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):4
4:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):5
5:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3
6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8
8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
-->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: insert#(@x,@l) -> c_4(insert#1#(@l,@x))
5: insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
4: insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
8: leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
7: leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
** Step 6.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/2,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):2
2:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
** Step 6.b:3: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(@y)) -> #GT()
#compare(#0(),#pos(@y)) -> #LT()
#compare(#0(),#s(@y)) -> #LT()
#compare(#neg(@x),#0()) -> #LT()
#compare(#neg(@x),#neg(@y)) -> #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) -> #LT()
#compare(#pos(@x),#0()) -> #GT()
#compare(#pos(@x),#neg(@y)) -> #GT()
#compare(#pos(@x),#pos(@y)) -> #compare(@x,@y)
#compare(#s(@x),#0()) -> #GT()
#compare(#s(@x),#s(@y)) -> #compare(@x,@y)
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
#or(#false(),#false()) -> #false()
#or(#false(),#true()) -> #true()
#or(#true(),#false()) -> #true()
#or(#true(),#true()) -> #true()
and(@x,@y) -> #and(@x,@y)
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
isortlist(@l) -> isortlist#1(@l)
isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs))
isortlist#1(nil()) -> nil()
leq(@l1,@l2) -> leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) -> #true()
leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) -> #false()
or(@x,@y) -> #or(@x,@y)
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
** Step 6.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: isortlist#(@l) -> c_9(isortlist#1#(@l))
2: isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
The strictly oriented rules are moved into the weak component.
*** Step 6.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_10) = {1}
Following symbols are considered usable:
{#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#
,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [0]
p(#cklt) = [0]
p(#compare) = [0]
p(#eq) = [1] x1 + [1] x2 + [0]
p(#equal) = [2]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [0]
p(#or) = [0]
p(#pos) = [1]
p(#s) = [4]
p(#true) = [2]
p(::) = [1] x2 + [2]
p(and) = [1] x1 + [8] x2 + [4]
p(insert) = [8] x1 + [1]
p(insert#1) = [8] x1 + [0]
p(insert#2) = [2] x4 + [1]
p(isortlist) = [8] x1 + [1]
p(isortlist#1) = [2] x1 + [2]
p(leq) = [1] x1 + [2] x2 + [1]
p(leq#1) = [1]
p(leq#2) = [0]
p(nil) = [0]
p(or) = [0]
p(#and#) = [0]
p(#cklt#) = [0]
p(#compare#) = [0]
p(#eq#) = [0]
p(#equal#) = [0]
p(#less#) = [0]
p(#or#) = [0]
p(and#) = [0]
p(insert#) = [0]
p(insert#1#) = [0]
p(insert#2#) = [0]
p(isortlist#) = [4] x1 + [3]
p(isortlist#1#) = [4] x1 + [0]
p(leq#) = [0]
p(leq#1#) = [0]
p(leq#2#) = [0]
p(or#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [4]
p(c_4) = [2] x1 + [0]
p(c_5) = [8] x1 + [1] x2 + [1]
p(c_6) = [1]
p(c_7) = [2]
p(c_8) = [4]
p(c_9) = [1] x1 + [2]
p(c_10) = [1] x1 + [0]
p(c_11) = [4]
p(c_12) = [1] x1 + [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [2] x1 + [0]
p(c_16) = [1]
p(c_17) = [1]
p(c_18) = [2]
p(c_19) = [1]
p(c_20) = [1]
p(c_21) = [8]
p(c_22) = [2]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [2]
p(c_26) = [0]
p(c_27) = [1]
p(c_28) = [1]
p(c_29) = [1]
p(c_30) = [2]
p(c_31) = [1]
p(c_32) = [1]
p(c_33) = [1]
p(c_34) = [2]
p(c_35) = [0]
p(c_36) = [1] x1 + [0]
p(c_37) = [1]
p(c_38) = [4]
p(c_39) = [2]
p(c_40) = [1]
p(c_41) = [0]
p(c_42) = [0]
p(c_43) = [1]
p(c_44) = [4]
p(c_45) = [1]
p(c_46) = [1]
p(c_47) = [2]
p(c_48) = [2] x1 + [1]
p(c_49) = [1] x2 + [1] x3 + [1]
p(c_50) = [1]
p(c_51) = [1]
p(c_52) = [0]
p(c_53) = [0]
p(c_54) = [0]
p(c_55) = [0]
p(c_56) = [0]
Following rules are strictly oriented:
isortlist#(@l) = [4] @l + [3]
> [4] @l + [2]
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = [4] @xs + [8]
> [4] @xs + [3]
= c_10(isortlist#(@xs))
Following rules are (at-least) weakly oriented:
*** Step 6.b:4.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 6.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)):2
2:W:isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
-->_1 isortlist#(@l) -> c_9(isortlist#1#(@l)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: isortlist#(@l) -> c_9(isortlist#1#(@l))
2: isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
*** Step 6.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1
,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2,#and#/2,#cklt#/1,#compare#/2,#eq#/2,#equal#/2,#less#/2,#or#/2
,and#/2,insert#/2,insert#1#/2,insert#2#/4,isortlist#/1,isortlist#1#/1,leq#/2,leq#1#/2,leq#2#/3
,or#/2} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/2,c_3/1,c_4/1
,c_5/2,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,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/0,c_28/0,c_29/0,c_30/1,c_31/0,c_32/0,c_33/0,c_34/1,c_35/0
,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/1,c_43/0,c_44/0,c_45/0,c_46/1,c_47/0,c_48/1,c_49/3,c_50/0
,c_51/0,c_52/0,c_53/0,c_54/0,c_55/0,c_56/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#
,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#} and constructors {#0,#EQ,#GT
,#LT,#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))