YES(O(1),O(n^2)) 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , findMin#2(::(@y, @ys), @x) -> 202.34/76.51 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.51 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.51 Weak Trs: 202.34/76.51 { #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.51 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.51 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#0(), #0()) -> #EQ() 202.34/76.51 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.51 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.51 , #compare(#s(@x), #0()) -> #GT() 202.34/76.51 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) } 202.34/76.51 Obligation: 202.34/76.51 innermost runtime complexity 202.34/76.51 Answer: 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 We add the following dependency tuples: 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort#1^#(nil()) -> c_2() 202.34/76.51 , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , findMin#1^#(nil()) -> c_6() 202.34/76.51 , findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , findMin^#(@l) -> c_7(findMin#1^#(@l)) 202.34/76.51 , #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) } 202.34/76.51 Weak DPs: 202.34/76.51 { #cklt^#(#LT()) -> c_12() 202.34/76.51 , #cklt^#(#EQ()) -> c_13() 202.34/76.51 , #cklt^#(#GT()) -> c_14() 202.34/76.51 , #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 202.34/76.51 and mark the set of starting terms. 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort#1^#(nil()) -> c_2() 202.34/76.51 , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , findMin#1^#(nil()) -> c_6() 202.34/76.51 , findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , findMin^#(@l) -> c_7(findMin#1^#(@l)) 202.34/76.51 , #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) } 202.34/76.51 Weak DPs: 202.34/76.51 { #cklt^#(#LT()) -> c_12() 202.34/76.51 , #cklt^#(#EQ()) -> c_13() 202.34/76.51 , #cklt^#(#GT()) -> c_14() 202.34/76.51 , #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 Weak Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.51 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.51 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#0(), #0()) -> #EQ() 202.34/76.51 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.51 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.51 , #compare(#s(@x), #0()) -> #GT() 202.34/76.51 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.51 , findMin#2(::(@y, @ys), @x) -> 202.34/76.51 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.51 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.51 Obligation: 202.34/76.51 innermost runtime complexity 202.34/76.51 Answer: 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 We estimate the number of application of {2,4,5,7,9,11} by 202.34/76.51 applications of Pre({2,4,5,7,9,11}) = {3,6,8,10}. Here rules are 202.34/76.51 labeled as follows: 202.34/76.51 202.34/76.51 DPs: 202.34/76.51 { 1: minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , 2: minSort#1^#(nil()) -> c_2() 202.34/76.51 , 3: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , 4: findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , 5: findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , 6: findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , 7: findMin#1^#(nil()) -> c_6() 202.34/76.51 , 8: findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , 9: findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , 10: findMin^#(@l) -> c_7(findMin#1^#(@l)) 202.34/76.51 , 11: #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 202.34/76.51 , 12: #cklt^#(#LT()) -> c_12() 202.34/76.51 , 13: #cklt^#(#EQ()) -> c_13() 202.34/76.51 , 14: #cklt^#(#GT()) -> c_14() 202.34/76.51 , 15: #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , 16: #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , 17: #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , 18: #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , 19: #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , 20: #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , 21: #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , 22: #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , 23: #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , 24: #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , 25: #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , 26: #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , findMin^#(@l) -> c_7(findMin#1^#(@l)) } 202.34/76.51 Weak DPs: 202.34/76.51 { minSort#1^#(nil()) -> c_2() 202.34/76.51 , findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , findMin#1^#(nil()) -> c_6() 202.34/76.51 , findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 202.34/76.51 , #cklt^#(#LT()) -> c_12() 202.34/76.51 , #cklt^#(#EQ()) -> c_13() 202.34/76.51 , #cklt^#(#GT()) -> c_14() 202.34/76.51 , #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 Weak Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.51 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.51 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#0(), #0()) -> #EQ() 202.34/76.51 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.51 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.51 , #compare(#s(@x), #0()) -> #GT() 202.34/76.51 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.51 , findMin#2(::(@y, @ys), @x) -> 202.34/76.51 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.51 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.51 Obligation: 202.34/76.51 innermost runtime complexity 202.34/76.51 Answer: 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 We estimate the number of application of {4} by applications of 202.34/76.51 Pre({4}) = {3}. Here rules are labeled as follows: 202.34/76.51 202.34/76.51 DPs: 202.34/76.51 { 1: minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , 2: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , 3: findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , 4: findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , 5: findMin^#(@l) -> c_7(findMin#1^#(@l)) 202.34/76.51 , 6: minSort#1^#(nil()) -> c_2() 202.34/76.51 , 7: findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , 8: findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , 9: findMin#1^#(nil()) -> c_6() 202.34/76.51 , 10: findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , 11: #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 202.34/76.51 , 12: #cklt^#(#LT()) -> c_12() 202.34/76.51 , 13: #cklt^#(#EQ()) -> c_13() 202.34/76.51 , 14: #cklt^#(#GT()) -> c_14() 202.34/76.51 , 15: #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , 16: #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , 17: #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , 18: #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , 19: #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , 20: #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , 21: #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , 22: #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , 23: #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , 24: #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , 25: #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , 26: #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , findMin^#(@l) -> c_7(findMin#1^#(@l)) } 202.34/76.51 Weak DPs: 202.34/76.51 { minSort#1^#(nil()) -> c_2() 202.34/76.51 , findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , findMin#1^#(nil()) -> c_6() 202.34/76.51 , findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 202.34/76.51 , #cklt^#(#LT()) -> c_12() 202.34/76.51 , #cklt^#(#EQ()) -> c_13() 202.34/76.51 , #cklt^#(#GT()) -> c_14() 202.34/76.51 , #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 Weak Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.51 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.51 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#0(), #0()) -> #EQ() 202.34/76.51 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.51 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.51 , #compare(#s(@x), #0()) -> #GT() 202.34/76.51 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.51 , findMin#2(::(@y, @ys), @x) -> 202.34/76.51 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.51 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.51 Obligation: 202.34/76.51 innermost runtime complexity 202.34/76.51 Answer: 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 The following weak DPs constitute a sub-graph of the DG that is 202.34/76.51 closed under successors. The DPs are removed. 202.34/76.51 202.34/76.51 { minSort#1^#(nil()) -> c_2() 202.34/76.51 , findMin#3^#(#true(), @x, @y, @ys) -> c_3() 202.34/76.51 , findMin#3^#(#false(), @x, @y, @ys) -> c_4() 202.34/76.51 , findMin#1^#(nil()) -> c_6() 202.34/76.51 , findMin#2^#(::(@y, @ys), @x) -> 202.34/76.51 c_10(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) 202.34/76.51 , findMin#2^#(nil(), @x) -> c_11() 202.34/76.51 , #less^#(@x, @y) -> 202.34/76.51 c_8(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) 202.34/76.51 , #cklt^#(#LT()) -> c_12() 202.34/76.51 , #cklt^#(#EQ()) -> c_13() 202.34/76.51 , #cklt^#(#GT()) -> c_14() 202.34/76.51 , #compare^#(#pos(@x), #pos(@y)) -> c_15(#compare^#(@x, @y)) 202.34/76.51 , #compare^#(#pos(@x), #0()) -> c_16() 202.34/76.51 , #compare^#(#pos(@x), #neg(@y)) -> c_17() 202.34/76.51 , #compare^#(#0(), #pos(@y)) -> c_18() 202.34/76.51 , #compare^#(#0(), #0()) -> c_19() 202.34/76.51 , #compare^#(#0(), #neg(@y)) -> c_20() 202.34/76.51 , #compare^#(#0(), #s(@y)) -> c_21() 202.34/76.51 , #compare^#(#neg(@x), #pos(@y)) -> c_22() 202.34/76.51 , #compare^#(#neg(@x), #0()) -> c_23() 202.34/76.51 , #compare^#(#neg(@x), #neg(@y)) -> c_24(#compare^#(@y, @x)) 202.34/76.51 , #compare^#(#s(@x), #0()) -> c_25() 202.34/76.51 , #compare^#(#s(@x), #s(@y)) -> c_26(#compare^#(@x, @y)) } 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) 202.34/76.51 , findMin^#(@l) -> c_7(findMin#1^#(@l)) } 202.34/76.51 Weak Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.51 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.51 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#0(), #0()) -> #EQ() 202.34/76.51 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.51 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.51 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.51 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.51 , #compare(#s(@x), #0()) -> #GT() 202.34/76.51 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.51 , findMin#2(::(@y, @ys), @x) -> 202.34/76.51 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.51 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.51 Obligation: 202.34/76.51 innermost runtime complexity 202.34/76.51 Answer: 202.34/76.51 YES(O(1),O(n^2)) 202.34/76.51 202.34/76.51 Due to missing edges in the dependency-graph, the right-hand sides 202.34/76.51 of following rules could be simplified: 202.34/76.51 202.34/76.51 { findMin#1^#(::(@x, @xs)) -> 202.34/76.51 c_5(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) } 202.34/76.51 202.34/76.51 We are left with following problem, upon which TcT provides the 202.34/76.51 certificate YES(O(1),O(n^2)). 202.34/76.51 202.34/76.51 Strict DPs: 202.34/76.51 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.51 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.51 , findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.51 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.51 Weak Trs: 202.34/76.51 { minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) 202.34/76.51 , minSort#1(nil()) -> nil() 202.34/76.51 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.51 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.51 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.51 , findMin#1(nil()) -> nil() 202.34/76.51 , #cklt(#LT()) -> #true() 202.34/76.51 , #cklt(#EQ()) -> #false() 202.34/76.51 , #cklt(#GT()) -> #false() 202.34/76.51 , findMin(@l) -> findMin#1(@l) 202.34/76.51 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.51 , minSort(@l) -> minSort#1(findMin(@l)) 202.34/76.51 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(n^2)) 202.34/76.52 202.34/76.52 We replace rewrite rules by usable rules: 202.34/76.52 202.34/76.52 Weak Usable Rules: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(n^2)). 202.34/76.52 202.34/76.52 Strict DPs: 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) 202.34/76.52 , findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(n^2)) 202.34/76.52 202.34/76.52 We decompose the input problem according to the dependency graph 202.34/76.52 into the upper component 202.34/76.52 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) } 202.34/76.52 202.34/76.52 and lower component 202.34/76.52 202.34/76.52 { findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.52 202.34/76.52 Further, following extension rules are added to the lower 202.34/76.52 component. 202.34/76.52 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) 202.34/76.52 , minSort^#(@l) -> minSort#1^#(findMin(@l)) 202.34/76.52 , minSort^#(@l) -> findMin^#(@l) } 202.34/76.52 202.34/76.52 TcT solves the upper component with certificate YES(O(1),O(n^1)). 202.34/76.52 202.34/76.52 Sub-proof: 202.34/76.52 ---------- 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(n^1)). 202.34/76.52 202.34/76.52 Strict DPs: 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) } 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(n^1)) 202.34/76.52 202.34/76.52 We use the processor 'matrix interpretation of dimension 1' to 202.34/76.52 orient following rules strictly. 202.34/76.52 202.34/76.52 DPs: 202.34/76.52 { 1: minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) } 202.34/76.52 202.34/76.52 Sub-proof: 202.34/76.52 ---------- 202.34/76.52 The following argument positions are usable: 202.34/76.52 Uargs(c_1) = {1}, Uargs(c_2) = {1} 202.34/76.52 202.34/76.52 TcT has computed the following constructor-based matrix 202.34/76.52 interpretation satisfying not(EDA). 202.34/76.52 202.34/76.52 [#true] = [0] 202.34/76.52 202.34/76.52 [#false] = [0] 202.34/76.52 202.34/76.52 [findMin#3](x1, x2, x3, x4) = [1] x4 + [2] 202.34/76.52 202.34/76.52 [::](x1, x2) = [1] x2 + [1] 202.34/76.52 202.34/76.52 [#LT] = [0] 202.34/76.52 202.34/76.52 [findMin#1](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#cklt](x1) = [0] 202.34/76.52 202.34/76.52 [#pos](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#0] = [0] 202.34/76.52 202.34/76.52 [findMin](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#neg](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#EQ] = [0] 202.34/76.52 202.34/76.52 [#less](x1, x2) = [0] 202.34/76.52 202.34/76.52 [#compare](x1, x2) = [0] 202.34/76.52 202.34/76.52 [#s](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#GT] = [0] 202.34/76.52 202.34/76.52 [nil] = [0] 202.34/76.52 202.34/76.52 [findMin#2](x1, x2) = [1] x1 + [1] 202.34/76.52 202.34/76.52 [minSort#1^#](x1) = [4] x1 + [0] 202.34/76.52 202.34/76.52 [minSort^#](x1) = [4] x1 + [0] 202.34/76.52 202.34/76.52 [findMin^#](x1) = [7] x1 + [7] 202.34/76.52 202.34/76.52 [c_1](x1) = [1] x1 + [1] 202.34/76.52 202.34/76.52 [c_2](x1, x2) = [1] x1 + [0] 202.34/76.52 202.34/76.52 The order satisfies the following ordering constraints: 202.34/76.52 202.34/76.52 [findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [2] 202.34/76.52 >= [1] @ys + [2] 202.34/76.52 = [::(@x, ::(@y, @ys))] 202.34/76.52 202.34/76.52 [findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [2] 202.34/76.52 >= [1] @ys + [2] 202.34/76.52 = [::(@y, ::(@x, @ys))] 202.34/76.52 202.34/76.52 [findMin#1(::(@x, @xs))] = [1] @xs + [1] 202.34/76.52 >= [1] @xs + [1] 202.34/76.52 = [findMin#2(findMin(@xs), @x)] 202.34/76.52 202.34/76.52 [findMin#1(nil())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [nil()] 202.34/76.52 202.34/76.52 [#cklt(#LT())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#true()] 202.34/76.52 202.34/76.52 [#cklt(#EQ())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#false()] 202.34/76.52 202.34/76.52 [#cklt(#GT())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#false()] 202.34/76.52 202.34/76.52 [findMin(@l)] = [1] @l + [0] 202.34/76.52 >= [1] @l + [0] 202.34/76.52 = [findMin#1(@l)] 202.34/76.52 202.34/76.52 [#less(@x, @y)] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#cklt(#compare(@x, @y))] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@x, @y)] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#EQ()] 202.34/76.52 202.34/76.52 [#compare(#0(), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #s(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@y, @x)] 202.34/76.52 202.34/76.52 [#compare(#s(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#s(@x), #s(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@x, @y)] 202.34/76.52 202.34/76.52 [findMin#2(::(@y, @ys), @x)] = [1] @ys + [2] 202.34/76.52 >= [1] @ys + [2] 202.34/76.52 = [findMin#3(#less(@x, @y), @x, @y, @ys)] 202.34/76.52 202.34/76.52 [findMin#2(nil(), @x)] = [1] 202.34/76.52 >= [1] 202.34/76.52 = [::(@x, nil())] 202.34/76.52 202.34/76.52 [minSort#1^#(::(@x, @xs))] = [4] @xs + [4] 202.34/76.52 > [4] @xs + [1] 202.34/76.52 = [c_1(minSort^#(@xs))] 202.34/76.52 202.34/76.52 [minSort^#(@l)] = [4] @l + [0] 202.34/76.52 >= [4] @l + [0] 202.34/76.52 = [c_2(minSort#1^#(findMin(@l)), findMin^#(@l))] 202.34/76.52 202.34/76.52 202.34/76.52 We return to the main proof. Consider the set of all dependency 202.34/76.52 pairs 202.34/76.52 202.34/76.52 : 202.34/76.52 { 1: minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , 2: minSort^#(@l) -> 202.34/76.52 c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) } 202.34/76.52 202.34/76.52 Processor 'matrix interpretation of dimension 1' induces the 202.34/76.52 complexity certificate YES(?,O(n^1)) on application of dependency 202.34/76.52 pairs {1}. These cover all (indirect) predecessors of dependency 202.34/76.52 pairs {1,2}, their number of application is equally bounded. The 202.34/76.52 dependency pairs are shifted into the weak component. 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Weak DPs: 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) } 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 The following weak DPs constitute a sub-graph of the DG that is 202.34/76.52 closed under successors. The DPs are removed. 202.34/76.52 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> c_1(minSort^#(@xs)) 202.34/76.52 , minSort^#(@l) -> c_2(minSort#1^#(findMin(@l)), findMin^#(@l)) } 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 No rule is usable, rules are removed from the input problem. 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Rules: Empty 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 Empty rules are trivially bounded 202.34/76.52 202.34/76.52 We return to the main proof. 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(n^1)). 202.34/76.52 202.34/76.52 Strict DPs: 202.34/76.52 { findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.52 Weak DPs: 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) 202.34/76.52 , minSort^#(@l) -> minSort#1^#(findMin(@l)) 202.34/76.52 , minSort^#(@l) -> findMin^#(@l) } 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(n^1)) 202.34/76.52 202.34/76.52 We use the processor 'matrix interpretation of dimension 1' to 202.34/76.52 orient following rules strictly. 202.34/76.52 202.34/76.52 DPs: 202.34/76.52 { 1: findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , 2: findMin^#(@l) -> c_4(findMin#1^#(@l)) 202.34/76.52 , 3: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) 202.34/76.52 , 4: minSort^#(@l) -> minSort#1^#(findMin(@l)) 202.34/76.52 , 5: minSort^#(@l) -> findMin^#(@l) } 202.34/76.52 202.34/76.52 Sub-proof: 202.34/76.52 ---------- 202.34/76.52 The following argument positions are usable: 202.34/76.52 Uargs(c_3) = {1}, Uargs(c_4) = {1} 202.34/76.52 202.34/76.52 TcT has computed the following constructor-based matrix 202.34/76.52 interpretation satisfying not(EDA). 202.34/76.52 202.34/76.52 [#true] = [2] 202.34/76.52 202.34/76.52 [#false] = [2] 202.34/76.52 202.34/76.52 [findMin#3](x1, x2, x3, x4) = [4] x1 + [1] x4 + [0] 202.34/76.52 202.34/76.52 [::](x1, x2) = [1] x2 + [4] 202.34/76.52 202.34/76.52 [#LT] = [0] 202.34/76.52 202.34/76.52 [findMin#1](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#cklt](x1) = [2] 202.34/76.52 202.34/76.52 [#pos](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#0] = [0] 202.34/76.52 202.34/76.52 [findMin](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#neg](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#EQ] = [0] 202.34/76.52 202.34/76.52 [#less](x1, x2) = [2] 202.34/76.52 202.34/76.52 [#compare](x1, x2) = [0] 202.34/76.52 202.34/76.52 [#s](x1) = [1] x1 + [0] 202.34/76.52 202.34/76.52 [#GT] = [0] 202.34/76.52 202.34/76.52 [nil] = [0] 202.34/76.52 202.34/76.52 [findMin#2](x1, x2) = [1] x1 + [4] 202.34/76.52 202.34/76.52 [minSort#1^#](x1) = [2] x1 + [0] 202.34/76.52 202.34/76.52 [minSort^#](x1) = [2] x1 + [5] 202.34/76.52 202.34/76.52 [findMin#1^#](x1) = [2] x1 + [0] 202.34/76.52 202.34/76.52 [findMin^#](x1) = [2] x1 + [4] 202.34/76.52 202.34/76.52 [c_3](x1) = [1] x1 + [1] 202.34/76.52 202.34/76.52 [c_4](x1) = [1] x1 + [3] 202.34/76.52 202.34/76.52 The order satisfies the following ordering constraints: 202.34/76.52 202.34/76.52 [findMin#3(#true(), @x, @y, @ys)] = [1] @ys + [8] 202.34/76.52 >= [1] @ys + [8] 202.34/76.52 = [::(@x, ::(@y, @ys))] 202.34/76.52 202.34/76.52 [findMin#3(#false(), @x, @y, @ys)] = [1] @ys + [8] 202.34/76.52 >= [1] @ys + [8] 202.34/76.52 = [::(@y, ::(@x, @ys))] 202.34/76.52 202.34/76.52 [findMin#1(::(@x, @xs))] = [1] @xs + [4] 202.34/76.52 >= [1] @xs + [4] 202.34/76.52 = [findMin#2(findMin(@xs), @x)] 202.34/76.52 202.34/76.52 [findMin#1(nil())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [nil()] 202.34/76.52 202.34/76.52 [#cklt(#LT())] = [2] 202.34/76.52 >= [2] 202.34/76.52 = [#true()] 202.34/76.52 202.34/76.52 [#cklt(#EQ())] = [2] 202.34/76.52 >= [2] 202.34/76.52 = [#false()] 202.34/76.52 202.34/76.52 [#cklt(#GT())] = [2] 202.34/76.52 >= [2] 202.34/76.52 = [#false()] 202.34/76.52 202.34/76.52 [findMin(@l)] = [1] @l + [0] 202.34/76.52 >= [1] @l + [0] 202.34/76.52 = [findMin#1(@l)] 202.34/76.52 202.34/76.52 [#less(@x, @y)] = [2] 202.34/76.52 >= [2] 202.34/76.52 = [#cklt(#compare(@x, @y))] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@x, @y)] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#pos(@x), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#EQ()] 202.34/76.52 202.34/76.52 [#compare(#0(), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#0(), #s(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #pos(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#LT()] 202.34/76.52 202.34/76.52 [#compare(#neg(@x), #neg(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@y, @x)] 202.34/76.52 202.34/76.52 [#compare(#s(@x), #0())] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#GT()] 202.34/76.52 202.34/76.52 [#compare(#s(@x), #s(@y))] = [0] 202.34/76.52 >= [0] 202.34/76.52 = [#compare(@x, @y)] 202.34/76.52 202.34/76.52 [findMin#2(::(@y, @ys), @x)] = [1] @ys + [8] 202.34/76.52 >= [1] @ys + [8] 202.34/76.52 = [findMin#3(#less(@x, @y), @x, @y, @ys)] 202.34/76.52 202.34/76.52 [findMin#2(nil(), @x)] = [4] 202.34/76.52 >= [4] 202.34/76.52 = [::(@x, nil())] 202.34/76.52 202.34/76.52 [minSort#1^#(::(@x, @xs))] = [2] @xs + [8] 202.34/76.52 > [2] @xs + [5] 202.34/76.52 = [minSort^#(@xs)] 202.34/76.52 202.34/76.52 [minSort^#(@l)] = [2] @l + [5] 202.34/76.52 > [2] @l + [0] 202.34/76.52 = [minSort#1^#(findMin(@l))] 202.34/76.52 202.34/76.52 [minSort^#(@l)] = [2] @l + [5] 202.34/76.52 > [2] @l + [4] 202.34/76.52 = [findMin^#(@l)] 202.34/76.52 202.34/76.52 [findMin#1^#(::(@x, @xs))] = [2] @xs + [8] 202.34/76.52 > [2] @xs + [5] 202.34/76.52 = [c_3(findMin^#(@xs))] 202.34/76.52 202.34/76.52 [findMin^#(@l)] = [2] @l + [4] 202.34/76.52 > [2] @l + [3] 202.34/76.52 = [c_4(findMin#1^#(@l))] 202.34/76.52 202.34/76.52 202.34/76.52 The strictly oriented rules are moved into the weak component. 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Weak DPs: 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) 202.34/76.52 , minSort^#(@l) -> minSort#1^#(findMin(@l)) 202.34/76.52 , minSort^#(@l) -> findMin^#(@l) 202.34/76.52 , findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 The following weak DPs constitute a sub-graph of the DG that is 202.34/76.52 closed under successors. The DPs are removed. 202.34/76.52 202.34/76.52 { minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) 202.34/76.52 , minSort^#(@l) -> minSort#1^#(findMin(@l)) 202.34/76.52 , minSort^#(@l) -> findMin^#(@l) 202.34/76.52 , findMin#1^#(::(@x, @xs)) -> c_3(findMin^#(@xs)) 202.34/76.52 , findMin^#(@l) -> c_4(findMin#1^#(@l)) } 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Weak Trs: 202.34/76.52 { findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) 202.34/76.52 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) 202.34/76.52 , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) 202.34/76.52 , findMin#1(nil()) -> nil() 202.34/76.52 , #cklt(#LT()) -> #true() 202.34/76.52 , #cklt(#EQ()) -> #false() 202.34/76.52 , #cklt(#GT()) -> #false() 202.34/76.52 , findMin(@l) -> findMin#1(@l) 202.34/76.52 , #less(@x, @y) -> #cklt(#compare(@x, @y)) 202.34/76.52 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) 202.34/76.52 , #compare(#pos(@x), #0()) -> #GT() 202.34/76.52 , #compare(#pos(@x), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#0(), #0()) -> #EQ() 202.34/76.52 , #compare(#0(), #neg(@y)) -> #GT() 202.34/76.52 , #compare(#0(), #s(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #pos(@y)) -> #LT() 202.34/76.52 , #compare(#neg(@x), #0()) -> #LT() 202.34/76.52 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) 202.34/76.52 , #compare(#s(@x), #0()) -> #GT() 202.34/76.52 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) 202.34/76.52 , findMin#2(::(@y, @ys), @x) -> 202.34/76.52 findMin#3(#less(@x, @y), @x, @y, @ys) 202.34/76.52 , findMin#2(nil(), @x) -> ::(@x, nil()) } 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 No rule is usable, rules are removed from the input problem. 202.34/76.52 202.34/76.52 We are left with following problem, upon which TcT provides the 202.34/76.52 certificate YES(O(1),O(1)). 202.34/76.52 202.34/76.52 Rules: Empty 202.34/76.52 Obligation: 202.34/76.52 innermost runtime complexity 202.34/76.52 Answer: 202.34/76.52 YES(O(1),O(1)) 202.34/76.52 202.34/76.52 Empty rules are trivially bounded 202.34/76.52 202.34/76.52 Hurray, we answered YES(O(1),O(n^2)) 202.34/76.53 EOF