WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
+ 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 2: PredecessorEstimation WORST_CASE(?,O(n^3))
+ 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 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
+ 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 4: SimplifyRHS WORST_CASE(?,O(n^3))
+ 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 5: DecomposeDG WORST_CASE(?,O(n^3))
+ 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:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
and a lower component
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))
Further, following extension rules are added to the lower component.
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) -> isortlist#(@xs)
** Step 5.a:1: 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 5.a:2: 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 5.a:3: WeightGap 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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_10) = {1}
Following symbols are considered usable:
all
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) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [1]
p(#neg) = [1] x1 + [0]
p(#or) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [1]
p(::) = [1] x1 + [0]
p(and) = [0]
p(insert) = [0]
p(insert#1) = [0]
p(insert#2) = [0]
p(isortlist) = [0]
p(isortlist#1) = [0]
p(leq) = [0]
p(leq#1) = [0]
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#) = [1] x1 + [1]
p(#or#) = [0]
p(and#) = [0]
p(insert#) = [0]
p(insert#1#) = [0]
p(insert#2#) = [0]
p(isortlist#) = [0]
p(isortlist#1#) = [3]
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) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [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) = [2]
p(c_56) = [0]
Following rules are strictly oriented:
isortlist#1#(::(@x,@xs)) = [3]
> [0]
= c_10(isortlist#(@xs))
Following rules are (at-least) weakly oriented:
isortlist#(@l) = [0]
>= [3]
= c_9(isortlist#1#(@l))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 5.a:4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isortlist#(@l) -> c_9(isortlist#1#(@l))
- Weak DPs:
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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_10) = {1}
Following symbols are considered usable:
all
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) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#or) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x1 + [1] x2 + [3]
p(and) = [0]
p(insert) = [0]
p(insert#1) = [0]
p(insert#2) = [0]
p(isortlist) = [0]
p(isortlist#1) = [0]
p(leq) = [0]
p(leq#1) = [0]
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#) = [2] x2 + [1] x3 + [1] x4 + [0]
p(isortlist#) = [3] x1 + [9]
p(isortlist#1#) = [3] 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) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [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:
isortlist#(@l) = [3] @l + [9]
> [3] @l + [0]
= c_9(isortlist#1#(@l))
Following rules are (at-least) weakly oriented:
isortlist#1#(::(@x,@xs)) = [3] @x + [3] @xs + [9]
>= [3] @xs + [9]
= c_10(isortlist#(@xs))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 5.a:5: EmptyProcessor 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:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 5.b:1: DecomposeDG 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) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
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) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) -> isortlist#(@xs)
and a lower component
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))
Further, following extension rules are added to the lower component.
insert#(@x,@l) -> insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) -> leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys)
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) -> isortlist#(@xs)
*** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^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))
- Weak DPs:
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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) -> isortlist#1#(@l)
-->_1 isortlist#1#(::(@x,@xs)) -> isortlist#(@xs):6
-->_1 isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
6:W:isortlist#1#(::(@x,@xs)) -> isortlist#(@xs)
-->_1 isortlist#(@l) -> isortlist#1#(@l):4
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 5.b:1.a:2: WeightGap WORST_CASE(?,O(n^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))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
- Weak DPs:
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(#cklt) = {1},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(insert) = {2},
uargs(insert#2) = {1},
uargs(or) = {1,2},
uargs(insert#) = {2},
uargs(insert#2#) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#cklt) = [1] x1 + [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#or) = [1] x1 + [0]
p(#pos) = [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(insert) = [1] x2 + [0]
p(insert#1) = [1] x1 + [0]
p(insert#2) = [1] x1 + [1] x4 + [0]
p(isortlist) = [0]
p(isortlist#1) = [0]
p(leq) = [0]
p(leq#1) = [0]
p(leq#2) = [0]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0]
p(insert#1#) = [1] x1 + [0]
p(insert#2#) = [1] x1 + [1] x4 + [1]
p(isortlist#) = [2] x1 + [0]
p(isortlist#1#) = [2] 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) = [1] x1 + [0]
p(c_5) = [1] x1 + [2]
p(c_6) = [4]
p(c_7) = [1] x1 + [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [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:
insert#2#(#false(),@x,@y,@ys) = [1] @ys + [1]
> [1] @ys + [0]
= c_7(insert#(@x,@ys))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [1] @l + [0]
>= [1] @l + [0]
= c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) = [1] @ys + [0]
>= [1] @ys + [3]
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
isortlist#(@l) = [2] @l + [0]
>= [2] @l + [0]
= isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) = [2] @xs + [0]
>= [0]
= insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) = [2] @xs + [0]
>= [2] @xs + [0]
= isortlist#(@xs)
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#cklt(#EQ()) = [0]
>= [0]
= #false()
#cklt(#GT()) = [0]
>= [0]
= #false()
#cklt(#LT()) = [0]
>= [0]
= #true()
#compare(#0(),#0()) = [0]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#0(),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [0]
>= [0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#pos(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [0]
>= [0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#s(@x),#s(@y)) = [0]
>= [0]
= #compare(@x,@y)
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
#less(@x,@y) = [0]
>= [0]
= #cklt(#compare(@x,@y))
#or(#false(),#false()) = [0]
>= [0]
= #false()
#or(#false(),#true()) = [0]
>= [0]
= #true()
#or(#true(),#false()) = [0]
>= [0]
= #true()
#or(#true(),#true()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
insert(@x,@l) = [1] @l + [0]
>= [1] @l + [0]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1] @ys + [0]
>= [1] @ys + [0]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [0]
>= [0]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@x,::(@y,@ys))
isortlist(@l) = [0]
>= [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [0]
>= [0]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
>= [0]
= nil()
leq(@l1,@l2) = [0]
>= [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0]
>= [0]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [0]
>= [0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [0]
>= [0]
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [0]
>= [0]
= #false()
or(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [0]
= #or(@x,@y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 5.b:1.a:3: WeightGap WORST_CASE(?,O(n^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))
- Weak DPs:
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(#cklt) = {1},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(insert) = {2},
uargs(insert#2) = {1},
uargs(or) = {1,2},
uargs(insert#) = {2},
uargs(insert#2#) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#cklt) = [1] x1 + [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [0]
p(#or) = [1] x2 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(insert) = [1] x2 + [0]
p(insert#1) = [1] x1 + [0]
p(insert#2) = [1] x1 + [1] x4 + [0]
p(isortlist) = [1] x1 + [0]
p(isortlist#1) = [1] x1 + [0]
p(leq) = [0]
p(leq#1) = [0]
p(leq#2) = [0]
p(nil) = [2]
p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0]
p(insert#1#) = [1] x1 + [3]
p(insert#2#) = [1] x1 + [1] x4 + [0]
p(isortlist#) = [1] x1 + [0]
p(isortlist#1#) = [1] 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) = [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [2]
p(c_6) = [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [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:
insert#1#(::(@y,@ys),@x) = [1] @ys + [3]
> [1] @ys + [2]
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [1] @l + [0]
>= [1] @l + [3]
= c_4(insert#1#(@l,@x))
insert#2#(#false(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [1] @l + [0]
>= [1] @l + [0]
= isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) = [1] @xs + [0]
>= [1] @xs + [0]
= insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) = [1] @xs + [0]
>= [1] @xs + [0]
= isortlist#(@xs)
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#cklt(#EQ()) = [0]
>= [0]
= #false()
#cklt(#GT()) = [0]
>= [0]
= #false()
#cklt(#LT()) = [0]
>= [0]
= #true()
#compare(#0(),#0()) = [0]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#0(),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [0]
>= [0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#pos(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [0]
>= [0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#s(@x),#s(@y)) = [0]
>= [0]
= #compare(@x,@y)
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
#less(@x,@y) = [0]
>= [0]
= #cklt(#compare(@x,@y))
#or(#false(),#false()) = [0]
>= [0]
= #false()
#or(#false(),#true()) = [0]
>= [0]
= #true()
#or(#true(),#false()) = [0]
>= [0]
= #true()
#or(#true(),#true()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
insert(@x,@l) = [1] @l + [0]
>= [1] @l + [0]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1] @ys + [0]
>= [1] @ys + [0]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [2]
>= [2]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1] @ys + [0]
>= [1] @ys + [0]
= ::(@x,::(@y,@ys))
isortlist(@l) = [1] @l + [0]
>= [1] @l + [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [1] @xs + [0]
>= [1] @xs + [0]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [2]
>= [2]
= nil()
leq(@l1,@l2) = [0]
>= [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0]
>= [0]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [0]
>= [0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [0]
>= [0]
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [0]
>= [0]
= #false()
or(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @y + [0]
= #or(@x,@y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 5.b:1.a:4: WeightGap WORST_CASE(?,O(n^1))
+ 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) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(#cklt) = {1},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(insert) = {2},
uargs(insert#2) = {1},
uargs(or) = {1,2},
uargs(insert#) = {2},
uargs(insert#2#) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#cklt) = [1] x1 + [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#or) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [1]
p(and) = [1] x1 + [1] x2 + [0]
p(insert) = [1] x2 + [1]
p(insert#1) = [1] x1 + [1]
p(insert#2) = [1] x1 + [1] x4 + [2]
p(isortlist) = [2] x1 + [1]
p(isortlist#1) = [2] x1 + [0]
p(leq) = [0]
p(leq#1) = [0]
p(leq#2) = [0]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [0]
p(#and#) = [0]
p(#cklt#) = [4] x1 + [1]
p(#compare#) = [1] x1 + [0]
p(#eq#) = [1] x1 + [4] x2 + [0]
p(#equal#) = [1]
p(#less#) = [1] x1 + [4] x2 + [0]
p(#or#) = [1] x1 + [2] x2 + [0]
p(and#) = [1] x1 + [1] x2 + [1]
p(insert#) = [1] x2 + [3]
p(insert#1#) = [1] x1 + [2]
p(insert#2#) = [1] x1 + [1] x4 + [3]
p(isortlist#) = [5] x1 + [3]
p(isortlist#1#) = [5] x1 + [3]
p(leq#) = [1] x1 + [0]
p(leq#1#) = [4] x1 + [1]
p(leq#2#) = [2] x1 + [1] x3 + [0]
p(or#) = [1] x1 + [1] x2 + [0]
p(c_1) = [1]
p(c_2) = [4]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [0]
p(c_9) = [1]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [1]
p(c_13) = [1] x1 + [1]
p(c_14) = [0]
p(c_15) = [0]
p(c_16) = [1]
p(c_17) = [1] x1 + [2]
p(c_18) = [0]
p(c_19) = [1]
p(c_20) = [1]
p(c_21) = [2]
p(c_22) = [2]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [0]
p(c_26) = [0]
p(c_27) = [1]
p(c_28) = [0]
p(c_29) = [0]
p(c_30) = [1] x1 + [1]
p(c_31) = [1]
p(c_32) = [0]
p(c_33) = [0]
p(c_34) = [1]
p(c_35) = [0]
p(c_36) = [1] x1 + [0]
p(c_37) = [1]
p(c_38) = [1]
p(c_39) = [2]
p(c_40) = [0]
p(c_41) = [4]
p(c_42) = [1] x1 + [1]
p(c_43) = [2]
p(c_44) = [1]
p(c_45) = [1]
p(c_46) = [4] x1 + [4]
p(c_47) = [1]
p(c_48) = [0]
p(c_49) = [4]
p(c_50) = [0]
p(c_51) = [1]
p(c_52) = [1]
p(c_53) = [1]
p(c_54) = [4]
p(c_55) = [0]
p(c_56) = [1]
Following rules are strictly oriented:
insert#(@x,@l) = [1] @l + [3]
> [1] @l + [2]
= c_4(insert#1#(@l,@x))
Following rules are (at-least) weakly oriented:
insert#1#(::(@y,@ys),@x) = [1] @ys + [3]
>= [1] @ys + [3]
= c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) = [1] @ys + [3]
>= [1] @ys + [3]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [5] @l + [3]
>= [5] @l + [3]
= isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) = [5] @xs + [8]
>= [2] @xs + [4]
= insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) = [5] @xs + [8]
>= [5] @xs + [3]
= isortlist#(@xs)
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#cklt(#EQ()) = [0]
>= [0]
= #false()
#cklt(#GT()) = [0]
>= [0]
= #false()
#cklt(#LT()) = [0]
>= [0]
= #true()
#compare(#0(),#0()) = [0]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#0(),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [0]
>= [0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#pos(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [0]
>= [0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#s(@x),#s(@y)) = [0]
>= [0]
= #compare(@x,@y)
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
#less(@x,@y) = [0]
>= [0]
= #cklt(#compare(@x,@y))
#or(#false(),#false()) = [0]
>= [0]
= #false()
#or(#false(),#true()) = [0]
>= [0]
= #true()
#or(#true(),#false()) = [0]
>= [0]
= #true()
#or(#true(),#true()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
insert(@x,@l) = [1] @l + [1]
>= [1] @l + [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1] @ys + [2]
>= [1] @ys + [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [1]
>= [1]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1] @ys + [2]
>= [1] @ys + [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1] @ys + [2]
>= [1] @ys + [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [2] @l + [1]
>= [2] @l + [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [2] @xs + [2]
>= [2] @xs + [2]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
>= [0]
= nil()
leq(@l1,@l2) = [0]
>= [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0]
>= [0]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [0]
>= [0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [0]
>= [0]
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [0]
>= [0]
= #false()
or(@x,@y) = [1] @x + [1] @y + [0]
>= [0]
= #or(@x,@y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 5.b:1.a:5: EmptyProcessor 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) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 5.b:1.b:1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
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:
insert#(@x,@l) -> insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) -> leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys)
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(#cklt) = {1},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(insert) = {2},
uargs(insert#2) = {1},
uargs(or) = {1,2},
uargs(insert#) = {2},
uargs(insert#2#) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#cklt) = [1] x1 + [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#or) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x1 + [1] x2 + [1]
p(and) = [1] x1 + [1] x2 + [0]
p(insert) = [1] x1 + [1] x2 + [1]
p(insert#1) = [1] x1 + [1] x2 + [1]
p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2]
p(isortlist) = [2] x1 + [2]
p(isortlist#1) = [2] x1 + [1]
p(leq) = [0]
p(leq#1) = [0]
p(leq#2) = [0]
p(nil) = [0]
p(or) = [1] x1 + [1] x2 + [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#) = [1] x2 + [0]
p(insert#1#) = [1] x1 + [0]
p(insert#2#) = [1] x1 + [1] x3 + [1] x4 + [1]
p(isortlist#) = [4] x1 + [0]
p(isortlist#1#) = [4] x1 + [0]
p(leq#) = [1]
p(leq#1#) = [0]
p(leq#2#) = [3]
p(or#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [0]
p(c_15) = [1] x1 + [0]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [0]
p(c_19) = [0]
p(c_20) = [0]
p(c_21) = [0]
p(c_22) = [0]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [0]
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]
> [0]
= c_12(leq#1#(@l1,@l2))
leq#2#(::(@y,@ys),@x,@xs) = [3]
> [1]
= c_15(leq#(@xs,@ys))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [1] @l + [0]
>= [1] @l + [0]
= insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1]
>= [1] @y + [1] @ys + [1]
= insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) = [1] @y + [1] @ys + [1]
>= [1]
= leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) = [1] @y + [1] @ys + [1]
>= [1] @ys + [0]
= insert#(@x,@ys)
isortlist#(@l) = [4] @l + [0]
>= [4] @l + [0]
= isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) = [4] @x + [4] @xs + [4]
>= [2] @xs + [2]
= insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) = [4] @x + [4] @xs + [4]
>= [4] @xs + [0]
= isortlist#(@xs)
leq#1#(::(@x,@xs),@l2) = [0]
>= [3]
= c_13(leq#2#(@l2,@x,@xs))
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#cklt(#EQ()) = [0]
>= [0]
= #false()
#cklt(#GT()) = [0]
>= [0]
= #false()
#cklt(#LT()) = [0]
>= [0]
= #true()
#compare(#0(),#0()) = [0]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#0(),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [0]
>= [0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#pos(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [0]
>= [0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#s(@x),#s(@y)) = [0]
>= [0]
= #compare(@x,@y)
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
#less(@x,@y) = [0]
>= [0]
= #cklt(#compare(@x,@y))
#or(#false(),#false()) = [0]
>= [0]
= #false()
#or(#false(),#true()) = [0]
>= [0]
= #true()
#or(#true(),#false()) = [0]
>= [0]
= #true()
#or(#true(),#true()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
insert(@x,@l) = [1] @l + [1] @x + [1]
>= [1] @l + [1] @x + [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [1] @x + [1]
>= [1] @x + [1]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [2] @l + [2]
>= [2] @l + [1]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [2] @x + [2] @xs + [3]
>= [1] @x + [2] @xs + [3]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [1]
>= [0]
= nil()
leq(@l1,@l2) = [0]
>= [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0]
>= [0]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [0]
>= [0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [0]
>= [0]
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [0]
>= [0]
= #false()
or(@x,@y) = [1] @x + [1] @y + [0]
>= [0]
= #or(@x,@y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 5.b:1.b:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
- Weak DPs:
insert#(@x,@l) -> insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) -> leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys)
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) -> isortlist#(@xs)
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(#cklt) = {1},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(insert) = {2},
uargs(insert#2) = {1},
uargs(or) = {1,2},
uargs(insert#) = {2},
uargs(insert#2#) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [2]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#cklt) = [1] x1 + [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#or) = [1] x2 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [4]
p(#true) = [0]
p(::) = [1] x1 + [1] x2 + [1]
p(and) = [1] x1 + [1] x2 + [0]
p(insert) = [1] x1 + [1] x2 + [1]
p(insert#1) = [1] x1 + [1] x2 + [1]
p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2]
p(isortlist) = [1] x1 + [0]
p(isortlist#1) = [1] x1 + [0]
p(leq) = [0]
p(leq#1) = [0]
p(leq#2) = [0]
p(nil) = [1]
p(or) = [1] x1 + [1] x2 + [0]
p(#and#) = [1] x2 + [0]
p(#cklt#) = [2] x1 + [1]
p(#compare#) = [4] x1 + [1] x2 + [4]
p(#eq#) = [2] x1 + [0]
p(#equal#) = [1] x1 + [2]
p(#less#) = [1] x1 + [2] x2 + [1]
p(#or#) = [4] x1 + [4]
p(and#) = [1] x1 + [1] x2 + [0]
p(insert#) = [1] x1 + [1] x2 + [0]
p(insert#1#) = [1] x1 + [1] x2 + [0]
p(insert#2#) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
p(isortlist#) = [1] x1 + [5]
p(isortlist#1#) = [1] x1 + [4]
p(leq#) = [1] x1 + [0]
p(leq#1#) = [1] x1 + [0]
p(leq#2#) = [1] x2 + [1] x3 + [0]
p(or#) = [1] x2 + [0]
p(c_1) = [1] x1 + [0]
p(c_2) = [4] x1 + [1] x2 + [1]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [2] x1 + [1]
p(c_6) = [2]
p(c_7) = [2]
p(c_8) = [0]
p(c_9) = [4] x1 + [2]
p(c_10) = [1] x1 + [1] x2 + [1]
p(c_11) = [1]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1]
p(c_15) = [1] x1 + [0]
p(c_16) = [1]
p(c_17) = [1] x1 + [0]
p(c_18) = [1]
p(c_19) = [4]
p(c_20) = [4]
p(c_21) = [0]
p(c_22) = [0]
p(c_23) = [0]
p(c_24) = [4]
p(c_25) = [0]
p(c_26) = [4]
p(c_27) = [1]
p(c_28) = [1]
p(c_29) = [4]
p(c_30) = [0]
p(c_31) = [0]
p(c_32) = [1]
p(c_33) = [1]
p(c_34) = [1] x1 + [0]
p(c_35) = [2]
p(c_36) = [1]
p(c_37) = [1]
p(c_38) = [0]
p(c_39) = [4]
p(c_40) = [1]
p(c_41) = [0]
p(c_42) = [0]
p(c_43) = [1]
p(c_44) = [4]
p(c_45) = [0]
p(c_46) = [4] x1 + [0]
p(c_47) = [0]
p(c_48) = [1] x1 + [2]
p(c_49) = [1] x1 + [1]
p(c_50) = [0]
p(c_51) = [1]
p(c_52) = [1]
p(c_53) = [1]
p(c_54) = [0]
p(c_55) = [1]
p(c_56) = [0]
Following rules are strictly oriented:
leq#1#(::(@x,@xs),@l2) = [1] @x + [1] @xs + [1]
> [1] @x + [1] @xs + [0]
= c_13(leq#2#(@l2,@x,@xs))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [1] @l + [1] @x + [0]
>= [1] @l + [1] @x + [0]
= insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [1]
>= [1] @x + [1] @y + [1] @ys + [0]
= insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [1]
>= [1] @x + [0]
= leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [0]
>= [1] @x + [1] @ys + [0]
= insert#(@x,@ys)
isortlist#(@l) = [1] @l + [5]
>= [1] @l + [4]
= isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) = [1] @x + [1] @xs + [5]
>= [1] @x + [1] @xs + [0]
= insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@xs)) = [1] @x + [1] @xs + [5]
>= [1] @xs + [5]
= isortlist#(@xs)
leq#(@l1,@l2) = [1] @l1 + [0]
>= [1] @l1 + [0]
= c_12(leq#1#(@l1,@l2))
leq#2#(::(@y,@ys),@x,@xs) = [1] @x + [1] @xs + [0]
>= [1] @xs + [0]
= c_15(leq#(@xs,@ys))
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#cklt(#EQ()) = [0]
>= [0]
= #false()
#cklt(#GT()) = [0]
>= [0]
= #false()
#cklt(#LT()) = [0]
>= [0]
= #true()
#compare(#0(),#0()) = [0]
>= [0]
= #EQ()
#compare(#0(),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#0(),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#0(),#s(@y)) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#0()) = [0]
>= [0]
= #LT()
#compare(#neg(@x),#neg(@y)) = [0]
>= [0]
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = [0]
>= [0]
= #LT()
#compare(#pos(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#neg(@y)) = [0]
>= [0]
= #GT()
#compare(#pos(@x),#pos(@y)) = [0]
>= [0]
= #compare(@x,@y)
#compare(#s(@x),#0()) = [0]
>= [0]
= #GT()
#compare(#s(@x),#s(@y)) = [0]
>= [0]
= #compare(@x,@y)
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
#less(@x,@y) = [0]
>= [0]
= #cklt(#compare(@x,@y))
#or(#false(),#false()) = [0]
>= [0]
= #false()
#or(#false(),#true()) = [0]
>= [0]
= #true()
#or(#true(),#false()) = [0]
>= [0]
= #true()
#or(#true(),#true()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
insert(@x,@l) = [1] @l + [1] @x + [1]
>= [1] @l + [1] @x + [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [1] @x + [2]
>= [1] @x + [2]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2]
>= [1] @x + [1] @y + [1] @ys + [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [1] @l + [0]
>= [1] @l + [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [1] @x + [1] @xs + [1]
>= [1] @x + [1] @xs + [1]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [1]
>= [1]
= nil()
leq(@l1,@l2) = [0]
>= [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0]
>= [0]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [0]
>= [0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [0]
>= [0]
= or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [0]
>= [0]
= #false()
or(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @y + [0]
= #or(@x,@y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 5.b:1.b:3: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
insert#(@x,@l) -> insert#1#(@l,@x)
insert#1#(::(@y,@ys),@x) -> insert#2#(leq(@x,@y),@x,@y,@ys)
insert#1#(::(@y,@ys),@x) -> leq#(@x,@y)
insert#2#(#false(),@x,@y,@ys) -> insert#(@x,@ys)
isortlist#(@l) -> isortlist#1#(@l)
isortlist#1#(::(@x,@xs)) -> insert#(@x,isortlist(@xs))
isortlist#1#(::(@x,@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:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^3))