WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(y,ys),x,xs) -> and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) -> #false() nub(l) -> nub#1(l) nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() remove(x,l) -> remove#1(l,x) remove#1(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/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,dd,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#0()) -> c_15() #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() #equal#(x,y) -> c_21(#eq#(x,y)) and#(x,y) -> c_22(#and#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) eq#3#(nil(),x,xs) -> c_29() nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) nub#1#(nil()) -> c_32() remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#1#(nil(),x) -> c_35() remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#0()) -> c_15() #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() #equal#(x,y) -> c_21(#eq#(x,y)) and#(x,y) -> c_22(#and#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) eq#3#(nil(),x,xs) -> c_29() nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) nub#1#(nil()) -> c_32() remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#1#(nil(),x) -> c_35() remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(y,ys),x,xs) -> and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) -> #false() nub(l) -> nub#1(l) nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() remove(x,l) -> remove#1(l,x) remove#1(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/3,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) -> remove(x,ys) #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#0()) -> c_15() #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() #equal#(x,y) -> c_21(#eq#(x,y)) and#(x,y) -> c_22(#and#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) eq#3#(nil(),x,xs) -> c_29() nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) nub#1#(nil()) -> c_32() remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#1#(nil(),x) -> c_35() remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#0()) -> c_15() #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() #equal#(x,y) -> c_21(#eq#(x,y)) and#(x,y) -> c_22(#and#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) eq#3#(nil(),x,xs) -> c_29() nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) nub#1#(nil()) -> c_32() remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#1#(nil(),x) -> c_35() remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/3,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,9,11,12,13,15,18,19,20,26,27,29,32,35} by application of Pre({1,2,3,4,5,6,7,8,9,11,12,13,15,18,19,20,26,27,29,32,35}) = {10,14,16,17,21,22,24,25,30,33}. Here rules are labelled as follows: 1: #and#(#false(),#false()) -> c_1() 2: #and#(#false(),#true()) -> c_2() 3: #and#(#true(),#false()) -> c_3() 4: #and#(#true(),#true()) -> c_4() 5: #eq#(#0(),#0()) -> c_5() 6: #eq#(#0(),#neg(y)) -> c_6() 7: #eq#(#0(),#pos(y)) -> c_7() 8: #eq#(#0(),#s(y)) -> c_8() 9: #eq#(#neg(x),#0()) -> c_9() 10: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) 11: #eq#(#neg(x),#pos(y)) -> c_11() 12: #eq#(#pos(x),#0()) -> c_12() 13: #eq#(#pos(x),#neg(y)) -> c_13() 14: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) 15: #eq#(#s(x),#0()) -> c_15() 16: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) 17: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) 18: #eq#(dd(x'1,x'2),nil()) -> c_18() 19: #eq#(nil(),dd(y'1,y'2)) -> c_19() 20: #eq#(nil(),nil()) -> c_20() 21: #equal#(x,y) -> c_21(#eq#(x,y)) 22: and#(x,y) -> c_22(#and#(x,y)) 23: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 24: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) 25: eq#1#(nil(),l2) -> c_25(eq#2#(l2)) 26: eq#2#(dd(y,ys)) -> c_26() 27: eq#2#(nil()) -> c_27() 28: eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) 29: eq#3#(nil(),x,xs) -> c_29() 30: nub#(l) -> c_30(nub#1#(l)) 31: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 32: nub#1#(nil()) -> c_32() 33: remove#(x,l) -> c_33(remove#1#(l,x)) 34: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 35: remove#1#(nil(),x) -> c_35() 36: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 37: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) * Step 4: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) and#(x,y) -> c_22(#and#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#s(x),#0()) -> c_15() #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(nil(),x,xs) -> c_29() nub#1#(nil()) -> c_32() remove#1#(nil(),x) -> c_35() - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/3,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,9} by application of Pre({6,9}) = {7,10}. Here rules are labelled as follows: 1: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) 2: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) 3: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) 4: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) 5: #equal#(x,y) -> c_21(#eq#(x,y)) 6: and#(x,y) -> c_22(#and#(x,y)) 7: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 8: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) 9: eq#1#(nil(),l2) -> c_25(eq#2#(l2)) 10: eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) 11: nub#(l) -> c_30(nub#1#(l)) 12: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 13: remove#(x,l) -> c_33(remove#1#(l,x)) 14: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 15: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 16: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) 17: #and#(#false(),#false()) -> c_1() 18: #and#(#false(),#true()) -> c_2() 19: #and#(#true(),#false()) -> c_3() 20: #and#(#true(),#true()) -> c_4() 21: #eq#(#0(),#0()) -> c_5() 22: #eq#(#0(),#neg(y)) -> c_6() 23: #eq#(#0(),#pos(y)) -> c_7() 24: #eq#(#0(),#s(y)) -> c_8() 25: #eq#(#neg(x),#0()) -> c_9() 26: #eq#(#neg(x),#pos(y)) -> c_11() 27: #eq#(#pos(x),#0()) -> c_12() 28: #eq#(#pos(x),#neg(y)) -> c_13() 29: #eq#(#s(x),#0()) -> c_15() 30: #eq#(dd(x'1,x'2),nil()) -> c_18() 31: #eq#(nil(),dd(y'1,y'2)) -> c_19() 32: #eq#(nil(),nil()) -> c_20() 33: eq#2#(dd(y,ys)) -> c_26() 34: eq#2#(nil()) -> c_27() 35: eq#3#(nil(),x,xs) -> c_29() 36: nub#1#(nil()) -> c_32() 37: remove#1#(nil(),x) -> c_35() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: #and#(#false(),#false()) -> c_1() #and#(#false(),#true()) -> c_2() #and#(#true(),#false()) -> c_3() #and#(#true(),#true()) -> c_4() #eq#(#0(),#0()) -> c_5() #eq#(#0(),#neg(y)) -> c_6() #eq#(#0(),#pos(y)) -> c_7() #eq#(#0(),#s(y)) -> c_8() #eq#(#neg(x),#0()) -> c_9() #eq#(#neg(x),#pos(y)) -> c_11() #eq#(#pos(x),#0()) -> c_12() #eq#(#pos(x),#neg(y)) -> c_13() #eq#(#s(x),#0()) -> c_15() #eq#(dd(x'1,x'2),nil()) -> c_18() #eq#(nil(),dd(y'1,y'2)) -> c_19() #eq#(nil(),nil()) -> c_20() and#(x,y) -> c_22(#and#(x,y)) eq#1#(nil(),l2) -> c_25(eq#2#(l2)) eq#2#(dd(y,ys)) -> c_26() eq#2#(nil()) -> c_27() eq#3#(nil(),x,xs) -> c_29() nub#1#(nil()) -> c_32() remove#1#(nil(),x) -> c_35() - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/3,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(nil(),nil()) -> c_20():30 -->_1 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_1 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_1 #eq#(#s(x),#0()) -> c_15():27 -->_1 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_1 #eq#(#pos(x),#0()) -> c_12():25 -->_1 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_1 #eq#(#neg(x),#0()) -> c_9():23 -->_1 #eq#(#0(),#s(y)) -> c_8():22 -->_1 #eq#(#0(),#pos(y)) -> c_7():21 -->_1 #eq#(#0(),#neg(y)) -> c_6():20 -->_1 #eq#(#0(),#0()) -> c_5():19 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 2:S:#eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(nil(),nil()) -> c_20():30 -->_1 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_1 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_1 #eq#(#s(x),#0()) -> c_15():27 -->_1 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_1 #eq#(#pos(x),#0()) -> c_12():25 -->_1 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_1 #eq#(#neg(x),#0()) -> c_9():23 -->_1 #eq#(#0(),#s(y)) -> c_8():22 -->_1 #eq#(#0(),#pos(y)) -> c_7():21 -->_1 #eq#(#0(),#neg(y)) -> c_6():20 -->_1 #eq#(#0(),#0()) -> c_5():19 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 3:S:#eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(nil(),nil()) -> c_20():30 -->_1 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_1 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_1 #eq#(#s(x),#0()) -> c_15():27 -->_1 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_1 #eq#(#pos(x),#0()) -> c_12():25 -->_1 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_1 #eq#(#neg(x),#0()) -> c_9():23 -->_1 #eq#(#0(),#s(y)) -> c_8():22 -->_1 #eq#(#0(),#pos(y)) -> c_7():21 -->_1 #eq#(#0(),#neg(y)) -> c_6():20 -->_1 #eq#(#0(),#0()) -> c_5():19 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 4:S:#eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#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_20():30 -->_2 #eq#(nil(),nil()) -> c_20():30 -->_3 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_2 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_3 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_2 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_3 #eq#(#s(x),#0()) -> c_15():27 -->_2 #eq#(#s(x),#0()) -> c_15():27 -->_3 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_2 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_3 #eq#(#pos(x),#0()) -> c_12():25 -->_2 #eq#(#pos(x),#0()) -> c_12():25 -->_3 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_2 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_3 #eq#(#neg(x),#0()) -> c_9():23 -->_2 #eq#(#neg(x),#0()) -> c_9():23 -->_3 #eq#(#0(),#s(y)) -> c_8():22 -->_2 #eq#(#0(),#s(y)) -> c_8():22 -->_3 #eq#(#0(),#pos(y)) -> c_7():21 -->_2 #eq#(#0(),#pos(y)) -> c_7():21 -->_3 #eq#(#0(),#neg(y)) -> c_6():20 -->_2 #eq#(#0(),#neg(y)) -> c_6():20 -->_3 #eq#(#0(),#0()) -> c_5():19 -->_2 #eq#(#0(),#0()) -> c_5():19 -->_1 #and#(#true(),#true()) -> c_4():18 -->_1 #and#(#true(),#false()) -> c_3():17 -->_1 #and#(#false(),#true()) -> c_2():16 -->_1 #and#(#false(),#false()) -> c_1():15 -->_3 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_2 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_3 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_2 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_3 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_2 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_3 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 -->_2 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 5:S:#equal#(x,y) -> c_21(#eq#(x,y)) -->_1 #eq#(nil(),nil()) -> c_20():30 -->_1 #eq#(nil(),dd(y'1,y'2)) -> c_19():29 -->_1 #eq#(dd(x'1,x'2),nil()) -> c_18():28 -->_1 #eq#(#s(x),#0()) -> c_15():27 -->_1 #eq#(#pos(x),#neg(y)) -> c_13():26 -->_1 #eq#(#pos(x),#0()) -> c_12():25 -->_1 #eq#(#neg(x),#pos(y)) -> c_11():24 -->_1 #eq#(#neg(x),#0()) -> c_9():23 -->_1 #eq#(#0(),#s(y)) -> c_8():22 -->_1 #eq#(#0(),#pos(y)) -> c_7():21 -->_1 #eq#(#0(),#neg(y)) -> c_6():20 -->_1 #eq#(#0(),#0()) -> c_5():19 -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 6:S:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(nil(),l2) -> c_25(eq#2#(l2)):32 -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):7 7:S:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)):8 -->_1 eq#3#(nil(),x,xs) -> c_29():35 8:S:eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) -->_1 and#(x,y) -> c_22(#and#(x,y)):31 -->_3 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 -->_2 #equal#(x,y) -> c_21(#eq#(x,y)):5 9:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):10 -->_1 nub#1#(nil()) -> c_32():36 10:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):11 -->_1 nub#(l) -> c_30(nub#1#(l)):9 11:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):12 -->_1 remove#1#(nil(),x) -> c_35():37 12:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):14 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):13 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 13:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 14:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 15:W:#and#(#false(),#false()) -> c_1() 16:W:#and#(#false(),#true()) -> c_2() 17:W:#and#(#true(),#false()) -> c_3() 18:W:#and#(#true(),#true()) -> c_4() 19:W:#eq#(#0(),#0()) -> c_5() 20:W:#eq#(#0(),#neg(y)) -> c_6() 21:W:#eq#(#0(),#pos(y)) -> c_7() 22:W:#eq#(#0(),#s(y)) -> c_8() 23:W:#eq#(#neg(x),#0()) -> c_9() 24:W:#eq#(#neg(x),#pos(y)) -> c_11() 25:W:#eq#(#pos(x),#0()) -> c_12() 26:W:#eq#(#pos(x),#neg(y)) -> c_13() 27:W:#eq#(#s(x),#0()) -> c_15() 28:W:#eq#(dd(x'1,x'2),nil()) -> c_18() 29:W:#eq#(nil(),dd(y'1,y'2)) -> c_19() 30:W:#eq#(nil(),nil()) -> c_20() 31:W:and#(x,y) -> c_22(#and#(x,y)) -->_1 #and#(#true(),#true()) -> c_4():18 -->_1 #and#(#true(),#false()) -> c_3():17 -->_1 #and#(#false(),#true()) -> c_2():16 -->_1 #and#(#false(),#false()) -> c_1():15 32:W:eq#1#(nil(),l2) -> c_25(eq#2#(l2)) -->_1 eq#2#(nil()) -> c_27():34 -->_1 eq#2#(dd(y,ys)) -> c_26():33 33:W:eq#2#(dd(y,ys)) -> c_26() 34:W:eq#2#(nil()) -> c_27() 35:W:eq#3#(nil(),x,xs) -> c_29() 36:W:nub#1#(nil()) -> c_32() 37:W:remove#1#(nil(),x) -> c_35() 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_32() 37: remove#1#(nil(),x) -> c_35() 35: eq#3#(nil(),x,xs) -> c_29() 31: and#(x,y) -> c_22(#and#(x,y)) 32: eq#1#(nil(),l2) -> c_25(eq#2#(l2)) 33: eq#2#(dd(y,ys)) -> c_26() 34: eq#2#(nil()) -> c_27() 15: #and#(#false(),#false()) -> c_1() 16: #and#(#false(),#true()) -> c_2() 17: #and#(#true(),#false()) -> c_3() 18: #and#(#true(),#true()) -> c_4() 19: #eq#(#0(),#0()) -> c_5() 20: #eq#(#0(),#neg(y)) -> c_6() 21: #eq#(#0(),#pos(y)) -> c_7() 22: #eq#(#0(),#s(y)) -> c_8() 23: #eq#(#neg(x),#0()) -> c_9() 24: #eq#(#neg(x),#pos(y)) -> c_11() 25: #eq#(#pos(x),#0()) -> c_12() 26: #eq#(#pos(x),#neg(y)) -> c_13() 27: #eq#(#s(x),#0()) -> c_15() 28: #eq#(dd(x'1,x'2),nil()) -> c_18() 29: #eq#(nil(),dd(y'1,y'2)) -> c_19() 30: #eq#(nil(),nil()) -> c_20() * Step 6: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/3,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 2:S:#eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 3:S:#eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 4:S:#eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)) -->_3 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_2 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)),#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_3 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_2 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_3 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_2 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_3 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 -->_2 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 5:S:#equal#(x,y) -> c_21(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#and#(#eq(x'1,y'1),#eq(x'2,y'2)) ,#eq#(x'1,y'1) ,#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 6:S:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):7 7:S:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)):8 8:S:eq#3#(dd(y,ys),x,xs) -> c_28(and#(#equal(x,y),eq(xs,ys)),#equal#(x,y),eq#(xs,ys)) -->_3 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 -->_2 #equal#(x,y) -> c_21(#eq#(x,y)):5 9:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):10 10:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):11 -->_1 nub#(l) -> c_30(nub#1#(l)):9 11:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):12 12:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):14 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):13 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 13:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 14:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) * Step 7: Decompose WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} Problem (S) - Strict DPs: #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} ** Step 7.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) The strictly oriented rules are moved into the weak component. *** Step 7.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1,2}, uargs(c_21) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1,2}, uargs(c_36) = {1}, uargs(c_37) = {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) = 0 p(#and) = x1 + x1*x2 p(#eq) = 1 p(#equal) = x1 + x1*x2 + x2 p(#false) = 0 p(#neg) = x1 p(#pos) = x1 p(#s) = 1 + x1 p(#true) = 0 p(and) = x2^2 p(dd) = x1 + x2 p(eq) = 1 + x2^2 p(eq#1) = x1*x2 p(eq#2) = x1^2 p(eq#3) = x1^2 + x2 p(nil) = 1 p(nub) = 0 p(nub#1) = 0 p(remove) = x2 p(remove#1) = x1 p(remove#2) = x3 + x4 p(#and#) = 0 p(#eq#) = x1*x2 p(#equal#) = x1*x2 p(and#) = 0 p(eq#) = x1*x2 p(eq#1#) = x1*x2 p(eq#2#) = 0 p(eq#3#) = x1*x2 + x1*x3 p(nub#) = x1^2 p(nub#1#) = x1^2 p(remove#) = x1*x2 + x1^2 p(remove#1#) = x1*x2 + x2^2 p(remove#2#) = x2*x4 + x2^2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 0 p(c_5) = 0 p(c_6) = 0 p(c_7) = 0 p(c_8) = 0 p(c_9) = 0 p(c_10) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = x1 p(c_15) = 0 p(c_16) = x1 p(c_17) = x1 + x2 p(c_18) = 0 p(c_19) = 0 p(c_20) = 0 p(c_21) = x1 p(c_22) = 0 p(c_23) = x1 p(c_24) = x1 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = x1 + x2 p(c_29) = 0 p(c_30) = x1 p(c_31) = x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 + x2 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: #eq#(#s(x),#s(y)) = 1 + x + x*y + y > x*y = c_16(#eq#(x,y)) Following rules are (at-least) weakly oriented: #eq#(#neg(x),#neg(y)) = x*y >= x*y = c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) = x*y >= x*y = c_14(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) = x'1*y'1 + x'1*y'2 + x'2*y'1 + x'2*y'2 >= x'1*y'1 + x'2*y'2 = c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) = x*y >= x*y = c_21(#eq#(x,y)) eq#(l1,l2) = l1*l2 >= l1*l2 = c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) = l2*x + l2*xs >= l2*x + l2*xs = c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) = x*y + x*ys + xs*y + xs*ys >= x*y + xs*ys = c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) = l^2 >= l^2 = c_30(nub#1#(l)) nub#1#(dd(x,xs)) = 2*x*xs + x^2 + xs^2 >= x*xs + x^2 + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) = l*x + x^2 >= l*x + x^2 = c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) = x*y + x*ys + x^2 >= x*y + x*ys + x^2 = c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) = x*ys + x^2 >= x*ys + x^2 = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = x*ys + x^2 >= x*ys + x^2 = c_37(remove#(x,ys)) remove(x,l) = l >= l = remove#1(l,x) remove#1(dd(y,ys),x) = y + ys >= y + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = 1 >= 1 = nil() remove#2(#false(),x,y,ys) = y + ys >= y + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = y + ys >= ys = remove(x,ys) *** Step 7.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.a:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) The strictly oriented rules are moved into the weak component. **** Step 7.a:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1,2}, uargs(c_21) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1,2}, uargs(c_36) = {1}, uargs(c_37) = {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) = 1 p(#and) = 0 p(#eq) = x2^2 p(#equal) = x1 + x2 p(#false) = 0 p(#neg) = x1 p(#pos) = x1 p(#s) = 1 + x1 p(#true) = 0 p(and) = x1 p(dd) = 1 + x1 + x2 p(eq) = 0 p(eq#1) = x1 p(eq#2) = x1 p(eq#3) = x1 + x3 p(nil) = 1 p(nub) = 0 p(nub#1) = 0 p(remove) = x1 + x2 p(remove#1) = x1 + x2 p(remove#2) = 1 + x2 + x3 + x4 p(#and#) = 0 p(#eq#) = x2 p(#equal#) = x2 p(and#) = 0 p(eq#) = x2 p(eq#1#) = x2 p(eq#2#) = 0 p(eq#3#) = x1 p(nub#) = x1^2 p(nub#1#) = x1^2 p(remove#) = x2 p(remove#1#) = x1 p(remove#2#) = x4 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) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = x1 p(c_15) = 0 p(c_16) = x1 p(c_17) = x1 + x2 p(c_18) = 0 p(c_19) = 0 p(c_20) = 0 p(c_21) = x1 p(c_22) = 0 p(c_23) = x1 p(c_24) = x1 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = 1 + x1 + x2 p(c_29) = 0 p(c_30) = x1 p(c_31) = 1 + x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 + x2 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: #eq#(dd(x'1,x'2),dd(y'1,y'2)) = 1 + y'1 + y'2 > y'1 + y'2 = c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) Following rules are (at-least) weakly oriented: #eq#(#neg(x),#neg(y)) = y >= y = c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) = y >= y = c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) = 1 + y >= y = c_16(#eq#(x,y)) #equal#(x,y) = y >= y = c_21(#eq#(x,y)) eq#(l1,l2) = l2 >= l2 = c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) = l2 >= l2 = c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) = 1 + y + ys >= 1 + y + ys = c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) = l^2 >= l^2 = c_30(nub#1#(l)) nub#1#(dd(x,xs)) = 1 + 2*x + 2*x*xs + x^2 + 2*xs + xs^2 >= 1 + 2*x*xs + x^2 + xs + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) = l >= l = c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) = 1 + y + ys >= y + ys = c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) = ys >= ys = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = ys >= ys = c_37(remove#(x,ys)) remove(x,l) = l + x >= l + x = remove#1(l,x) remove#1(dd(y,ys),x) = 1 + x + y + ys >= 1 + x + y + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = 1 + x >= 1 = nil() remove#2(#false(),x,y,ys) = 1 + x + y + ys >= 1 + x + y + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = 1 + x + y + ys >= x + ys = remove(x,ys) **** Step 7.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 7.a:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) The strictly oriented rules are moved into the weak component. ***** Step 7.a:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) - Weak DPs: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1,2}, uargs(c_21) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1,2}, uargs(c_36) = {1}, uargs(c_37) = {1} Following symbols are considered usable: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,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) = 0 p(#and) = x1*x2 p(#eq) = 1 p(#equal) = 1 p(#false) = 1 p(#neg) = 1 + x1 p(#pos) = 1 + x1 p(#s) = x1 p(#true) = 1 p(and) = x1*x2 p(dd) = 1 + x1 + x2 p(eq) = 1 p(eq#1) = 1 p(eq#2) = 1 p(eq#3) = 1 p(nil) = 0 p(nub) = 0 p(nub#1) = 0 p(remove) = 1 + x2 p(remove#1) = 1 + x1 p(remove#2) = 1 + x1*x4 + x1^2 + x3 p(#and#) = 0 p(#eq#) = x2 p(#equal#) = x2 p(and#) = 0 p(eq#) = x1 + x1*x2 p(eq#1#) = x1*x2 p(eq#2#) = 0 p(eq#3#) = x1 + x1*x3 p(nub#) = 1 + x1^2 p(nub#1#) = 1 + x1^2 p(remove#) = x1*x2 p(remove#1#) = x1*x2 p(remove#2#) = x2*x4 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) = 1 + x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = x1 p(c_15) = 0 p(c_16) = x1 p(c_17) = x1 + x2 p(c_18) = 0 p(c_19) = 0 p(c_20) = 0 p(c_21) = x1 p(c_22) = 0 p(c_23) = x1 p(c_24) = x1 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = x1 + x2 p(c_29) = 0 p(c_30) = x1 p(c_31) = x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 + x2 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: #eq#(#pos(x),#pos(y)) = 1 + y > y = c_14(#eq#(x,y)) Following rules are (at-least) weakly oriented: #eq#(#neg(x),#neg(y)) = 1 + y >= 1 + y = c_10(#eq#(x,y)) #eq#(#s(x),#s(y)) = y >= y = c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) = 1 + y'1 + y'2 >= y'1 + y'2 = c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) = y >= y = c_21(#eq#(x,y)) eq#(l1,l2) = l1 + l1*l2 >= l1*l2 = c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) = l2 + l2*x + l2*xs >= l2 + l2*xs = c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) = 1 + xs + xs*y + xs*ys + y + ys >= xs + xs*ys + y = c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) = 1 + l^2 >= 1 + l^2 = c_30(nub#1#(l)) nub#1#(dd(x,xs)) = 2 + 2*x + 2*x*xs + x^2 + 2*xs + xs^2 >= 2 + x*xs + 2*xs + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) = l*x >= l*x = c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) = x + x*y + x*ys >= x + x*y + x*ys = c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) = x*ys >= x*ys = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = x*ys >= x*ys = c_37(remove#(x,ys)) #and(#false(),#false()) = 1 >= 1 = #false() #and(#false(),#true()) = 1 >= 1 = #false() #and(#true(),#false()) = 1 >= 1 = #false() #and(#true(),#true()) = 1 >= 1 = #true() #eq(#0(),#0()) = 1 >= 1 = #true() #eq(#0(),#neg(y)) = 1 >= 1 = #false() #eq(#0(),#pos(y)) = 1 >= 1 = #false() #eq(#0(),#s(y)) = 1 >= 1 = #false() #eq(#neg(x),#0()) = 1 >= 1 = #false() #eq(#neg(x),#neg(y)) = 1 >= 1 = #eq(x,y) #eq(#neg(x),#pos(y)) = 1 >= 1 = #false() #eq(#pos(x),#0()) = 1 >= 1 = #false() #eq(#pos(x),#neg(y)) = 1 >= 1 = #false() #eq(#pos(x),#pos(y)) = 1 >= 1 = #eq(x,y) #eq(#s(x),#0()) = 1 >= 1 = #false() #eq(#s(x),#s(y)) = 1 >= 1 = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = 1 >= 1 = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = 1 >= 1 = #false() #eq(nil(),dd(y'1,y'2)) = 1 >= 1 = #false() #eq(nil(),nil()) = 1 >= 1 = #true() #equal(x,y) = 1 >= 1 = #eq(x,y) and(x,y) = x*y >= x*y = #and(x,y) eq(l1,l2) = 1 >= 1 = eq#1(l1,l2) eq#1(dd(x,xs),l2) = 1 >= 1 = eq#3(l2,x,xs) eq#1(nil(),l2) = 1 >= 1 = eq#2(l2) eq#2(dd(y,ys)) = 1 >= 1 = #false() eq#2(nil()) = 1 >= 1 = #true() eq#3(dd(y,ys),x,xs) = 1 >= 1 = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = 1 >= 1 = #false() remove(x,l) = 1 + l >= 1 + l = remove#1(l,x) remove#1(dd(y,ys),x) = 2 + y + ys >= 2 + y + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = 1 >= 0 = nil() remove#2(#false(),x,y,ys) = 2 + y + ys >= 2 + y + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = 2 + y + ys >= 1 + ys = remove(x,ys) ***** Step 7.a:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) - Weak DPs: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 7.a:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) - Weak DPs: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) The strictly oriented rules are moved into the weak component. ****** Step 7.a:1.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) - Weak DPs: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_14) = {1}, uargs(c_16) = {1}, uargs(c_17) = {1,2}, uargs(c_21) = {1}, uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_28) = {1,2}, uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1,2}, uargs(c_36) = {1}, uargs(c_37) = {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) = 1 p(#and) = x1*x2 + x2 p(#eq) = 1 + x2 p(#equal) = x2 p(#false) = 0 p(#neg) = 1 + x1 p(#pos) = 1 + x1 p(#s) = x1 p(#true) = 0 p(and) = 0 p(dd) = 1 + x1 + x2 p(eq) = 0 p(eq#1) = 0 p(eq#2) = 0 p(eq#3) = x1 + x1^2 p(nil) = 0 p(nub) = 0 p(nub#1) = 0 p(remove) = x1 + x2 p(remove#1) = x1 + x2 p(remove#2) = 1 + x2 + x3 + x4 p(#and#) = 0 p(#eq#) = x2 p(#equal#) = 1 + x2 p(and#) = 0 p(eq#) = 1 + x2 p(eq#1#) = 1 + x2 p(eq#2#) = 0 p(eq#3#) = 1 + x1 p(nub#) = x1^2 p(nub#1#) = x1^2 p(remove#) = x1 + x2 p(remove#1#) = x1 + x2 p(remove#2#) = x2 + x4 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) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = x1 p(c_15) = 0 p(c_16) = x1 p(c_17) = x1 + x2 p(c_18) = 0 p(c_19) = 0 p(c_20) = 0 p(c_21) = x1 p(c_22) = 0 p(c_23) = x1 p(c_24) = x1 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = x1 + x2 p(c_29) = 0 p(c_30) = x1 p(c_31) = x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 + x2 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: #eq#(#neg(x),#neg(y)) = 1 + y > y = c_10(#eq#(x,y)) Following rules are (at-least) weakly oriented: #eq#(#pos(x),#pos(y)) = 1 + y >= y = c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) = y >= y = c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) = 1 + y'1 + y'2 >= y'1 + y'2 = c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) = 1 + y >= y = c_21(#eq#(x,y)) eq#(l1,l2) = 1 + l2 >= 1 + l2 = c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) = 1 + l2 >= 1 + l2 = c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) = 2 + y + ys >= 2 + y + ys = c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) = l^2 >= l^2 = c_30(nub#1#(l)) nub#1#(dd(x,xs)) = 1 + 2*x + 2*x*xs + x^2 + 2*xs + xs^2 >= x + 2*x*xs + x^2 + xs + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) = l + x >= l + x = c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) = 1 + x + y + ys >= 1 + x + y + ys = c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) = x + ys >= x + ys = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = x + ys >= x + ys = c_37(remove#(x,ys)) remove(x,l) = l + x >= l + x = remove#1(l,x) remove#1(dd(y,ys),x) = 1 + x + y + ys >= 1 + x + y + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = x >= 0 = nil() remove#2(#false(),x,y,ys) = 1 + x + y + ys >= 1 + x + y + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = 1 + x + y + ys >= x + ys = remove(x,ys) ****** Step 7.a:1.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 7.a:1.b:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:#eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 2:W:#eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 3:W:#eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 4:W:#eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) -->_2 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_2 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_2 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_2 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 5:W:#equal#(x,y) -> c_21(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):4 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):3 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):2 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):1 6:W:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):7 7:W:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)):8 8:W:eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 -->_1 #equal#(x,y) -> c_21(#eq#(x,y)):5 9:W:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):10 10:W:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):11 -->_1 nub#(l) -> c_30(nub#1#(l)):9 11:W:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):12 12:W:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):14 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):13 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):6 13:W:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 14:W:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):11 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: nub#(l) -> c_30(nub#1#(l)) 10: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 11: remove#(x,l) -> c_33(remove#1#(l,x)) 14: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) 12: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 13: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 6: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 8: eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) 7: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) 5: #equal#(x,y) -> c_21(#eq#(x,y)) 1: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) 4: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) 3: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) 2: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) ****** Step 7.a:1.b:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #equal#(x,y) -> c_21(#eq#(x,y)) eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {4}. Here rules are labelled as follows: 1: #equal#(x,y) -> c_21(#eq#(x,y)) 2: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 3: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) 4: eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) 5: nub#(l) -> c_30(nub#1#(l)) 6: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 7: remove#(x,l) -> c_33(remove#1#(l,x)) 8: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 9: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 10: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) 11: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) 12: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) 13: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) 14: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) ** Step 7.b:2: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) #equal#(x,y) -> c_21(#eq#(x,y)) - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):2 2:S:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)):3 3:S:eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) -->_1 #equal#(x,y) -> c_21(#eq#(x,y)):14 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 4:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):5 5:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):6 -->_1 nub#(l) -> c_30(nub#1#(l)):4 6:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):7 7:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):9 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):8 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 8:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):6 9:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):6 10:W:#eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 11:W:#eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 12:W:#eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 13:W:#eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) -->_2 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_2 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_2 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_2 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 14:W:#equal#(x,y) -> c_21(#eq#(x,y)) -->_1 #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)):13 -->_1 #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)):12 -->_1 #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)):11 -->_1 #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)):10 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: #equal#(x,y) -> c_21(#eq#(x,y)) 13: #eq#(dd(x'1,x'2),dd(y'1,y'2)) -> c_17(#eq#(x'1,y'1),#eq#(x'2,y'2)) 12: #eq#(#s(x),#s(y)) -> c_16(#eq#(x,y)) 11: #eq#(#pos(x),#pos(y)) -> c_14(#eq#(x,y)) 10: #eq#(#neg(x),#neg(y)) -> c_10(#eq#(x,y)) ** Step 7.b:3: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):2 2:S:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)):3 3:S:eq#3#(dd(y,ys),x,xs) -> c_28(#equal#(x,y),eq#(xs,ys)) -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 4:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):5 5:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):6 -->_1 nub#(l) -> c_30(nub#1#(l)):4 6:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):7 7:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):9 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):8 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 8:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):6 9:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(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#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) ** Step 7.b:4: Decompose WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) - Weak DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} Problem (S) - Strict DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} *** Step 7.b:4.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) - Weak DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) Consider the set of all dependency pairs 1: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 2: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) 3: eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) 4: nub#(l) -> c_30(nub#1#(l)) 5: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 6: remove#(x,l) -> c_33(remove#1#(l,x)) 7: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 8: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 9: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2,3} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 7.b:4.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) - Weak DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_23) = {1}, uargs(c_24) = {1}, uargs(c_28) = {1}, uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1,2}, uargs(c_36) = {1}, uargs(c_37) = {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) = 1 p(#and) = 1 + x1 + x1^2 + x2 p(#eq) = x1 + x2 p(#equal) = 1 p(#false) = 0 p(#neg) = 1 + x1 p(#pos) = 1 p(#s) = 0 p(#true) = 0 p(and) = 0 p(dd) = 1 + x1 + x2 p(eq) = 0 p(eq#1) = x2 p(eq#2) = 1 + x1^2 p(eq#3) = 1 + x1*x3 + x1^2 p(nil) = 0 p(nub) = 0 p(nub#1) = 0 p(remove) = x2 p(remove#1) = x1 p(remove#2) = 1 + x3 + x4 p(#and#) = 0 p(#eq#) = 0 p(#equal#) = 0 p(and#) = 0 p(eq#) = 1 + x1 + x2 p(eq#1#) = x1 + x2 p(eq#2#) = 0 p(eq#3#) = x1 + x3 p(nub#) = x1^2 p(nub#1#) = x1^2 p(remove#) = 1 + x1*x2 + x2 p(remove#1#) = 1 + x1 + x1*x2 p(remove#2#) = 1 + x2*x3 + x2*x4 + x4 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) = 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) = x1 p(c_24) = 1 + x1 p(c_25) = 0 p(c_26) = 0 p(c_27) = 0 p(c_28) = x1 p(c_29) = 0 p(c_30) = x1 p(c_31) = x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 + x2 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: eq#(l1,l2) = 1 + l1 + l2 > l1 + l2 = c_23(eq#1#(l1,l2)) Following rules are (at-least) weakly oriented: eq#1#(dd(x,xs),l2) = 1 + l2 + x + xs >= 1 + l2 + xs = c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) = 1 + xs + y + ys >= 1 + xs + ys = c_28(eq#(xs,ys)) nub#(l) = l^2 >= l^2 = c_30(nub#1#(l)) nub#1#(dd(x,xs)) = 1 + 2*x + 2*x*xs + x^2 + 2*xs + xs^2 >= 1 + x*xs + xs + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) = 1 + l + l*x >= 1 + l + l*x = c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) = 2 + x + x*y + x*ys + y + ys >= 2 + x + x*y + x*ys + y + ys = c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) = 1 + x*y + x*ys + ys >= 1 + x*ys + ys = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = 1 + x*y + x*ys + ys >= 1 + x*ys + ys = c_37(remove#(x,ys)) remove(x,l) = l >= l = remove#1(l,x) remove#1(dd(y,ys),x) = 1 + y + ys >= 1 + y + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = 0 >= 0 = nil() remove#2(#false(),x,y,ys) = 1 + y + ys >= 1 + y + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = 1 + y + ys >= ys = remove(x,ys) **** Step 7.b:4.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) - Weak DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 7.b:4.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):2 2:W:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)):3 3:W:eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) -->_1 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 4:W:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):5 5:W:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):6 -->_1 nub#(l) -> c_30(nub#1#(l)):4 6:W:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):7 7:W:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):9 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):8 -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):1 8:W:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):6 9:W:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):6 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: nub#(l) -> c_30(nub#1#(l)) 5: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 6: remove#(x,l) -> c_33(remove#1#(l,x)) 9: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) 7: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) 8: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 1: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 3: eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) 2: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) **** Step 7.b:4.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 7.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):2 2:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):3 -->_1 nub#(l) -> c_30(nub#1#(l)):1 3:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):4 4:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_2 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):7 -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):6 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):5 5:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 6:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 7:W:eq#(l1,l2) -> c_23(eq#1#(l1,l2)) -->_1 eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)):8 8:W:eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) -->_1 eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)):9 9:W:eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) -->_1 eq#(l1,l2) -> c_23(eq#1#(l1,l2)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: eq#(l1,l2) -> c_23(eq#1#(l1,l2)) 9: eq#3#(dd(y,ys),x,xs) -> c_28(eq#(xs,ys)) 8: eq#1#(dd(x,xs),l2) -> c_24(eq#3#(l2,x,xs)) *** Step 7.b:4.b:2: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/2,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):2 2:S:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):3 -->_1 nub#(l) -> c_30(nub#1#(l)):1 3:S:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)):4 4:S:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys),eq#(x,y)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):6 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):5 5:S:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 6:S:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) *** Step 7.b:4.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/1,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 4: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) Consider the set of all dependency pairs 1: nub#(l) -> c_30(nub#1#(l)) 2: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 3: remove#(x,l) -> c_33(remove#1#(l,x)) 4: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) 5: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) 6: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {2,4} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 7.b:4.b:3.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/1,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_30) = {1}, uargs(c_31) = {1,2}, uargs(c_33) = {1}, uargs(c_34) = {1}, uargs(c_36) = {1}, uargs(c_37) = {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) = 0 p(#and) = x1 p(#eq) = x1*x2 + x1^2 p(#equal) = 1 p(#false) = 0 p(#neg) = 0 p(#pos) = 0 p(#s) = 1 p(#true) = 0 p(and) = 1 + x1 p(dd) = 1 + x2 p(eq) = 1 p(eq#1) = 0 p(eq#2) = 0 p(eq#3) = 1 + x1*x2 p(nil) = 0 p(nub) = 0 p(nub#1) = 0 p(remove) = x2 p(remove#1) = x1 p(remove#2) = 1 + x4 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#) = x1^2 p(nub#1#) = x1^2 p(remove#) = x2 p(remove#1#) = x1 p(remove#2#) = x4 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) = 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) = x1 p(c_31) = x1 + x2 p(c_32) = 0 p(c_33) = x1 p(c_34) = x1 p(c_35) = 0 p(c_36) = x1 p(c_37) = x1 Following rules are strictly oriented: nub#1#(dd(x,xs)) = 1 + 2*xs + xs^2 > xs + xs^2 = c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#1#(dd(y,ys),x) = 1 + ys > ys = c_34(remove#2#(eq(x,y),x,y,ys)) Following rules are (at-least) weakly oriented: nub#(l) = l^2 >= l^2 = c_30(nub#1#(l)) remove#(x,l) = l >= l = c_33(remove#1#(l,x)) remove#2#(#false(),x,y,ys) = ys >= ys = c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) = ys >= ys = c_37(remove#(x,ys)) remove(x,l) = l >= l = remove#1(l,x) remove#1(dd(y,ys),x) = 1 + ys >= 1 + ys = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = 0 >= 0 = nil() remove#2(#false(),x,y,ys) = 1 + ys >= 1 + ys = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = 1 + ys >= ys = remove(x,ys) **** Step 7.b:4.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: nub#(l) -> c_30(nub#1#(l)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) - Weak DPs: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/1,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 7.b:4.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: nub#(l) -> c_30(nub#1#(l)) nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) remove#(x,l) -> c_33(remove#1#(l,x)) remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) remove#2#(#true(),x,y,ys) -> c_37(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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/1,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:nub#(l) -> c_30(nub#1#(l)) -->_1 nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)):2 2:W:nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) -->_2 remove#(x,l) -> c_33(remove#1#(l,x)):3 -->_1 nub#(l) -> c_30(nub#1#(l)):1 3:W:remove#(x,l) -> c_33(remove#1#(l,x)) -->_1 remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)):4 4:W:remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) -->_1 remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)):6 -->_1 remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)):5 5:W:remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 6:W:remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) -->_1 remove#(x,l) -> c_33(remove#1#(l,x)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: nub#(l) -> c_30(nub#1#(l)) 2: nub#1#(dd(x,xs)) -> c_31(nub#(remove(x,xs)),remove#(x,xs)) 3: remove#(x,l) -> c_33(remove#1#(l,x)) 6: remove#2#(#true(),x,y,ys) -> c_37(remove#(x,ys)) 4: remove#1#(dd(y,ys),x) -> c_34(remove#2#(eq(x,y),x,y,ys)) 5: remove#2#(#false(),x,y,ys) -> c_36(remove#(x,ys)) **** Step 7.b:4.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(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(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#1(nil(),l2) -> eq#2(l2) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() eq#3(dd(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(dd(y,ys),x) -> remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(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,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0 ,c_7/0,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/1,c_15/0,c_16/1,c_17/2,c_18/0,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/0,c_30/1,c_31/2,c_32/0,c_33/1,c_34/1,c_35/0,c_36/1 ,c_37/1} - 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,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))