YES(O(1),O(n^2)) 531.97/149.84 YES(O(1),O(n^2)) 531.97/149.84 531.97/149.84 We are left with following problem, upon which TcT provides the 531.97/149.84 certificate YES(O(1),O(n^2)). 531.97/149.84 531.97/149.84 Strict Trs: 531.97/149.84 { flattensort(@t) -> insertionsort(flatten(@t)) 531.97/149.84 , insertionsort#1(nil()) -> nil() 531.97/149.84 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.84 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.84 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.84 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.84 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.84 , append#1(nil(), @l2) -> @l2 531.97/149.84 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.84 , flatten#1(leaf()) -> nil() 531.97/149.84 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.84 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.84 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.84 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.84 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.84 , flatten(@t) -> flatten#1(@t) 531.97/149.84 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.84 Weak Trs: 531.97/149.84 { #cklt(#EQ()) -> #false() 531.97/149.84 , #cklt(#LT()) -> #true() 531.97/149.84 , #cklt(#GT()) -> #false() 531.97/149.84 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.84 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.84 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#0(), #0()) -> #EQ() 531.97/149.84 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.84 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.84 , #compare(#s(@x), #0()) -> #GT() 531.97/149.84 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) } 531.97/149.84 Obligation: 531.97/149.84 innermost runtime complexity 531.97/149.84 Answer: 531.97/149.84 YES(O(1),O(n^2)) 531.97/149.84 531.97/149.84 We add the following dependency tuples: 531.97/149.84 531.97/149.84 Strict DPs: 531.97/149.84 { flattensort^#(@t) -> 531.97/149.84 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.84 , insertionsort^#(@l) -> c_16(insertionsort#1^#(@l)) 531.97/149.84 , flatten^#(@t) -> c_15(flatten#1^#(@t)) 531.97/149.84 , insertionsort#1^#(nil()) -> c_2() 531.97/149.84 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.84 c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.84 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.84 , append^#(@l1, @l2) -> c_4(append#1^#(@l1, @l2)) 531.97/149.84 , append#1^#(nil(), @l2) -> c_8() 531.97/149.84 , append#1^#(::(@x, @xs), @l2) -> c_9(append^#(@xs, @l2)) 531.97/149.84 , insert#1^#(nil(), @x) -> c_12() 531.97/149.84 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.84 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) 531.97/149.84 , insert#2^#(#true(), @x, @y, @ys) -> c_6(insert^#(@x, @ys)) 531.97/149.84 , insert#2^#(#false(), @x, @y, @ys) -> c_7() 531.97/149.84 , flatten#1^#(leaf()) -> c_10() 531.97/149.84 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.84 c_11(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.84 append^#(flatten(@t1), flatten(@t2)), 531.97/149.84 flatten^#(@t1), 531.97/149.84 flatten^#(@t2)) 531.97/149.84 , #less^#(@x, @y) -> 531.97/149.84 c_14(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) } 531.97/149.84 Weak DPs: 531.97/149.84 { #cklt^#(#EQ()) -> c_17() 531.97/149.84 , #cklt^#(#LT()) -> c_18() 531.97/149.84 , #cklt^#(#GT()) -> c_19() 531.97/149.84 , #compare^#(#pos(@x), #pos(@y)) -> c_20(#compare^#(@x, @y)) 531.97/149.84 , #compare^#(#pos(@x), #0()) -> c_21() 531.97/149.84 , #compare^#(#pos(@x), #neg(@y)) -> c_22() 531.97/149.84 , #compare^#(#0(), #pos(@y)) -> c_23() 531.97/149.84 , #compare^#(#0(), #0()) -> c_24() 531.97/149.84 , #compare^#(#0(), #neg(@y)) -> c_25() 531.97/149.84 , #compare^#(#0(), #s(@y)) -> c_26() 531.97/149.84 , #compare^#(#neg(@x), #pos(@y)) -> c_27() 531.97/149.84 , #compare^#(#neg(@x), #0()) -> c_28() 531.97/149.84 , #compare^#(#neg(@x), #neg(@y)) -> c_29(#compare^#(@y, @x)) 531.97/149.84 , #compare^#(#s(@x), #0()) -> c_30() 531.97/149.84 , #compare^#(#s(@x), #s(@y)) -> c_31(#compare^#(@x, @y)) } 531.97/149.84 531.97/149.84 and mark the set of starting terms. 531.97/149.84 531.97/149.84 We are left with following problem, upon which TcT provides the 531.97/149.84 certificate YES(O(1),O(n^2)). 531.97/149.84 531.97/149.84 Strict DPs: 531.97/149.84 { flattensort^#(@t) -> 531.97/149.84 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.84 , insertionsort^#(@l) -> c_16(insertionsort#1^#(@l)) 531.97/149.84 , flatten^#(@t) -> c_15(flatten#1^#(@t)) 531.97/149.84 , insertionsort#1^#(nil()) -> c_2() 531.97/149.84 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.84 c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.84 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.84 , append^#(@l1, @l2) -> c_4(append#1^#(@l1, @l2)) 531.97/149.84 , append#1^#(nil(), @l2) -> c_8() 531.97/149.84 , append#1^#(::(@x, @xs), @l2) -> c_9(append^#(@xs, @l2)) 531.97/149.84 , insert#1^#(nil(), @x) -> c_12() 531.97/149.84 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.84 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) 531.97/149.84 , insert#2^#(#true(), @x, @y, @ys) -> c_6(insert^#(@x, @ys)) 531.97/149.84 , insert#2^#(#false(), @x, @y, @ys) -> c_7() 531.97/149.84 , flatten#1^#(leaf()) -> c_10() 531.97/149.84 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.84 c_11(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.84 append^#(flatten(@t1), flatten(@t2)), 531.97/149.84 flatten^#(@t1), 531.97/149.84 flatten^#(@t2)) 531.97/149.84 , #less^#(@x, @y) -> 531.97/149.84 c_14(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) } 531.97/149.84 Weak DPs: 531.97/149.84 { #cklt^#(#EQ()) -> c_17() 531.97/149.84 , #cklt^#(#LT()) -> c_18() 531.97/149.84 , #cklt^#(#GT()) -> c_19() 531.97/149.84 , #compare^#(#pos(@x), #pos(@y)) -> c_20(#compare^#(@x, @y)) 531.97/149.84 , #compare^#(#pos(@x), #0()) -> c_21() 531.97/149.84 , #compare^#(#pos(@x), #neg(@y)) -> c_22() 531.97/149.84 , #compare^#(#0(), #pos(@y)) -> c_23() 531.97/149.84 , #compare^#(#0(), #0()) -> c_24() 531.97/149.84 , #compare^#(#0(), #neg(@y)) -> c_25() 531.97/149.84 , #compare^#(#0(), #s(@y)) -> c_26() 531.97/149.84 , #compare^#(#neg(@x), #pos(@y)) -> c_27() 531.97/149.84 , #compare^#(#neg(@x), #0()) -> c_28() 531.97/149.84 , #compare^#(#neg(@x), #neg(@y)) -> c_29(#compare^#(@y, @x)) 531.97/149.84 , #compare^#(#s(@x), #0()) -> c_30() 531.97/149.84 , #compare^#(#s(@x), #s(@y)) -> c_31(#compare^#(@x, @y)) } 531.97/149.84 Weak Trs: 531.97/149.84 { flattensort(@t) -> insertionsort(flatten(@t)) 531.97/149.84 , insertionsort#1(nil()) -> nil() 531.97/149.84 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.84 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.84 , #cklt(#EQ()) -> #false() 531.97/149.84 , #cklt(#LT()) -> #true() 531.97/149.84 , #cklt(#GT()) -> #false() 531.97/149.84 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.84 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.84 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.84 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.84 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.84 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#0(), #0()) -> #EQ() 531.97/149.84 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.84 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.84 , #compare(#s(@x), #0()) -> #GT() 531.97/149.84 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.84 , append#1(nil(), @l2) -> @l2 531.97/149.84 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.84 , flatten#1(leaf()) -> nil() 531.97/149.84 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.84 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.84 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.84 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.84 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.84 , flatten(@t) -> flatten#1(@t) 531.97/149.84 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.84 Obligation: 531.97/149.84 innermost runtime complexity 531.97/149.84 Answer: 531.97/149.84 YES(O(1),O(n^2)) 531.97/149.84 531.97/149.84 We estimate the number of application of {4,8,10,13,14,16} by 531.97/149.84 applications of Pre({4,8,10,13,14,16}) = {2,3,6,7,11}. Here rules 531.97/149.84 are labeled as follows: 531.97/149.84 531.97/149.84 DPs: 531.97/149.84 { 1: flattensort^#(@t) -> 531.97/149.84 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.84 , 2: insertionsort^#(@l) -> c_16(insertionsort#1^#(@l)) 531.97/149.84 , 3: flatten^#(@t) -> c_15(flatten#1^#(@t)) 531.97/149.84 , 4: insertionsort#1^#(nil()) -> c_2() 531.97/149.84 , 5: insertionsort#1^#(::(@x, @xs)) -> 531.97/149.84 c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.84 , 6: insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.84 , 7: append^#(@l1, @l2) -> c_4(append#1^#(@l1, @l2)) 531.97/149.84 , 8: append#1^#(nil(), @l2) -> c_8() 531.97/149.84 , 9: append#1^#(::(@x, @xs), @l2) -> c_9(append^#(@xs, @l2)) 531.97/149.84 , 10: insert#1^#(nil(), @x) -> c_12() 531.97/149.84 , 11: insert#1^#(::(@y, @ys), @x) -> 531.97/149.84 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) 531.97/149.84 , 12: insert#2^#(#true(), @x, @y, @ys) -> c_6(insert^#(@x, @ys)) 531.97/149.84 , 13: insert#2^#(#false(), @x, @y, @ys) -> c_7() 531.97/149.84 , 14: flatten#1^#(leaf()) -> c_10() 531.97/149.84 , 15: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.84 c_11(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.84 append^#(flatten(@t1), flatten(@t2)), 531.97/149.84 flatten^#(@t1), 531.97/149.84 flatten^#(@t2)) 531.97/149.84 , 16: #less^#(@x, @y) -> 531.97/149.84 c_14(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 531.97/149.84 , 17: #cklt^#(#EQ()) -> c_17() 531.97/149.84 , 18: #cklt^#(#LT()) -> c_18() 531.97/149.84 , 19: #cklt^#(#GT()) -> c_19() 531.97/149.84 , 20: #compare^#(#pos(@x), #pos(@y)) -> c_20(#compare^#(@x, @y)) 531.97/149.84 , 21: #compare^#(#pos(@x), #0()) -> c_21() 531.97/149.84 , 22: #compare^#(#pos(@x), #neg(@y)) -> c_22() 531.97/149.84 , 23: #compare^#(#0(), #pos(@y)) -> c_23() 531.97/149.84 , 24: #compare^#(#0(), #0()) -> c_24() 531.97/149.84 , 25: #compare^#(#0(), #neg(@y)) -> c_25() 531.97/149.84 , 26: #compare^#(#0(), #s(@y)) -> c_26() 531.97/149.84 , 27: #compare^#(#neg(@x), #pos(@y)) -> c_27() 531.97/149.84 , 28: #compare^#(#neg(@x), #0()) -> c_28() 531.97/149.84 , 29: #compare^#(#neg(@x), #neg(@y)) -> c_29(#compare^#(@y, @x)) 531.97/149.84 , 30: #compare^#(#s(@x), #0()) -> c_30() 531.97/149.84 , 31: #compare^#(#s(@x), #s(@y)) -> c_31(#compare^#(@x, @y)) } 531.97/149.84 531.97/149.84 We are left with following problem, upon which TcT provides the 531.97/149.84 certificate YES(O(1),O(n^2)). 531.97/149.84 531.97/149.84 Strict DPs: 531.97/149.84 { flattensort^#(@t) -> 531.97/149.84 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.84 , insertionsort^#(@l) -> c_16(insertionsort#1^#(@l)) 531.97/149.84 , flatten^#(@t) -> c_15(flatten#1^#(@t)) 531.97/149.84 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.84 c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.84 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.84 , append^#(@l1, @l2) -> c_4(append#1^#(@l1, @l2)) 531.97/149.84 , append#1^#(::(@x, @xs), @l2) -> c_9(append^#(@xs, @l2)) 531.97/149.84 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.84 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) 531.97/149.84 , insert#2^#(#true(), @x, @y, @ys) -> c_6(insert^#(@x, @ys)) 531.97/149.84 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.84 c_11(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.84 append^#(flatten(@t1), flatten(@t2)), 531.97/149.84 flatten^#(@t1), 531.97/149.84 flatten^#(@t2)) } 531.97/149.84 Weak DPs: 531.97/149.84 { insertionsort#1^#(nil()) -> c_2() 531.97/149.84 , append#1^#(nil(), @l2) -> c_8() 531.97/149.84 , insert#1^#(nil(), @x) -> c_12() 531.97/149.84 , insert#2^#(#false(), @x, @y, @ys) -> c_7() 531.97/149.84 , flatten#1^#(leaf()) -> c_10() 531.97/149.84 , #less^#(@x, @y) -> 531.97/149.84 c_14(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 531.97/149.84 , #cklt^#(#EQ()) -> c_17() 531.97/149.84 , #cklt^#(#LT()) -> c_18() 531.97/149.84 , #cklt^#(#GT()) -> c_19() 531.97/149.84 , #compare^#(#pos(@x), #pos(@y)) -> c_20(#compare^#(@x, @y)) 531.97/149.84 , #compare^#(#pos(@x), #0()) -> c_21() 531.97/149.84 , #compare^#(#pos(@x), #neg(@y)) -> c_22() 531.97/149.84 , #compare^#(#0(), #pos(@y)) -> c_23() 531.97/149.84 , #compare^#(#0(), #0()) -> c_24() 531.97/149.84 , #compare^#(#0(), #neg(@y)) -> c_25() 531.97/149.84 , #compare^#(#0(), #s(@y)) -> c_26() 531.97/149.84 , #compare^#(#neg(@x), #pos(@y)) -> c_27() 531.97/149.84 , #compare^#(#neg(@x), #0()) -> c_28() 531.97/149.84 , #compare^#(#neg(@x), #neg(@y)) -> c_29(#compare^#(@y, @x)) 531.97/149.84 , #compare^#(#s(@x), #0()) -> c_30() 531.97/149.84 , #compare^#(#s(@x), #s(@y)) -> c_31(#compare^#(@x, @y)) } 531.97/149.84 Weak Trs: 531.97/149.84 { flattensort(@t) -> insertionsort(flatten(@t)) 531.97/149.84 , insertionsort#1(nil()) -> nil() 531.97/149.84 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.84 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.84 , #cklt(#EQ()) -> #false() 531.97/149.84 , #cklt(#LT()) -> #true() 531.97/149.84 , #cklt(#GT()) -> #false() 531.97/149.84 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.84 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.84 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.84 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.84 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.84 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#0(), #0()) -> #EQ() 531.97/149.84 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.84 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.84 , #compare(#s(@x), #0()) -> #GT() 531.97/149.84 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.84 , append#1(nil(), @l2) -> @l2 531.97/149.84 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.84 , flatten#1(leaf()) -> nil() 531.97/149.84 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.84 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.84 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.84 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.84 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.84 , flatten(@t) -> flatten#1(@t) 531.97/149.84 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.84 Obligation: 531.97/149.84 innermost runtime complexity 531.97/149.84 Answer: 531.97/149.84 YES(O(1),O(n^2)) 531.97/149.84 531.97/149.84 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.84 closed under successors. The DPs are removed. 531.97/149.84 531.97/149.84 { insertionsort#1^#(nil()) -> c_2() 531.97/149.84 , append#1^#(nil(), @l2) -> c_8() 531.97/149.84 , insert#1^#(nil(), @x) -> c_12() 531.97/149.84 , insert#2^#(#false(), @x, @y, @ys) -> c_7() 531.97/149.84 , flatten#1^#(leaf()) -> c_10() 531.97/149.84 , #less^#(@x, @y) -> 531.97/149.84 c_14(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 531.97/149.84 , #cklt^#(#EQ()) -> c_17() 531.97/149.84 , #cklt^#(#LT()) -> c_18() 531.97/149.84 , #cklt^#(#GT()) -> c_19() 531.97/149.84 , #compare^#(#pos(@x), #pos(@y)) -> c_20(#compare^#(@x, @y)) 531.97/149.84 , #compare^#(#pos(@x), #0()) -> c_21() 531.97/149.84 , #compare^#(#pos(@x), #neg(@y)) -> c_22() 531.97/149.84 , #compare^#(#0(), #pos(@y)) -> c_23() 531.97/149.84 , #compare^#(#0(), #0()) -> c_24() 531.97/149.84 , #compare^#(#0(), #neg(@y)) -> c_25() 531.97/149.84 , #compare^#(#0(), #s(@y)) -> c_26() 531.97/149.84 , #compare^#(#neg(@x), #pos(@y)) -> c_27() 531.97/149.84 , #compare^#(#neg(@x), #0()) -> c_28() 531.97/149.84 , #compare^#(#neg(@x), #neg(@y)) -> c_29(#compare^#(@y, @x)) 531.97/149.84 , #compare^#(#s(@x), #0()) -> c_30() 531.97/149.84 , #compare^#(#s(@x), #s(@y)) -> c_31(#compare^#(@x, @y)) } 531.97/149.84 531.97/149.84 We are left with following problem, upon which TcT provides the 531.97/149.84 certificate YES(O(1),O(n^2)). 531.97/149.84 531.97/149.84 Strict DPs: 531.97/149.84 { flattensort^#(@t) -> 531.97/149.84 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.84 , insertionsort^#(@l) -> c_16(insertionsort#1^#(@l)) 531.97/149.84 , flatten^#(@t) -> c_15(flatten#1^#(@t)) 531.97/149.84 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.84 c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.84 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.84 , append^#(@l1, @l2) -> c_4(append#1^#(@l1, @l2)) 531.97/149.84 , append#1^#(::(@x, @xs), @l2) -> c_9(append^#(@xs, @l2)) 531.97/149.84 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.84 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) 531.97/149.84 , insert#2^#(#true(), @x, @y, @ys) -> c_6(insert^#(@x, @ys)) 531.97/149.84 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.84 c_11(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.84 append^#(flatten(@t1), flatten(@t2)), 531.97/149.84 flatten^#(@t1), 531.97/149.84 flatten^#(@t2)) } 531.97/149.84 Weak Trs: 531.97/149.84 { flattensort(@t) -> insertionsort(flatten(@t)) 531.97/149.84 , insertionsort#1(nil()) -> nil() 531.97/149.84 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.84 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.84 , #cklt(#EQ()) -> #false() 531.97/149.84 , #cklt(#LT()) -> #true() 531.97/149.84 , #cklt(#GT()) -> #false() 531.97/149.84 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.84 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.84 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.84 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.84 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.84 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#0(), #0()) -> #EQ() 531.97/149.84 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.84 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.84 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.84 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.84 , #compare(#s(@x), #0()) -> #GT() 531.97/149.84 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.84 , append#1(nil(), @l2) -> @l2 531.97/149.84 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.84 , flatten#1(leaf()) -> nil() 531.97/149.84 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.84 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.84 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.84 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.84 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 Obligation: 531.97/149.85 innermost runtime complexity 531.97/149.85 Answer: 531.97/149.85 YES(O(1),O(n^2)) 531.97/149.85 531.97/149.85 Due to missing edges in the dependency-graph, the right-hand sides 531.97/149.85 of following rules could be simplified: 531.97/149.85 531.97/149.85 { insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_13(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) } 531.97/149.85 531.97/149.85 We are left with following problem, upon which TcT provides the 531.97/149.85 certificate YES(O(1),O(n^2)). 531.97/149.85 531.97/149.85 Strict DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak Trs: 531.97/149.85 { flattensort(@t) -> insertionsort(flatten(@t)) 531.97/149.85 , insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 Obligation: 531.97/149.85 innermost runtime complexity 531.97/149.85 Answer: 531.97/149.85 YES(O(1),O(n^2)) 531.97/149.85 531.97/149.85 We replace rewrite rules by usable rules: 531.97/149.85 531.97/149.85 Weak Usable Rules: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 531.97/149.85 We are left with following problem, upon which TcT provides the 531.97/149.85 certificate YES(O(1),O(n^2)). 531.97/149.85 531.97/149.85 Strict DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak Trs: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 Obligation: 531.97/149.85 innermost runtime complexity 531.97/149.85 Answer: 531.97/149.85 YES(O(1),O(n^2)) 531.97/149.85 531.97/149.85 We analyse the complexity of following sub-problems (R) and (S). 531.97/149.85 Problem (S) is obtained from the input problem by shifting strict 531.97/149.85 rules from (R) into the weak component: 531.97/149.85 531.97/149.85 Problem (R): 531.97/149.85 ------------ 531.97/149.85 Strict DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak DPs: 531.97/149.85 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.85 Weak Trs: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 StartTerms: basic terms 531.97/149.85 Strategy: innermost 531.97/149.85 531.97/149.85 Problem (S): 531.97/149.85 ------------ 531.97/149.85 Strict DPs: 531.97/149.85 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.85 Weak DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak Trs: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 StartTerms: basic terms 531.97/149.85 Strategy: innermost 531.97/149.85 531.97/149.85 Overall, the transformation results in the following sub-problem(s): 531.97/149.85 531.97/149.85 Generated new problems: 531.97/149.85 ----------------------- 531.97/149.85 R) Strict DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak DPs: 531.97/149.85 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.85 Weak Trs: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 StartTerms: basic terms 531.97/149.85 Strategy: innermost 531.97/149.85 531.97/149.85 This problem was proven YES(O(1),O(n^2)). 531.97/149.85 531.97/149.85 S) Strict DPs: 531.97/149.85 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.85 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.85 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.85 Weak DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak Trs: 531.97/149.85 { insertionsort#1(nil()) -> nil() 531.97/149.85 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.85 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.85 , #cklt(#EQ()) -> #false() 531.97/149.85 , #cklt(#LT()) -> #true() 531.97/149.85 , #cklt(#GT()) -> #false() 531.97/149.85 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.85 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.85 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.85 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.85 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.85 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#0(), #0()) -> #EQ() 531.97/149.85 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.85 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.85 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.85 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.85 , #compare(#s(@x), #0()) -> #GT() 531.97/149.85 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.85 , append#1(nil(), @l2) -> @l2 531.97/149.85 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.85 , flatten#1(leaf()) -> nil() 531.97/149.85 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.85 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.85 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.85 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.85 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.85 , flatten(@t) -> flatten#1(@t) 531.97/149.85 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.85 StartTerms: basic terms 531.97/149.85 Strategy: innermost 531.97/149.85 531.97/149.85 This problem was proven YES(O(1),O(n^2)). 531.97/149.85 531.97/149.85 531.97/149.85 Proofs for generated problems: 531.97/149.85 ------------------------------ 531.97/149.85 R) We are left with following problem, upon which TcT provides the 531.97/149.85 certificate YES(O(1),O(n^2)). 531.97/149.85 531.97/149.85 Strict DPs: 531.97/149.85 { flattensort^#(@t) -> 531.97/149.85 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.85 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.85 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.85 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.85 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.85 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.85 append^#(flatten(@t1), flatten(@t2)), 531.97/149.85 flatten^#(@t1), 531.97/149.85 flatten^#(@t2)) } 531.97/149.85 Weak DPs: 531.97/149.85 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.85 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.85 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.85 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.85 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.86 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.86 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.86 Weak Trs: 531.97/149.86 { insertionsort#1(nil()) -> nil() 531.97/149.86 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.86 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , #cklt(#EQ()) -> #false() 531.97/149.86 , #cklt(#LT()) -> #true() 531.97/149.86 , #cklt(#GT()) -> #false() 531.97/149.86 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.86 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.86 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.86 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.86 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.86 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#0(), #0()) -> #EQ() 531.97/149.86 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.86 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.86 , #compare(#s(@x), #0()) -> #GT() 531.97/149.86 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.86 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.86 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.86 , flatten(@t) -> flatten#1(@t) 531.97/149.86 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^2)) 531.97/149.86 531.97/149.86 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.86 closed under successors. The DPs are removed. 531.97/149.86 531.97/149.86 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.86 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.86 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.86 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.86 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.86 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.86 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(n^2)). 531.97/149.86 531.97/149.86 Strict DPs: 531.97/149.86 { flattensort^#(@t) -> 531.97/149.86 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.86 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.86 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { insertionsort#1(nil()) -> nil() 531.97/149.86 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.86 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , #cklt(#EQ()) -> #false() 531.97/149.86 , #cklt(#LT()) -> #true() 531.97/149.86 , #cklt(#GT()) -> #false() 531.97/149.86 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.86 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.86 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.86 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.86 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.86 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#0(), #0()) -> #EQ() 531.97/149.86 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.86 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.86 , #compare(#s(@x), #0()) -> #GT() 531.97/149.86 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.86 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.86 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.86 , flatten(@t) -> flatten#1(@t) 531.97/149.86 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^2)) 531.97/149.86 531.97/149.86 Due to missing edges in the dependency-graph, the right-hand sides 531.97/149.86 of following rules could be simplified: 531.97/149.86 531.97/149.86 { flattensort^#(@t) -> 531.97/149.86 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) } 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(n^2)). 531.97/149.86 531.97/149.86 Strict DPs: 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.86 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { insertionsort#1(nil()) -> nil() 531.97/149.86 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.86 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , #cklt(#EQ()) -> #false() 531.97/149.86 , #cklt(#LT()) -> #true() 531.97/149.86 , #cklt(#GT()) -> #false() 531.97/149.86 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.86 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.86 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.86 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.86 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.86 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#0(), #0()) -> #EQ() 531.97/149.86 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.86 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.86 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.86 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.86 , #compare(#s(@x), #0()) -> #GT() 531.97/149.86 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.86 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.86 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.86 , flatten(@t) -> flatten#1(@t) 531.97/149.86 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^2)) 531.97/149.86 531.97/149.86 We replace rewrite rules by usable rules: 531.97/149.86 531.97/149.86 Weak Usable Rules: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(n^2)). 531.97/149.86 531.97/149.86 Strict DPs: 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.86 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^2)) 531.97/149.86 531.97/149.86 We decompose the input problem according to the dependency graph 531.97/149.86 into the upper component 531.97/149.86 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 531.97/149.86 and lower component 531.97/149.86 531.97/149.86 { append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.86 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) } 531.97/149.86 531.97/149.86 Further, following extension rules are added to the lower 531.97/149.86 component. 531.97/149.86 531.97/149.86 { flattensort^#(@t) -> flatten^#(@t) 531.97/149.86 , flatten^#(@t) -> flatten#1^#(@t) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.86 531.97/149.86 TcT solves the upper component with certificate YES(O(1),O(n^1)). 531.97/149.86 531.97/149.86 Sub-proof: 531.97/149.86 ---------- 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(n^1)). 531.97/149.86 531.97/149.86 Strict DPs: 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^1)) 531.97/149.86 531.97/149.86 We use the processor 'matrix interpretation of dimension 1' to 531.97/149.86 orient following rules strictly. 531.97/149.86 531.97/149.86 DPs: 531.97/149.86 { 1: flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , 2: flatten^#(@t) -> c_2(flatten#1^#(@t)) } 531.97/149.86 531.97/149.86 Sub-proof: 531.97/149.86 ---------- 531.97/149.86 The following argument positions are usable: 531.97/149.86 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_5) = {1, 2, 3, 4} 531.97/149.86 531.97/149.86 TcT has computed the following constructor-based matrix 531.97/149.86 interpretation satisfying not(EDA). 531.97/149.86 531.97/149.86 [leaf] = [7] 531.97/149.86 531.97/149.86 [append](x1, x2) = [0] 531.97/149.86 531.97/149.86 [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 531.97/149.86 531.97/149.86 [nil] = [4] 531.97/149.86 531.97/149.86 [append#1](x1, x2) = [7] x2 + [0] 531.97/149.86 531.97/149.86 [flatten#1](x1) = [0] 531.97/149.86 531.97/149.86 [::](x1, x2) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [flatten](x1) = [0] 531.97/149.86 531.97/149.86 [flattensort^#](x1) = [7] x1 + [7] 531.97/149.86 531.97/149.86 [flatten^#](x1) = [1] x1 + [1] 531.97/149.86 531.97/149.86 [append^#](x1, x2) = [0] 531.97/149.86 531.97/149.86 [flatten#1^#](x1) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [c_1](x1) = [3] x1 + [3] 531.97/149.86 531.97/149.86 [c_2](x1) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [c_5](x1, x2, x3, x4) = [4] x1 + [1] x2 + [1] x3 + [1] x4 + [0] 531.97/149.86 531.97/149.86 The order satisfies the following ordering constraints: 531.97/149.86 531.97/149.86 [append(@l1, @l2)] = [0] 531.97/149.86 ? [7] @l2 + [0] 531.97/149.86 = [append#1(@l1, @l2)] 531.97/149.86 531.97/149.86 [append#1(nil(), @l2)] = [7] @l2 + [0] 531.97/149.86 >= [1] @l2 + [0] 531.97/149.86 = [@l2] 531.97/149.86 531.97/149.86 [append#1(::(@x, @xs), @l2)] = [7] @l2 + [0] 531.97/149.86 ? [1] @x + [0] 531.97/149.86 = [::(@x, append(@xs, @l2))] 531.97/149.86 531.97/149.86 [flatten#1(leaf())] = [0] 531.97/149.86 ? [4] 531.97/149.86 = [nil()] 531.97/149.86 531.97/149.86 [flatten#1(node(@l, @t1, @t2))] = [0] 531.97/149.86 >= [0] 531.97/149.86 = [append(@l, append(flatten(@t1), flatten(@t2)))] 531.97/149.86 531.97/149.86 [flatten(@t)] = [0] 531.97/149.86 >= [0] 531.97/149.86 = [flatten#1(@t)] 531.97/149.86 531.97/149.86 [flattensort^#(@t)] = [7] @t + [7] 531.97/149.86 > [3] @t + [6] 531.97/149.86 = [c_1(flatten^#(@t))] 531.97/149.86 531.97/149.86 [flatten^#(@t)] = [1] @t + [1] 531.97/149.86 > [1] @t + [0] 531.97/149.86 = [c_2(flatten#1^#(@t))] 531.97/149.86 531.97/149.86 [flatten#1^#(node(@l, @t1, @t2))] = [1] @l + [1] @t1 + [1] @t2 + [2] 531.97/149.86 >= [1] @t1 + [1] @t2 + [2] 531.97/149.86 = [c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2))] 531.97/149.86 531.97/149.86 531.97/149.86 We return to the main proof. Consider the set of all dependency 531.97/149.86 pairs 531.97/149.86 531.97/149.86 : 531.97/149.86 { 1: flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , 2: flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , 3: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 531.97/149.86 Processor 'matrix interpretation of dimension 1' induces the 531.97/149.86 complexity certificate YES(?,O(n^1)) on application of dependency 531.97/149.86 pairs {1,2}. These cover all (indirect) predecessors of dependency 531.97/149.86 pairs {1,2,3}, their number of application is equally bounded. The 531.97/149.86 dependency pairs are shifted into the weak component. 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(1)). 531.97/149.86 531.97/149.86 Weak DPs: 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(1)) 531.97/149.86 531.97/149.86 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.86 closed under successors. The DPs are removed. 531.97/149.86 531.97/149.86 { flattensort^#(@t) -> c_1(flatten^#(@t)) 531.97/149.86 , flatten^#(@t) -> c_2(flatten#1^#(@t)) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 c_5(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.86 append^#(flatten(@t1), flatten(@t2)), 531.97/149.86 flatten^#(@t1), 531.97/149.86 flatten^#(@t2)) } 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(1)). 531.97/149.86 531.97/149.86 Weak Trs: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(1)) 531.97/149.86 531.97/149.86 No rule is usable, rules are removed from the input problem. 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(1)). 531.97/149.86 531.97/149.86 Rules: Empty 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(1)) 531.97/149.86 531.97/149.86 Empty rules are trivially bounded 531.97/149.86 531.97/149.86 We return to the main proof. 531.97/149.86 531.97/149.86 We are left with following problem, upon which TcT provides the 531.97/149.86 certificate YES(O(1),O(n^1)). 531.97/149.86 531.97/149.86 Strict DPs: 531.97/149.86 { append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.86 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) } 531.97/149.86 Weak DPs: 531.97/149.86 { flattensort^#(@t) -> flatten^#(@t) 531.97/149.86 , flatten^#(@t) -> flatten#1^#(@t) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.86 Weak Trs: 531.97/149.86 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.86 , append#1(nil(), @l2) -> @l2 531.97/149.86 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.86 , flatten#1(leaf()) -> nil() 531.97/149.86 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , flatten(@t) -> flatten#1(@t) } 531.97/149.86 Obligation: 531.97/149.86 innermost runtime complexity 531.97/149.86 Answer: 531.97/149.86 YES(O(1),O(n^1)) 531.97/149.86 531.97/149.86 We use the processor 'matrix interpretation of dimension 1' to 531.97/149.86 orient following rules strictly. 531.97/149.86 531.97/149.86 DPs: 531.97/149.86 { 2: append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.86 , 3: flattensort^#(@t) -> flatten^#(@t) 531.97/149.86 , 5: flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.86 , 6: flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.86 , 7: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.86 , 8: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.86 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.86 Trs: 531.97/149.86 { flatten#1(node(@l, @t1, @t2)) -> 531.97/149.86 append(@l, append(flatten(@t1), flatten(@t2))) } 531.97/149.86 531.97/149.86 Sub-proof: 531.97/149.86 ---------- 531.97/149.86 The following argument positions are usable: 531.97/149.86 Uargs(c_3) = {1}, Uargs(c_4) = {1} 531.97/149.86 531.97/149.86 TcT has computed the following constructor-based matrix 531.97/149.86 interpretation satisfying not(EDA). 531.97/149.86 531.97/149.86 [leaf] = [0] 531.97/149.86 531.97/149.86 [append](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.86 531.97/149.86 [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 531.97/149.86 531.97/149.86 [nil] = [0] 531.97/149.86 531.97/149.86 [append#1](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.86 531.97/149.86 [flatten#1](x1) = [2] x1 + [0] 531.97/149.86 531.97/149.86 [::](x1, x2) = [1] x1 + [1] x2 + [1] 531.97/149.86 531.97/149.86 [flatten](x1) = [2] x1 + [0] 531.97/149.86 531.97/149.86 [flattensort^#](x1) = [7] x1 + [7] 531.97/149.86 531.97/149.86 [flatten^#](x1) = [4] x1 + [0] 531.97/149.86 531.97/149.86 [append^#](x1, x2) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [append#1^#](x1, x2) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [flatten#1^#](x1) = [4] x1 + [0] 531.97/149.86 531.97/149.86 [c_3](x1) = [1] x1 + [0] 531.97/149.86 531.97/149.86 [c_4](x1) = [1] x1 + [0] 531.97/149.86 531.97/149.86 The order satisfies the following ordering constraints: 531.97/149.86 531.97/149.86 [append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] 531.97/149.86 >= [1] @l1 + [1] @l2 + [0] 531.97/149.86 = [append#1(@l1, @l2)] 531.97/149.86 531.97/149.86 [append#1(nil(), @l2)] = [1] @l2 + [0] 531.97/149.86 >= [1] @l2 + [0] 531.97/149.86 = [@l2] 531.97/149.86 531.97/149.86 [append#1(::(@x, @xs), @l2)] = [1] @x + [1] @l2 + [1] @xs + [1] 531.97/149.86 >= [1] @x + [1] @l2 + [1] @xs + [1] 531.97/149.86 = [::(@x, append(@xs, @l2))] 531.97/149.87 531.97/149.87 [flatten#1(leaf())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [nil()] 531.97/149.87 531.97/149.87 [flatten#1(node(@l, @t1, @t2))] = [2] @l + [2] @t1 + [2] @t2 + [4] 531.97/149.87 > [1] @l + [2] @t1 + [2] @t2 + [0] 531.97/149.87 = [append(@l, append(flatten(@t1), flatten(@t2)))] 531.97/149.87 531.97/149.87 [flatten(@t)] = [2] @t + [0] 531.97/149.87 >= [2] @t + [0] 531.97/149.87 = [flatten#1(@t)] 531.97/149.87 531.97/149.87 [flattensort^#(@t)] = [7] @t + [7] 531.97/149.87 > [4] @t + [0] 531.97/149.87 = [flatten^#(@t)] 531.97/149.87 531.97/149.87 [flatten^#(@t)] = [4] @t + [0] 531.97/149.87 >= [4] @t + [0] 531.97/149.87 = [flatten#1^#(@t)] 531.97/149.87 531.97/149.87 [append^#(@l1, @l2)] = [1] @l1 + [0] 531.97/149.87 >= [1] @l1 + [0] 531.97/149.87 = [c_3(append#1^#(@l1, @l2))] 531.97/149.87 531.97/149.87 [append#1^#(::(@x, @xs), @l2)] = [1] @x + [1] @xs + [1] 531.97/149.87 > [1] @xs + [0] 531.97/149.87 = [c_4(append^#(@xs, @l2))] 531.97/149.87 531.97/149.87 [flatten#1^#(node(@l, @t1, @t2))] = [4] @l + [4] @t1 + [4] @t2 + [8] 531.97/149.87 > [4] @t1 + [0] 531.97/149.87 = [flatten^#(@t1)] 531.97/149.87 531.97/149.87 [flatten#1^#(node(@l, @t1, @t2))] = [4] @l + [4] @t1 + [4] @t2 + [8] 531.97/149.87 > [4] @t2 + [0] 531.97/149.87 = [flatten^#(@t2)] 531.97/149.87 531.97/149.87 [flatten#1^#(node(@l, @t1, @t2))] = [4] @l + [4] @t1 + [4] @t2 + [8] 531.97/149.87 > [1] @l + [0] 531.97/149.87 = [append^#(@l, append(flatten(@t1), flatten(@t2)))] 531.97/149.87 531.97/149.87 [flatten#1^#(node(@l, @t1, @t2))] = [4] @l + [4] @t1 + [4] @t2 + [8] 531.97/149.87 > [2] @t1 + [0] 531.97/149.87 = [append^#(flatten(@t1), flatten(@t2))] 531.97/149.87 531.97/149.87 531.97/149.87 We return to the main proof. Consider the set of all dependency 531.97/149.87 pairs 531.97/149.87 531.97/149.87 : 531.97/149.87 { 1: append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.87 , 2: append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.87 , 3: flattensort^#(@t) -> flatten^#(@t) 531.97/149.87 , 4: flatten^#(@t) -> flatten#1^#(@t) 531.97/149.87 , 5: flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.87 , 6: flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.87 , 7: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , 8: flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.87 531.97/149.87 Processor 'matrix interpretation of dimension 1' induces the 531.97/149.87 complexity certificate YES(?,O(n^1)) on application of dependency 531.97/149.87 pairs {2,3,5,6,7,8}. These cover all (indirect) predecessors of 531.97/149.87 dependency pairs {1,2,3,4,5,6,7,8}, their number of application is 531.97/149.87 equally bounded. The dependency pairs are shifted into the weak 531.97/149.87 component. 531.97/149.87 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(1)). 531.97/149.87 531.97/149.87 Weak DPs: 531.97/149.87 { flattensort^#(@t) -> flatten^#(@t) 531.97/149.87 , flatten^#(@t) -> flatten#1^#(@t) 531.97/149.87 , append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.87 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.87 Weak Trs: 531.97/149.87 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , flatten(@t) -> flatten#1(@t) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(1)) 531.97/149.87 531.97/149.87 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.87 closed under successors. The DPs are removed. 531.97/149.87 531.97/149.87 { flattensort^#(@t) -> flatten^#(@t) 531.97/149.87 , flatten^#(@t) -> flatten#1^#(@t) 531.97/149.87 , append^#(@l1, @l2) -> c_3(append#1^#(@l1, @l2)) 531.97/149.87 , append#1^#(::(@x, @xs), @l2) -> c_4(append^#(@xs, @l2)) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t1) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> flatten^#(@t2) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 append^#(flatten(@t1), flatten(@t2)) } 531.97/149.87 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(1)). 531.97/149.87 531.97/149.87 Weak Trs: 531.97/149.87 { append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , flatten(@t) -> flatten#1(@t) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(1)) 531.97/149.87 531.97/149.87 No rule is usable, rules are removed from the input problem. 531.97/149.87 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(1)). 531.97/149.87 531.97/149.87 Rules: Empty 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(1)) 531.97/149.87 531.97/149.87 Empty rules are trivially bounded 531.97/149.87 531.97/149.87 S) We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(n^2)). 531.97/149.87 531.97/149.87 Strict DPs: 531.97/149.87 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.87 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.87 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.87 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.87 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.87 Weak DPs: 531.97/149.87 { flattensort^#(@t) -> 531.97/149.87 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) 531.97/149.87 , flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.87 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.87 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.87 append^#(flatten(@t1), flatten(@t2)), 531.97/149.87 flatten^#(@t1), 531.97/149.87 flatten^#(@t2)) } 531.97/149.87 Weak Trs: 531.97/149.87 { insertionsort#1(nil()) -> nil() 531.97/149.87 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.87 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , #cklt(#EQ()) -> #false() 531.97/149.87 , #cklt(#LT()) -> #true() 531.97/149.87 , #cklt(#GT()) -> #false() 531.97/149.87 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.87 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.87 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.87 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.87 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.87 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#0(), #0()) -> #EQ() 531.97/149.87 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.87 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.87 , #compare(#s(@x), #0()) -> #GT() 531.97/149.87 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.87 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.87 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.87 , flatten(@t) -> flatten#1(@t) 531.97/149.87 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(n^2)) 531.97/149.87 531.97/149.87 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.87 closed under successors. The DPs are removed. 531.97/149.87 531.97/149.87 { flatten^#(@t) -> c_3(flatten#1^#(@t)) 531.97/149.87 , append^#(@l1, @l2) -> c_6(append#1^#(@l1, @l2)) 531.97/149.87 , append#1^#(::(@x, @xs), @l2) -> c_7(append^#(@xs, @l2)) 531.97/149.87 , flatten#1^#(node(@l, @t1, @t2)) -> 531.97/149.87 c_10(append^#(@l, append(flatten(@t1), flatten(@t2))), 531.97/149.87 append^#(flatten(@t1), flatten(@t2)), 531.97/149.87 flatten^#(@t1), 531.97/149.87 flatten^#(@t2)) } 531.97/149.87 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(n^2)). 531.97/149.87 531.97/149.87 Strict DPs: 531.97/149.87 { insertionsort^#(@l) -> c_2(insertionsort#1^#(@l)) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_4(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.87 , insert^#(@x, @l) -> c_5(insert#1^#(@l, @x)) 531.97/149.87 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.87 c_8(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.87 , insert#2^#(#true(), @x, @y, @ys) -> c_9(insert^#(@x, @ys)) } 531.97/149.87 Weak DPs: 531.97/149.87 { flattensort^#(@t) -> 531.97/149.87 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) } 531.97/149.87 Weak Trs: 531.97/149.87 { insertionsort#1(nil()) -> nil() 531.97/149.87 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.87 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , #cklt(#EQ()) -> #false() 531.97/149.87 , #cklt(#LT()) -> #true() 531.97/149.87 , #cklt(#GT()) -> #false() 531.97/149.87 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.87 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.87 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.87 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.87 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.87 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#0(), #0()) -> #EQ() 531.97/149.87 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.87 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.87 , #compare(#s(@x), #0()) -> #GT() 531.97/149.87 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.87 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.87 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.87 , flatten(@t) -> flatten#1(@t) 531.97/149.87 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(n^2)) 531.97/149.87 531.97/149.87 Due to missing edges in the dependency-graph, the right-hand sides 531.97/149.87 of following rules could be simplified: 531.97/149.87 531.97/149.87 { flattensort^#(@t) -> 531.97/149.87 c_1(insertionsort^#(flatten(@t)), flatten^#(@t)) } 531.97/149.87 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(n^2)). 531.97/149.87 531.97/149.87 Strict DPs: 531.97/149.87 { insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.87 , insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.87 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.87 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.87 , insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) } 531.97/149.87 Weak DPs: 531.97/149.87 { flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) } 531.97/149.87 Weak Trs: 531.97/149.87 { insertionsort#1(nil()) -> nil() 531.97/149.87 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.87 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , #cklt(#EQ()) -> #false() 531.97/149.87 , #cklt(#LT()) -> #true() 531.97/149.87 , #cklt(#GT()) -> #false() 531.97/149.87 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.87 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.87 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.87 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.87 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.87 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#0(), #0()) -> #EQ() 531.97/149.87 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.87 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.87 , #compare(#s(@x), #0()) -> #GT() 531.97/149.87 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.87 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.87 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.87 , flatten(@t) -> flatten#1(@t) 531.97/149.87 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(n^2)) 531.97/149.87 531.97/149.87 We decompose the input problem according to the dependency graph 531.97/149.87 into the upper component 531.97/149.87 531.97/149.87 { flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) 531.97/149.87 , insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) } 531.97/149.87 531.97/149.87 and lower component 531.97/149.87 531.97/149.87 { insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.87 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.87 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.87 , insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) } 531.97/149.87 531.97/149.87 Further, following extension rules are added to the lower 531.97/149.87 component. 531.97/149.87 531.97/149.87 { flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.87 , insertionsort^#(@l) -> insertionsort#1^#(@l) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 insert^#(@x, insertionsort(@xs)) } 531.97/149.87 531.97/149.87 TcT solves the upper component with certificate YES(O(1),O(n^1)). 531.97/149.87 531.97/149.87 Sub-proof: 531.97/149.87 ---------- 531.97/149.87 We are left with following problem, upon which TcT provides the 531.97/149.87 certificate YES(O(1),O(n^1)). 531.97/149.87 531.97/149.87 Strict DPs: 531.97/149.87 { insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.87 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) } 531.97/149.87 Weak DPs: 531.97/149.87 { flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) } 531.97/149.87 Weak Trs: 531.97/149.87 { insertionsort#1(nil()) -> nil() 531.97/149.87 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.87 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.87 , #cklt(#EQ()) -> #false() 531.97/149.87 , #cklt(#LT()) -> #true() 531.97/149.87 , #cklt(#GT()) -> #false() 531.97/149.87 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.87 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.87 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.87 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.87 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.87 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#0(), #0()) -> #EQ() 531.97/149.87 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.87 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.87 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.87 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.87 , #compare(#s(@x), #0()) -> #GT() 531.97/149.87 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.87 , append#1(nil(), @l2) -> @l2 531.97/149.87 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.87 , flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.87 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.87 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.87 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.87 , flatten(@t) -> flatten#1(@t) 531.97/149.87 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.87 Obligation: 531.97/149.87 innermost runtime complexity 531.97/149.87 Answer: 531.97/149.87 YES(O(1),O(n^1)) 531.97/149.87 531.97/149.87 We use the processor 'matrix interpretation of dimension 1' to 531.97/149.87 orient following rules strictly. 531.97/149.87 531.97/149.87 DPs: 531.97/149.87 { 2: insertionsort#1^#(::(@x, @xs)) -> 531.97/149.87 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.87 , 3: flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) } 531.97/149.87 Trs: 531.97/149.87 { flatten#1(leaf()) -> nil() 531.97/149.87 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.87 append(@l, append(flatten(@t1), flatten(@t2))) } 531.97/149.87 531.97/149.87 Sub-proof: 531.97/149.87 ---------- 531.97/149.87 The following argument positions are usable: 531.97/149.87 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_6) = {1} 531.97/149.87 531.97/149.87 TcT has computed the following constructor-based matrix 531.97/149.87 interpretation satisfying not(EDA). 531.97/149.87 531.97/149.87 [insertionsort#1](x1) = [0] 531.97/149.87 531.97/149.87 [#true] = [0] 531.97/149.87 531.97/149.87 [leaf] = [4] 531.97/149.87 531.97/149.87 [append](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.87 531.97/149.87 [#cklt](x1) = [0] 531.97/149.87 531.97/149.87 [insert](x1, x2) = [4] 531.97/149.87 531.97/149.87 [#pos](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 531.97/149.87 531.97/149.87 [#EQ] = [0] 531.97/149.87 531.97/149.87 [insert#2](x1, x2, x3, x4) = [1] x3 + [4] x4 + [0] 531.97/149.87 531.97/149.87 [#compare](x1, x2) = [0] 531.97/149.87 531.97/149.87 [nil] = [0] 531.97/149.87 531.97/149.87 [append#1](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.87 531.97/149.87 [#false] = [0] 531.97/149.87 531.97/149.87 [flatten#1](x1) = [1] x1 + [1] 531.97/149.87 531.97/149.87 [::](x1, x2) = [1] x2 + [4] 531.97/149.87 531.97/149.87 [#LT] = [0] 531.97/149.87 531.97/149.87 [insert#1](x1, x2) = [6] x2 + [0] 531.97/149.87 531.97/149.87 [#0] = [0] 531.97/149.87 531.97/149.87 [#neg](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [#less](x1, x2) = [0] 531.97/149.87 531.97/149.87 [flatten](x1) = [1] x1 + [1] 531.97/149.87 531.97/149.87 [#s](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [#GT] = [0] 531.97/149.87 531.97/149.87 [insertionsort](x1) = [0] 531.97/149.87 531.97/149.87 [flattensort^#](x1) = [7] x1 + [7] 531.97/149.87 531.97/149.87 [insertionsort^#](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [insertionsort#1^#](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [insert^#](x1, x2) = [0] 531.97/149.87 531.97/149.87 [c_1](x1) = [1] x1 + [0] 531.97/149.87 531.97/149.87 [c_2](x1, x2) = [4] x1 + [1] x2 + [1] 531.97/149.87 531.97/149.87 [c_6](x1) = [4] x1 + [1] 531.97/149.87 531.97/149.87 The order satisfies the following ordering constraints: 531.97/149.87 531.97/149.87 [insertionsort#1(nil())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [nil()] 531.97/149.87 531.97/149.87 [insertionsort#1(::(@x, @xs))] = [0] 531.97/149.87 ? [4] 531.97/149.87 = [insert(@x, insertionsort(@xs))] 531.97/149.87 531.97/149.87 [append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] 531.97/149.87 >= [1] @l1 + [1] @l2 + [0] 531.97/149.87 = [append#1(@l1, @l2)] 531.97/149.87 531.97/149.87 [#cklt(#EQ())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#false()] 531.97/149.87 531.97/149.87 [#cklt(#LT())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#true()] 531.97/149.87 531.97/149.87 [#cklt(#GT())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#false()] 531.97/149.87 531.97/149.87 [insert(@x, @l)] = [4] 531.97/149.87 ? [6] @x + [0] 531.97/149.87 = [insert#1(@l, @x)] 531.97/149.87 531.97/149.87 [insert#2(#true(), @x, @y, @ys)] = [1] @y + [4] @ys + [0] 531.97/149.87 ? [8] 531.97/149.87 = [::(@y, insert(@x, @ys))] 531.97/149.87 531.97/149.87 [insert#2(#false(), @x, @y, @ys)] = [1] @y + [4] @ys + [0] 531.97/149.87 ? [1] @ys + [8] 531.97/149.87 = [::(@x, ::(@y, @ys))] 531.97/149.87 531.97/149.87 [#compare(#pos(@x), #pos(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#compare(@x, @y)] 531.97/149.87 531.97/149.87 [#compare(#pos(@x), #0())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#GT()] 531.97/149.87 531.97/149.87 [#compare(#pos(@x), #neg(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#GT()] 531.97/149.87 531.97/149.87 [#compare(#0(), #pos(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#LT()] 531.97/149.87 531.97/149.87 [#compare(#0(), #0())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#EQ()] 531.97/149.87 531.97/149.87 [#compare(#0(), #neg(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#GT()] 531.97/149.87 531.97/149.87 [#compare(#0(), #s(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#LT()] 531.97/149.87 531.97/149.87 [#compare(#neg(@x), #pos(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#LT()] 531.97/149.87 531.97/149.87 [#compare(#neg(@x), #0())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#LT()] 531.97/149.87 531.97/149.87 [#compare(#neg(@x), #neg(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#compare(@y, @x)] 531.97/149.87 531.97/149.87 [#compare(#s(@x), #0())] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#GT()] 531.97/149.87 531.97/149.87 [#compare(#s(@x), #s(@y))] = [0] 531.97/149.87 >= [0] 531.97/149.87 = [#compare(@x, @y)] 531.97/149.87 531.97/149.87 [append#1(nil(), @l2)] = [1] @l2 + [0] 531.97/149.88 >= [1] @l2 + [0] 531.97/149.88 = [@l2] 531.97/149.88 531.97/149.88 [append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [4] 531.97/149.88 >= [1] @l2 + [1] @xs + [4] 531.97/149.88 = [::(@x, append(@xs, @l2))] 531.97/149.88 531.97/149.88 [flatten#1(leaf())] = [5] 531.97/149.88 > [0] 531.97/149.88 = [nil()] 531.97/149.88 531.97/149.88 [flatten#1(node(@l, @t1, @t2))] = [1] @l + [1] @t1 + [1] @t2 + [8] 531.97/149.88 > [1] @l + [1] @t1 + [1] @t2 + [2] 531.97/149.88 = [append(@l, append(flatten(@t1), flatten(@t2)))] 531.97/149.88 531.97/149.88 [insert#1(nil(), @x)] = [6] @x + [0] 531.97/149.88 ? [4] 531.97/149.88 = [::(@x, nil())] 531.97/149.88 531.97/149.88 [insert#1(::(@y, @ys), @x)] = [6] @x + [0] 531.97/149.88 ? [1] @y + [4] @ys + [0] 531.97/149.88 = [insert#2(#less(@y, @x), @x, @y, @ys)] 531.97/149.88 531.97/149.88 [#less(@x, @y)] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#cklt(#compare(@x, @y))] 531.97/149.88 531.97/149.88 [flatten(@t)] = [1] @t + [1] 531.97/149.88 >= [1] @t + [1] 531.97/149.88 = [flatten#1(@t)] 531.97/149.88 531.97/149.88 [insertionsort(@l)] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [insertionsort#1(@l)] 531.97/149.88 531.97/149.88 [flattensort^#(@t)] = [7] @t + [7] 531.97/149.88 > [4] @t + [5] 531.97/149.88 = [c_6(insertionsort^#(flatten(@t)))] 531.97/149.88 531.97/149.88 [insertionsort^#(@l)] = [1] @l + [0] 531.97/149.88 >= [1] @l + [0] 531.97/149.88 = [c_1(insertionsort#1^#(@l))] 531.97/149.88 531.97/149.88 [insertionsort#1^#(::(@x, @xs))] = [1] @xs + [4] 531.97/149.88 > [1] @xs + [1] 531.97/149.88 = [c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))] 531.97/149.88 531.97/149.88 531.97/149.88 We return to the main proof. Consider the set of all dependency 531.97/149.88 pairs 531.97/149.88 531.97/149.88 : 531.97/149.88 { 1: insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.88 , 2: insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) 531.97/149.88 , 3: flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) } 531.97/149.88 531.97/149.88 Processor 'matrix interpretation of dimension 1' induces the 531.97/149.88 complexity certificate YES(?,O(n^1)) on application of dependency 531.97/149.88 pairs {2,3}. These cover all (indirect) predecessors of dependency 531.97/149.88 pairs {1,2,3}, their number of application is equally bounded. The 531.97/149.88 dependency pairs are shifted into the weak component. 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Weak DPs: 531.97/149.88 { flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) 531.97/149.88 , insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) } 531.97/149.88 Weak Trs: 531.97/149.88 { insertionsort#1(nil()) -> nil() 531.97/149.88 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.88 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.88 , #cklt(#EQ()) -> #false() 531.97/149.88 , #cklt(#LT()) -> #true() 531.97/149.88 , #cklt(#GT()) -> #false() 531.97/149.88 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.88 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.88 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.88 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.88 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.88 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#0(), #0()) -> #EQ() 531.97/149.88 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.88 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.88 , #compare(#s(@x), #0()) -> #GT() 531.97/149.88 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.88 , append#1(nil(), @l2) -> @l2 531.97/149.88 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.88 , flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.88 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.88 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.88 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.88 , flatten(@t) -> flatten#1(@t) 531.97/149.88 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.88 closed under successors. The DPs are removed. 531.97/149.88 531.97/149.88 { flattensort^#(@t) -> c_6(insertionsort^#(flatten(@t))) 531.97/149.88 , insertionsort^#(@l) -> c_1(insertionsort#1^#(@l)) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 c_2(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) } 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Weak Trs: 531.97/149.88 { insertionsort#1(nil()) -> nil() 531.97/149.88 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.88 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.88 , #cklt(#EQ()) -> #false() 531.97/149.88 , #cklt(#LT()) -> #true() 531.97/149.88 , #cklt(#GT()) -> #false() 531.97/149.88 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.88 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.88 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.88 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.88 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.88 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#0(), #0()) -> #EQ() 531.97/149.88 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.88 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.88 , #compare(#s(@x), #0()) -> #GT() 531.97/149.88 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.88 , append#1(nil(), @l2) -> @l2 531.97/149.88 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.88 , flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.88 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.88 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.88 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.88 , flatten(@t) -> flatten#1(@t) 531.97/149.88 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 No rule is usable, rules are removed from the input problem. 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Rules: Empty 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 Empty rules are trivially bounded 531.97/149.88 531.97/149.88 We return to the main proof. 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(n^1)). 531.97/149.88 531.97/149.88 Strict DPs: 531.97/149.88 { insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.88 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.88 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.88 , insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) } 531.97/149.88 Weak DPs: 531.97/149.88 { flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.88 , insertionsort^#(@l) -> insertionsort#1^#(@l) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 insert^#(@x, insertionsort(@xs)) } 531.97/149.88 Weak Trs: 531.97/149.88 { insertionsort#1(nil()) -> nil() 531.97/149.88 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.88 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.88 , #cklt(#EQ()) -> #false() 531.97/149.88 , #cklt(#LT()) -> #true() 531.97/149.88 , #cklt(#GT()) -> #false() 531.97/149.88 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.88 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.88 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.88 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.88 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.88 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#0(), #0()) -> #EQ() 531.97/149.88 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.88 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.88 , #compare(#s(@x), #0()) -> #GT() 531.97/149.88 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.88 , append#1(nil(), @l2) -> @l2 531.97/149.88 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.88 , flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.88 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.88 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.88 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.88 , flatten(@t) -> flatten#1(@t) 531.97/149.88 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(n^1)) 531.97/149.88 531.97/149.88 We use the processor 'matrix interpretation of dimension 1' to 531.97/149.88 orient following rules strictly. 531.97/149.88 531.97/149.88 DPs: 531.97/149.88 { 2: insert#1^#(::(@y, @ys), @x) -> 531.97/149.88 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.88 , 4: flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.88 , 6: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.88 , 7: insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 insert^#(@x, insertionsort(@xs)) } 531.97/149.88 Trs: 531.97/149.88 { flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) } 531.97/149.88 531.97/149.88 Sub-proof: 531.97/149.88 ---------- 531.97/149.88 The following argument positions are usable: 531.97/149.88 Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1} 531.97/149.88 531.97/149.88 TcT has computed the following constructor-based matrix 531.97/149.88 interpretation satisfying not(EDA). 531.97/149.88 531.97/149.88 [insertionsort#1](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [#true] = [0] 531.97/149.88 531.97/149.88 [leaf] = [0] 531.97/149.88 531.97/149.88 [append](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.88 531.97/149.88 [#cklt](x1) = [0] 531.97/149.88 531.97/149.88 [insert](x1, x2) = [1] x2 + [2] 531.97/149.88 531.97/149.88 [#pos](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 531.97/149.88 531.97/149.88 [#EQ] = [0] 531.97/149.88 531.97/149.88 [insert#2](x1, x2, x3, x4) = [1] x4 + [4] 531.97/149.88 531.97/149.88 [#compare](x1, x2) = [0] 531.97/149.88 531.97/149.88 [nil] = [0] 531.97/149.88 531.97/149.88 [append#1](x1, x2) = [1] x1 + [1] x2 + [0] 531.97/149.88 531.97/149.88 [#false] = [0] 531.97/149.88 531.97/149.88 [flatten#1](x1) = [1] x1 + [1] 531.97/149.88 531.97/149.88 [::](x1, x2) = [1] x2 + [2] 531.97/149.88 531.97/149.88 [#LT] = [0] 531.97/149.88 531.97/149.88 [insert#1](x1, x2) = [1] x1 + [2] 531.97/149.88 531.97/149.88 [#0] = [0] 531.97/149.88 531.97/149.88 [#neg](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [#less](x1, x2) = [0] 531.97/149.88 531.97/149.88 [flatten](x1) = [1] x1 + [1] 531.97/149.88 531.97/149.88 [#s](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [#GT] = [0] 531.97/149.88 531.97/149.88 [insertionsort](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [flattensort^#](x1) = [7] x1 + [7] 531.97/149.88 531.97/149.88 [insertionsort^#](x1) = [2] x1 + [4] 531.97/149.88 531.97/149.88 [insertionsort#1^#](x1) = [2] x1 + [4] 531.97/149.88 531.97/149.88 [insert^#](x1, x2) = [2] x2 + [0] 531.97/149.88 531.97/149.88 [insert#1^#](x1, x2) = [2] x1 + [0] 531.97/149.88 531.97/149.88 [insert#2^#](x1, x2, x3, x4) = [2] x4 + [0] 531.97/149.88 531.97/149.88 [c_3](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 [c_4](x1) = [1] x1 + [1] 531.97/149.88 531.97/149.88 [c_5](x1) = [1] x1 + [0] 531.97/149.88 531.97/149.88 The order satisfies the following ordering constraints: 531.97/149.88 531.97/149.88 [insertionsort#1(nil())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [nil()] 531.97/149.88 531.97/149.88 [insertionsort#1(::(@x, @xs))] = [1] @xs + [2] 531.97/149.88 >= [1] @xs + [2] 531.97/149.88 = [insert(@x, insertionsort(@xs))] 531.97/149.88 531.97/149.88 [append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] 531.97/149.88 >= [1] @l1 + [1] @l2 + [0] 531.97/149.88 = [append#1(@l1, @l2)] 531.97/149.88 531.97/149.88 [#cklt(#EQ())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#false()] 531.97/149.88 531.97/149.88 [#cklt(#LT())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#true()] 531.97/149.88 531.97/149.88 [#cklt(#GT())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#false()] 531.97/149.88 531.97/149.88 [insert(@x, @l)] = [1] @l + [2] 531.97/149.88 >= [1] @l + [2] 531.97/149.88 = [insert#1(@l, @x)] 531.97/149.88 531.97/149.88 [insert#2(#true(), @x, @y, @ys)] = [1] @ys + [4] 531.97/149.88 >= [1] @ys + [4] 531.97/149.88 = [::(@y, insert(@x, @ys))] 531.97/149.88 531.97/149.88 [insert#2(#false(), @x, @y, @ys)] = [1] @ys + [4] 531.97/149.88 >= [1] @ys + [4] 531.97/149.88 = [::(@x, ::(@y, @ys))] 531.97/149.88 531.97/149.88 [#compare(#pos(@x), #pos(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#compare(@x, @y)] 531.97/149.88 531.97/149.88 [#compare(#pos(@x), #0())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#GT()] 531.97/149.88 531.97/149.88 [#compare(#pos(@x), #neg(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#GT()] 531.97/149.88 531.97/149.88 [#compare(#0(), #pos(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#LT()] 531.97/149.88 531.97/149.88 [#compare(#0(), #0())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#EQ()] 531.97/149.88 531.97/149.88 [#compare(#0(), #neg(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#GT()] 531.97/149.88 531.97/149.88 [#compare(#0(), #s(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#LT()] 531.97/149.88 531.97/149.88 [#compare(#neg(@x), #pos(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#LT()] 531.97/149.88 531.97/149.88 [#compare(#neg(@x), #0())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#LT()] 531.97/149.88 531.97/149.88 [#compare(#neg(@x), #neg(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#compare(@y, @x)] 531.97/149.88 531.97/149.88 [#compare(#s(@x), #0())] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#GT()] 531.97/149.88 531.97/149.88 [#compare(#s(@x), #s(@y))] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#compare(@x, @y)] 531.97/149.88 531.97/149.88 [append#1(nil(), @l2)] = [1] @l2 + [0] 531.97/149.88 >= [1] @l2 + [0] 531.97/149.88 = [@l2] 531.97/149.88 531.97/149.88 [append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [2] 531.97/149.88 >= [1] @l2 + [1] @xs + [2] 531.97/149.88 = [::(@x, append(@xs, @l2))] 531.97/149.88 531.97/149.88 [flatten#1(leaf())] = [1] 531.97/149.88 > [0] 531.97/149.88 = [nil()] 531.97/149.88 531.97/149.88 [flatten#1(node(@l, @t1, @t2))] = [1] @l + [1] @t1 + [1] @t2 + [8] 531.97/149.88 > [1] @l + [1] @t1 + [1] @t2 + [2] 531.97/149.88 = [append(@l, append(flatten(@t1), flatten(@t2)))] 531.97/149.88 531.97/149.88 [insert#1(nil(), @x)] = [2] 531.97/149.88 >= [2] 531.97/149.88 = [::(@x, nil())] 531.97/149.88 531.97/149.88 [insert#1(::(@y, @ys), @x)] = [1] @ys + [4] 531.97/149.88 >= [1] @ys + [4] 531.97/149.88 = [insert#2(#less(@y, @x), @x, @y, @ys)] 531.97/149.88 531.97/149.88 [#less(@x, @y)] = [0] 531.97/149.88 >= [0] 531.97/149.88 = [#cklt(#compare(@x, @y))] 531.97/149.88 531.97/149.88 [flatten(@t)] = [1] @t + [1] 531.97/149.88 >= [1] @t + [1] 531.97/149.88 = [flatten#1(@t)] 531.97/149.88 531.97/149.88 [insertionsort(@l)] = [1] @l + [0] 531.97/149.88 >= [1] @l + [0] 531.97/149.88 = [insertionsort#1(@l)] 531.97/149.88 531.97/149.88 [flattensort^#(@t)] = [7] @t + [7] 531.97/149.88 > [2] @t + [6] 531.97/149.88 = [insertionsort^#(flatten(@t))] 531.97/149.88 531.97/149.88 [insertionsort^#(@l)] = [2] @l + [4] 531.97/149.88 >= [2] @l + [4] 531.97/149.88 = [insertionsort#1^#(@l)] 531.97/149.88 531.97/149.88 [insertionsort#1^#(::(@x, @xs))] = [2] @xs + [8] 531.97/149.88 > [2] @xs + [4] 531.97/149.88 = [insertionsort^#(@xs)] 531.97/149.88 531.97/149.88 [insertionsort#1^#(::(@x, @xs))] = [2] @xs + [8] 531.97/149.88 > [2] @xs + [0] 531.97/149.88 = [insert^#(@x, insertionsort(@xs))] 531.97/149.88 531.97/149.88 [insert^#(@x, @l)] = [2] @l + [0] 531.97/149.88 >= [2] @l + [0] 531.97/149.88 = [c_3(insert#1^#(@l, @x))] 531.97/149.88 531.97/149.88 [insert#1^#(::(@y, @ys), @x)] = [2] @ys + [4] 531.97/149.88 > [2] @ys + [1] 531.97/149.88 = [c_4(insert#2^#(#less(@y, @x), @x, @y, @ys))] 531.97/149.88 531.97/149.88 [insert#2^#(#true(), @x, @y, @ys)] = [2] @ys + [0] 531.97/149.88 >= [2] @ys + [0] 531.97/149.88 = [c_5(insert^#(@x, @ys))] 531.97/149.88 531.97/149.88 531.97/149.88 We return to the main proof. Consider the set of all dependency 531.97/149.88 pairs 531.97/149.88 531.97/149.88 : 531.97/149.88 { 1: insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.88 , 2: insert#1^#(::(@y, @ys), @x) -> 531.97/149.88 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.88 , 3: insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) 531.97/149.88 , 4: flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.88 , 5: insertionsort^#(@l) -> insertionsort#1^#(@l) 531.97/149.88 , 6: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.88 , 7: insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 insert^#(@x, insertionsort(@xs)) } 531.97/149.88 531.97/149.88 Processor 'matrix interpretation of dimension 1' induces the 531.97/149.88 complexity certificate YES(?,O(n^1)) on application of dependency 531.97/149.88 pairs {2,4,6,7}. These cover all (indirect) predecessors of 531.97/149.88 dependency pairs {1,2,3,4,5,6,7}, their number of application is 531.97/149.88 equally bounded. The dependency pairs are shifted into the weak 531.97/149.88 component. 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Weak DPs: 531.97/149.88 { flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.88 , insertionsort^#(@l) -> insertionsort#1^#(@l) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 insert^#(@x, insertionsort(@xs)) 531.97/149.88 , insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.88 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.88 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.88 , insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) } 531.97/149.88 Weak Trs: 531.97/149.88 { insertionsort#1(nil()) -> nil() 531.97/149.88 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.88 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.88 , #cklt(#EQ()) -> #false() 531.97/149.88 , #cklt(#LT()) -> #true() 531.97/149.88 , #cklt(#GT()) -> #false() 531.97/149.88 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.88 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.88 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.88 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.88 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.88 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#0(), #0()) -> #EQ() 531.97/149.88 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.88 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.88 , #compare(#s(@x), #0()) -> #GT() 531.97/149.88 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.88 , append#1(nil(), @l2) -> @l2 531.97/149.88 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.88 , flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.88 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.88 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.88 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.88 , flatten(@t) -> flatten#1(@t) 531.97/149.88 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 The following weak DPs constitute a sub-graph of the DG that is 531.97/149.88 closed under successors. The DPs are removed. 531.97/149.88 531.97/149.88 { flattensort^#(@t) -> insertionsort^#(flatten(@t)) 531.97/149.88 , insertionsort^#(@l) -> insertionsort#1^#(@l) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) 531.97/149.88 , insertionsort#1^#(::(@x, @xs)) -> 531.97/149.88 insert^#(@x, insertionsort(@xs)) 531.97/149.88 , insert^#(@x, @l) -> c_3(insert#1^#(@l, @x)) 531.97/149.88 , insert#1^#(::(@y, @ys), @x) -> 531.97/149.88 c_4(insert#2^#(#less(@y, @x), @x, @y, @ys)) 531.97/149.88 , insert#2^#(#true(), @x, @y, @ys) -> c_5(insert^#(@x, @ys)) } 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Weak Trs: 531.97/149.88 { insertionsort#1(nil()) -> nil() 531.97/149.88 , insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs)) 531.97/149.88 , append(@l1, @l2) -> append#1(@l1, @l2) 531.97/149.88 , #cklt(#EQ()) -> #false() 531.97/149.88 , #cklt(#LT()) -> #true() 531.97/149.88 , #cklt(#GT()) -> #false() 531.97/149.88 , insert(@x, @l) -> insert#1(@l, @x) 531.97/149.88 , insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys)) 531.97/149.88 , insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 531.97/149.88 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 531.97/149.88 , #compare(#pos(@x), #0()) -> #GT() 531.97/149.88 , #compare(#pos(@x), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#0(), #0()) -> #EQ() 531.97/149.88 , #compare(#0(), #neg(@y)) -> #GT() 531.97/149.88 , #compare(#0(), #s(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #pos(@y)) -> #LT() 531.97/149.88 , #compare(#neg(@x), #0()) -> #LT() 531.97/149.88 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 531.97/149.88 , #compare(#s(@x), #0()) -> #GT() 531.97/149.88 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 531.97/149.88 , append#1(nil(), @l2) -> @l2 531.97/149.88 , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2)) 531.97/149.88 , flatten#1(leaf()) -> nil() 531.97/149.88 , flatten#1(node(@l, @t1, @t2)) -> 531.97/149.88 append(@l, append(flatten(@t1), flatten(@t2))) 531.97/149.88 , insert#1(nil(), @x) -> ::(@x, nil()) 531.97/149.88 , insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys) 531.97/149.88 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 531.97/149.88 , flatten(@t) -> flatten#1(@t) 531.97/149.88 , insertionsort(@l) -> insertionsort#1(@l) } 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 No rule is usable, rules are removed from the input problem. 531.97/149.88 531.97/149.88 We are left with following problem, upon which TcT provides the 531.97/149.88 certificate YES(O(1),O(1)). 531.97/149.88 531.97/149.88 Rules: Empty 531.97/149.88 Obligation: 531.97/149.88 innermost runtime complexity 531.97/149.88 Answer: 531.97/149.88 YES(O(1),O(1)) 531.97/149.88 531.97/149.88 Empty rules are trivially bounded 531.97/149.88 531.97/149.88 531.97/149.88 Hurray, we answered YES(O(1),O(n^2)) 532.37/150.09 EOF