WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #equal#(@x,@y) -> c_1(#eq#(@x,@y)) and#(@x,@y) -> c_2(#and#(@x,@y)) eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) eq#2#(::(@y,@ys)) -> c_6() eq#2#(nil()) -> c_7() eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) eq#3#(nil(),@x,@xs) -> c_9() nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) nub#1#(nil()) -> c_12() remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#1#(nil(),@x) -> c_15() remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) Weak DPs #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #eq#(#0(),#0()) -> c_22() #eq#(#0(),#neg(@y)) -> c_23() #eq#(#0(),#pos(@y)) -> c_24() #eq#(#0(),#s(@y)) -> c_25() #eq#(#neg(@x),#0()) -> c_26() #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_28() #eq#(#pos(@x),#0()) -> c_29() #eq#(#pos(@x),#neg(@y)) -> c_30() #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_32() #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_35() #eq#(nil(),::(@y_1,@y_2)) -> c_36() #eq#(nil(),nil()) -> c_37() and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) and#(@x,@y) -> c_2(#and#(@x,@y)) eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) eq#2#(::(@y,@ys)) -> c_6() eq#2#(nil()) -> c_7() eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) eq#3#(nil(),@x,@xs) -> c_9() nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) nub#1#(nil()) -> c_12() remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#1#(nil(),@x) -> c_15() remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #eq#(#0(),#0()) -> c_22() #eq#(#0(),#neg(@y)) -> c_23() #eq#(#0(),#pos(@y)) -> c_24() #eq#(#0(),#s(@y)) -> c_25() #eq#(#neg(@x),#0()) -> c_26() #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_28() #eq#(#pos(@x),#0()) -> c_29() #eq#(#pos(@x),#neg(@y)) -> c_30() #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_32() #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_35() #eq#(nil(),::(@y_1,@y_2)) -> c_36() #eq#(nil(),nil()) -> c_37() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,6,7,9,12,15} by application of Pre({1,2,6,7,9,12,15}) = {4,5,8,10,13}. Here rules are labelled as follows: 1: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 2: and#(@x,@y) -> c_2(#and#(@x,@y)) 3: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) 4: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) 5: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) 6: eq#2#(::(@y,@ys)) -> c_6() 7: eq#2#(nil()) -> c_7() 8: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) 9: eq#3#(nil(),@x,@xs) -> c_9() 10: nub#(@l) -> c_10(nub#1#(@l)) 11: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) 12: nub#1#(nil()) -> c_12() 13: remove#(@x,@l) -> c_13(remove#1#(@l,@x)) 14: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) 15: remove#1#(nil(),@x) -> c_15() 16: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) 17: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) 18: #and#(#false(),#false()) -> c_18() 19: #and#(#false(),#true()) -> c_19() 20: #and#(#true(),#false()) -> c_20() 21: #and#(#true(),#true()) -> c_21() 22: #eq#(#0(),#0()) -> c_22() 23: #eq#(#0(),#neg(@y)) -> c_23() 24: #eq#(#0(),#pos(@y)) -> c_24() 25: #eq#(#0(),#s(@y)) -> c_25() 26: #eq#(#neg(@x),#0()) -> c_26() 27: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) 28: #eq#(#neg(@x),#pos(@y)) -> c_28() 29: #eq#(#pos(@x),#0()) -> c_29() 30: #eq#(#pos(@x),#neg(@y)) -> c_30() 31: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) 32: #eq#(#s(@x),#0()) -> c_32() 33: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) 34: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 35: #eq#(::(@x_1,@x_2),nil()) -> c_35() 36: #eq#(nil(),::(@y_1,@y_2)) -> c_36() 37: #eq#(nil(),nil()) -> c_37() * Step 3: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #eq#(#0(),#0()) -> c_22() #eq#(#0(),#neg(@y)) -> c_23() #eq#(#0(),#pos(@y)) -> c_24() #eq#(#0(),#s(@y)) -> c_25() #eq#(#neg(@x),#0()) -> c_26() #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_28() #eq#(#pos(@x),#0()) -> c_29() #eq#(#pos(@x),#neg(@y)) -> c_30() #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_32() #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_35() #eq#(nil(),::(@y_1,@y_2)) -> c_36() #eq#(nil(),nil()) -> c_37() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) and#(@x,@y) -> c_2(#and#(@x,@y)) eq#2#(::(@y,@ys)) -> c_6() eq#2#(nil()) -> c_7() eq#3#(nil(),@x,@xs) -> c_9() nub#1#(nil()) -> c_12() remove#1#(nil(),@x) -> c_15() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3} by application of Pre({3}) = {1}. Here rules are labelled as follows: 1: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) 2: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) 3: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) 4: eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) 5: nub#(@l) -> c_10(nub#1#(@l)) 6: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) 7: remove#(@x,@l) -> c_13(remove#1#(@l,@x)) 8: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) 9: remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) 10: remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) 11: #and#(#false(),#false()) -> c_18() 12: #and#(#false(),#true()) -> c_19() 13: #and#(#true(),#false()) -> c_20() 14: #and#(#true(),#true()) -> c_21() 15: #eq#(#0(),#0()) -> c_22() 16: #eq#(#0(),#neg(@y)) -> c_23() 17: #eq#(#0(),#pos(@y)) -> c_24() 18: #eq#(#0(),#s(@y)) -> c_25() 19: #eq#(#neg(@x),#0()) -> c_26() 20: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) 21: #eq#(#neg(@x),#pos(@y)) -> c_28() 22: #eq#(#pos(@x),#0()) -> c_29() 23: #eq#(#pos(@x),#neg(@y)) -> c_30() 24: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) 25: #eq#(#s(@x),#0()) -> c_32() 26: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) 27: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 28: #eq#(::(@x_1,@x_2),nil()) -> c_35() 29: #eq#(nil(),::(@y_1,@y_2)) -> c_36() 30: #eq#(nil(),nil()) -> c_37() 31: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 32: and#(@x,@y) -> c_2(#and#(@x,@y)) 33: eq#2#(::(@y,@ys)) -> c_6() 34: eq#2#(nil()) -> c_7() 35: eq#3#(nil(),@x,@xs) -> c_9() 36: nub#1#(nil()) -> c_12() 37: remove#1#(nil(),@x) -> c_15() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: #and#(#false(),#false()) -> c_18() #and#(#false(),#true()) -> c_19() #and#(#true(),#false()) -> c_20() #and#(#true(),#true()) -> c_21() #eq#(#0(),#0()) -> c_22() #eq#(#0(),#neg(@y)) -> c_23() #eq#(#0(),#pos(@y)) -> c_24() #eq#(#0(),#s(@y)) -> c_25() #eq#(#neg(@x),#0()) -> c_26() #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) #eq#(#neg(@x),#pos(@y)) -> c_28() #eq#(#pos(@x),#0()) -> c_29() #eq#(#pos(@x),#neg(@y)) -> c_30() #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) #eq#(#s(@x),#0()) -> c_32() #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) #eq#(::(@x_1,@x_2),nil()) -> c_35() #eq#(nil(),::(@y_1,@y_2)) -> c_36() #eq#(nil(),nil()) -> c_37() #equal#(@x,@y) -> c_1(#eq#(@x,@y)) and#(@x,@y) -> c_2(#and#(@x,@y)) eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) eq#2#(::(@y,@ys)) -> c_6() eq#2#(nil()) -> c_7() eq#3#(nil(),@x,@xs) -> c_9() nub#1#(nil()) -> c_12() remove#1#(nil(),@x) -> c_15() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) -->_1 eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)):32 -->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2 2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) -->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3 -->_1 eq#3#(nil(),@x,@xs) -> c_9():35 3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) -->_1 and#(@x,@y) -> c_2(#and#(@x,@y)):31 -->_2 #equal#(@x,@y) -> c_1(#eq#(@x,@y)):30 -->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1 4:S:nub#(@l) -> c_10(nub#1#(@l)) -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5 -->_1 nub#1#(nil()) -> c_12():36 5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) -->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 -->_1 nub#(@l) -> c_10(nub#1#(@l)):4 6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x)) -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7 -->_1 remove#1#(nil(),@x) -> c_15():37 7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9 -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8 -->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1 8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 10:W:#and#(#false(),#false()) -> c_18() 11:W:#and#(#false(),#true()) -> c_19() 12:W:#and#(#true(),#false()) -> c_20() 13:W:#and#(#true(),#true()) -> c_21() 14:W:#eq#(#0(),#0()) -> c_22() 15:W:#eq#(#0(),#neg(@y)) -> c_23() 16:W:#eq#(#0(),#pos(@y)) -> c_24() 17:W:#eq#(#0(),#s(@y)) -> c_25() 18:W:#eq#(#neg(@x),#0()) -> c_26() 19:W:#eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_1 #eq#(nil(),nil()) -> c_37():29 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_1 #eq#(#s(@x),#0()) -> c_32():24 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_1 #eq#(#pos(@x),#0()) -> c_29():21 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_1 #eq#(#neg(@x),#0()) -> c_26():18 -->_1 #eq#(#0(),#s(@y)) -> c_25():17 -->_1 #eq#(#0(),#pos(@y)) -> c_24():16 -->_1 #eq#(#0(),#neg(@y)) -> c_23():15 -->_1 #eq#(#0(),#0()) -> c_22():14 20:W:#eq#(#neg(@x),#pos(@y)) -> c_28() 21:W:#eq#(#pos(@x),#0()) -> c_29() 22:W:#eq#(#pos(@x),#neg(@y)) -> c_30() 23:W:#eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_1 #eq#(nil(),nil()) -> c_37():29 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_1 #eq#(#s(@x),#0()) -> c_32():24 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_1 #eq#(#pos(@x),#0()) -> c_29():21 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_1 #eq#(#neg(@x),#0()) -> c_26():18 -->_1 #eq#(#0(),#s(@y)) -> c_25():17 -->_1 #eq#(#0(),#pos(@y)) -> c_24():16 -->_1 #eq#(#0(),#neg(@y)) -> c_23():15 -->_1 #eq#(#0(),#0()) -> c_22():14 24:W:#eq#(#s(@x),#0()) -> c_32() 25:W:#eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_1 #eq#(nil(),nil()) -> c_37():29 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_1 #eq#(#s(@x),#0()) -> c_32():24 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_1 #eq#(#pos(@x),#0()) -> c_29():21 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_1 #eq#(#neg(@x),#0()) -> c_26():18 -->_1 #eq#(#0(),#s(@y)) -> c_25():17 -->_1 #eq#(#0(),#pos(@y)) -> c_24():16 -->_1 #eq#(#0(),#neg(@y)) -> c_23():15 -->_1 #eq#(#0(),#0()) -> c_22():14 26:W:#eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) -->_3 #eq#(nil(),nil()) -> c_37():29 -->_2 #eq#(nil(),nil()) -> c_37():29 -->_3 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_2 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_3 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_2 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_3 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_2 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_3 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_2 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_3 #eq#(#s(@x),#0()) -> c_32():24 -->_2 #eq#(#s(@x),#0()) -> c_32():24 -->_3 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_2 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_3 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_2 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_3 #eq#(#pos(@x),#0()) -> c_29():21 -->_2 #eq#(#pos(@x),#0()) -> c_29():21 -->_3 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_2 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_3 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_2 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_3 #eq#(#neg(@x),#0()) -> c_26():18 -->_2 #eq#(#neg(@x),#0()) -> c_26():18 -->_3 #eq#(#0(),#s(@y)) -> c_25():17 -->_2 #eq#(#0(),#s(@y)) -> c_25():17 -->_3 #eq#(#0(),#pos(@y)) -> c_24():16 -->_2 #eq#(#0(),#pos(@y)) -> c_24():16 -->_3 #eq#(#0(),#neg(@y)) -> c_23():15 -->_2 #eq#(#0(),#neg(@y)) -> c_23():15 -->_3 #eq#(#0(),#0()) -> c_22():14 -->_2 #eq#(#0(),#0()) -> c_22():14 -->_1 #and#(#true(),#true()) -> c_21():13 -->_1 #and#(#true(),#false()) -> c_20():12 -->_1 #and#(#false(),#true()) -> c_19():11 -->_1 #and#(#false(),#false()) -> c_18():10 27:W:#eq#(::(@x_1,@x_2),nil()) -> c_35() 28:W:#eq#(nil(),::(@y_1,@y_2)) -> c_36() 29:W:#eq#(nil(),nil()) -> c_37() 30:W:#equal#(@x,@y) -> c_1(#eq#(@x,@y)) -->_1 #eq#(nil(),nil()) -> c_37():29 -->_1 #eq#(nil(),::(@y_1,@y_2)) -> c_36():28 -->_1 #eq#(::(@x_1,@x_2),nil()) -> c_35():27 -->_1 #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)):26 -->_1 #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)):25 -->_1 #eq#(#s(@x),#0()) -> c_32():24 -->_1 #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)):23 -->_1 #eq#(#pos(@x),#neg(@y)) -> c_30():22 -->_1 #eq#(#pos(@x),#0()) -> c_29():21 -->_1 #eq#(#neg(@x),#pos(@y)) -> c_28():20 -->_1 #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)):19 -->_1 #eq#(#neg(@x),#0()) -> c_26():18 -->_1 #eq#(#0(),#s(@y)) -> c_25():17 -->_1 #eq#(#0(),#pos(@y)) -> c_24():16 -->_1 #eq#(#0(),#neg(@y)) -> c_23():15 -->_1 #eq#(#0(),#0()) -> c_22():14 31:W:and#(@x,@y) -> c_2(#and#(@x,@y)) -->_1 #and#(#true(),#true()) -> c_21():13 -->_1 #and#(#true(),#false()) -> c_20():12 -->_1 #and#(#false(),#true()) -> c_19():11 -->_1 #and#(#false(),#false()) -> c_18():10 32:W:eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) -->_1 eq#2#(nil()) -> c_7():34 -->_1 eq#2#(::(@y,@ys)) -> c_6():33 33:W:eq#2#(::(@y,@ys)) -> c_6() 34:W:eq#2#(nil()) -> c_7() 35:W:eq#3#(nil(),@x,@xs) -> c_9() 36:W:nub#1#(nil()) -> c_12() 37:W:remove#1#(nil(),@x) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 36: nub#1#(nil()) -> c_12() 37: remove#1#(nil(),@x) -> c_15() 35: eq#3#(nil(),@x,@xs) -> c_9() 30: #equal#(@x,@y) -> c_1(#eq#(@x,@y)) 26: #eq#(::(@x_1,@x_2),::(@y_1,@y_2)) -> c_34(#and#(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) ,#eq#(@x_1,@y_1) ,#eq#(@x_2,@y_2)) 25: #eq#(#s(@x),#s(@y)) -> c_33(#eq#(@x,@y)) 23: #eq#(#pos(@x),#pos(@y)) -> c_31(#eq#(@x,@y)) 19: #eq#(#neg(@x),#neg(@y)) -> c_27(#eq#(@x,@y)) 14: #eq#(#0(),#0()) -> c_22() 15: #eq#(#0(),#neg(@y)) -> c_23() 16: #eq#(#0(),#pos(@y)) -> c_24() 17: #eq#(#0(),#s(@y)) -> c_25() 18: #eq#(#neg(@x),#0()) -> c_26() 20: #eq#(#neg(@x),#pos(@y)) -> c_28() 21: #eq#(#pos(@x),#0()) -> c_29() 22: #eq#(#pos(@x),#neg(@y)) -> c_30() 24: #eq#(#s(@x),#0()) -> c_32() 27: #eq#(::(@x_1,@x_2),nil()) -> c_35() 28: #eq#(nil(),::(@y_1,@y_2)) -> c_36() 29: #eq#(nil(),nil()) -> c_37() 31: and#(@x,@y) -> c_2(#and#(@x,@y)) 10: #and#(#false(),#false()) -> c_18() 11: #and#(#false(),#true()) -> c_19() 12: #and#(#true(),#false()) -> c_20() 13: #and#(#true(),#true()) -> c_21() 32: eq#1#(nil(),@l2) -> c_5(eq#2#(@l2)) 33: eq#2#(::(@y,@ys)) -> c_6() 34: eq#2#(nil()) -> c_7() * Step 5: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/3,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) -->_1 eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)):2 2:S:eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) -->_1 eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)):3 3:S:eq#3#(::(@y,@ys),@x,@xs) -> c_8(and#(#equal(@x,@y),eq(@xs,@ys)),#equal#(@x,@y),eq#(@xs,@ys)) -->_3 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1 4:S:nub#(@l) -> c_10(nub#1#(@l)) -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):5 5:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) -->_2 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 -->_1 nub#(@l) -> c_10(nub#1#(@l)):4 6:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x)) -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):7 7:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):9 -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):8 -->_2 eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)):1 8:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 9:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) * Step 6: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) * Step 7: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) and a lower component eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) Further, following extension rules are added to the lower component. nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:nub#(@l) -> c_10(nub#1#(@l)) -->_1 nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)):2 2:S:nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs)),remove#(@x,@xs)) -->_1 nub#(@l) -> c_10(nub#1#(@l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs))) ** Step 7.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs))) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_11) = {1} Following symbols are considered usable: {remove,remove#1,remove#2,#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1#,remove#,remove#1# ,remove#2#} TcT has computed the following interpretation: p(#0) = [2] p(#and) = [0] p(#eq) = [2] x1 + [1] x2 + [3] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [4] p(and) = [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [1] x4 + [4] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [0] p(eq#1#) = [0] p(eq#2#) = [0] p(eq#3#) = [0] p(nub#) = [2] x1 + [0] p(nub#1#) = [2] x1 + [0] p(remove#) = [0] p(remove#1#) = [0] p(remove#2#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [4] p(c_6) = [0] p(c_7) = [1] p(c_8) = [1] x1 + [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [6] p(c_12) = [1] p(c_13) = [1] x1 + [1] p(c_14) = [1] x1 + [2] x2 + [0] p(c_15) = [1] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [1] p(c_20) = [4] p(c_21) = [2] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [4] p(c_27) = [2] p(c_28) = [0] p(c_29) = [2] p(c_30) = [1] p(c_31) = [1] p(c_32) = [0] p(c_33) = [4] x1 + [4] p(c_34) = [4] x1 + [1] x2 + [1] x3 + [2] p(c_35) = [0] p(c_36) = [4] p(c_37) = [0] Following rules are strictly oriented: nub#1#(::(@x,@xs)) = [2] @xs + [8] > [2] @xs + [6] = c_11(nub#(remove(@x,@xs))) Following rules are (at-least) weakly oriented: nub#(@l) = [2] @l + [0] >= [2] @l + [0] = c_10(nub#1#(@l)) remove(@x,@l) = [1] @l + [0] >= [1] @l + [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [1] @ys + [4] >= [1] @ys + [4] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [4] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [0] = remove(@x,@ys) ** Step 7.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: nub#(@l) -> c_10(nub#1#(@l)) - Weak DPs: nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs))) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [2] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [1] x1 + [1] x4 + [2] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [1] x2 + [0] p(eq#1#) = [1] x1 + [2] p(eq#2#) = [1] p(eq#3#) = [2] x2 + [4] x3 + [0] p(nub#) = [1] x1 + [2] p(nub#1#) = [1] x1 + [0] p(remove#) = [1] x2 + [0] p(remove#1#) = [2] x1 + [0] p(remove#2#) = [2] x2 + [1] x3 + [0] p(c_1) = [4] x1 + [1] p(c_2) = [1] x1 + [1] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [4] x1 + [0] p(c_9) = [1] p(c_10) = [1] x1 + [1] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] p(c_14) = [2] p(c_15) = [4] p(c_16) = [2] x1 + [0] p(c_17) = [2] p(c_18) = [0] p(c_19) = [1] p(c_20) = [2] p(c_21) = [0] p(c_22) = [0] p(c_23) = [2] p(c_24) = [2] p(c_25) = [0] p(c_26) = [0] p(c_27) = [2] p(c_28) = [0] p(c_29) = [2] p(c_30) = [0] p(c_31) = [1] x1 + [1] p(c_32) = [1] p(c_33) = [2] x1 + [2] p(c_34) = [2] x3 + [0] p(c_35) = [1] p(c_36) = [0] p(c_37) = [1] Following rules are strictly oriented: nub#(@l) = [1] @l + [2] > [1] @l + [1] = c_10(nub#1#(@l)) Following rules are (at-least) weakly oriented: nub#1#(::(@x,@xs)) = [1] @xs + [2] >= [1] @xs + [2] = c_11(nub#(remove(@x,@xs))) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [1] @l + [0] >= [1] @l + [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [1] @ys + [2] >= [1] @ys + [2] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: nub#(@l) -> c_10(nub#1#(@l)) nub#1#(::(@x,@xs)) -> c_11(nub#(remove(@x,@xs))) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) and a lower component eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) Further, following extension rules are added to the lower component. nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) -> eq#(@x,@y) remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys) *** Step 7.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:remove#(@x,@l) -> c_13(remove#1#(@l,@x)) -->_1 remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)):2 2:S:remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys),eq#(@x,@y)) -->_1 remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)):4 -->_1 remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)):3 3:S:remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1 4:S:remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1 5:W:nub#(@l) -> nub#1#(@l) -->_1 nub#1#(::(@x,@xs)) -> remove#(@x,@xs):7 -->_1 nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)):6 6:W:nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) -->_1 nub#(@l) -> nub#1#(@l):5 7:W:nub#1#(::(@x,@xs)) -> remove#(@x,@xs) -->_1 remove#(@x,@l) -> c_13(remove#1#(@l,@x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) *** Step 7.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [0] p(eq#1#) = [1] p(eq#2#) = [0] p(eq#3#) = [0] p(nub#) = [1] x1 + [0] p(nub#1#) = [0] p(remove#) = [0] p(remove#1#) = [0] p(remove#2#) = [1] x1 + [3] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] Following rules are strictly oriented: remove#2#(#false(),@x,@y,@ys) = [3] > [0] = c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) = [3] > [0] = c_17(remove#(@x,@ys)) Following rules are (at-least) weakly oriented: nub#(@l) = [1] @l + [0] >= [0] = nub#1#(@l) nub#1#(::(@x,@xs)) = [0] >= [0] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [0] >= [0] = remove#(@x,@xs) remove#(@x,@l) = [0] >= [0] = c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) = [0] >= [3] = c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [0] p(eq#1#) = [0] p(eq#2#) = [0] p(eq#3#) = [0] p(nub#) = [1] x1 + [6] p(nub#1#) = [6] p(remove#) = [5] p(remove#1#) = [1] p(remove#2#) = [1] x1 + [7] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [3] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [4] p(c_28) = [1] p(c_29) = [1] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] p(c_33) = [0] p(c_34) = [4] x1 + [1] x2 + [1] p(c_35) = [2] p(c_36) = [0] p(c_37) = [0] Following rules are strictly oriented: remove#(@x,@l) = [5] > [1] = c_13(remove#1#(@l,@x)) Following rules are (at-least) weakly oriented: nub#(@l) = [1] @l + [6] >= [6] = nub#1#(@l) nub#1#(::(@x,@xs)) = [6] >= [6] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [6] >= [5] = remove#(@x,@xs) remove#1#(::(@y,@ys),@x) = [1] >= [10] = c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) remove#2#(#false(),@x,@y,@ys) = [7] >= [5] = c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) = [7] >= [5] = c_17(remove#(@x,@ys)) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.a:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [0] p(#true) = [0] p(::) = [1] x2 + [4] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [1] p(nub) = [4] x1 + [4] p(nub#1) = [2] x1 + [4] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [1] x1 + [1] x4 + [4] p(#and#) = [4] x1 + [1] x2 + [4] p(#eq#) = [4] x1 + [0] p(#equal#) = [4] x1 + [4] x2 + [2] p(and#) = [1] x1 + [1] p(eq#) = [2] x1 + [4] x2 + [0] p(eq#1#) = [1] p(eq#2#) = [2] x1 + [0] p(eq#3#) = [4] x2 + [1] x3 + [4] p(nub#) = [1] x1 + [1] p(nub#1#) = [1] x1 + [0] p(remove#) = [1] x2 + [1] p(remove#1#) = [1] x1 + [1] p(remove#2#) = [1] x1 + [1] x4 + [4] p(c_1) = [2] x1 + [1] p(c_2) = [2] x1 + [1] p(c_3) = [2] x1 + [0] p(c_4) = [2] x1 + [1] p(c_5) = [4] x1 + [1] p(c_6) = [0] p(c_7) = [2] p(c_8) = [2] x1 + [0] p(c_9) = [1] p(c_10) = [1] x1 + [2] p(c_11) = [1] x1 + [1] x2 + [1] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [3] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] p(c_23) = [0] p(c_24) = [2] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [1] p(c_28) = [1] p(c_29) = [0] p(c_30) = [1] p(c_31) = [4] p(c_32) = [1] p(c_33) = [2] x1 + [0] p(c_34) = [2] x2 + [2] x3 + [2] p(c_35) = [1] p(c_36) = [0] p(c_37) = [2] Following rules are strictly oriented: remove#1#(::(@y,@ys),@x) = [1] @ys + [5] > [1] @ys + [4] = c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) Following rules are (at-least) weakly oriented: nub#(@l) = [1] @l + [1] >= [1] @l + [0] = nub#1#(@l) nub#1#(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [1] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [1] = remove#(@x,@xs) remove#(@x,@l) = [1] @l + [1] >= [1] @l + [1] = c_13(remove#1#(@l,@x)) remove#2#(#false(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [1] = c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [4] = c_17(remove#(@x,@ys)) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [1] @l + [0] >= [1] @l + [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [1] @ys + [4] >= [1] @ys + [4] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [1] >= [1] = nil() remove#2(#false(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [4] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] @ys + [4] >= [1] @ys + [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> c_13(remove#1#(@l,@x)) remove#1#(::(@y,@ys),@x) -> c_14(remove#2#(eq(@x,@y),@x,@y,@ys)) remove#2#(#false(),@x,@y,@ys) -> c_16(remove#(@x,@ys)) remove#2#(#true(),@x,@y,@ys) -> c_17(remove#(@x,@ys)) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/1,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 7.b:1.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) - Weak DPs: nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) -> eq#(@x,@y) remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_8) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [0] p(eq#1#) = [4] p(eq#2#) = [0] p(eq#3#) = [0] p(nub#) = [1] x1 + [1] p(nub#1#) = [1] p(remove#) = [0] p(remove#1#) = [0] p(remove#2#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [1] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] Following rules are strictly oriented: eq#1#(::(@x,@xs),@l2) = [4] > [0] = c_4(eq#3#(@l2,@x,@xs)) Following rules are (at-least) weakly oriented: eq#(@l1,@l2) = [0] >= [4] = c_3(eq#1#(@l1,@l2)) eq#3#(::(@y,@ys),@x,@xs) = [0] >= [1] = c_8(eq#(@xs,@ys)) nub#(@l) = [1] @l + [1] >= [1] = nub#1#(@l) nub#1#(::(@x,@xs)) = [1] >= [1] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [1] >= [0] = remove#(@x,@xs) remove#(@x,@l) = [0] >= [0] = remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) = [0] >= [0] = eq#(@x,@y) remove#1#(::(@y,@ys),@x) = [0] >= [0] = remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) = [0] >= [0] = remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) = [0] >= [0] = remove#(@x,@ys) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) - Weak DPs: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) -> eq#(@x,@y) remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_8) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] p(#and#) = [0] p(#eq#) = [0] p(#equal#) = [0] p(and#) = [0] p(eq#) = [0] p(eq#1#) = [1] p(eq#2#) = [0] p(eq#3#) = [1] p(nub#) = [1] x1 + [0] p(nub#1#) = [0] p(remove#) = [0] p(remove#1#) = [0] p(remove#2#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [0] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] Following rules are strictly oriented: eq#3#(::(@y,@ys),@x,@xs) = [1] > [0] = c_8(eq#(@xs,@ys)) Following rules are (at-least) weakly oriented: eq#(@l1,@l2) = [0] >= [1] = c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) = [1] >= [1] = c_4(eq#3#(@l2,@x,@xs)) nub#(@l) = [1] @l + [0] >= [0] = nub#1#(@l) nub#1#(::(@x,@xs)) = [0] >= [0] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [0] >= [0] = remove#(@x,@xs) remove#(@x,@l) = [0] >= [0] = remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) = [0] >= [0] = eq#(@x,@y) remove#1#(::(@y,@ys),@x) = [0] >= [0] = remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) = [0] >= [0] = remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) = [0] >= [0] = remove#(@x,@ys) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.b:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) - Weak DPs: eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) -> eq#(@x,@y) remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(remove#2) = {1}, uargs(nub#) = {1}, uargs(remove#2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_8) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [1] p(#s) = [1] x1 + [4] p(#true) = [0] p(::) = [1] x1 + [1] x2 + [4] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [0] p(nub#1) = [4] x1 + [0] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [1] x1 + [1] x3 + [1] x4 + [4] p(#and#) = [1] x1 + [0] p(#eq#) = [4] x1 + [2] x2 + [0] p(#equal#) = [1] x2 + [4] p(and#) = [4] x1 + [1] p(eq#) = [1] x1 + [1] p(eq#1#) = [1] x1 + [0] p(eq#2#) = [1] x1 + [0] p(eq#3#) = [1] x2 + [1] x3 + [3] p(nub#) = [1] x1 + [5] p(nub#1#) = [1] x1 + [4] p(remove#) = [1] x1 + [2] p(remove#1#) = [1] x2 + [2] p(remove#2#) = [1] x1 + [1] x2 + [2] p(c_1) = [1] x1 + [1] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [1] p(c_5) = [1] x1 + [0] p(c_6) = [4] p(c_7) = [1] p(c_8) = [1] x1 + [2] p(c_9) = [2] p(c_10) = [4] p(c_11) = [4] x1 + [4] p(c_12) = [0] p(c_13) = [0] p(c_14) = [4] x2 + [4] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] p(c_18) = [1] p(c_19) = [2] p(c_20) = [0] p(c_21) = [0] p(c_22) = [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x1 + [0] p(c_28) = [0] p(c_29) = [1] p(c_30) = [1] p(c_31) = [0] p(c_32) = [1] p(c_33) = [2] p(c_34) = [1] x3 + [1] p(c_35) = [1] p(c_36) = [0] p(c_37) = [0] Following rules are strictly oriented: eq#(@l1,@l2) = [1] @l1 + [1] > [1] @l1 + [0] = c_3(eq#1#(@l1,@l2)) Following rules are (at-least) weakly oriented: eq#1#(::(@x,@xs),@l2) = [1] @x + [1] @xs + [4] >= [1] @x + [1] @xs + [4] = c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) = [1] @x + [1] @xs + [3] >= [1] @xs + [3] = c_8(eq#(@xs,@ys)) nub#(@l) = [1] @l + [5] >= [1] @l + [4] = nub#1#(@l) nub#1#(::(@x,@xs)) = [1] @x + [1] @xs + [8] >= [1] @xs + [5] = nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) = [1] @x + [1] @xs + [8] >= [1] @x + [2] = remove#(@x,@xs) remove#(@x,@l) = [1] @x + [2] >= [1] @x + [2] = remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) = [1] @x + [2] >= [1] @x + [1] = eq#(@x,@y) remove#1#(::(@y,@ys),@x) = [1] @x + [2] >= [1] @x + [2] = remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) = [1] @x + [2] >= [1] @x + [2] = remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) = [1] @x + [2] >= [1] @x + [2] = remove#(@x,@ys) #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() remove(@x,@l) = [1] @l + [0] >= [1] @l + [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [1] @y + [1] @ys + [4] >= [1] @y + [1] @ys + [4] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [1] @y + [1] @ys + [4] >= [1] @y + [1] @ys + [4] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [4] >= [1] @ys + [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(@l1,@l2) -> c_3(eq#1#(@l1,@l2)) eq#1#(::(@x,@xs),@l2) -> c_4(eq#3#(@l2,@x,@xs)) eq#3#(::(@y,@ys),@x,@xs) -> c_8(eq#(@xs,@ys)) nub#(@l) -> nub#1#(@l) nub#1#(::(@x,@xs)) -> nub#(remove(@x,@xs)) nub#1#(::(@x,@xs)) -> remove#(@x,@xs) remove#(@x,@l) -> remove#1#(@l,@x) remove#1#(::(@y,@ys),@x) -> eq#(@x,@y) remove#1#(::(@y,@ys),@x) -> remove#2#(eq(@x,@y),@x,@y,@ys) remove#2#(#false(),@x,@y,@ys) -> remove#(@x,@ys) remove#2#(#true(),@x,@y,@ys) -> remove#(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4,#and#/2 ,#eq#/2,#equal#/2,and#/2,eq#/2,eq#1#/2,eq#2#/1,eq#3#/3,nub#/1,nub#1#/1,remove#/2,remove#1#/2 ,remove#2#/4} / {#0/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/2,c_12/0,c_13/1,c_14/2,c_15/0,c_16/1,c_17/1,c_18/0,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/1,c_32/0,c_33/1,c_34/3,c_35/0,c_36/0 ,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and#,#eq#,#equal#,and#,eq#,eq#1#,eq#2#,eq#3#,nub#,nub#1# ,remove#,remove#1#,remove#2#} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))