WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: group3(l) -> group3#1(l) group3#1(cons(x,xs)) -> group3#2(xs,x) group3#1(nil()) -> nil() group3#2(cons(y,ys),x) -> group3#3(ys,x,y) group3#2(nil(),x) -> nil() group3#3(cons(z,zs),x,y) -> cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) -> nil() zip3(l1,l2,l3) -> zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) -> zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) -> nil() zip3#2(cons(y,ys),l3,x,xs) -> zip3#3(l3,x,xs,y,ys) zip3#2(nil(),l3,x,xs) -> nil() zip3#3(cons(z,zs),x,xs,y,ys) -> cons(tuple#3(x,y,z),zip3(xs,ys,zs)) zip3#3(nil(),x,xs,y,ys) -> nil() - Signature: {group3/1,group3#1/1,group3#2/2,group3#3/3,zip3/3,zip3#1/3,zip3#2/4,zip3#3/5} / {cons/2,nil/0,tuple#3/3} - Obligation: innermost runtime complexity wrt. defined symbols {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2 ,zip3#3} and constructors {cons,nil,tuple#3} + 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(cons) = {2} Following symbols are considered usable: {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2,zip3#3} TcT has computed the following interpretation: p(cons) = [1] x1 + [1] x2 + [4] p(group3) = [4] x1 + [3] p(group3#1) = [4] x1 + [3] p(group3#2) = [4] x1 + [4] x2 + [11] p(group3#3) = [4] x1 + [1] x3 + [0] p(nil) = [3] p(tuple#3) = [0] p(zip3) = [2] x1 + [2] x2 + [8] p(zip3#1) = [2] x1 + [2] x2 + [1] p(zip3#2) = [2] x1 + [2] x3 + [2] x4 + [4] p(zip3#3) = [2] x2 + [2] x3 + [2] x4 + [2] x5 + [12] Following rules are strictly oriented: group3#1(cons(x,xs)) = [4] x + [4] xs + [19] > [4] x + [4] xs + [11] = group3#2(xs,x) group3#1(nil()) = [15] > [3] = nil() group3#2(cons(y,ys),x) = [4] x + [4] y + [4] ys + [27] > [1] y + [4] ys + [0] = group3#3(ys,x,y) group3#2(nil(),x) = [4] x + [23] > [3] = nil() group3#3(cons(z,zs),x,y) = [1] y + [4] z + [4] zs + [16] > [4] zs + [7] = cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) = [1] y + [12] > [3] = nil() zip3(l1,l2,l3) = [2] l1 + [2] l2 + [8] > [2] l1 + [2] l2 + [1] = zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) = [2] l2 + [2] x + [2] xs + [9] > [2] l2 + [2] x + [2] xs + [4] = zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) = [2] l2 + [7] > [3] = nil() zip3#2(nil(),l3,x,xs) = [2] x + [2] xs + [10] > [3] = nil() zip3#3(nil(),x,xs,y,ys) = [2] x + [2] xs + [2] y + [2] ys + [12] > [3] = nil() Following rules are (at-least) weakly oriented: group3(l) = [4] l + [3] >= [4] l + [3] = group3#1(l) zip3#2(cons(y,ys),l3,x,xs) = [2] x + [2] xs + [2] y + [2] ys + [12] >= [2] x + [2] xs + [2] y + [2] ys + [12] = zip3#3(l3,x,xs,y,ys) zip3#3(cons(z,zs),x,xs,y,ys) = [2] x + [2] xs + [2] y + [2] ys + [12] >= [2] xs + [2] ys + [12] = cons(tuple#3(x,y,z),zip3(xs,ys,zs)) * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: group3(l) -> group3#1(l) zip3#2(cons(y,ys),l3,x,xs) -> zip3#3(l3,x,xs,y,ys) zip3#3(cons(z,zs),x,xs,y,ys) -> cons(tuple#3(x,y,z),zip3(xs,ys,zs)) - Weak TRS: group3#1(cons(x,xs)) -> group3#2(xs,x) group3#1(nil()) -> nil() group3#2(cons(y,ys),x) -> group3#3(ys,x,y) group3#2(nil(),x) -> nil() group3#3(cons(z,zs),x,y) -> cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) -> nil() zip3(l1,l2,l3) -> zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) -> zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) -> nil() zip3#2(nil(),l3,x,xs) -> nil() zip3#3(nil(),x,xs,y,ys) -> nil() - Signature: {group3/1,group3#1/1,group3#2/2,group3#3/3,zip3/3,zip3#1/3,zip3#2/4,zip3#3/5} / {cons/2,nil/0,tuple#3/3} - Obligation: innermost runtime complexity wrt. defined symbols {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2 ,zip3#3} and constructors {cons,nil,tuple#3} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {2} Following symbols are considered usable: {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2,zip3#3} TcT has computed the following interpretation: p(cons) = 2 + x2 p(group3) = 4*x1 p(group3#1) = 4*x1 p(group3#2) = 4*x1 p(group3#3) = 4*x1 p(nil) = 2 p(tuple#3) = x1 p(zip3) = 6*x1 p(zip3#1) = 6*x1 p(zip3#2) = 6 + 6*x4 p(zip3#3) = 4 + 6*x3 Following rules are strictly oriented: zip3#2(cons(y,ys),l3,x,xs) = 6 + 6*xs > 4 + 6*xs = zip3#3(l3,x,xs,y,ys) zip3#3(cons(z,zs),x,xs,y,ys) = 4 + 6*xs > 2 + 6*xs = cons(tuple#3(x,y,z),zip3(xs,ys,zs)) Following rules are (at-least) weakly oriented: group3(l) = 4*l >= 4*l = group3#1(l) group3#1(cons(x,xs)) = 8 + 4*xs >= 4*xs = group3#2(xs,x) group3#1(nil()) = 8 >= 2 = nil() group3#2(cons(y,ys),x) = 8 + 4*ys >= 4*ys = group3#3(ys,x,y) group3#2(nil(),x) = 8 >= 2 = nil() group3#3(cons(z,zs),x,y) = 8 + 4*zs >= 2 + 4*zs = cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) = 8 >= 2 = nil() zip3(l1,l2,l3) = 6*l1 >= 6*l1 = zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) = 12 + 6*xs >= 6 + 6*xs = zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) = 12 >= 2 = nil() zip3#2(nil(),l3,x,xs) = 6 + 6*xs >= 2 = nil() zip3#3(nil(),x,xs,y,ys) = 4 + 6*xs >= 2 = nil() * Step 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: group3(l) -> group3#1(l) - Weak TRS: group3#1(cons(x,xs)) -> group3#2(xs,x) group3#1(nil()) -> nil() group3#2(cons(y,ys),x) -> group3#3(ys,x,y) group3#2(nil(),x) -> nil() group3#3(cons(z,zs),x,y) -> cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) -> nil() zip3(l1,l2,l3) -> zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) -> zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) -> nil() zip3#2(cons(y,ys),l3,x,xs) -> zip3#3(l3,x,xs,y,ys) zip3#2(nil(),l3,x,xs) -> nil() zip3#3(cons(z,zs),x,xs,y,ys) -> cons(tuple#3(x,y,z),zip3(xs,ys,zs)) zip3#3(nil(),x,xs,y,ys) -> nil() - Signature: {group3/1,group3#1/1,group3#2/2,group3#3/3,zip3/3,zip3#1/3,zip3#2/4,zip3#3/5} / {cons/2,nil/0,tuple#3/3} - Obligation: innermost runtime complexity wrt. defined symbols {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2 ,zip3#3} and constructors {cons,nil,tuple#3} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {2} Following symbols are considered usable: {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2,zip3#3} TcT has computed the following interpretation: p(cons) = 2 + x1 + x2 p(group3) = 4 + 4*x1 p(group3#1) = 4*x1 p(group3#2) = 1 + 4*x1 p(group3#3) = 4*x1 p(nil) = 0 p(tuple#3) = 2 p(zip3) = 7 + x1 + 4*x2 + 4*x3 p(zip3#1) = x1 + 4*x2 + 4*x3 p(zip3#2) = 4*x1 + 4*x2 + x3 + x4 p(zip3#3) = 3 + 4*x1 + x3 + 4*x5 Following rules are strictly oriented: group3(l) = 4 + 4*l > 4*l = group3#1(l) Following rules are (at-least) weakly oriented: group3#1(cons(x,xs)) = 8 + 4*x + 4*xs >= 1 + 4*xs = group3#2(xs,x) group3#1(nil()) = 0 >= 0 = nil() group3#2(cons(y,ys),x) = 9 + 4*y + 4*ys >= 4*ys = group3#3(ys,x,y) group3#2(nil(),x) = 1 >= 0 = nil() group3#3(cons(z,zs),x,y) = 8 + 4*z + 4*zs >= 8 + 4*zs = cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) = 0 >= 0 = nil() zip3(l1,l2,l3) = 7 + l1 + 4*l2 + 4*l3 >= l1 + 4*l2 + 4*l3 = zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) = 2 + 4*l2 + 4*l3 + x + xs >= 4*l2 + 4*l3 + x + xs = zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) = 4*l2 + 4*l3 >= 0 = nil() zip3#2(cons(y,ys),l3,x,xs) = 8 + 4*l3 + x + xs + 4*y + 4*ys >= 3 + 4*l3 + xs + 4*ys = zip3#3(l3,x,xs,y,ys) zip3#2(nil(),l3,x,xs) = 4*l3 + x + xs >= 0 = nil() zip3#3(cons(z,zs),x,xs,y,ys) = 11 + xs + 4*ys + 4*z + 4*zs >= 11 + xs + 4*ys + 4*zs = cons(tuple#3(x,y,z),zip3(xs,ys,zs)) zip3#3(nil(),x,xs,y,ys) = 3 + xs + 4*ys >= 0 = nil() * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: group3(l) -> group3#1(l) group3#1(cons(x,xs)) -> group3#2(xs,x) group3#1(nil()) -> nil() group3#2(cons(y,ys),x) -> group3#3(ys,x,y) group3#2(nil(),x) -> nil() group3#3(cons(z,zs),x,y) -> cons(tuple#3(x,y,z),group3(zs)) group3#3(nil(),x,y) -> nil() zip3(l1,l2,l3) -> zip3#1(l1,l2,l3) zip3#1(cons(x,xs),l2,l3) -> zip3#2(l2,l3,x,xs) zip3#1(nil(),l2,l3) -> nil() zip3#2(cons(y,ys),l3,x,xs) -> zip3#3(l3,x,xs,y,ys) zip3#2(nil(),l3,x,xs) -> nil() zip3#3(cons(z,zs),x,xs,y,ys) -> cons(tuple#3(x,y,z),zip3(xs,ys,zs)) zip3#3(nil(),x,xs,y,ys) -> nil() - Signature: {group3/1,group3#1/1,group3#2/2,group3#3/3,zip3/3,zip3#1/3,zip3#2/4,zip3#3/5} / {cons/2,nil/0,tuple#3/3} - Obligation: innermost runtime complexity wrt. defined symbols {group3,group3#1,group3#2,group3#3,zip3,zip3#1,zip3#2 ,zip3#3} and constructors {cons,nil,tuple#3} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))