*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
flattensort(@t) -> insertionsort(flatten(@t))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Weak DP Rules:
Weak TRS Rules:
#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)
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3}
Obligation:
Innermost
basic terms: {#cklt,#compare,#less,append,append#1,flatten,flatten#1,flattensort,insert,insert#1,insert#2,insertionsort,insertionsort#1}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
append#1#(nil(),@l2) -> c_4()
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(leaf()) -> c_6()
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#1#(nil(),@x) -> c_11()
insert#2#(#false(),@x,@y,@ys) -> c_12()
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
insertionsort#1#(nil()) -> c_16()
Weak DPs
#cklt#(#EQ()) -> c_17()
#cklt#(#GT()) -> c_18()
#cklt#(#LT()) -> c_19()
#compare#(#0(),#0()) -> c_20()
#compare#(#0(),#neg(@y)) -> c_21()
#compare#(#0(),#pos(@y)) -> c_22()
#compare#(#0(),#s(@y)) -> c_23()
#compare#(#neg(@x),#0()) -> c_24()
#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_26()
#compare#(#pos(@x),#0()) -> c_27()
#compare#(#pos(@x),#neg(@y)) -> c_28()
#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_30()
#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
append#1#(nil(),@l2) -> c_4()
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(leaf()) -> c_6()
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#1#(nil(),@x) -> c_11()
insert#2#(#false(),@x,@y,@ys) -> c_12()
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
insertionsort#1#(nil()) -> c_16()
Strict TRS Rules:
Weak DP Rules:
#cklt#(#EQ()) -> c_17()
#cklt#(#GT()) -> c_18()
#cklt#(#LT()) -> c_19()
#compare#(#0(),#0()) -> c_20()
#compare#(#0(),#neg(@y)) -> c_21()
#compare#(#0(),#pos(@y)) -> c_22()
#compare#(#0(),#s(@y)) -> c_23()
#compare#(#neg(@x),#0()) -> c_24()
#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_26()
#compare#(#pos(@x),#0()) -> c_27()
#compare#(#pos(@x),#neg(@y)) -> c_28()
#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_30()
#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
flattensort(@t) -> insertionsort(flatten(@t))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/2,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
#cklt#(#EQ()) -> c_17()
#cklt#(#GT()) -> c_18()
#cklt#(#LT()) -> c_19()
#compare#(#0(),#0()) -> c_20()
#compare#(#0(),#neg(@y)) -> c_21()
#compare#(#0(),#pos(@y)) -> c_22()
#compare#(#0(),#s(@y)) -> c_23()
#compare#(#neg(@x),#0()) -> c_24()
#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_26()
#compare#(#pos(@x),#0()) -> c_27()
#compare#(#pos(@x),#neg(@y)) -> c_28()
#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_30()
#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
append#1#(nil(),@l2) -> c_4()
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(leaf()) -> c_6()
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#1#(nil(),@x) -> c_11()
insert#2#(#false(),@x,@y,@ys) -> c_12()
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
insertionsort#1#(nil()) -> c_16()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
append#1#(nil(),@l2) -> c_4()
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(leaf()) -> c_6()
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#1#(nil(),@x) -> c_11()
insert#2#(#false(),@x,@y,@ys) -> c_12()
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
insertionsort#1#(nil()) -> c_16()
Strict TRS Rules:
Weak DP Rules:
#cklt#(#EQ()) -> c_17()
#cklt#(#GT()) -> c_18()
#cklt#(#LT()) -> c_19()
#compare#(#0(),#0()) -> c_20()
#compare#(#0(),#neg(@y)) -> c_21()
#compare#(#0(),#pos(@y)) -> c_22()
#compare#(#0(),#s(@y)) -> c_23()
#compare#(#neg(@x),#0()) -> c_24()
#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_26()
#compare#(#pos(@x),#0()) -> c_27()
#compare#(#pos(@x),#neg(@y)) -> c_28()
#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_30()
#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/2,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,4,6,11,12,16}
by application of
Pre({1,4,6,11,12,16}) = {2,5,9,10,14}.
Here rules are labelled as follows:
1: #less#(@x,@y) ->
c_1(#cklt#(#compare(@x,@y))
,#compare#(@x,@y))
2: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
3: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
4: append#1#(nil(),@l2) -> c_4()
5: flatten#(@t) ->
c_5(flatten#1#(@t))
6: flatten#1#(leaf()) -> c_6()
7: flatten#1#(node(@l,@t1,@t2)) ->
c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
8: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t))
,flatten#(@t))
9: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
10: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys)
,#less#(@y,@x))
11: insert#1#(nil(),@x) -> c_11()
12: insert#2#(#false(),@x,@y,@ys) ->
c_12()
13: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
14: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
15: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
16: insertionsort#1#(nil()) ->
c_16()
17: #cklt#(#EQ()) -> c_17()
18: #cklt#(#GT()) -> c_18()
19: #cklt#(#LT()) -> c_19()
20: #compare#(#0(),#0()) -> c_20()
21: #compare#(#0(),#neg(@y)) ->
c_21()
22: #compare#(#0(),#pos(@y)) ->
c_22()
23: #compare#(#0(),#s(@y)) -> c_23()
24: #compare#(#neg(@x),#0()) ->
c_24()
25: #compare#(#neg(@x),#neg(@y)) ->
c_25(#compare#(@y,@x))
26: #compare#(#neg(@x),#pos(@y)) ->
c_26()
27: #compare#(#pos(@x),#0()) ->
c_27()
28: #compare#(#pos(@x),#neg(@y)) ->
c_28()
29: #compare#(#pos(@x),#pos(@y)) ->
c_29(#compare#(@x,@y))
30: #compare#(#s(@x),#0()) -> c_30()
31: #compare#(#s(@x),#s(@y)) ->
c_31(#compare#(@x,@y))
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
#cklt#(#EQ()) -> c_17()
#cklt#(#GT()) -> c_18()
#cklt#(#LT()) -> c_19()
#compare#(#0(),#0()) -> c_20()
#compare#(#0(),#neg(@y)) -> c_21()
#compare#(#0(),#pos(@y)) -> c_22()
#compare#(#0(),#s(@y)) -> c_23()
#compare#(#neg(@x),#0()) -> c_24()
#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
#compare#(#neg(@x),#pos(@y)) -> c_26()
#compare#(#pos(@x),#0()) -> c_27()
#compare#(#pos(@x),#neg(@y)) -> c_28()
#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
#compare#(#s(@x),#0()) -> c_30()
#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
append#1#(nil(),@l2) -> c_4()
flatten#1#(leaf()) -> c_6()
insert#1#(nil(),@x) -> c_11()
insert#2#(#false(),@x,@y,@ys) -> c_12()
insertionsort#1#(nil()) -> c_16()
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/2,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):2
-->_1 append#1#(nil(),@l2) -> c_4():27
2:S:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
3:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):4
-->_1 flatten#1#(leaf()) -> c_6():28
4:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
5:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):3
6:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):7
-->_1 insert#1#(nil(),@x) -> c_11():29
7:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
-->_2 #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):26
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):8
-->_1 insert#2#(#false(),@x,@y,@ys) -> c_12():30
8:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
9:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):10
-->_1 insertionsort#1#(nil()) -> c_16():31
10:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
11:W:#cklt#(#EQ()) -> c_17()
12:W:#cklt#(#GT()) -> c_18()
13:W:#cklt#(#LT()) -> c_19()
14:W:#compare#(#0(),#0()) -> c_20()
15:W:#compare#(#0(),#neg(@y)) -> c_21()
16:W:#compare#(#0(),#pos(@y)) -> c_22()
17:W:#compare#(#0(),#s(@y)) -> c_23()
18:W:#compare#(#neg(@x),#0()) -> c_24()
19:W:#compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x))
-->_1 #compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y)):25
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y)):23
-->_1 #compare#(#s(@x),#0()) -> c_30():24
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_28():22
-->_1 #compare#(#pos(@x),#0()) -> c_27():21
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_26():20
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x)):19
-->_1 #compare#(#neg(@x),#0()) -> c_24():18
-->_1 #compare#(#0(),#s(@y)) -> c_23():17
-->_1 #compare#(#0(),#pos(@y)) -> c_22():16
-->_1 #compare#(#0(),#neg(@y)) -> c_21():15
-->_1 #compare#(#0(),#0()) -> c_20():14
20:W:#compare#(#neg(@x),#pos(@y)) -> c_26()
21:W:#compare#(#pos(@x),#0()) -> c_27()
22:W:#compare#(#pos(@x),#neg(@y)) -> c_28()
23:W:#compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y))
-->_1 #compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y)):25
-->_1 #compare#(#s(@x),#0()) -> c_30():24
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y)):23
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_28():22
-->_1 #compare#(#pos(@x),#0()) -> c_27():21
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_26():20
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x)):19
-->_1 #compare#(#neg(@x),#0()) -> c_24():18
-->_1 #compare#(#0(),#s(@y)) -> c_23():17
-->_1 #compare#(#0(),#pos(@y)) -> c_22():16
-->_1 #compare#(#0(),#neg(@y)) -> c_21():15
-->_1 #compare#(#0(),#0()) -> c_20():14
24:W:#compare#(#s(@x),#0()) -> c_30()
25:W:#compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y))
-->_1 #compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y)):25
-->_1 #compare#(#s(@x),#0()) -> c_30():24
-->_1 #compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y)):23
-->_1 #compare#(#pos(@x),#neg(@y)) -> c_28():22
-->_1 #compare#(#pos(@x),#0()) -> c_27():21
-->_1 #compare#(#neg(@x),#pos(@y)) -> c_26():20
-->_1 #compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x)):19
-->_1 #compare#(#neg(@x),#0()) -> c_24():18
-->_1 #compare#(#0(),#s(@y)) -> c_23():17
-->_1 #compare#(#0(),#pos(@y)) -> c_22():16
-->_1 #compare#(#0(),#neg(@y)) -> c_21():15
-->_1 #compare#(#0(),#0()) -> c_20():14
26:W:#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y))
-->_2 #compare#(#s(@x),#s(@y)) -> c_31(#compare#(@x,@y)):25
-->_2 #compare#(#s(@x),#0()) -> c_30():24
-->_2 #compare#(#pos(@x),#pos(@y)) -> c_29(#compare#(@x,@y)):23
-->_2 #compare#(#pos(@x),#neg(@y)) -> c_28():22
-->_2 #compare#(#pos(@x),#0()) -> c_27():21
-->_2 #compare#(#neg(@x),#pos(@y)) -> c_26():20
-->_2 #compare#(#neg(@x),#neg(@y)) -> c_25(#compare#(@y,@x)):19
-->_2 #compare#(#neg(@x),#0()) -> c_24():18
-->_2 #compare#(#0(),#s(@y)) -> c_23():17
-->_2 #compare#(#0(),#pos(@y)) -> c_22():16
-->_2 #compare#(#0(),#neg(@y)) -> c_21():15
-->_2 #compare#(#0(),#0()) -> c_20():14
-->_1 #cklt#(#LT()) -> c_19():13
-->_1 #cklt#(#GT()) -> c_18():12
-->_1 #cklt#(#EQ()) -> c_17():11
27:W:append#1#(nil(),@l2) -> c_4()
28:W:flatten#1#(leaf()) -> c_6()
29:W:insert#1#(nil(),@x) -> c_11()
30:W:insert#2#(#false(),@x,@y,@ys) -> c_12()
31:W:insertionsort#1#(nil()) -> c_16()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
31: insertionsort#1#(nil()) ->
c_16()
29: insert#1#(nil(),@x) -> c_11()
30: insert#2#(#false(),@x,@y,@ys) ->
c_12()
26: #less#(@x,@y) ->
c_1(#cklt#(#compare(@x,@y))
,#compare#(@x,@y))
11: #cklt#(#EQ()) -> c_17()
12: #cklt#(#GT()) -> c_18()
13: #cklt#(#LT()) -> c_19()
25: #compare#(#s(@x),#s(@y)) ->
c_31(#compare#(@x,@y))
23: #compare#(#pos(@x),#pos(@y)) ->
c_29(#compare#(@x,@y))
19: #compare#(#neg(@x),#neg(@y)) ->
c_25(#compare#(@y,@x))
14: #compare#(#0(),#0()) -> c_20()
15: #compare#(#0(),#neg(@y)) ->
c_21()
16: #compare#(#0(),#pos(@y)) ->
c_22()
17: #compare#(#0(),#s(@y)) -> c_23()
18: #compare#(#neg(@x),#0()) ->
c_24()
20: #compare#(#neg(@x),#pos(@y)) ->
c_26()
21: #compare#(#pos(@x),#0()) ->
c_27()
22: #compare#(#pos(@x),#neg(@y)) ->
c_28()
24: #compare#(#s(@x),#0()) -> c_30()
28: flatten#1#(leaf()) -> c_6()
27: append#1#(nil(),@l2) -> c_4()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/2,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):2
2:S:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
3:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):4
4:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
5:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):3
6:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x)):7
7:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys),#less#(@y,@x))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):8
8:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
9:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):10
10:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Problem (S)
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):2
2:S:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
3:W:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):4
4:W:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
5:W:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):3
6:W:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):7
7:W:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):8
8:W:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
9:W:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):10
10:W:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):6
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):9
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
10: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
6: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
8: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
7: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):2
2:S:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
3:W:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):4
4:W:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
5:W:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
flattensort#(@t) -> c_8(flatten#(@t))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
2: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
Consider the set of all dependency pairs
1: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
2: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
3: flatten#(@t) ->
c_5(flatten#1#(@t))
4: flatten#1#(node(@l,@t1,@t2)) ->
c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
5: flattensort#(@t) ->
c_8(flatten#(@t))
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
{2}
These cover all (indirect) predecessors of dependency pairs
{2,5}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_2) = {1},
uargs(c_3) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1,2,3,4},
uargs(c_8) = {1}
Following symbols are considered usable:
{append,append#1,flatten,flatten#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = 0
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#cklt) = 0
p(#compare) = 0
p(#false) = 0
p(#less) = 0
p(#neg) = 0
p(#pos) = 0
p(#s) = 0
p(#true) = 0
p(::) = 1 + x2
p(append) = x1 + x2
p(append#1) = x1 + x2
p(flatten) = x1
p(flatten#1) = x1
p(flattensort) = 0
p(insert) = 0
p(insert#1) = 0
p(insert#2) = 0
p(insertionsort) = 0
p(insertionsort#1) = 0
p(leaf) = 0
p(nil) = 0
p(node) = 1 + x1 + x2 + x3
p(#cklt#) = 0
p(#compare#) = 0
p(#less#) = 0
p(append#) = x1
p(append#1#) = x1
p(flatten#) = x1 + x1^2
p(flatten#1#) = x1 + x1^2
p(flattensort#) = x1 + x1^2
p(insert#) = 0
p(insert#1#) = 0
p(insert#2#) = 0
p(insertionsort#) = 0
p(insertionsort#1#) = 0
p(c_1) = 0
p(c_2) = x1
p(c_3) = x1
p(c_4) = 0
p(c_5) = x1
p(c_6) = 0
p(c_7) = x1 + x2 + x3 + x4
p(c_8) = x1
p(c_9) = 0
p(c_10) = 0
p(c_11) = 0
p(c_12) = 0
p(c_13) = 0
p(c_14) = 0
p(c_15) = 0
p(c_16) = 0
p(c_17) = 0
p(c_18) = 0
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = 0
p(c_25) = 0
p(c_26) = 0
p(c_27) = 0
p(c_28) = 0
p(c_29) = 0
p(c_30) = 0
p(c_31) = 0
Following rules are strictly oriented:
append#1#(::(@x,@xs),@l2) = 1 + @xs
> @xs
= c_3(append#(@xs,@l2))
Following rules are (at-least) weakly oriented:
append#(@l1,@l2) = @l1
>= @l1
= c_2(append#1#(@l1,@l2))
flatten#(@t) = @t + @t^2
>= @t + @t^2
= c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) = 2 + 3*@l + 2*@l*@t1 + 2*@l*@t2 + @l^2 + 3*@t1 + 2*@t1*@t2 + @t1^2 + 3*@t2 + @t2^2
>= @l + 2*@t1 + @t1^2 + @t2 + @t2^2
= c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
flattensort#(@t) = @t + @t^2
>= @t + @t^2
= c_8(flatten#(@t))
append(@l1,@l2) = @l1 + @l2
>= @l1 + @l2
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = 1 + @l2 + @xs
>= 1 + @l2 + @xs
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = @l2
>= @l2
= @l2
flatten(@t) = @t
>= @t
= flatten#1(@t)
flatten#1(leaf()) = 0
>= 0
= nil()
flatten#1(node(@l,@t1,@t2)) = 1 + @l + @t1 + @t2
>= @l + @t1 + @t2
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
*** 1.1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
Strict TRS Rules:
Weak DP Rules:
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
Strict TRS Rules:
Weak DP Rules:
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
1: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
Consider the set of all dependency pairs
1: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
2: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
3: flatten#(@t) ->
c_5(flatten#1#(@t))
4: flatten#1#(node(@l,@t1,@t2)) ->
c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
5: flattensort#(@t) ->
c_8(flatten#(@t))
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
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,5}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
Strict TRS Rules:
Weak DP Rules:
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_2) = {1},
uargs(c_3) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1,2,3,4},
uargs(c_8) = {1}
Following symbols are considered usable:
{append,append#1,flatten,flatten#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = 0
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#cklt) = 0
p(#compare) = 0
p(#false) = 0
p(#less) = 0
p(#neg) = 0
p(#pos) = 0
p(#s) = 0
p(#true) = 0
p(::) = 1 + x2
p(append) = x1 + x2
p(append#1) = x1 + x2
p(flatten) = x1
p(flatten#1) = x1
p(flattensort) = 0
p(insert) = 0
p(insert#1) = 0
p(insert#2) = 0
p(insertionsort) = 0
p(insertionsort#1) = 0
p(leaf) = 0
p(nil) = 0
p(node) = 1 + x1 + x2 + x3
p(#cklt#) = 0
p(#compare#) = 0
p(#less#) = 0
p(append#) = 1 + x1
p(append#1#) = x1
p(flatten#) = x1 + x1^2
p(flatten#1#) = x1 + x1^2
p(flattensort#) = x1 + x1^2
p(insert#) = 0
p(insert#1#) = 0
p(insert#2#) = 0
p(insertionsort#) = 0
p(insertionsort#1#) = 0
p(c_1) = 0
p(c_2) = x1
p(c_3) = x1
p(c_4) = 0
p(c_5) = x1
p(c_6) = 0
p(c_7) = x1 + x2 + x3 + x4
p(c_8) = x1
p(c_9) = 0
p(c_10) = 0
p(c_11) = 0
p(c_12) = 0
p(c_13) = 0
p(c_14) = 0
p(c_15) = 0
p(c_16) = 0
p(c_17) = 0
p(c_18) = 0
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = 0
p(c_25) = 0
p(c_26) = 0
p(c_27) = 0
p(c_28) = 0
p(c_29) = 0
p(c_30) = 0
p(c_31) = 0
Following rules are strictly oriented:
append#(@l1,@l2) = 1 + @l1
> @l1
= c_2(append#1#(@l1,@l2))
Following rules are (at-least) weakly oriented:
append#1#(::(@x,@xs),@l2) = 1 + @xs
>= 1 + @xs
= c_3(append#(@xs,@l2))
flatten#(@t) = @t + @t^2
>= @t + @t^2
= c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) = 2 + 3*@l + 2*@l*@t1 + 2*@l*@t2 + @l^2 + 3*@t1 + 2*@t1*@t2 + @t1^2 + 3*@t2 + @t2^2
>= 2 + @l + 2*@t1 + @t1^2 + @t2 + @t2^2
= c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
flattensort#(@t) = @t + @t^2
>= @t + @t^2
= c_8(flatten#(@t))
append(@l1,@l2) = @l1 + @l2
>= @l1 + @l2
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = 1 + @l2 + @xs
>= 1 + @l2 + @xs
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = @l2
>= @l2
= @l2
flatten(@t) = @t
>= @t
= flatten#1(@t)
flatten#1(leaf()) = 0
>= 0
= nil()
flatten#1(node(@l,@t1,@t2)) = 1 + @l + @t1 + @t2
>= @l + @t1 + @t2
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
*** 1.1.1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):2
2:W:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
3:W:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):4
4:W:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):3
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):1
5:W:flattensort#(@t) -> c_8(flatten#(@t))
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: flattensort#(@t) ->
c_8(flatten#(@t))
3: flatten#(@t) ->
c_5(flatten#1#(@t))
4: flatten#1#(node(@l,@t1,@t2)) ->
c_7(append#(@l
,append(flatten(@t1)
,flatten(@t2)))
,append#(flatten(@t1)
,flatten(@t2))
,flatten#(@t1)
,flatten#(@t2))
1: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
2: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
*** 1.1.1.1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):2
2:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_2 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):9
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):9
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):1
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):1
3:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
4:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):5
5:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):6
6:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
7:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):8
8:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
9:W:append#(@l1,@l2) -> c_2(append#1#(@l1,@l2))
-->_1 append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2)):10
10:W:append#1#(::(@x,@xs),@l2) -> c_3(append#(@xs,@l2))
-->_1 append#(@l1,@l2) -> c_2(append#1#(@l1,@l2)):9
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: append#(@l1,@l2) ->
c_2(append#1#(@l1,@l2))
10: append#1#(::(@x,@xs),@l2) ->
c_3(append#(@xs,@l2))
*** 1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/4,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2)):2
2:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(append#(@l,append(flatten(@t1),flatten(@t2))),append#(flatten(@t1),flatten(@t2)),flatten#(@t1),flatten#(@t2))
-->_4 flatten#(@t) -> c_5(flatten#1#(@t)):1
-->_3 flatten#(@t) -> c_5(flatten#1#(@t)):1
3:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
4:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):5
5:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):6
6:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
7:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):8
8:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
*** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Problem (S)
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
*** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2)):2
2:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):1
3:W:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
4:W:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):5
5:W:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):6
6:W:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
7:W:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):8
8:W:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):4
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):7
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
8: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
4: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
6: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
5: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
*** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2)):2
2:S:flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):1
3:W:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
flattensort#(@t) -> c_8(flatten#(@t))
*** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
*** 1.1.1.1.1.1.2.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
1: flatten#(@t) ->
c_5(flatten#1#(@t))
Consider the set of all dependency pairs
1: flatten#(@t) ->
c_5(flatten#1#(@t))
2: flatten#1#(node(@l,@t1,@t2)) ->
c_7(flatten#(@t1),flatten#(@t2))
3: flattensort#(@t) ->
c_8(flatten#(@t))
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
{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.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_5) = {1},
uargs(c_7) = {1,2},
uargs(c_8) = {1}
Following symbols are considered usable:
{#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = [0]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#cklt) = [0]
p(#compare) = [0]
p(#false) = [0]
p(#less) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x1 + [1] x2 + [0]
p(append) = [0]
p(append#1) = [0]
p(flatten) = [0]
p(flatten#1) = [0]
p(flattensort) = [0]
p(insert) = [0]
p(insert#1) = [0]
p(insert#2) = [0]
p(insertionsort) = [0]
p(insertionsort#1) = [0]
p(leaf) = [0]
p(nil) = [0]
p(node) = [1] x1 + [1] x2 + [1] x3 + [2]
p(#cklt#) = [0]
p(#compare#) = [0]
p(#less#) = [0]
p(append#) = [0]
p(append#1#) = [2] x1 + [0]
p(flatten#) = [8] x1 + [10]
p(flatten#1#) = [8] x1 + [4]
p(flattensort#) = [8] x1 + [13]
p(insert#) = [1] x1 + [2]
p(insert#1#) = [1]
p(insert#2#) = [1] x3 + [1]
p(insertionsort#) = [0]
p(insertionsort#1#) = [2] x1 + [0]
p(c_1) = [1] x1 + [0]
p(c_2) = [4]
p(c_3) = [1]
p(c_4) = [1]
p(c_5) = [1] x1 + [4]
p(c_6) = [2]
p(c_7) = [1] x1 + [1] x2 + [0]
p(c_8) = [1] x1 + [3]
p(c_9) = [1] x1 + [8]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [8]
p(c_13) = [1]
p(c_14) = [1]
p(c_15) = [0]
p(c_16) = [4]
p(c_17) = [0]
p(c_18) = [1]
p(c_19) = [2]
p(c_20) = [1]
p(c_21) = [1]
p(c_22) = [1]
p(c_23) = [0]
p(c_24) = [0]
p(c_25) = [8] x1 + [1]
p(c_26) = [8]
p(c_27) = [0]
p(c_28) = [2]
p(c_29) = [1] x1 + [2]
p(c_30) = [8]
p(c_31) = [8]
Following rules are strictly oriented:
flatten#(@t) = [8] @t + [10]
> [8] @t + [8]
= c_5(flatten#1#(@t))
Following rules are (at-least) weakly oriented:
flatten#1#(node(@l,@t1,@t2)) = [8] @l + [8] @t1 + [8] @t2 + [20]
>= [8] @t1 + [8] @t2 + [20]
= c_7(flatten#(@t1),flatten#(@t2))
flattensort#(@t) = [8] @t + [13]
>= [8] @t + [13]
= c_8(flatten#(@t))
*** 1.1.1.1.1.1.2.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
flattensort#(@t) -> c_8(flatten#(@t))
Weak TRS Rules:
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2)):2
2:W:flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):1
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):1
3:W:flattensort#(@t) -> c_8(flatten#(@t))
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: flattensort#(@t) ->
c_8(flatten#(@t))
1: flatten#(@t) ->
c_5(flatten#1#(@t))
2: flatten#1#(node(@l,@t1,@t2)) ->
c_7(flatten#(@t1),flatten#(@t2))
*** 1.1.1.1.1.1.2.1.1.1.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:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.2.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
flatten#(@t) -> c_5(flatten#1#(@t))
flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):7
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
2:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):3
3:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):4
4:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
5:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):6
6:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
7:W:flatten#(@t) -> c_5(flatten#1#(@t))
-->_1 flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2)):8
8:W:flatten#1#(node(@l,@t1,@t2)) -> c_7(flatten#(@t1),flatten#(@t2))
-->_2 flatten#(@t) -> c_5(flatten#1#(@t)):7
-->_1 flatten#(@t) -> c_5(flatten#1#(@t)):7
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: flatten#(@t) ->
c_5(flatten#1#(@t))
8: flatten#1#(node(@l,@t1,@t2)) ->
c_7(flatten#(@t1),flatten#(@t2))
*** 1.1.1.1.1.1.2.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)),flatten#(@t))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
2:S:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):3
3:S:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):4
4:S:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
5:S:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):6
6:S:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
*** 1.1.1.1.1.1.2.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
4: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
Consider the set of all dependency pairs
1: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t)))
2: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
3: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
4: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
5: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
6: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
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
{4}
These cover all (indirect) predecessors of dependency pairs
{1,4}
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.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_15) = {1,2}
Following symbols are considered usable:
{#cklt,#compare,#less,append,append#1,flatten,flatten#1,insert,insert#1,insert#2,insertionsort,insertionsort#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = 1
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 1
p(#cklt) = x1
p(#compare) = x1*x2
p(#false) = 0
p(#less) = x1*x2
p(#neg) = 1 + x1
p(#pos) = 1 + x1
p(#s) = 1 + x1
p(#true) = 1
p(::) = x1 + x2
p(append) = x1 + x2
p(append#1) = x1 + x2
p(flatten) = x1
p(flatten#1) = x1
p(flattensort) = 0
p(insert) = x1 + x2
p(insert#1) = x1 + x2
p(insert#2) = x2 + x3 + x4
p(insertionsort) = x1
p(insertionsort#1) = x1
p(leaf) = 0
p(nil) = 0
p(node) = x1 + x2 + x3
p(#cklt#) = 0
p(#compare#) = 0
p(#less#) = 0
p(append#) = 0
p(append#1#) = 0
p(flatten#) = 0
p(flatten#1#) = 0
p(flattensort#) = x1 + x1^2
p(insert#) = x1*x2
p(insert#1#) = x1*x2
p(insert#2#) = x1 + x2*x4
p(insertionsort#) = x1^2
p(insertionsort#1#) = x1^2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = x1
p(c_9) = x1
p(c_10) = x1
p(c_11) = 0
p(c_12) = 0
p(c_13) = x1
p(c_14) = x1
p(c_15) = x1 + x2
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
Following rules are strictly oriented:
insert#2#(#true(),@x,@y,@ys) = 1 + @x*@ys
> @x*@ys
= c_13(insert#(@x,@ys))
Following rules are (at-least) weakly oriented:
flattensort#(@t) = @t + @t^2
>= @t^2
= c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) = @l*@x
>= @l*@x
= c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) = @x*@y + @x*@ys
>= @x*@y + @x*@ys
= c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
insertionsort#(@l) = @l^2
>= @l^2
= c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) = 2*@x*@xs + @x^2 + @xs^2
>= @x*@xs + @xs^2
= c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
#cklt(#EQ()) = 0
>= 0
= #false()
#cklt(#GT()) = 0
>= 0
= #false()
#cklt(#LT()) = 1
>= 1
= #true()
#compare(#0(),#0()) = 1
>= 0
= #EQ()
#compare(#0(),#neg(@y)) = 1 + @y
>= 0
= #GT()
#compare(#0(),#pos(@y)) = 1 + @y
>= 1
= #LT()
#compare(#0(),#s(@y)) = 1 + @y
>= 1
= #LT()
#compare(#neg(@x),#0()) = 1 + @x
>= 1
= #LT()
#compare(#neg(@x),#neg(@y)) = 1 + @x + @x*@y + @y
>= @x*@y
= #compare(@y,@x)
#compare(#neg(@x),#pos(@y)) = 1 + @x + @x*@y + @y
>= 1
= #LT()
#compare(#pos(@x),#0()) = 1 + @x
>= 0
= #GT()
#compare(#pos(@x),#neg(@y)) = 1 + @x + @x*@y + @y
>= 0
= #GT()
#compare(#pos(@x),#pos(@y)) = 1 + @x + @x*@y + @y
>= @x*@y
= #compare(@x,@y)
#compare(#s(@x),#0()) = 1 + @x
>= 0
= #GT()
#compare(#s(@x),#s(@y)) = 1 + @x + @x*@y + @y
>= @x*@y
= #compare(@x,@y)
#less(@x,@y) = @x*@y
>= @x*@y
= #cklt(#compare(@x,@y))
append(@l1,@l2) = @l1 + @l2
>= @l1 + @l2
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = @l2 + @x + @xs
>= @l2 + @x + @xs
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = @l2
>= @l2
= @l2
flatten(@t) = @t
>= @t
= flatten#1(@t)
flatten#1(leaf()) = 0
>= 0
= nil()
flatten#1(node(@l,@t1,@t2)) = @l + @t1 + @t2
>= @l + @t1 + @t2
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
insert(@x,@l) = @l + @x
>= @l + @x
= insert#1(@l,@x)
insert#1(::(@y,@ys),@x) = @x + @y + @ys
>= @x + @y + @ys
= insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) = @x
>= @x
= ::(@x,nil())
insert#2(#false(),@x,@y,@ys) = @x + @y + @ys
>= @x + @y + @ys
= ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) = @x + @y + @ys
>= @x + @y + @ys
= ::(@y,insert(@x,@ys))
insertionsort(@l) = @l
>= @l
= insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) = @x + @xs
>= @x + @xs
= insert(@x,insertionsort(@xs))
insertionsort#1(nil()) = 0
>= 0
= nil()
*** 1.1.1.1.1.1.2.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
4: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
3: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
4: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
5: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t)))
6: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
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
{4}
These cover all (indirect) predecessors of dependency pairs
{3,4,5}
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.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_15) = {1,2}
Following symbols are considered usable:
{append,append#1,flatten,flatten#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = [2]
p(#EQ) = [0]
p(#GT) = [0]
p(#LT) = [0]
p(#cklt) = [7]
p(#compare) = [2] x1 + [4] x2 + [0]
p(#false) = [0]
p(#less) = [1] x2 + [0]
p(#neg) = [0]
p(#pos) = [2]
p(#s) = [0]
p(#true) = [0]
p(::) = [1] x2 + [2]
p(append) = [1] x1 + [1] x2 + [0]
p(append#1) = [1] x1 + [1] x2 + [0]
p(flatten) = [1] x1 + [0]
p(flatten#1) = [1] x1 + [0]
p(flattensort) = [1]
p(insert) = [4]
p(insert#1) = [0]
p(insert#2) = [1] x2 + [2]
p(insertionsort) = [0]
p(insertionsort#1) = [0]
p(leaf) = [1]
p(nil) = [1]
p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
p(#cklt#) = [0]
p(#compare#) = [1]
p(#less#) = [2] x2 + [0]
p(append#) = [2] x2 + [1]
p(append#1#) = [1] x1 + [2]
p(flatten#) = [4]
p(flatten#1#) = [4]
p(flattensort#) = [5] x1 + [1]
p(insert#) = [4]
p(insert#1#) = [4]
p(insert#2#) = [4]
p(insertionsort#) = [4] x1 + [0]
p(insertionsort#1#) = [4] x1 + [0]
p(c_1) = [1] x2 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [2]
p(c_7) = [2] x1 + [4] x2 + [0]
p(c_8) = [1] x1 + [1]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [1]
p(c_12) = [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [1] x1 + [0]
p(c_15) = [1] x1 + [1] x2 + [2]
p(c_16) = [0]
p(c_17) = [0]
p(c_18) = [1]
p(c_19) = [1]
p(c_20) = [1]
p(c_21) = [1]
p(c_22) = [4]
p(c_23) = [0]
p(c_24) = [4]
p(c_25) = [4] x1 + [0]
p(c_26) = [1]
p(c_27) = [1]
p(c_28) = [1]
p(c_29) = [0]
p(c_30) = [1]
p(c_31) = [0]
Following rules are strictly oriented:
insertionsort#1#(::(@x,@xs)) = [4] @xs + [8]
> [4] @xs + [6]
= c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
Following rules are (at-least) weakly oriented:
flattensort#(@t) = [5] @t + [1]
>= [4] @t + [1]
= c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) = [4]
>= [4]
= c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) = [4]
>= [4]
= c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
insert#2#(#true(),@x,@y,@ys) = [4]
>= [4]
= c_13(insert#(@x,@ys))
insertionsort#(@l) = [4] @l + [0]
>= [4] @l + [0]
= c_14(insertionsort#1#(@l))
append(@l1,@l2) = [1] @l1 + [1] @l2 + [0]
>= [1] @l1 + [1] @l2 + [0]
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = [1] @l2 + [1] @xs + [2]
>= [1] @l2 + [1] @xs + [2]
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = [1] @l2 + [1]
>= [1] @l2 + [0]
= @l2
flatten(@t) = [1] @t + [0]
>= [1] @t + [0]
= flatten#1(@t)
flatten#1(leaf()) = [1]
>= [1]
= nil()
flatten#1(node(@l,@t1,@t2)) = [1] @l + [1] @t1 + [1] @t2 + [0]
>= [1] @l + [1] @t1 + [1] @t2 + [0]
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
2: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
2: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
3: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t)))
4: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
5: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
6: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
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
{2}
These cover all (indirect) predecessors of dependency pairs
{2,3,4}
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.1.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_15) = {1,2}
Following symbols are considered usable:
{#cklt,#less,append,append#1,flatten,flatten#1,insert,insert#1,insert#2,insertionsort,insertionsort#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = 0
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#cklt) = 1
p(#compare) = x2 + x2^2
p(#false) = 1
p(#less) = 1
p(#neg) = 0
p(#pos) = 0
p(#s) = 1
p(#true) = 1
p(::) = 1 + x1 + x2
p(append) = x1 + x2
p(append#1) = x1 + x2
p(flatten) = x1
p(flatten#1) = x1
p(flattensort) = 0
p(insert) = 1 + x1 + x2
p(insert#1) = 1 + x1 + x2
p(insert#2) = 1 + x1*x4 + x1^2 + x2 + x3
p(insertionsort) = x1
p(insertionsort#1) = x1
p(leaf) = 0
p(nil) = 0
p(node) = x1 + x2 + x3
p(#cklt#) = 0
p(#compare#) = 0
p(#less#) = 0
p(append#) = 0
p(append#1#) = 0
p(flatten#) = 0
p(flatten#1#) = 0
p(flattensort#) = 1 + x1^2
p(insert#) = x1^2 + x2
p(insert#1#) = x1 + x2^2
p(insert#2#) = x1*x4 + x2^2
p(insertionsort#) = 1 + x1^2
p(insertionsort#1#) = 1 + x1^2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = x1
p(c_9) = x1
p(c_10) = x1
p(c_11) = 0
p(c_12) = 0
p(c_13) = x1
p(c_14) = x1
p(c_15) = 1 + x1 + x2
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
Following rules are strictly oriented:
insert#1#(::(@y,@ys),@x) = 1 + @x^2 + @y + @ys
> @x^2 + @ys
= c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
Following rules are (at-least) weakly oriented:
flattensort#(@t) = 1 + @t^2
>= 1 + @t^2
= c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) = @l + @x^2
>= @l + @x^2
= c_9(insert#1#(@l,@x))
insert#2#(#true(),@x,@y,@ys) = @x^2 + @ys
>= @x^2 + @ys
= c_13(insert#(@x,@ys))
insertionsort#(@l) = 1 + @l^2
>= 1 + @l^2
= c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) = 2 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2
>= 2 + @x^2 + @xs + @xs^2
= c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
#cklt(#EQ()) = 1
>= 1
= #false()
#cklt(#GT()) = 1
>= 1
= #false()
#cklt(#LT()) = 1
>= 1
= #true()
#less(@x,@y) = 1
>= 1
= #cklt(#compare(@x,@y))
append(@l1,@l2) = @l1 + @l2
>= @l1 + @l2
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = 1 + @l2 + @x + @xs
>= 1 + @l2 + @x + @xs
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = @l2
>= @l2
= @l2
flatten(@t) = @t
>= @t
= flatten#1(@t)
flatten#1(leaf()) = 0
>= 0
= nil()
flatten#1(node(@l,@t1,@t2)) = @l + @t1 + @t2
>= @l + @t1 + @t2
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
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(#less(@y,@x),@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
= ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@y,insert(@x,@ys))
insertionsort(@l) = @l
>= @l
= insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) = 1 + @x + @xs
>= 1 + @x + @xs
= insert(@x,insertionsort(@xs))
insertionsort#1(nil()) = 0
>= 0
= nil()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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:
1: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
Consider the set of all dependency pairs
1: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
2: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t)))
3: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
4: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
5: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
6: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
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
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,3,4}
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.1.2.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
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_8) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_13) = {1},
uargs(c_14) = {1},
uargs(c_15) = {1,2}
Following symbols are considered usable:
{#cklt,#less,append,append#1,flatten,flatten#1,insert,insert#1,insert#2,insertionsort,insertionsort#1,#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}
TcT has computed the following interpretation:
p(#0) = 0
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 1
p(#cklt) = 1
p(#compare) = x1
p(#false) = 1
p(#less) = 1
p(#neg) = 1
p(#pos) = 0
p(#s) = 1
p(#true) = 1
p(::) = 1 + x1 + x2
p(append) = x1 + x2
p(append#1) = x1 + x2
p(flatten) = x1
p(flatten#1) = x1
p(flattensort) = 0
p(insert) = 1 + x1 + x2
p(insert#1) = 1 + x1 + x2
p(insert#2) = 1 + x1 + x1*x4 + x2 + x3
p(insertionsort) = 1 + x1
p(insertionsort#1) = 1 + x1
p(leaf) = 0
p(nil) = 0
p(node) = x1 + x2 + x3
p(#cklt#) = 0
p(#compare#) = 0
p(#less#) = 0
p(append#) = 0
p(append#1#) = 0
p(flatten#) = 0
p(flatten#1#) = 0
p(flattensort#) = 1 + x1 + x1^2
p(insert#) = 1 + x1 + x1^2 + x2
p(insert#1#) = x1 + x2 + x2^2
p(insert#2#) = x1 + x1*x2 + x2^2 + x3 + x4
p(insertionsort#) = 1 + x1 + x1^2
p(insertionsort#1#) = 1 + x1 + x1^2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 0
p(c_7) = 0
p(c_8) = x1
p(c_9) = x1
p(c_10) = x1
p(c_11) = 0
p(c_12) = 0
p(c_13) = x1
p(c_14) = x1
p(c_15) = x1 + x2
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
Following rules are strictly oriented:
insert#(@x,@l) = 1 + @l + @x + @x^2
> @l + @x + @x^2
= c_9(insert#1#(@l,@x))
Following rules are (at-least) weakly oriented:
flattensort#(@t) = 1 + @t + @t^2
>= 1 + @t + @t^2
= c_8(insertionsort#(flatten(@t)))
insert#1#(::(@y,@ys),@x) = 1 + @x + @x^2 + @y + @ys
>= 1 + @x + @x^2 + @y + @ys
= c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
insert#2#(#true(),@x,@y,@ys) = 1 + @x + @x^2 + @y + @ys
>= 1 + @x + @x^2 + @ys
= c_13(insert#(@x,@ys))
insertionsort#(@l) = 1 + @l + @l^2
>= 1 + @l + @l^2
= c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) = 3 + 3*@x + 2*@x*@xs + @x^2 + 3*@xs + @xs^2
>= 3 + @x + @x^2 + 2*@xs + @xs^2
= c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
#cklt(#EQ()) = 1
>= 1
= #false()
#cklt(#GT()) = 1
>= 1
= #false()
#cklt(#LT()) = 1
>= 1
= #true()
#less(@x,@y) = 1
>= 1
= #cklt(#compare(@x,@y))
append(@l1,@l2) = @l1 + @l2
>= @l1 + @l2
= append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) = 1 + @l2 + @x + @xs
>= 1 + @l2 + @x + @xs
= ::(@x,append(@xs,@l2))
append#1(nil(),@l2) = @l2
>= @l2
= @l2
flatten(@t) = @t
>= @t
= flatten#1(@t)
flatten#1(leaf()) = 0
>= 0
= nil()
flatten#1(node(@l,@t1,@t2)) = @l + @t1 + @t2
>= @l + @t1 + @t2
= append(@l
,append(flatten(@t1)
,flatten(@t2)))
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(#less(@y,@x),@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
= ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) = 2 + @x + @y + @ys
>= 2 + @x + @y + @ys
= ::(@y,insert(@x,@ys))
insertionsort(@l) = 1 + @l
>= 1 + @l
= insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) = 2 + @x + @xs
>= 2 + @x + @xs
= insert(@x,insertionsort(@xs))
insertionsort#1(nil()) = 1
>= 0
= nil()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
insert#(@x,@l) -> c_9(insert#1#(@l,@x))
insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
insertionsort#(@l) -> c_14(insertionsort#1#(@l))
insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:flattensort#(@t) -> c_8(insertionsort#(flatten(@t)))
-->_1 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
2:W:insert#(@x,@l) -> c_9(insert#1#(@l,@x))
-->_1 insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys)):3
3:W:insert#1#(::(@y,@ys),@x) -> c_10(insert#2#(#less(@y,@x),@x,@y,@ys))
-->_1 insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys)):4
4:W:insert#2#(#true(),@x,@y,@ys) -> c_13(insert#(@x,@ys))
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
5:W:insertionsort#(@l) -> c_14(insertionsort#1#(@l))
-->_1 insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs)):6
6:W:insertionsort#1#(::(@x,@xs)) -> c_15(insert#(@x,insertionsort(@xs)),insertionsort#(@xs))
-->_2 insertionsort#(@l) -> c_14(insertionsort#1#(@l)):5
-->_1 insert#(@x,@l) -> c_9(insert#1#(@l,@x)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: flattensort#(@t) ->
c_8(insertionsort#(flatten(@t)))
5: insertionsort#(@l) ->
c_14(insertionsort#1#(@l))
6: insertionsort#1#(::(@x,@xs)) ->
c_15(insert#(@x
,insertionsort(@xs))
,insertionsort#(@xs))
2: insert#(@x,@l) ->
c_9(insert#1#(@l,@x))
4: insert#2#(#true(),@x,@y,@ys) ->
c_13(insert#(@x,@ys))
3: insert#1#(::(@y,@ys),@x) ->
c_10(insert#2#(#less(@y,@x)
,@x
,@y
,@ys))
*** 1.1.1.1.1.1.2.1.1.2.1.1.2.2.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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)
#less(@x,@y) -> #cklt(#compare(@x,@y))
append(@l1,@l2) -> append#1(@l1,@l2)
append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
append#1(nil(),@l2) -> @l2
flatten(@t) -> flatten#1(@t)
flatten#1(leaf()) -> nil()
flatten#1(node(@l,@t1,@t2)) -> append(@l,append(flatten(@t1),flatten(@t2)))
insert(@x,@l) -> insert#1(@l,@x)
insert#1(::(@y,@ys),@x) -> insert#2(#less(@y,@x),@x,@y,@ys)
insert#1(nil(),@x) -> ::(@x,nil())
insert#2(#false(),@x,@y,@ys) -> ::(@x,::(@y,@ys))
insert#2(#true(),@x,@y,@ys) -> ::(@y,insert(@x,@ys))
insertionsort(@l) -> insertionsort#1(@l)
insertionsort#1(::(@x,@xs)) -> insert(@x,insertionsort(@xs))
insertionsort#1(nil()) -> nil()
Signature:
{#cklt/1,#compare/2,#less/2,append/2,append#1/2,flatten/1,flatten#1/1,flattensort/1,insert/2,insert#1/2,insert#2/4,insertionsort/1,insertionsort#1/1,#cklt#/1,#compare#/2,#less#/2,append#/2,append#1#/2,flatten#/1,flatten#1#/1,flattensort#/1,insert#/2,insert#1#/2,insert#2#/4,insertionsort#/1,insertionsort#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,leaf/0,nil/0,node/3,c_1/2,c_2/1,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1,c_14/1,c_15/2,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/0,c_27/0,c_28/0,c_29/1,c_30/0,c_31/1}
Obligation:
Innermost
basic terms: {#cklt#,#compare#,#less#,append#,append#1#,flatten#,flatten#1#,flattensort#,insert#,insert#1#,insert#2#,insertionsort#,insertionsort#1#}/{#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,::,leaf,nil,node}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).