WORST_CASE(?,O(n^2)) * Step 1: WeightGap 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: 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(and) = {1,2}, uargs(dd) = {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 + [1] p(#eq) = [7] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [1] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [5] 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 + [0] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [1] x1 + [1] x4 + [0] Following rules are strictly oriented: #and(#false(),#false()) = [1] > [0] = #false() #and(#false(),#true()) = [2] > [0] = #false() #and(#true(),#false()) = [2] > [0] = #false() #and(#true(),#true()) = [3] > [1] = #true() #eq(#0(),#0()) = [7] > [1] = #true() #eq(#0(),#neg(y)) = [7] > [0] = #false() #eq(#0(),#pos(y)) = [7] > [0] = #false() #eq(#0(),#s(y)) = [7] > [0] = #false() #eq(#neg(x),#0()) = [7] > [0] = #false() #eq(#neg(x),#pos(y)) = [7] > [0] = #false() #eq(#pos(x),#0()) = [7] > [0] = #false() #eq(#pos(x),#neg(y)) = [7] > [0] = #false() #eq(#s(x),#0()) = [7] > [0] = #false() #eq(dd(x'1,x'2),nil()) = [7] > [0] = #false() #eq(nil(),dd(y'1,y'2)) = [7] > [0] = #false() #eq(nil(),nil()) = [7] > [1] = #true() remove#1(dd(y,ys),x) = [1] ys + [5] > [1] ys + [0] = remove#2(eq(x,y),x,y,ys) remove#2(#true(),x,y,ys) = [1] ys + [1] > [1] ys + [0] = remove(x,ys) Following rules are (at-least) weakly oriented: #eq(#neg(x),#neg(y)) = [7] >= [7] = #eq(x,y) #eq(#pos(x),#pos(y)) = [7] >= [7] = #eq(x,y) #eq(#s(x),#s(y)) = [7] >= [7] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [7] >= [15] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #equal(x,y) = [0] >= [7] = #eq(x,y) and(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [1] = #and(x,y) eq(l1,l2) = [0] >= [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0] >= [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] >= [0] = eq#2(l2) eq#2(dd(y,ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [1] = #true() eq#3(dd(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 + [0] = nub#1(l) nub#1(dd(x,xs)) = [1] xs + [5] >= [1] xs + [5] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] >= [0] = nil() remove(x,l) = [1] l + [0] >= [1] l + [0] = remove#1(l,x) remove#1(nil(),x) = [0] >= [0] = nil() remove#2(#false(),x,y,ys) = [1] ys + [0] >= [1] ys + [5] = dd(y,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: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #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(nil(),x) -> nil() remove#2(#false(),x,y,ys) -> dd(y,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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() remove#1(dd(y,ys),x) -> remove#2(eq(x,y),x,y,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: 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(and) = {1,2}, uargs(dd) = {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) = [7] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [1] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [7] p(eq#3) = [0] p(nil) = [6] p(nub) = [1] x1 + [5] p(nub#1) = [1] x1 + [7] p(remove) = [1] x2 + [1] p(remove#1) = [1] x1 + [2] p(remove#2) = [1] x1 + [1] x4 + [3] Following rules are strictly oriented: eq#2(dd(y,ys)) = [7] > [0] = #false() eq#2(nil()) = [7] > [0] = #true() nub#1(dd(x,xs)) = [1] xs + [8] > [1] xs + [7] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [13] > [6] = nil() remove#1(nil(),x) = [8] > [6] = nil() remove#2(#false(),x,y,ys) = [1] ys + [3] > [1] ys + [2] = dd(y,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()) = [7] >= [0] = #true() #eq(#0(),#neg(y)) = [7] >= [0] = #false() #eq(#0(),#pos(y)) = [7] >= [0] = #false() #eq(#0(),#s(y)) = [7] >= [0] = #false() #eq(#neg(x),#0()) = [7] >= [0] = #false() #eq(#neg(x),#neg(y)) = [7] >= [7] = #eq(x,y) #eq(#neg(x),#pos(y)) = [7] >= [0] = #false() #eq(#pos(x),#0()) = [7] >= [0] = #false() #eq(#pos(x),#neg(y)) = [7] >= [0] = #false() #eq(#pos(x),#pos(y)) = [7] >= [7] = #eq(x,y) #eq(#s(x),#0()) = [7] >= [0] = #false() #eq(#s(x),#s(y)) = [7] >= [7] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [7] >= [14] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [7] >= [0] = #false() #eq(nil(),dd(y'1,y'2)) = [7] >= [0] = #false() #eq(nil(),nil()) = [7] >= [0] = #true() #equal(x,y) = [0] >= [7] = #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(dd(x,xs),l2) = [0] >= [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] >= [7] = eq#2(l2) eq#3(dd(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 + [5] >= [1] l + [7] = nub#1(l) remove(x,l) = [1] l + [1] >= [1] l + [2] = remove#1(l,x) remove#1(dd(y,ys),x) = [1] ys + [3] >= [1] ys + [3] = remove#2(eq(x,y),x,y,ys) remove#2(#true(),x,y,ys) = [1] ys + [3] >= [1] ys + [1] = remove(x,ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #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#3(dd(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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() 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: 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(and) = {1,2}, uargs(dd) = {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 + [1] x2 + [0] p(#eq) = [0] p(#equal) = [0] p(#false) = [0] p(#neg) = [1] p(#pos) = [0] p(#s) = [1] p(#true) = [0] p(and) = [2] x1 + [1] x2 + [0] p(dd) = [1] x1 + [1] x2 + [1] p(eq) = [0] p(eq#1) = [0] p(eq#2) = [0] p(eq#3) = [0] p(nil) = [0] p(nub) = [2] x1 + [2] p(nub#1) = [2] x1 + [1] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [0] p(remove#2) = [4] x1 + [1] x3 + [1] x4 + [1] Following rules are strictly oriented: nub(l) = [2] l + [2] > [2] l + [1] = 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(dd(x'1,x'2),dd(y'1,y'2)) = [0] >= [0] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [0] >= [0] = #false() #eq(nil(),dd(y'1,y'2)) = [0] >= [0] = #false() #eq(nil(),nil()) = [0] >= [0] = #true() #equal(x,y) = [0] >= [0] = #eq(x,y) and(x,y) = [2] x + [1] y + [0] >= [2] x + [1] y + [0] = #and(x,y) eq(l1,l2) = [0] >= [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0] >= [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] >= [0] = eq#2(l2) eq#2(dd(y,ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(dd(y,ys),x,xs) = [0] >= [0] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] >= [0] = #false() nub#1(dd(x,xs)) = [2] x + [2] xs + [3] >= [1] x + [2] xs + [3] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [1] >= [0] = nil() remove(x,l) = [1] l + [0] >= [1] l + [0] = remove#1(l,x) remove#1(dd(y,ys),x) = [1] y + [1] ys + [1] >= [1] y + [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] y + [1] ys + [1] >= [1] y + [1] ys + [1] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [1] y + [1] ys + [1] >= [1] ys + [0] = remove(x,ys) * Step 4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #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#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) - 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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() nub(l) -> nub#1(l) nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() 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: 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(and) = {1,2}, uargs(dd) = {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 + [6] p(#eq) = [2] p(#equal) = [0] p(#false) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [0] p(#true) = [1] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [0] p(eq) = [0] p(eq#1) = [3] p(eq#2) = [3] 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: eq#1(dd(x,xs),l2) = [3] > [0] = eq#3(l2,x,xs) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [6] >= [0] = #false() #and(#false(),#true()) = [7] >= [0] = #false() #and(#true(),#false()) = [7] >= [0] = #false() #and(#true(),#true()) = [8] >= [1] = #true() #eq(#0(),#0()) = [2] >= [1] = #true() #eq(#0(),#neg(y)) = [2] >= [0] = #false() #eq(#0(),#pos(y)) = [2] >= [0] = #false() #eq(#0(),#s(y)) = [2] >= [0] = #false() #eq(#neg(x),#0()) = [2] >= [0] = #false() #eq(#neg(x),#neg(y)) = [2] >= [2] = #eq(x,y) #eq(#neg(x),#pos(y)) = [2] >= [0] = #false() #eq(#pos(x),#0()) = [2] >= [0] = #false() #eq(#pos(x),#neg(y)) = [2] >= [0] = #false() #eq(#pos(x),#pos(y)) = [2] >= [2] = #eq(x,y) #eq(#s(x),#0()) = [2] >= [0] = #false() #eq(#s(x),#s(y)) = [2] >= [2] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [2] >= [10] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [2] >= [0] = #false() #eq(nil(),dd(y'1,y'2)) = [2] >= [0] = #false() #eq(nil(),nil()) = [2] >= [1] = #true() #equal(x,y) = [0] >= [2] = #eq(x,y) and(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [6] = #and(x,y) eq(l1,l2) = [0] >= [3] = eq#1(l1,l2) eq#1(nil(),l2) = [3] >= [3] = eq#2(l2) eq#2(dd(y,ys)) = [3] >= [0] = #false() eq#2(nil()) = [3] >= [1] = #true() eq#3(dd(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(dd(x,xs)) = [0] >= [0] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] >= [0] = nil() remove(x,l) = [0] >= [0] = remove#1(l,x) remove#1(dd(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] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [1] >= [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: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #equal(x,y) -> #eq(x,y) and(x,y) -> #and(x,y) eq(l1,l2) -> eq#1(l1,l2) eq#1(nil(),l2) -> eq#2(l2) 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) - 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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() eq#1(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() nub(l) -> nub#1(l) nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() 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: 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(and) = {1,2}, uargs(dd) = {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 + [2] p(#eq) = [6] p(#equal) = [4] p(#false) = [4] p(#neg) = [0] p(#pos) = [0] p(#s) = [0] p(#true) = [2] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [4] p(eq) = [5] p(eq#1) = [0] p(eq#2) = [7] p(eq#3) = [0] p(nil) = [1] p(nub) = [1] x1 + [5] p(nub#1) = [1] x1 + [5] p(remove) = [1] x2 + [0] p(remove#1) = [1] x1 + [1] p(remove#2) = [1] x1 + [1] x4 + [0] Following rules are strictly oriented: eq(l1,l2) = [5] > [0] = eq#1(l1,l2) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [10] >= [4] = #false() #and(#false(),#true()) = [8] >= [4] = #false() #and(#true(),#false()) = [8] >= [4] = #false() #and(#true(),#true()) = [6] >= [2] = #true() #eq(#0(),#0()) = [6] >= [2] = #true() #eq(#0(),#neg(y)) = [6] >= [4] = #false() #eq(#0(),#pos(y)) = [6] >= [4] = #false() #eq(#0(),#s(y)) = [6] >= [4] = #false() #eq(#neg(x),#0()) = [6] >= [4] = #false() #eq(#neg(x),#neg(y)) = [6] >= [6] = #eq(x,y) #eq(#neg(x),#pos(y)) = [6] >= [4] = #false() #eq(#pos(x),#0()) = [6] >= [4] = #false() #eq(#pos(x),#neg(y)) = [6] >= [4] = #false() #eq(#pos(x),#pos(y)) = [6] >= [6] = #eq(x,y) #eq(#s(x),#0()) = [6] >= [4] = #false() #eq(#s(x),#s(y)) = [6] >= [6] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [6] >= [14] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [6] >= [4] = #false() #eq(nil(),dd(y'1,y'2)) = [6] >= [4] = #false() #eq(nil(),nil()) = [6] >= [2] = #true() #equal(x,y) = [4] >= [6] = #eq(x,y) and(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [2] = #and(x,y) eq#1(dd(x,xs),l2) = [0] >= [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] >= [7] = eq#2(l2) eq#2(dd(y,ys)) = [7] >= [4] = #false() eq#2(nil()) = [7] >= [2] = #true() eq#3(dd(y,ys),x,xs) = [0] >= [9] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] >= [4] = #false() nub(l) = [1] l + [5] >= [1] l + [5] = nub#1(l) nub#1(dd(x,xs)) = [1] xs + [9] >= [1] xs + [9] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [6] >= [1] = nil() remove(x,l) = [1] l + [0] >= [1] l + [1] = remove#1(l,x) remove#1(dd(y,ys),x) = [1] ys + [5] >= [1] ys + [5] = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = [2] >= [1] = nil() remove#2(#false(),x,y,ys) = [1] ys + [4] >= [1] ys + [4] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [1] ys + [2] >= [1] ys + [0] = remove(x,ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #equal(x,y) -> #eq(x,y) and(x,y) -> #and(x,y) eq#1(nil(),l2) -> eq#2(l2) 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) - 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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() eq(l1,l2) -> eq#1(l1,l2) eq#1(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() nub(l) -> nub#1(l) nub#1(dd(x,xs)) -> dd(x,nub(remove(x,xs))) nub#1(nil()) -> nil() 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: 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(and) = {1,2}, uargs(dd) = {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) = [6] p(#equal) = [0] p(#false) = [1] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [1] p(eq) = [4] p(eq#1) = [3] p(eq#2) = [4] p(eq#3) = [3] p(nil) = [4] p(nub) = [1] x1 + [0] p(nub#1) = [1] x1 + [0] p(remove) = [0] p(remove#1) = [4] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: eq#3(nil(),x,xs) = [3] > [1] = #false() Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [2] >= [1] = #false() #and(#false(),#true()) = [1] >= [1] = #false() #and(#true(),#false()) = [1] >= [1] = #false() #and(#true(),#true()) = [0] >= [0] = #true() #eq(#0(),#0()) = [6] >= [0] = #true() #eq(#0(),#neg(y)) = [6] >= [1] = #false() #eq(#0(),#pos(y)) = [6] >= [1] = #false() #eq(#0(),#s(y)) = [6] >= [1] = #false() #eq(#neg(x),#0()) = [6] >= [1] = #false() #eq(#neg(x),#neg(y)) = [6] >= [6] = #eq(x,y) #eq(#neg(x),#pos(y)) = [6] >= [1] = #false() #eq(#pos(x),#0()) = [6] >= [1] = #false() #eq(#pos(x),#neg(y)) = [6] >= [1] = #false() #eq(#pos(x),#pos(y)) = [6] >= [6] = #eq(x,y) #eq(#s(x),#0()) = [6] >= [1] = #false() #eq(#s(x),#s(y)) = [6] >= [6] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [6] >= [12] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [6] >= [1] = #false() #eq(nil(),dd(y'1,y'2)) = [6] >= [1] = #false() #eq(nil(),nil()) = [6] >= [0] = #true() #equal(x,y) = [0] >= [6] = #eq(x,y) and(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = #and(x,y) eq(l1,l2) = [4] >= [3] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [3] >= [3] = eq#3(l2,x,xs) eq#1(nil(),l2) = [3] >= [4] = eq#2(l2) eq#2(dd(y,ys)) = [4] >= [1] = #false() eq#2(nil()) = [4] >= [0] = #true() eq#3(dd(y,ys),x,xs) = [3] >= [4] = and(#equal(x,y),eq(xs,ys)) nub(l) = [1] l + [0] >= [1] l + [0] = nub#1(l) nub#1(dd(x,xs)) = [1] xs + [1] >= [1] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [4] >= [4] = nil() remove(x,l) = [0] >= [4] = remove#1(l,x) remove#1(dd(y,ys),x) = [4] >= [4] = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = [4] >= [4] = nil() remove#2(#false(),x,y,ys) = [1] >= [1] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [0] >= [0] = remove(x,ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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)) #equal(x,y) -> #eq(x,y) and(x,y) -> #and(x,y) eq#1(nil(),l2) -> eq#2(l2) eq#3(dd(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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #eq(dd(x'1,x'2),nil()) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() eq(l1,l2) -> eq#1(l1,l2) eq#1(dd(x,xs),l2) -> eq#3(l2,x,xs) eq#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() 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#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: 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(and) = {1,2}, uargs(dd) = {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 + [3] p(#eq) = [4] p(#equal) = [5] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [4] p(and) = [1] x1 + [1] x2 + [4] p(dd) = [1] x2 + [0] p(eq) = [1] p(eq#1) = [0] p(eq#2) = [7] p(eq#3) = [0] p(nil) = [4] p(nub) = [1] x1 + [4] p(nub#1) = [4] p(remove) = [0] p(remove#1) = [4] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: #equal(x,y) = [5] > [4] = #eq(x,y) and(x,y) = [1] x + [1] y + [4] > [1] x + [1] y + [3] = #and(x,y) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [3] >= [0] = #false() #and(#false(),#true()) = [7] >= [0] = #false() #and(#true(),#false()) = [7] >= [0] = #false() #and(#true(),#true()) = [11] >= [4] = #true() #eq(#0(),#0()) = [4] >= [4] = #true() #eq(#0(),#neg(y)) = [4] >= [0] = #false() #eq(#0(),#pos(y)) = [4] >= [0] = #false() #eq(#0(),#s(y)) = [4] >= [0] = #false() #eq(#neg(x),#0()) = [4] >= [0] = #false() #eq(#neg(x),#neg(y)) = [4] >= [4] = #eq(x,y) #eq(#neg(x),#pos(y)) = [4] >= [0] = #false() #eq(#pos(x),#0()) = [4] >= [0] = #false() #eq(#pos(x),#neg(y)) = [4] >= [0] = #false() #eq(#pos(x),#pos(y)) = [4] >= [4] = #eq(x,y) #eq(#s(x),#0()) = [4] >= [0] = #false() #eq(#s(x),#s(y)) = [4] >= [4] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [4] >= [11] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [4] >= [0] = #false() #eq(nil(),dd(y'1,y'2)) = [4] >= [0] = #false() #eq(nil(),nil()) = [4] >= [4] = #true() eq(l1,l2) = [1] >= [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0] >= [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] >= [7] = eq#2(l2) eq#2(dd(y,ys)) = [7] >= [0] = #false() eq#2(nil()) = [7] >= [4] = #true() eq#3(dd(y,ys),x,xs) = [0] >= [10] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] >= [0] = #false() nub(l) = [1] l + [4] >= [4] = nub#1(l) nub#1(dd(x,xs)) = [4] >= [4] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [4] >= [4] = nil() remove(x,l) = [0] >= [4] = remove#1(l,x) remove#1(dd(y,ys),x) = [4] >= [1] = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = [4] >= [4] = nil() remove#2(#false(),x,y,ys) = [0] >= [0] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [4] >= [0] = remove(x,ys) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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#1(nil(),l2) -> eq#2(l2) eq#3(dd(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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #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#2(dd(y,ys)) -> #false() eq#2(nil()) -> #true() 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#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: 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(and) = {1,2}, uargs(dd) = {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) = [1] p(#equal) = [5] p(#false) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(and) = [1] x1 + [1] x2 + [0] p(dd) = [1] x2 + [0] p(eq) = [3] p(eq#1) = [3] 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) = [3] p(remove#2) = [1] x1 + [0] Following rules are strictly oriented: eq#1(nil(),l2) = [3] > [0] = eq#2(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()) = [1] >= [0] = #true() #eq(#0(),#neg(y)) = [1] >= [0] = #false() #eq(#0(),#pos(y)) = [1] >= [0] = #false() #eq(#0(),#s(y)) = [1] >= [0] = #false() #eq(#neg(x),#0()) = [1] >= [0] = #false() #eq(#neg(x),#neg(y)) = [1] >= [1] = #eq(x,y) #eq(#neg(x),#pos(y)) = [1] >= [0] = #false() #eq(#pos(x),#0()) = [1] >= [0] = #false() #eq(#pos(x),#neg(y)) = [1] >= [0] = #false() #eq(#pos(x),#pos(y)) = [1] >= [1] = #eq(x,y) #eq(#s(x),#0()) = [1] >= [0] = #false() #eq(#s(x),#s(y)) = [1] >= [1] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [1] >= [2] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [1] >= [0] = #false() #eq(nil(),dd(y'1,y'2)) = [1] >= [0] = #false() #eq(nil(),nil()) = [1] >= [0] = #true() #equal(x,y) = [5] >= [1] = #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#1(dd(x,xs),l2) = [3] >= [0] = eq#3(l2,x,xs) eq#2(dd(y,ys)) = [0] >= [0] = #false() eq#2(nil()) = [0] >= [0] = #true() eq#3(dd(y,ys),x,xs) = [0] >= [8] = 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(dd(x,xs)) = [0] >= [0] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] >= [0] = nil() remove(x,l) = [0] >= [3] = remove#1(l,x) remove#1(dd(y,ys),x) = [3] >= [3] = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = [3] >= [0] = nil() remove#2(#false(),x,y,ys) = [0] >= [0] = dd(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 9: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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#3(dd(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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #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(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#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: 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(and) = {1,2}, uargs(dd) = {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] [2] p(#and) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 0] [0] p(#eq) = [0] [2] p(#equal) = [0] [2] p(#false) = [0] [2] p(#neg) = [0 1] x1 + [1] [0 0] [0] p(#pos) = [1] [2] p(#s) = [2] [0] p(#true) = [0] [2] p(and) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 0] [0] p(dd) = [1 2] x2 + [2] [0 1] [2] p(eq) = [0] [2] p(eq#1) = [0] [2] p(eq#2) = [0] [2] p(eq#3) = [0] [2] p(nil) = [0] [0] p(nub) = [2 1] x1 + [0] [0 1] [0] p(nub#1) = [2 1] x1 + [0] [0 1] [0] p(remove) = [1 1] x2 + [2] [0 1] [0] p(remove#1) = [1 1] x1 + [0] [0 1] [0] p(remove#2) = [2 2] x1 + [1 3] x4 + [0] [0 1] [0 1] [0] Following rules are strictly oriented: remove(x,l) = [1 1] l + [2] [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] [2] >= [0] [2] = #false() #and(#false(),#true()) = [0] [2] >= [0] [2] = #false() #and(#true(),#false()) = [0] [2] >= [0] [2] = #false() #and(#true(),#true()) = [0] [2] >= [0] [2] = #true() #eq(#0(),#0()) = [0] [2] >= [0] [2] = #true() #eq(#0(),#neg(y)) = [0] [2] >= [0] [2] = #false() #eq(#0(),#pos(y)) = [0] [2] >= [0] [2] = #false() #eq(#0(),#s(y)) = [0] [2] >= [0] [2] = #false() #eq(#neg(x),#0()) = [0] [2] >= [0] [2] = #false() #eq(#neg(x),#neg(y)) = [0] [2] >= [0] [2] = #eq(x,y) #eq(#neg(x),#pos(y)) = [0] [2] >= [0] [2] = #false() #eq(#pos(x),#0()) = [0] [2] >= [0] [2] = #false() #eq(#pos(x),#neg(y)) = [0] [2] >= [0] [2] = #false() #eq(#pos(x),#pos(y)) = [0] [2] >= [0] [2] = #eq(x,y) #eq(#s(x),#0()) = [0] [2] >= [0] [2] = #false() #eq(#s(x),#s(y)) = [0] [2] >= [0] [2] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0] [2] >= [0] [2] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [0] [2] >= [0] [2] = #false() #eq(nil(),dd(y'1,y'2)) = [0] [2] >= [0] [2] = #false() #eq(nil(),nil()) = [0] [2] >= [0] [2] = #true() #equal(x,y) = [0] [2] >= [0] [2] = #eq(x,y) and(x,y) = [1 0] x + [1 0] y + [0] [0 1] [0 0] [0] >= [1 0] x + [1 0] y + [0] [0 1] [0 0] [0] = #and(x,y) eq(l1,l2) = [0] [2] >= [0] [2] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0] [2] >= [0] [2] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0] [2] >= [0] [2] = eq#2(l2) eq#2(dd(y,ys)) = [0] [2] >= [0] [2] = #false() eq#2(nil()) = [0] [2] >= [0] [2] = #true() eq#3(dd(y,ys),x,xs) = [0] [2] >= [0] [2] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] [2] >= [0] [2] = #false() nub(l) = [2 1] l + [0] [0 1] [0] >= [2 1] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [2 5] xs + [6] [0 1] [2] >= [2 5] xs + [6] [0 1] [2] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [0] >= [0] [0] = nil() remove#1(dd(y,ys),x) = [1 3] ys + [4] [0 1] [2] >= [1 3] ys + [4] [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) = [1 3] ys + [4] [0 1] [2] >= [1 3] ys + [4] [0 1] [2] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [1 3] ys + [4] [0 1] [2] >= [1 1] ys + [2] [0 1] [0] = remove(x,ys) * Step 10: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #eq(#pos(x),#pos(y)) -> #eq(x,y) #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#3(dd(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),#pos(y)) -> #false() #eq(#pos(x),#0()) -> #false() #eq(#pos(x),#neg(y)) -> #false() #eq(#s(x),#0()) -> #false() #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(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: 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(and) = {1,2}, uargs(dd) = {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] [1] p(#and) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(#eq) = [0 0] x1 + [0 1] x2 + [0] [1 0] [0 0] [0] p(#equal) = [0 0] x1 + [0 1] x2 + [0] [2 2] [0 0] [0] p(#false) = [0] [0] p(#neg) = [1 2] x1 + [2] [0 1] [0] p(#pos) = [1 0] x1 + [1] [0 1] [2] p(#s) = [1 0] x1 + [0] [0 1] [0] p(#true) = [0] [0] p(and) = [1 0] x1 + [1 0] x2 + [0] [1 0] [0 0] [0] p(dd) = [0 0] x1 + [1 2] x2 + [0] [0 1] [0 1] [0] p(eq) = [0 0] x1 + [0 1] x2 + [0] [0 3] [0 1] [2] p(eq#1) = [0 0] x1 + [0 1] x2 + [0] [0 3] [0 1] [0] p(eq#2) = [0 1] x1 + [0] [0 0] [0] p(eq#3) = [0 1] x1 + [0 0] x3 + [0] [0 1] [0 3] [0] p(nil) = [0] [0] p(nub) = [2 0] x1 + [0] [0 1] [0] p(nub#1) = [2 0] x1 + [0] [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] [0] Following rules are strictly oriented: #eq(#pos(x),#pos(y)) = [0 0] x + [0 1] y + [2] [1 0] [0 0] [1] > [0 0] x + [0 1] y + [0] [1 0] [0 0] [0] = #eq(x,y) 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()) = [1] [0] >= [0] [0] = #true() #eq(#0(),#neg(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#pos(y)) = [0 1] y + [2] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#s(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#neg(x),#0()) = [0 0] x + [1] [1 2] [2] >= [0] [0] = #false() #eq(#neg(x),#neg(y)) = [0 0] x + [0 1] y + [0] [1 2] [0 0] [2] >= [0 0] x + [0 1] y + [0] [1 0] [0 0] [0] = #eq(x,y) #eq(#neg(x),#pos(y)) = [0 0] x + [0 1] y + [2] [1 2] [0 0] [2] >= [0] [0] = #false() #eq(#pos(x),#0()) = [0 0] x + [1] [1 0] [1] >= [0] [0] = #false() #eq(#pos(x),#neg(y)) = [0 0] x + [0 1] y + [0] [1 0] [0 0] [1] >= [0] [0] = #false() #eq(#s(x),#0()) = [0 0] x + [1] [1 0] [0] >= [0] [0] = #false() #eq(#s(x),#s(y)) = [0 0] x + [0 1] y + [0] [1 0] [0 0] [0] >= [0 0] x + [0 1] y + [0] [1 0] [0 0] [0] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0 0] x'2 + [0 1] y'1 + [0 1] y'2 + [0] [1 2] [0 0] [0 0] [0] >= [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [0] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [0 0] x'2 + [0] [1 2] [0] >= [0] [0] = #false() #eq(nil(),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [0] >= [0] [0] = #false() #eq(nil(),nil()) = [0] [0] >= [0] [0] = #true() #equal(x,y) = [0 0] x + [0 1] y + [0] [2 2] [0 0] [0] >= [0 0] x + [0 1] y + [0] [1 0] [0 0] [0] = #eq(x,y) and(x,y) = [1 0] x + [1 0] y + [0] [1 0] [0 0] [0] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] = #and(x,y) eq(l1,l2) = [0 0] l1 + [0 1] l2 + [0] [0 3] [0 1] [2] >= [0 0] l1 + [0 1] l2 + [0] [0 3] [0 1] [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0 1] l2 + [0 0] x + [0 0] xs + [0] [0 1] [0 3] [0 3] [0] >= [0 1] l2 + [0 0] xs + [0] [0 1] [0 3] [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0 1] l2 + [0] [0 1] [0] >= [0 1] l2 + [0] [0 0] [0] = eq#2(l2) eq#2(dd(y,ys)) = [0 1] y + [0 1] ys + [0] [0 0] [0 0] [0] >= [0] [0] = #false() eq#2(nil()) = [0] [0] >= [0] [0] = #true() eq#3(dd(y,ys),x,xs) = [0 0] xs + [0 1] y + [0 1] ys + [0] [0 3] [0 1] [0 1] [0] >= [0 1] y + [0 1] ys + [0] [0 1] [0 0] [0] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0 0] xs + [0] [0 3] [0] >= [0] [0] = #false() nub(l) = [2 0] l + [0] [0 1] [0] >= [2 0] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [0 0] x + [2 4] xs + [0] [0 1] [0 1] [0] >= [0 0] x + [2 4] xs + [0] [0 1] [0 1] [0] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [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(dd(y,ys),x) = [0 1] y + [1 3] ys + [0] [0 1] [0 1] [0] >= [0 1] y + [1 3] ys + [0] [0 1] [0 1] [0] = 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] [0] >= [0 0] y + [1 3] ys + [0] [0 1] [0 1] [0] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [0 0] y + [1 3] ys + [0] [0 1] [0 1] [0] >= [1 1] ys + [0] [0 1] [0] = remove(x,ys) * Step 11: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #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#3(dd(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),#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(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(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: 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(and) = {1,2}, uargs(dd) = {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] [1] p(#eq) = [0] [1] p(#equal) = [0 0] x1 + [0 0] x2 + [0] [2 1] [1 2] [1] p(#false) = [0] [1] p(#neg) = [0 0] x1 + [2] [0 1] [0] p(#pos) = [0 2] x1 + [0] [0 0] [2] p(#s) = [1] [0] p(#true) = [0] [0] p(and) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] p(dd) = [0 0] x1 + [1 2] x2 + [1] [0 1] [0 1] [1] p(eq) = [0 1] x2 + [0] [0 0] [1] p(eq#1) = [0 1] x2 + [0] [0 0] [1] p(eq#2) = [0] [1] p(eq#3) = [0 1] x1 + [0] [0 0] [1] p(nil) = [0] [0] p(nub) = [2 0] x1 + [0] [0 1] [0] p(nub#1) = [2 0] x1 + [0] [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 2] x1 + [0 0] x3 + [1 3] x4 + [0] [0 0] [0 1] [0 1] [1] Following rules are strictly oriented: eq#3(dd(y,ys),x,xs) = [0 1] y + [0 1] ys + [1] [0 0] [0 0] [1] > [0 1] ys + [0] [0 0] [1] = and(#equal(x,y),eq(xs,ys)) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [0] [1] >= [0] [1] = #false() #and(#false(),#true()) = [0] [1] >= [0] [1] = #false() #and(#true(),#false()) = [0] [1] >= [0] [1] = #false() #and(#true(),#true()) = [0] [1] >= [0] [0] = #true() #eq(#0(),#0()) = [0] [1] >= [0] [0] = #true() #eq(#0(),#neg(y)) = [0] [1] >= [0] [1] = #false() #eq(#0(),#pos(y)) = [0] [1] >= [0] [1] = #false() #eq(#0(),#s(y)) = [0] [1] >= [0] [1] = #false() #eq(#neg(x),#0()) = [0] [1] >= [0] [1] = #false() #eq(#neg(x),#neg(y)) = [0] [1] >= [0] [1] = #eq(x,y) #eq(#neg(x),#pos(y)) = [0] [1] >= [0] [1] = #false() #eq(#pos(x),#0()) = [0] [1] >= [0] [1] = #false() #eq(#pos(x),#neg(y)) = [0] [1] >= [0] [1] = #false() #eq(#pos(x),#pos(y)) = [0] [1] >= [0] [1] = #eq(x,y) #eq(#s(x),#0()) = [0] [1] >= [0] [1] = #false() #eq(#s(x),#s(y)) = [0] [1] >= [0] [1] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0] [1] >= [0] [1] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [0] [1] >= [0] [1] = #false() #eq(nil(),dd(y'1,y'2)) = [0] [1] >= [0] [1] = #false() #eq(nil(),nil()) = [0] [1] >= [0] [0] = #true() #equal(x,y) = [0 0] x + [0 0] y + [0] [2 1] [1 2] [1] >= [0] [1] = #eq(x,y) and(x,y) = [2 0] x + [1 0] y + [0] [0 0] [0 0] [1] >= [2 0] x + [1 0] y + [0] [0 0] [0 0] [1] = #and(x,y) eq(l1,l2) = [0 1] l2 + [0] [0 0] [1] >= [0 1] l2 + [0] [0 0] [1] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0 1] l2 + [0] [0 0] [1] >= [0 1] l2 + [0] [0 0] [1] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0 1] l2 + [0] [0 0] [1] >= [0] [1] = eq#2(l2) eq#2(dd(y,ys)) = [0] [1] >= [0] [1] = #false() eq#2(nil()) = [0] [1] >= [0] [0] = #true() eq#3(nil(),x,xs) = [0] [1] >= [0] [1] = #false() nub(l) = [2 0] l + [0] [0 1] [0] >= [2 0] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [0 0] x + [2 4] xs + [2] [0 1] [0 1] [1] >= [0 0] x + [2 4] xs + [1] [0 1] [0 1] [1] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [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(dd(y,ys),x) = [0 1] y + [1 3] ys + [2] [0 1] [0 1] [1] >= [0 1] y + [1 3] ys + [2] [0 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) = [0 0] y + [1 3] ys + [2] [0 1] [0 1] [1] >= [0 0] y + [1 3] ys + [1] [0 1] [0 1] [1] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [0 0] y + [1 3] ys + [0] [0 1] [0 1] [1] >= [1 1] ys + [0] [0 1] [0] = remove(x,ys) * Step 12: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #eq(x,y) #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)) - 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),#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(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: 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(and) = {1,2}, uargs(dd) = {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] [1] p(#and) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(#eq) = [0 1] x2 + [0] [0 0] [1] p(#equal) = [0 0] x1 + [0 1] x2 + [0] [2 0] [2 2] [1] p(#false) = [0] [0] p(#neg) = [0 0] x1 + [0] [0 1] [0] p(#pos) = [0 0] x1 + [0] [0 1] [0] p(#s) = [0 0] x1 + [0] [0 1] [2] p(#true) = [0] [0] p(and) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(dd) = [0 0] x1 + [1 2] x2 + [0] [0 1] [0 1] [0] p(eq) = [0 1] x2 + [0] [2 0] [1] p(eq#1) = [0 1] x2 + [0] [0 0] [1] p(eq#2) = [0] [1] p(eq#3) = [0 1] x1 + [0] [0 0] [1] p(nil) = [0] [0] p(nub) = [2 2] x1 + [0] [0 1] [0] p(nub#1) = [2 2] x1 + [0] [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] [0] Following rules are strictly oriented: #eq(#s(x),#s(y)) = [0 1] y + [2] [0 0] [1] > [0 1] y + [0] [0 0] [1] = #eq(x,y) 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()) = [1] [1] >= [0] [0] = #true() #eq(#0(),#neg(y)) = [0 1] y + [0] [0 0] [1] >= [0] [0] = #false() #eq(#0(),#pos(y)) = [0 1] y + [0] [0 0] [1] >= [0] [0] = #false() #eq(#0(),#s(y)) = [0 1] y + [2] [0 0] [1] >= [0] [0] = #false() #eq(#neg(x),#0()) = [1] [1] >= [0] [0] = #false() #eq(#neg(x),#neg(y)) = [0 1] y + [0] [0 0] [1] >= [0 1] y + [0] [0 0] [1] = #eq(x,y) #eq(#neg(x),#pos(y)) = [0 1] y + [0] [0 0] [1] >= [0] [0] = #false() #eq(#pos(x),#0()) = [1] [1] >= [0] [0] = #false() #eq(#pos(x),#neg(y)) = [0 1] y + [0] [0 0] [1] >= [0] [0] = #false() #eq(#pos(x),#pos(y)) = [0 1] y + [0] [0 0] [1] >= [0 1] y + [0] [0 0] [1] = #eq(x,y) #eq(#s(x),#0()) = [1] [1] >= [0] [0] = #false() #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [1] >= [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [0] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [0] [1] >= [0] [0] = #false() #eq(nil(),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [1] >= [0] [0] = #false() #eq(nil(),nil()) = [0] [1] >= [0] [0] = #true() #equal(x,y) = [0 0] x + [0 1] y + [0] [2 0] [2 2] [1] >= [0 1] y + [0] [0 0] [1] = #eq(x,y) and(x,y) = [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] = #and(x,y) eq(l1,l2) = [0 1] l2 + [0] [2 0] [1] >= [0 1] l2 + [0] [0 0] [1] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0 1] l2 + [0] [0 0] [1] >= [0 1] l2 + [0] [0 0] [1] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0 1] l2 + [0] [0 0] [1] >= [0] [1] = eq#2(l2) eq#2(dd(y,ys)) = [0] [1] >= [0] [0] = #false() eq#2(nil()) = [0] [1] >= [0] [0] = #true() eq#3(dd(y,ys),x,xs) = [0 1] y + [0 1] ys + [0] [0 0] [0 0] [1] >= [0 1] y + [0 1] ys + [0] [0 0] [0 0] [0] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] [1] >= [0] [0] = #false() nub(l) = [2 2] l + [0] [0 1] [0] >= [2 2] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [0 2] x + [2 6] xs + [0] [0 1] [0 1] [0] >= [0 0] x + [2 6] xs + [0] [0 1] [0 1] [0] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [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(dd(y,ys),x) = [0 1] y + [1 3] ys + [0] [0 1] [0 1] [0] >= [0 1] y + [1 3] ys + [0] [0 1] [0 1] [0] = 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] [0] >= [0 0] y + [1 3] ys + [0] [0 1] [0 1] [0] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [0 0] y + [1 3] ys + [0] [0 1] [0 1] [0] >= [1 1] ys + [0] [0 1] [0] = remove(x,ys) * Step 13: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(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)) - 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),#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),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: 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(and) = {1,2}, uargs(dd) = {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] [0] p(#and) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(#eq) = [0 0] x1 + [0 1] x2 + [0] [0 1] [0 0] [0] p(#equal) = [0 0] x1 + [0 1] x2 + [2] [2 2] [0 0] [0] p(#false) = [0] [0] p(#neg) = [1 0] x1 + [0] [0 1] [0] p(#pos) = [0 1] x1 + [0] [0 1] [0] p(#s) = [0 0] x1 + [1] [0 1] [0] p(#true) = [0] [0] p(and) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(dd) = [1 0] x1 + [1 2] x2 + [0] [0 1] [0 1] [2] p(eq) = [0 0] x1 + [0 1] x2 + [0] [0 2] [1 1] [0] p(eq#1) = [0 1] x2 + [0] [0 1] [0] p(eq#2) = [0 0] x1 + [0] [0 1] [0] p(eq#3) = [0 1] x1 + [0] [0 0] [0] p(nil) = [0] [0] p(nub) = [2 0] x1 + [0] [0 1] [0] p(nub#1) = [2 0] x1 + [0] [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 + [1 0] x3 + [1 3] x4 + [0] [0 0] [0 1] [0 1] [2] Following rules are strictly oriented: #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0 0] x'1 + [0 0] x'2 + [0 1] y'1 + [0 1] y'2 + [2] [0 1] [0 1] [0 0] [0 0] [2] > [0 1] y'1 + [0 1] y'2 + [0] [0 0] [0 0] [0] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) 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] [0] >= [0] [0] = #true() #eq(#0(),#neg(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#pos(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#s(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#neg(x),#0()) = [0 0] x + [0] [0 1] [0] >= [0] [0] = #false() #eq(#neg(x),#neg(y)) = [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] >= [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] = #eq(x,y) #eq(#neg(x),#pos(y)) = [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] >= [0] [0] = #false() #eq(#pos(x),#0()) = [0 0] x + [0] [0 1] [0] >= [0] [0] = #false() #eq(#pos(x),#neg(y)) = [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] >= [0] [0] = #false() #eq(#pos(x),#pos(y)) = [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] >= [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] = #eq(x,y) #eq(#s(x),#0()) = [0 0] x + [0] [0 1] [0] >= [0] [0] = #false() #eq(#s(x),#s(y)) = [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] >= [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] = #eq(x,y) #eq(dd(x'1,x'2),nil()) = [0 0] x'1 + [0 0] x'2 + [0] [0 1] [0 1] [2] >= [0] [0] = #false() #eq(nil(),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [2] [0 0] [0 0] [0] >= [0] [0] = #false() #eq(nil(),nil()) = [0] [0] >= [0] [0] = #true() #equal(x,y) = [0 0] x + [0 1] y + [2] [2 2] [0 0] [0] >= [0 0] x + [0 1] y + [0] [0 1] [0 0] [0] = #eq(x,y) and(x,y) = [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] >= [1 0] x + [1 0] y + [0] [0 0] [0 0] [0] = #and(x,y) eq(l1,l2) = [0 0] l1 + [0 1] l2 + [0] [0 2] [1 1] [0] >= [0 1] l2 + [0] [0 1] [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0 1] l2 + [0] [0 1] [0] >= [0 1] l2 + [0] [0 0] [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0 1] l2 + [0] [0 1] [0] >= [0 0] l2 + [0] [0 1] [0] = eq#2(l2) eq#2(dd(y,ys)) = [0 0] y + [0 0] ys + [0] [0 1] [0 1] [2] >= [0] [0] = #false() eq#2(nil()) = [0] [0] >= [0] [0] = #true() eq#3(dd(y,ys),x,xs) = [0 1] y + [0 1] ys + [2] [0 0] [0 0] [0] >= [0 1] y + [0 1] ys + [2] [0 0] [0 0] [0] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [0] [0] >= [0] [0] = #false() nub(l) = [2 0] l + [0] [0 1] [0] >= [2 0] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [2 0] x + [2 4] xs + [0] [0 1] [0 1] [2] >= [1 0] x + [2 4] xs + [0] [0 1] [0 1] [2] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [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(dd(y,ys),x) = [1 1] y + [1 3] ys + [2] [0 1] [0 1] [2] >= [1 1] y + [1 3] ys + [0] [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) = [1 0] y + [1 3] ys + [0] [0 1] [0 1] [2] >= [1 0] y + [1 3] ys + [0] [0 1] [0 1] [2] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [1 0] y + [1 3] ys + [0] [0 1] [0 1] [2] >= [1 1] ys + [0] [0 1] [0] = remove(x,ys) * Step 14: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #eq(#neg(x),#neg(y)) -> #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),#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: 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(and) = {1,2}, uargs(dd) = {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] [0] p(#and) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [0] p(#eq) = [0 1] x2 + [0] [0 0] [0] p(#equal) = [0 0] x1 + [0 1] x2 + [0] [2 0] [0 0] [0] p(#false) = [0] [0] p(#neg) = [0 2] x1 + [0] [0 1] [2] p(#pos) = [0 0] x1 + [1] [0 1] [2] p(#s) = [0 0] x1 + [0] [0 1] [0] p(#true) = [0] [0] p(and) = [1 0] x1 + [1 0] x2 + [1] [0 0] [2 0] [0] p(dd) = [0 0] x1 + [1 2] x2 + [0] [0 1] [0 1] [1] p(eq) = [0 0] x1 + [0 1] x2 + [0] [2 2] [2 3] [0] p(eq#1) = [0 0] x1 + [0 1] x2 + [0] [0 1] [0 3] [0] p(eq#2) = [0] [0] p(eq#3) = [0 1] x1 + [0] [0 2] [0] p(nil) = [0] [1] p(nub) = [3 1] x1 + [0] [0 1] [0] p(nub#1) = [3 0] x1 + [0] [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] [1] Following rules are strictly oriented: #eq(#neg(x),#neg(y)) = [0 1] y + [2] [0 0] [0] > [0 1] y + [0] [0 0] [0] = #eq(x,y) Following rules are (at-least) weakly oriented: #and(#false(),#false()) = [1] [0] >= [0] [0] = #false() #and(#false(),#true()) = [1] [0] >= [0] [0] = #false() #and(#true(),#false()) = [1] [0] >= [0] [0] = #false() #and(#true(),#true()) = [1] [0] >= [0] [0] = #true() #eq(#0(),#0()) = [0] [0] >= [0] [0] = #true() #eq(#0(),#neg(y)) = [0 1] y + [2] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#pos(y)) = [0 1] y + [2] [0 0] [0] >= [0] [0] = #false() #eq(#0(),#s(y)) = [0 1] y + [0] [0 0] [0] >= [0] [0] = #false() #eq(#neg(x),#0()) = [0] [0] >= [0] [0] = #false() #eq(#neg(x),#pos(y)) = [0 1] y + [2] [0 0] [0] >= [0] [0] = #false() #eq(#pos(x),#0()) = [0] [0] >= [0] [0] = #false() #eq(#pos(x),#neg(y)) = [0 1] y + [2] [0 0] [0] >= [0] [0] = #false() #eq(#pos(x),#pos(y)) = [0 1] y + [2] [0 0] [0] >= [0 1] y + [0] [0 0] [0] = #eq(x,y) #eq(#s(x),#0()) = [0] [0] >= [0] [0] = #false() #eq(#s(x),#s(y)) = [0 1] y + [0] [0 0] [0] >= [0 1] y + [0] [0 0] [0] = #eq(x,y) #eq(dd(x'1,x'2),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [1] [0 0] [0 0] [0] >= [0 1] y'1 + [0 1] y'2 + [1] [0 0] [0 0] [0] = #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) = [1] [0] >= [0] [0] = #false() #eq(nil(),dd(y'1,y'2)) = [0 1] y'1 + [0 1] y'2 + [1] [0 0] [0 0] [0] >= [0] [0] = #false() #eq(nil(),nil()) = [1] [0] >= [0] [0] = #true() #equal(x,y) = [0 0] x + [0 1] y + [0] [2 0] [0 0] [0] >= [0 1] y + [0] [0 0] [0] = #eq(x,y) and(x,y) = [1 0] x + [1 0] y + [1] [0 0] [2 0] [0] >= [1 0] x + [1 0] y + [1] [0 0] [0 0] [0] = #and(x,y) eq(l1,l2) = [0 0] l1 + [0 1] l2 + [0] [2 2] [2 3] [0] >= [0 0] l1 + [0 1] l2 + [0] [0 1] [0 3] [0] = eq#1(l1,l2) eq#1(dd(x,xs),l2) = [0 1] l2 + [0 0] x + [0 0] xs + [0] [0 3] [0 1] [0 1] [1] >= [0 1] l2 + [0] [0 2] [0] = eq#3(l2,x,xs) eq#1(nil(),l2) = [0 1] l2 + [0] [0 3] [1] >= [0] [0] = eq#2(l2) eq#2(dd(y,ys)) = [0] [0] >= [0] [0] = #false() eq#2(nil()) = [0] [0] >= [0] [0] = #true() eq#3(dd(y,ys),x,xs) = [0 1] y + [0 1] ys + [1] [0 2] [0 2] [2] >= [0 1] y + [0 1] ys + [1] [0 0] [0 2] [0] = and(#equal(x,y),eq(xs,ys)) eq#3(nil(),x,xs) = [1] [2] >= [0] [0] = #false() nub(l) = [3 1] l + [0] [0 1] [0] >= [3 0] l + [0] [0 1] [0] = nub#1(l) nub#1(dd(x,xs)) = [0 0] x + [3 6] xs + [0] [0 1] [0 1] [1] >= [0 0] x + [3 6] xs + [0] [0 1] [0 1] [1] = dd(x,nub(remove(x,xs))) nub#1(nil()) = [0] [1] >= [0] [1] = nil() remove(x,l) = [1 1] l + [0] [0 1] [0] >= [1 1] l + [0] [0 1] [0] = remove#1(l,x) remove#1(dd(y,ys),x) = [0 1] y + [1 3] ys + [1] [0 1] [0 1] [1] >= [0 1] y + [1 3] ys + [0] [0 1] [0 1] [1] = remove#2(eq(x,y),x,y,ys) remove#1(nil(),x) = [1] [1] >= [0] [1] = nil() remove#2(#false(),x,y,ys) = [0 0] y + [1 3] ys + [0] [0 1] [0 1] [1] >= [0 0] y + [1 3] ys + [0] [0 1] [0 1] [1] = dd(y,remove(x,ys)) remove#2(#true(),x,y,ys) = [0 0] y + [1 3] ys + [0] [0 1] [0 1] [1] >= [1 1] ys + [0] [0 1] [0] = remove(x,ys) * Step 15: 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() 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))