WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [5] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [4] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [1] x1 + [0] p(nub#1) = [1] x1 + [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: eq(@l1,@l2) = [4] > [0] = eq#1(@l1,@l2) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [4] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [0] >= [1] @l + [0] = nub#1(@l) nub#1(::(@x,@xs)) = [1] @xs + [5] >= [5] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [0] >= [0] = nil() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [4] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [5] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() eq(@l1,@l2) -> eq#1(@l1,@l2) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [7] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [1] x1 + [0] p(nub#1) = [1] x1 + [2] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: nub#1(::(@x,@xs)) = [1] @xs + [9] > [7] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [2] > [0] = nil() Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [0] >= [1] @l + [2] = nub#1(@l) remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [7] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() eq(@l1,@l2) -> eq#1(@l1,@l2) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [3] p(eq#1) = [3] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [5] p(nub) = [1] x1 + [5] p(nub#1) = [5] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [5] Following rules are strictly oriented: eq#1(::(@x,@xs),@l2) = [3] > [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [3] > [0] = eq#2(@l2) remove#2(#false(),@x,@y,@ys) = [5] > [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [5] > [0] = remove(@x,@ys) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [3] >= [3] = eq#1(@l1,@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [3] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [5] >= [5] = nub#1(@l) nub#1(::(@x,@xs)) = [5] >= [5] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [5] >= [5] = nil() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [8] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [5] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [1] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [1] x1 + [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [0] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: #equal(@x,@y) = [1] > [0] = #eq(@x,@y) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [1] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [0] >= [0] = nub#1(@l) nub#1(::(@x,@xs)) = [0] >= [0] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [0] >= [0] = nil() remove(@x,@l) = [0] >= [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0] >= [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: and(@x,@y) -> #and(@x,@y) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [1] x1 + [0] p(nub#1) = [0] p(remove) = [0] p(remove#1) = [5] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: remove#1(::(@y,@ys),@x) = [5] > [0] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [5] > [0] = nil() Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [0] >= [0] = nub#1(@l) nub#1(::(@x,@xs)) = [0] >= [0] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [0] >= [0] = nil() remove(@x,@l) = [0] >= [5] = remove#1(@l,@x) remove#2(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: and(@x,@y) -> #and(@x,@y) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [0] p(eq) = [1] p(eq#1) = [1] p(eq#2) = [1] p(eq#3) = [1] p(nil) = [6] p(nub) = [1] x1 + [0] p(nub#1) = [1] x1 + [0] p(remove) = [0] p(remove#1) = [6] p(remove#2) = [1] x1 + [5] Following rules are strictly oriented: eq#2(::(@y,@ys)) = [1] > [0] = #false() eq#2(nil()) = [1] > [0] = #true() eq#3(nil(),@x,@xs) = [1] > [0] = #false() Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [1] @x + [1] @y + [0] >= [1] @x + [1] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [1] >= [1] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [1] >= [1] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [1] >= [1] = eq#2(@l2) eq#3(::(@y,@ys),@x,@xs) = [1] >= [1] = and(#equal(@x,@y),eq(@xs,@ys)) nub(@l) = [1] @l + [0] >= [1] @l + [0] = nub#1(@l) nub#1(::(@x,@xs)) = [1] @xs + [0] >= [0] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [6] >= [6] = nil() remove(@x,@l) = [0] >= [6] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [6] >= [6] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [6] >= [6] = nil() remove#2(#false(),@x,@y,@ys) = [5] >= [0] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [5] >= [0] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: and(@x,@y) -> #and(@x,@y) eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(nil(),@x,@xs) -> #false() nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#and) = [1] x1 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(::) = [1] x2 + [0] p(and) = [1] x1 + [1] x2 + [1] p(eq) = [1] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [1] p(nub) = [1] x1 + [0] p(nub#1) = [1] p(remove) = [1] p(remove#1) = [2] p(remove#2) = [1] x1 + [1] Following rules are strictly oriented: and(@x,@y) = [1] @x + [1] @y + [1] > [1] @x + [1] @y + [0] = #and(@x,@y) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) eq(@l1,@l2) = [1] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [2] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub(@l) = [1] @l + [0] >= [1] = nub#1(@l) nub#1(::(@x,@xs)) = [1] >= [1] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [1] >= [1] = nil() remove(@x,@l) = [1] >= [2] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [2] >= [2] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [2] >= [1] = nil() remove#2(#false(),@x,@y,@ys) = [1] >= [1] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] >= [1] = remove(@x,@ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) nub(@l) -> nub#1(@l) remove(@x,@l) -> remove#1(@l,@x) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(nil(),@x,@xs) -> #false() nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: {#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) = [2] x1 + [2] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] p(#pos) = [1] p(#s) = [1] p(#true) = [0] p(::) = [1] x2 + [1] p(and) = [4] x1 + [2] x2 + [0] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [3] x1 + [4] p(nub#1) = [3] x1 + [2] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [4] x1 + [1] x4 + [1] Following rules are strictly oriented: nub(@l) = [3] @l + [4] > [3] @l + [2] = nub#1(@l) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] >= [0] = #false() #and(#false(),#true()) = [0] >= [0] = #false() #and(#true(),#false()) = [0] >= [0] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [0] >= [0] = #true() #eq(#0(),#neg(@y)) = [0] >= [0] = #false() #eq(#0(),#pos(@y)) = [0] >= [0] = #false() #eq(#0(),#s(@y)) = [0] >= [0] = #false() #eq(#neg(@x),#0()) = [0] >= [0] = #false() #eq(#neg(@x),#neg(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#0()) = [0] >= [0] = #false() #eq(#pos(@x),#neg(@y)) = [0] >= [0] = #false() #eq(#pos(@x),#pos(@y)) = [0] >= [0] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] >= [0] = #false() #eq(#s(@x),#s(@y)) = [0] >= [0] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0] >= [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] >= [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(@x,@y) = [0] >= [0] = #eq(@x,@y) and(@x,@y) = [4] @x + [2] @y + [0] >= [2] @x + [2] @y + [0] = #and(@x,@y) eq(@l1,@l2) = [0] >= [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] >= [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] >= [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] >= [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] >= [0] = #false() nub#1(::(@x,@xs)) = [3] @xs + [5] >= [3] @xs + [5] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [2] >= [0] = nil() remove(@x,@l) = [1] @l + [0] >= [1] @l + [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [1] @ys + [1] >= [1] @ys + [1] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] >= [0] = nil() remove#2(#false(),@x,@y,@ys) = [1] @ys + [1] >= [1] @ys + [1] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1] @ys + [1] >= [1] @ys + [0] = remove(@x,@ys) * Step 9: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) remove(@x,@l) -> remove#1(@l,@x) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2} TcT has computed the following interpretation: p(#0) = [2] [0] p(#and) = [2 0] x1 + [2 0] x2 + [0] [2 0] [2 1] [0] p(#eq) = [0 0] x2 + [0] [2 0] [1] p(#equal) = [0 0] x1 + [0 0] x2 + [0] [0 2] [2 2] [2] p(#false) = [0] [0] p(#neg) = [1 2] x1 + [2] [0 1] [0] p(#pos) = [1 2] x1 + [2] [0 0] [0] p(#s) = [1 0] x1 + [3] [0 0] [0] p(#true) = [0] [0] p(::) = [1 2] x2 + [0] [0 1] [1] p(and) = [2 0] x1 + [2 0] x2 + [0] [2 0] [2 2] [0] p(eq) = [0] [0] p(eq#1) = [0] [0] p(eq#2) = [0] [0] p(eq#3) = [0] [0] p(nil) = [0] [0] p(nub) = [2 2] x1 + [3] [0 1] [0] p(nub#1) = [2 2] x1 + [3] [0 1] [0] p(remove) = [1 1] x2 + [1] [0 1] [0] p(remove#1) = [1 1] x1 + [0] [0 1] [0] p(remove#2) = [1 0] x1 + [1 3] x4 + [1] [0 0] [0 1] [1] Following rules are strictly oriented: remove(@x,@l) = [1 1] @l + [1] [0 1] [0] > [1 1] @l + [0] [0 1] [0] = remove#1(@l,@x) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] [0] >= [0] [0] = #false() #and(#false(),#true()) = [0] [0] >= [0] [0] = #false() #and(#true(),#false()) = [0] [0] >= [0] [0] = #false() #and(#true(),#true()) = [0] [0] >= [0] [0] = #true() #eq(#0(),#0()) = [0] [5] >= [0] [0] = #true() #eq(#0(),#neg(@y)) = [0 0] @y + [0] [2 4] [5] >= [0] [0] = #false() #eq(#0(),#pos(@y)) = [0 0] @y + [0] [2 4] [5] >= [0] [0] = #false() #eq(#0(),#s(@y)) = [0 0] @y + [0] [2 0] [7] >= [0] [0] = #false() #eq(#neg(@x),#0()) = [0] [5] >= [0] [0] = #false() #eq(#neg(@x),#neg(@y)) = [0 0] @y + [0] [2 4] [5] >= [0 0] @y + [0] [2 0] [1] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0 0] @y + [0] [2 4] [5] >= [0] [0] = #false() #eq(#pos(@x),#0()) = [0] [5] >= [0] [0] = #false() #eq(#pos(@x),#neg(@y)) = [0 0] @y + [0] [2 4] [5] >= [0] [0] = #false() #eq(#pos(@x),#pos(@y)) = [0 0] @y + [0] [2 4] [5] >= [0 0] @y + [0] [2 0] [1] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] [5] >= [0] [0] = #false() #eq(#s(@x),#s(@y)) = [0 0] @y + [0] [2 0] [7] >= [0 0] @y + [0] [2 0] [1] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0 0] @y_2 + [0] [2 4] [1] >= [0 0] @y_2 + [0] [2 0] [1] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] [1] >= [0] [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0 0] @y_2 + [0] [2 4] [1] >= [0] [0] = #false() #eq(nil(),nil()) = [0] [1] >= [0] [0] = #true() #equal(@x,@y) = [0 0] @x + [0 0] @y + [0] [0 2] [2 2] [2] >= [0 0] @y + [0] [2 0] [1] = #eq(@x,@y) and(@x,@y) = [2 0] @x + [2 0] @y + [0] [2 0] [2 2] [0] >= [2 0] @x + [2 0] @y + [0] [2 0] [2 1] [0] = #and(@x,@y) eq(@l1,@l2) = [0] [0] >= [0] [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0] [0] >= [0] [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0] [0] >= [0] [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0] [0] >= [0] [0] = #false() eq#2(nil()) = [0] [0] >= [0] [0] = #true() eq#3(::(@y,@ys),@x,@xs) = [0] [0] >= [0] [0] = and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) = [0] [0] >= [0] [0] = #false() nub(@l) = [2 2] @l + [3] [0 1] [0] >= [2 2] @l + [3] [0 1] [0] = nub#1(@l) nub#1(::(@x,@xs)) = [2 6] @xs + [5] [0 1] [1] >= [2 6] @xs + [5] [0 1] [1] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [3] [0] >= [0] [0] = nil() remove#1(::(@y,@ys),@x) = [1 3] @ys + [1] [0 1] [1] >= [1 3] @ys + [1] [0 1] [1] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] [0] >= [0] [0] = nil() remove#2(#false(),@x,@y,@ys) = [1 3] @ys + [1] [0 1] [1] >= [1 3] @ys + [1] [0 1] [1] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [1 3] @ys + [1] [0 1] [1] >= [1 1] @ys + [1] [0 1] [0] = remove(@x,@ys) * Step 10: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),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(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#and) = {1,2}, uargs(::) = {2}, uargs(and) = {1,2}, uargs(nub) = {1}, uargs(remove#2) = {1} Following symbols are considered usable: {#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] [0] p(#and) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(#eq) = [0 0] x2 + [0] [2 0] [2] p(#equal) = [0 0] x2 + [0] [2 1] [2] p(#false) = [0] [0] p(#neg) = [1 2] x1 + [2] [0 0] [1] p(#pos) = [1 0] x1 + [1] [0 0] [0] p(#s) = [1 2] x1 + [0] [0 1] [1] p(#true) = [0] [0] p(::) = [0 0] x1 + [1 2] x2 + [0] [0 1] [0 1] [2] p(and) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 2] [0] p(eq) = [0 1] x2 + [2] [0 0] [0] p(eq#1) = [0 1] x2 + [2] [0 0] [0] p(eq#2) = [0 1] x1 + [2] [0 0] [0] p(eq#3) = [0 1] x1 + [2] [0 0] [0] p(nil) = [0] [0] p(nub) = [2 0] x1 + [2] [0 1] [0] p(nub#1) = [2 0] x1 + [2] [0 1] [0] p(remove) = [1 1] x2 + [0] [0 1] [0] p(remove#1) = [1 1] x1 + [0] [0 1] [0] p(remove#2) = [1 0] x1 + [0 0] x3 + [1 3] x4 + [0] [0 0] [0 1] [0 1] [2] Following rules are strictly oriented: eq#3(::(@y,@ys),@x,@xs) = [0 1] @y + [0 1] @ys + [4] [0 0] [0 0] [0] > [0 1] @ys + [2] [0 0] [0] = and(#equal(@x,@y),eq(@xs,@ys)) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] [0] >= [0] [0] = #false() #and(#false(),#true()) = [0] [0] >= [0] [0] = #false() #and(#true(),#false()) = [0] [0] >= [0] [0] = #false() #and(#true(),#true()) = [0] [0] >= [0] [0] = #true() #eq(#0(),#0()) = [0] [4] >= [0] [0] = #true() #eq(#0(),#neg(@y)) = [0 0] @y + [0] [2 4] [6] >= [0] [0] = #false() #eq(#0(),#pos(@y)) = [0 0] @y + [0] [2 0] [4] >= [0] [0] = #false() #eq(#0(),#s(@y)) = [0 0] @y + [0] [2 4] [2] >= [0] [0] = #false() #eq(#neg(@x),#0()) = [0] [4] >= [0] [0] = #false() #eq(#neg(@x),#neg(@y)) = [0 0] @y + [0] [2 4] [6] >= [0 0] @y + [0] [2 0] [2] = #eq(@x,@y) #eq(#neg(@x),#pos(@y)) = [0 0] @y + [0] [2 0] [4] >= [0] [0] = #false() #eq(#pos(@x),#0()) = [0] [4] >= [0] [0] = #false() #eq(#pos(@x),#neg(@y)) = [0 0] @y + [0] [2 4] [6] >= [0] [0] = #false() #eq(#pos(@x),#pos(@y)) = [0 0] @y + [0] [2 0] [4] >= [0 0] @y + [0] [2 0] [2] = #eq(@x,@y) #eq(#s(@x),#0()) = [0] [4] >= [0] [0] = #false() #eq(#s(@x),#s(@y)) = [0 0] @y + [0] [2 4] [2] >= [0 0] @y + [0] [2 0] [2] = #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0 0] @y_2 + [0] [2 4] [2] >= [0] [0] = #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) = [0] [2] >= [0] [0] = #false() #eq(nil(),::(@y_1,@y_2)) = [0 0] @y_2 + [0] [2 4] [2] >= [0] [0] = #false() #eq(nil(),nil()) = [0] [2] >= [0] [0] = #true() #equal(@x,@y) = [0 0] @y + [0] [2 1] [2] >= [0 0] @y + [0] [2 0] [2] = #eq(@x,@y) and(@x,@y) = [2 0] @x + [1 0] @y + [0] [0 0] [0 2] [0] >= [2 0] @x + [1 0] @y + [0] [0 0] [0 0] [0] = #and(@x,@y) eq(@l1,@l2) = [0 1] @l2 + [2] [0 0] [0] >= [0 1] @l2 + [2] [0 0] [0] = eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) = [0 1] @l2 + [2] [0 0] [0] >= [0 1] @l2 + [2] [0 0] [0] = eq#3(@l2,@x,@xs) eq#1(nil(),@l2) = [0 1] @l2 + [2] [0 0] [0] >= [0 1] @l2 + [2] [0 0] [0] = eq#2(@l2) eq#2(::(@y,@ys)) = [0 1] @y + [0 1] @ys + [4] [0 0] [0 0] [0] >= [0] [0] = #false() eq#2(nil()) = [2] [0] >= [0] [0] = #true() eq#3(nil(),@x,@xs) = [2] [0] >= [0] [0] = #false() nub(@l) = [2 0] @l + [2] [0 1] [0] >= [2 0] @l + [2] [0 1] [0] = nub#1(@l) nub#1(::(@x,@xs)) = [0 0] @x + [2 4] @xs + [2] [0 1] [0 1] [2] >= [0 0] @x + [2 4] @xs + [2] [0 1] [0 1] [2] = ::(@x,nub(remove(@x,@xs))) nub#1(nil()) = [2] [0] >= [0] [0] = nil() remove(@x,@l) = [1 1] @l + [0] [0 1] [0] >= [1 1] @l + [0] [0 1] [0] = remove#1(@l,@x) remove#1(::(@y,@ys),@x) = [0 1] @y + [1 3] @ys + [2] [0 1] [0 1] [2] >= [0 1] @y + [1 3] @ys + [2] [0 1] [0 1] [2] = remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) = [0] [0] >= [0] [0] = nil() remove#2(#false(),@x,@y,@ys) = [0 0] @y + [1 3] @ys + [0] [0 1] [0 1] [2] >= [0 0] @y + [1 3] @ys + [0] [0 1] [0 1] [2] = ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) = [0 0] @y + [1 3] @ys + [0] [0 1] [0 1] [2] >= [1 1] @ys + [0] [0 1] [0] = remove(@x,@ys) * Step 11: 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(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #equal(@x,@y) -> #eq(@x,@y) and(@x,@y) -> #and(@x,@y) eq(@l1,@l2) -> eq#1(@l1,@l2) eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs) eq#1(nil(),@l2) -> eq#2(@l2) eq#2(::(@y,@ys)) -> #false() eq#2(nil()) -> #true() eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys)) eq#3(nil(),@x,@xs) -> #false() nub(@l) -> nub#1(@l) nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs))) nub#1(nil()) -> nil() remove(@x,@l) -> remove#1(@l,@x) remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys) remove#1(nil(),@x) -> nil() remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys)) remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys) - Signature: {#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove ,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))