*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
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.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
#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))
Strict TRS Rules:
Weak DP Rules:
#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 Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
#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 Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
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()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Problem (S)
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1
,@l2))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys)
,leq#(@x,@y))
3: insert#2#(#false(),@x,@y,@ys) ->
c_7(insert#(@x,@ys))
4: isortlist#(@l) ->
c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) ->
c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1
,@l2))
7: leq#1#(::(@x,@xs),@l2) ->
c_13(leq#2#(@l2,@x,@xs))
8: leq#2#(::(@y,@ys),@x,@xs) ->
c_15(leq#(@xs,@ys))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{6}
These cover all (indirect) predecessors of dependency pairs
{6,7,8}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_5) = {1,2},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2},
uargs(c_12) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1}
Following symbols are considered usable:
{#and,#or,and,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = 1
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#and) = 1
p(#cklt) = 1
p(#compare) = 0
p(#eq) = x2^2
p(#equal) = 0
p(#false) = 1
p(#less) = 0
p(#neg) = 0
p(#or) = x2
p(#pos) = 0
p(#s) = 0
p(#true) = 1
p(::) = 1 + x1 + x2
p(and) = 1
p(insert) = 1 + x1 + x2
p(insert#1) = 1 + x1 + x2
p(insert#2) = 1 + x1 + x2 + x3 + x4
p(isortlist) = x1
p(isortlist#1) = x1
p(leq) = 1
p(leq#1) = 1
p(leq#2) = 1
p(nil) = 0
p(or) = x2
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#) = x2
p(insert#1#) = x1
p(insert#2#) = x4
p(isortlist#) = 1 + x1^2
p(isortlist#1#) = 1 + x1^2
p(leq#) = 1 + x2
p(leq#1#) = x2
p(leq#2#) = x1
p(or#) = 0
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = x1
p(c_5) = x1 + x2
p(c_6) = 0
p(c_7) = x1
p(c_8) = 0
p(c_9) = x1
p(c_10) = 1 + x1 + x2
p(c_11) = 0
p(c_12) = x1
p(c_13) = x1
p(c_14) = 0
p(c_15) = x1
p(c_16) = 0
p(c_17) = 0
p(c_18) = 0
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = 0
p(c_25) = 0
p(c_26) = 0
p(c_27) = 0
p(c_28) = 0
p(c_29) = 0
p(c_30) = 0
p(c_31) = 0
p(c_32) = 0
p(c_33) = 0
p(c_34) = 0
p(c_35) = 0
p(c_36) = 0
p(c_37) = 0
p(c_38) = 0
p(c_39) = 0
p(c_40) = 0
p(c_41) = 0
p(c_42) = 0
p(c_43) = 0
p(c_44) = 0
p(c_45) = 0
p(c_46) = 0
p(c_47) = 0
p(c_48) = 0
p(c_49) = 0
p(c_50) = 0
p(c_51) = 0
p(c_52) = 0
p(c_53) = 0
p(c_54) = 0
p(c_55) = 0
p(c_56) = 0
Following rules are strictly oriented:
leq#(@l1,@l2) = 1 + @l2
> @l2
= c_12(leq#1#(@l1,@l2))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = @l
>= @l
= c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) = 1 + @y + @ys
>= 1 + @y + @ys
= c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys)
,leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) = @ys
>= @ys
= c_7(insert#(@x,@ys))
isortlist#(@l) = 1 + @l^2
>= 1 + @l^2
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = 2 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2
>= 2 + @xs + @xs^2
= c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
leq#1#(::(@x,@xs),@l2) = @l2
>= @l2
= c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) = 1 + @y + @ys
>= 1 + @ys
= c_15(leq#(@xs,@ys))
#and(#false(),#false()) = 1
>= 1
= #false()
#and(#false(),#true()) = 1
>= 1
= #false()
#and(#true(),#false()) = 1
>= 1
= #false()
#and(#true(),#true()) = 1
>= 1
= #true()
#or(#false(),#false()) = 1
>= 1
= #false()
#or(#false(),#true()) = 1
>= 1
= #true()
#or(#true(),#false()) = 1
>= 1
= #true()
#or(#true(),#true()) = 1
>= 1
= #true()
and(@x,@y) = 1
>= 1
= #and(@x,@y)
insert(@x,@l) = 1 + @l + @x
>= 1 + @l + @x
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = 1 + @x
>= 1 + @x
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@x,::(@y,@ys))
isortlist(@l) = @l
>= @l
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = 1 + @x + @xs
>= 1 + @x + @xs
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = 0
>= 0
= nil()
leq(@l1,@l2) = 1
>= 1
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = 1
>= 1
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = 1
>= 1
= #true()
leq#2(::(@y,@ys),@x,@xs) = 1
>= 1
= or(#less(@x,@y)
,and(#equal(@x,@y)
,leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = 1
>= 1
= #false()
or(@x,@y) = @y
>= @y
= #or(@x,@y)
*** 1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8
8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
-->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1
,@l2))
8: leq#2#(::(@y,@ys),@x,@xs) ->
c_15(leq#(@xs,@ys))
7: leq#1#(::(@x,@xs),@l2) ->
c_13(leq#2#(@l2,@x,@xs))
*** 1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):2
2:S:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:S:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
*** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
2: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
3: insert#2#(#false(),@x,@y,@ys) ->
c_7(insert#(@x,@ys))
4: isortlist#(@l) ->
c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) ->
c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{2}
These cover all (indirect) predecessors of dependency pairs
{2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2}
Following symbols are considered usable:
{#or,insert,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or,#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [2]
[0]
p(#EQ) = [0]
[0]
p(#GT) = [0]
[1]
p(#LT) = [0]
[1]
p(#and) = [2 0] x1 + [1 0] x2 + [2]
[1 0] [1 0] [2]
p(#cklt) = [0]
[0]
p(#compare) = [0 0] x1 + [1]
[0 1] [1]
p(#eq) = [1 0] x1 + [2 0] x2 + [1]
[0 0] [0 0] [2]
p(#equal) = [0]
[0]
p(#false) = [1]
[0]
p(#less) = [0]
[0]
p(#neg) = [1 0] x1 + [0]
[0 0] [1]
p(#or) = [1]
[0]
p(#pos) = [0 0] x1 + [1]
[0 1] [0]
p(#s) = [0 1] x1 + [0]
[0 1] [1]
p(#true) = [1]
[0]
p(::) = [1 1] x2 + [0]
[0 1] [2]
p(and) = [0 0] x2 + [0]
[2 2] [2]
p(insert) = [1 1] x2 + [0]
[0 1] [2]
p(insert#1) = [1 1] x1 + [0]
[0 1] [2]
p(insert#2) = [2 0] x1 + [1 2] x4 + [0]
[2 0] [0 1] [2]
p(isortlist) = [1 2] x1 + [0]
[0 1] [0]
p(isortlist#1) = [1 2] x1 + [0]
[0 1] [0]
p(leq) = [0 0] x1 + [1]
[0 2] [1]
p(leq#1) = [0 0] x1 + [1]
[0 1] [0]
p(leq#2) = [1]
[2]
p(nil) = [0]
[0]
p(or) = [1]
[2]
p(#and#) = [0 2] x2 + [0]
[1 2] [1]
p(#cklt#) = [1 1] x1 + [0]
[0 0] [2]
p(#compare#) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [1 1] [1]
p(#eq#) = [2 0] x2 + [0]
[1 0] [1]
p(#equal#) = [0 0] x1 + [2]
[1 2] [1]
p(#less#) = [1 0] x2 + [0]
[0 2] [1]
p(#or#) = [0 0] x1 + [0 0] x2 + [0]
[0 2] [1 0] [2]
p(and#) = [0 2] x1 + [2]
[1 0] [0]
p(insert#) = [0 1] x2 + [0]
[2 0] [2]
p(insert#1#) = [0 1] x1 + [0 0] x2 + [0]
[2 0] [2 0] [3]
p(insert#2#) = [0 1] x4 + [0]
[0 0] [1]
p(isortlist#) = [1 1] x1 + [0]
[3 3] [2]
p(isortlist#1#) = [1 1] x1 + [0]
[2 0] [0]
p(leq#) = [0 1] x2 + [0]
[0 0] [0]
p(leq#1#) = [0 0] x1 + [0]
[2 0] [1]
p(leq#2#) = [0 2] x1 + [0 0] x3 + [1]
[0 0] [2 0] [0]
p(or#) = [1 2] x1 + [2]
[0 2] [0]
p(c_1) = [0]
[0]
p(c_2) = [0 0] x2 + [1]
[1 0] [0]
p(c_3) = [0]
[0]
p(c_4) = [1 0] x1 + [0]
[0 0] [2]
p(c_5) = [1 1] x1 + [0]
[0 3] [0]
p(c_6) = [2]
[0]
p(c_7) = [1 0] x1 + [0]
[0 0] [0]
p(c_8) = [1]
[0]
p(c_9) = [1 0] x1 + [0]
[3 0] [1]
p(c_10) = [1 0] x1 + [1 0] x2 + [2]
[1 0] [1 0] [0]
p(c_11) = [2]
[2]
p(c_12) = [2 0] x1 + [0]
[0 0] [0]
p(c_13) = [0]
[0]
p(c_14) = [0]
[1]
p(c_15) = [2]
[0]
p(c_16) = [0]
[0]
p(c_17) = [2 2] x1 + [0]
[1 0] [0]
p(c_18) = [0]
[0]
p(c_19) = [0]
[2]
p(c_20) = [1]
[2]
p(c_21) = [0]
[0]
p(c_22) = [0]
[0]
p(c_23) = [2]
[2]
p(c_24) = [1]
[1]
p(c_25) = [2]
[0]
p(c_26) = [1]
[0]
p(c_27) = [0]
[0]
p(c_28) = [2]
[0]
p(c_29) = [1]
[2]
p(c_30) = [0 0] x1 + [0]
[1 2] [0]
p(c_31) = [2]
[0]
p(c_32) = [0]
[0]
p(c_33) = [1]
[1]
p(c_34) = [1]
[1]
p(c_35) = [2]
[0]
p(c_36) = [2 2] x1 + [0]
[0 2] [0]
p(c_37) = [0]
[2]
p(c_38) = [0]
[0]
p(c_39) = [2]
[0]
p(c_40) = [1]
[1]
p(c_41) = [0]
[1]
p(c_42) = [1]
[2]
p(c_43) = [1]
[0]
p(c_44) = [1]
[0]
p(c_45) = [0]
[0]
p(c_46) = [2 2] x1 + [0]
[1 2] [1]
p(c_47) = [0]
[0]
p(c_48) = [1 2] x1 + [0]
[2 2] [2]
p(c_49) = [2 0] x3 + [1]
[0 2] [0]
p(c_50) = [0]
[0]
p(c_51) = [0]
[0]
p(c_52) = [2]
[0]
p(c_53) = [0]
[0]
p(c_54) = [1]
[1]
p(c_55) = [0]
[0]
p(c_56) = [1]
[2]
Following rules are strictly oriented:
insert#1#(::(@y,@ys),@x) = [0 0] @x + [0 1] @ys + [2]
[2 0] [2 2] [3]
> [0 1] @ys + [1]
[0 0] [3]
= c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
Following rules are (at-least) weakly oriented:
insert#(@x,@l) = [0 1] @l + [0]
[2 0] [2]
>= [0 1] @l + [0]
[0 0] [2]
= c_4(insert#1#(@l,@x))
insert#2#(#false(),@x,@y,@ys) = [0 1] @ys + [0]
[0 0] [1]
>= [0 1] @ys + [0]
[0 0] [0]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [1 1] @l + [0]
[3 3] [2]
>= [1 1] @l + [0]
[3 3] [1]
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = [1 2] @xs + [2]
[2 2] [0]
>= [1 2] @xs + [2]
[1 2] [0]
= c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
#or(#false(),#false()) = [1]
[0]
>= [1]
[0]
= #false()
#or(#false(),#true()) = [1]
[0]
>= [1]
[0]
= #true()
#or(#true(),#false()) = [1]
[0]
>= [1]
[0]
= #true()
#or(#true(),#true()) = [1]
[0]
>= [1]
[0]
= #true()
insert(@x,@l) = [1 1] @l + [0]
[0 1] [2]
>= [1 1] @l + [0]
[0 1] [2]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1 2] @ys + [2]
[0 1] [4]
>= [1 2] @ys + [2]
[0 1] [4]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [0]
[2]
>= [0]
[2]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1 2] @ys + [2]
[0 1] [4]
>= [1 2] @ys + [2]
[0 1] [4]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1 2] @ys + [2]
[0 1] [4]
>= [1 2] @ys + [2]
[0 1] [4]
= ::(@x,::(@y,@ys))
isortlist(@l) = [1 2] @l + [0]
[0 1] [0]
>= [1 2] @l + [0]
[0 1] [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [1 3] @xs + [4]
[0 1] [2]
>= [1 3] @xs + [0]
[0 1] [2]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
leq(@l1,@l2) = [0 0] @l1 + [1]
[0 2] [1]
>= [0 0] @l1 + [1]
[0 1] [0]
= leq#1(@l1,@l2)
leq#1(::(@x,@xs),@l2) = [0 0] @xs + [1]
[0 1] [2]
>= [1]
[2]
= leq#2(@l2,@x,@xs)
leq#1(nil(),@l2) = [1]
[0]
>= [1]
[0]
= #true()
leq#2(::(@y,@ys),@x,@xs) = [1]
[2]
>= [1]
[2]
= or(#less(@x,@y)
,and(#equal(@x,@y)
,leq(@xs,@ys)))
leq#2(nil(),@x,@xs) = [1]
[2]
>= [1]
[0]
= #false()
or(@x,@y) = [1]
[2]
>= [1]
[0]
= #or(@x,@y)
*** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
Strict TRS Rules:
Weak DP Rules:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
Strict TRS Rules:
Weak DP Rules:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
3: insert#2#(#false(),@x,@y,@ys) ->
c_7(insert#(@x,@ys))
4: isortlist#(@l) ->
c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) ->
c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.2.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
Strict TRS Rules:
Weak DP Rules:
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1,2}
Following symbols are considered usable:
{insert,insert#1,insert#2,isortlist,isortlist#1,#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [3]
[0]
p(#EQ) = [1]
[0]
p(#GT) = [0]
[3]
p(#LT) = [2]
[0]
p(#and) = [1 1] x1 + [1 0] x2 + [2]
[0 2] [0 0] [2]
p(#cklt) = [1 1] x1 + [3]
[0 2] [0]
p(#compare) = [1 1] x1 + [0 0] x2 + [1]
[1 1] [1 0] [0]
p(#eq) = [2 0] x1 + [1]
[1 1] [2]
p(#equal) = [2 0] x1 + [1 0] x2 + [0]
[1 0] [2 2] [1]
p(#false) = [0]
[0]
p(#less) = [0 1] x1 + [1 2] x2 + [0]
[0 2] [1 1] [0]
p(#neg) = [0 2] x1 + [0]
[0 1] [0]
p(#or) = [2]
[2]
p(#pos) = [0 2] x1 + [1]
[0 0] [2]
p(#s) = [1 0] x1 + [3]
[0 0] [0]
p(#true) = [0]
[0]
p(::) = [1 1] x2 + [0]
[0 1] [1]
p(and) = [1 2] x1 + [0 0] x2 + [2]
[2 2] [2 0] [2]
p(insert) = [1 1] x2 + [0]
[0 1] [1]
p(insert#1) = [1 1] x1 + [0]
[0 1] [1]
p(insert#2) = [1 2] x4 + [1]
[0 1] [2]
p(isortlist) = [2 0] x1 + [0]
[0 2] [0]
p(isortlist#1) = [2 0] x1 + [0]
[0 2] [0]
p(leq) = [0]
[0]
p(leq#1) = [0]
[0]
p(leq#2) = [0]
[0]
p(nil) = [0]
[0]
p(or) = [1 2] x1 + [0 0] x2 + [0]
[1 0] [1 0] [0]
p(#and#) = [0]
[2]
p(#cklt#) = [2]
[0]
p(#compare#) = [0]
[1]
p(#eq#) = [0]
[0]
p(#equal#) = [0]
[2]
p(#less#) = [0 0] x1 + [2]
[0 2] [1]
p(#or#) = [0 0] x2 + [0]
[0 2] [0]
p(and#) = [1]
[0]
p(insert#) = [0 0] x1 + [0 1] x2 + [1]
[2 0] [2 3] [2]
p(insert#1#) = [0 1] x1 + [0 0] x2 + [0]
[0 0] [2 2] [0]
p(insert#2#) = [0 1] x4 + [1]
[0 1] [0]
p(isortlist#) = [2 2] x1 + [1]
[2 0] [0]
p(isortlist#1#) = [2 2] x1 + [0]
[0 0] [0]
p(leq#) = [0 0] x2 + [0]
[0 1] [0]
p(leq#1#) = [2]
[0]
p(leq#2#) = [1 2] x2 + [1]
[2 0] [1]
p(or#) = [0 0] x2 + [0]
[2 0] [2]
p(c_1) = [1 2] x1 + [0]
[0 2] [1]
p(c_2) = [1 2] x1 + [2 1] x2 + [0]
[0 1] [0 0] [1]
p(c_3) = [0 0] x1 + [0]
[0 1] [0]
p(c_4) = [1 0] x1 + [0]
[3 0] [0]
p(c_5) = [1 0] x1 + [0]
[0 0] [0]
p(c_6) = [0]
[1]
p(c_7) = [1 0] x1 + [0]
[0 0] [0]
p(c_8) = [0]
[0]
p(c_9) = [1 0] x1 + [0]
[0 0] [0]
p(c_10) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
p(c_11) = [0]
[0]
p(c_12) = [2]
[0]
p(c_13) = [0]
[0]
p(c_14) = [0]
[0]
p(c_15) = [0 1] x1 + [1]
[0 0] [0]
p(c_16) = [0]
[0]
p(c_17) = [0]
[1]
p(c_18) = [0]
[0]
p(c_19) = [0]
[0]
p(c_20) = [0]
[1]
p(c_21) = [2]
[2]
p(c_22) = [0]
[0]
p(c_23) = [0]
[0]
p(c_24) = [0]
[0]
p(c_25) = [0]
[0]
p(c_26) = [1]
[1]
p(c_27) = [0]
[1]
p(c_28) = [0]
[2]
p(c_29) = [0]
[0]
p(c_30) = [0 0] x1 + [1]
[0 1] [0]
p(c_31) = [0]
[0]
p(c_32) = [0]
[1]
p(c_33) = [0]
[1]
p(c_34) = [2 1] x1 + [0]
[0 0] [1]
p(c_35) = [2]
[1]
p(c_36) = [0 0] x1 + [2]
[2 0] [2]
p(c_37) = [0]
[0]
p(c_38) = [0]
[0]
p(c_39) = [1]
[2]
p(c_40) = [0]
[2]
p(c_41) = [1]
[2]
p(c_42) = [2 2] x1 + [0]
[0 0] [1]
p(c_43) = [0]
[1]
p(c_44) = [0]
[2]
p(c_45) = [0]
[2]
p(c_46) = [2]
[2]
p(c_47) = [1]
[1]
p(c_48) = [0]
[0]
p(c_49) = [1 1] x1 + [0]
[2 0] [0]
p(c_50) = [2]
[0]
p(c_51) = [0]
[2]
p(c_52) = [0]
[2]
p(c_53) = [0]
[0]
p(c_54) = [0]
[2]
p(c_55) = [1]
[0]
p(c_56) = [1]
[2]
Following rules are strictly oriented:
insert#(@x,@l) = [0 1] @l + [0 0] @x + [1]
[2 3] [2 0] [2]
> [0 1] @l + [0]
[0 3] [0]
= c_4(insert#1#(@l,@x))
Following rules are (at-least) weakly oriented:
insert#1#(::(@y,@ys),@x) = [0 0] @x + [0 1] @ys + [1]
[2 2] [0 0] [0]
>= [0 1] @ys + [1]
[0 0] [0]
= c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
insert#2#(#false(),@x,@y,@ys) = [0 1] @ys + [1]
[0 1] [0]
>= [0 1] @ys + [1]
[0 0] [0]
= c_7(insert#(@x,@ys))
isortlist#(@l) = [2 2] @l + [1]
[2 0] [0]
>= [2 2] @l + [0]
[0 0] [0]
= c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) = [2 4] @xs + [2]
[0 0] [0]
>= [2 4] @xs + [2]
[0 0] [0]
= c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
insert(@x,@l) = [1 1] @l + [0]
[0 1] [1]
>= [1 1] @l + [0]
[0 1] [1]
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= insert#2(leq(@x,@y),@x,@y,@ys)
insert#1(nil(),@x) = [0]
[1]
>= [0]
[1]
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= ::(@y,insert(@x,@ys))
insert#2(#true(),@x,@y,@ys) = [1 2] @ys + [1]
[0 1] [2]
>= [1 2] @ys + [1]
[0 1] [2]
= ::(@x,::(@y,@ys))
isortlist(@l) = [2 0] @l + [0]
[0 2] [0]
>= [2 0] @l + [0]
[0 2] [0]
= isortlist#1(@l)
isortlist#1(::(@x,@xs)) = [2 2] @xs + [0]
[0 2] [2]
>= [2 2] @xs + [0]
[0 2] [1]
= insert(@x,isortlist(@xs))
isortlist#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
*** 1.1.1.1.1.1.2.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys)):2
2:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys))
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):3
3:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
4:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):5
5:W:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):4
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: isortlist#(@l) ->
c_9(isortlist#1#(@l))
5: isortlist#1#(::(@x,@xs)) ->
c_10(insert#(@x,isortlist(@xs))
,isortlist#(@xs))
1: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
3: insert#2#(#false(),@x,@y,@ys) ->
c_7(insert#(@x,@ys))
2: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys))
*** 1.1.1.1.1.1.2.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
insert#(@x,@l) -> c_4(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs)):2
2:S:isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3
-->_2 isortlist#(@l) -> c_9(isortlist#1#(@l)):1
3:W:insert#(@x,@l) -> c_4(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y)):4
4:W:insert#1#(::(@y,@ys),@x) -> c_5(insert#2#(leq(@x,@y),@x,@y,@ys),leq#(@x,@y))
-->_2 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys)):5
5:W:insert#2#(#false(),@x,@y,@ys) -> c_7(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_4(insert#1#(@l,@x)):3
6:W:leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2))
-->_1 leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs)):7
7:W:leq#1#(::(@x,@xs),@l2) -> c_13(leq#2#(@l2,@x,@xs))
-->_1 leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys)):8
8:W:leq#2#(::(@y,@ys),@x,@xs) -> c_15(leq#(@xs,@ys))
-->_1 leq#(@l1,@l2) -> c_12(leq#1#(@l1,@l2)):6
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: insert#(@x,@l) ->
c_4(insert#1#(@l,@x))
5: insert#2#(#false(),@x,@y,@ys) ->
c_7(insert#(@x,@ys))
4: insert#1#(::(@y,@ys),@x) ->
c_5(insert#2#(leq(@x,@y)
,@x
,@y
,@ys)
,leq#(@x,@y))
6: leq#(@l1,@l2) -> c_12(leq#1#(@l1
,@l2))
8: leq#2#(::(@y,@ys),@x,@xs) ->
c_15(leq#(@xs,@ys))
7: leq#1#(::(@x,@xs),@l2) ->
c_13(leq#2#(@l2,@x,@xs))
*** 1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(insert#(@x,isortlist(@xs)),isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
SimplifyRHS
Proof:
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))
*** 1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
*** 1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
2: isortlist#1#(::(@x,@xs)) ->
c_10(isortlist#(@xs))
Consider the set of all dependency pairs
1: isortlist#(@l) ->
c_9(isortlist#1#(@l))
2: isortlist#1#(::(@x,@xs)) ->
c_10(isortlist#(@xs))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{2}
These cover all (indirect) predecessors of dependency pairs
{1,2}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_10) = {1}
Following symbols are considered usable:
{#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}
TcT has computed the following interpretation:
p(#0) = [2]
p(#EQ) = [0]
p(#GT) = [2]
p(#LT) = [1]
p(#and) = [1] x1 + [0]
p(#cklt) = [0]
p(#compare) = [0]
p(#eq) = [0]
p(#equal) = [1] x1 + [1] x2 + [1]
p(#false) = [0]
p(#less) = [4] x1 + [0]
p(#neg) = [1] x1 + [0]
p(#or) = [1] x1 + [2] x2 + [0]
p(#pos) = [0]
p(#s) = [0]
p(#true) = [0]
p(::) = [1] x2 + [1]
p(and) = [1] x2 + [0]
p(insert) = [0]
p(insert#1) = [1] x2 + [0]
p(insert#2) = [1] x1 + [4] x2 + [4] x3 + [2] x4 + [0]
p(isortlist) = [2] x1 + [0]
p(isortlist#1) = [0]
p(leq) = [1] x2 + [0]
p(leq#1) = [1] x2 + [0]
p(leq#2) = [1] x1 + [2] x2 + [0]
p(nil) = [0]
p(or) = [1] x2 + [0]
p(#and#) = [2] x1 + [0]
p(#cklt#) = [1] x1 + [0]
p(#compare#) = [1] x2 + [2]
p(#eq#) = [1] x1 + [1]
p(#equal#) = [1] x1 + [2] x2 + [2]
p(#less#) = [2] x2 + [1]
p(#or#) = [1] x1 + [1] x2 + [1]
p(and#) = [2] x1 + [1]
p(insert#) = [4] x2 + [0]
p(insert#1#) = [1] x1 + [1]
p(insert#2#) = [2] x3 + [0]
p(isortlist#) = [8] x1 + [0]
p(isortlist#1#) = [8] x1 + [0]
p(leq#) = [2]
p(leq#1#) = [2] x2 + [0]
p(leq#2#) = [1] x1 + [1] x2 + [2] x3 + [2]
p(or#) = [8] x1 + [4]
p(c_1) = [2] x1 + [1]
p(c_2) = [1] x1 + [8]
p(c_3) = [1] x1 + [1]
p(c_4) = [1] x1 + [1]
p(c_5) = [2] x1 + [8]
p(c_6) = [0]
p(c_7) = [8] x1 + [8]
p(c_8) = [8]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [0]
p(c_12) = [2] x1 + [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) = [1]
p(c_39) = [0]
p(c_40) = [0]
p(c_41) = [1]
p(c_42) = [0]
p(c_43) = [0]
p(c_44) = [1]
p(c_45) = [1]
p(c_46) = [2]
p(c_47) = [1]
p(c_48) = [1]
p(c_49) = [2]
p(c_50) = [0]
p(c_51) = [2]
p(c_52) = [1]
p(c_53) = [0]
p(c_54) = [8]
p(c_55) = [0]
p(c_56) = [1]
Following rules are strictly oriented:
isortlist#1#(::(@x,@xs)) = [8] @xs + [8]
> [8] @xs + [0]
= c_10(isortlist#(@xs))
Following rules are (at-least) weakly oriented:
isortlist#(@l) = [8] @l + [0]
>= [8] @l + [0]
= c_9(isortlist#1#(@l))
*** 1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
Strict TRS Rules:
Weak DP Rules:
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
Weak TRS Rules:
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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
isortlist#(@l) -> c_9(isortlist#1#(@l))
isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
Weak TRS Rules:
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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:isortlist#(@l) -> c_9(isortlist#1#(@l))
-->_1 isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs)):2
2:W:isortlist#1#(::(@x,@xs)) -> c_10(isortlist#(@xs))
-->_1 isortlist#(@l) -> c_9(isortlist#1#(@l)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: isortlist#(@l) ->
c_9(isortlist#1#(@l))
2: isortlist#1#(::(@x,@xs)) ->
c_10(isortlist#(@xs))
*** 1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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
basic terms: {#and#,#cklt#,#compare#,#eq#,#equal#,#less#,#or#,and#,insert#,insert#1#,insert#2#,isortlist#,isortlist#1#,leq#,leq#1#,leq#2#,or#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).