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