YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { group3#1(nil()) -> nil() , group3#2(nil(), @x) -> nil() , group3#3(nil(), @x, @y) -> nil() , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(nil(), @l3, @x, @xs) -> nil() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [2] x1 + [0] [group3#1](x1) = [2] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [group3#2](x1, x2) = [2] x1 + [0] [nil] = [2] [group3#3](x1, x2, x3) = [2] x1 + [0] [tuple#3](x1, x2, x3) = [0] [zip3](x1, x2, x3) = [2] x1 + [2] x2 + [1] x3 + [0] [zip3#1](x1, x2, x3) = [2] x1 + [2] x2 + [1] x3 + [0] [zip3#2](x1, x2, x3, x4) = [2] x1 + [1] x2 + [2] x4 + [0] [zip3#3](x1, x2, x3, x4, x5) = [1] x1 + [2] x3 + [2] x5 + [0] This order satisfies following ordering constraints [group3(@l)] = [2] @l + [0] >= [2] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [2] @x + [2] @xs + [0] >= [2] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [4] > [2] = [nil()] [group3#2(::(@y, @ys), @x)] = [2] @y + [2] @ys + [0] >= [2] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [4] > [2] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [2] @z + [2] @zs + [0] >= [2] @zs + [0] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [4] > [2] = [nil()] [zip3(@l1, @l2, @l3)] = [2] @l1 + [2] @l2 + [1] @l3 + [0] >= [2] @l1 + [2] @l2 + [1] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [2] @l2 + [1] @l3 + [2] @x + [2] @xs + [0] >= [2] @l2 + [1] @l3 + [2] @xs + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [2] @l2 + [1] @l3 + [4] > [2] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [1] @l3 + [2] @xs + [2] @y + [2] @ys + [0] >= [1] @l3 + [2] @xs + [2] @ys + [0] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [1] @l3 + [2] @xs + [4] > [2] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @xs + [2] @ys + [1] @z + [1] @zs + [0] >= [2] @xs + [2] @ys + [1] @zs + [0] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [2] @xs + [2] @ys + [2] >= [2] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Weak Trs: { group3#1(nil()) -> nil() , group3#2(nil(), @x) -> nil() , group3#3(nil(), @x, @y) -> nil() , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(nil(), @l3, @x, @xs) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [1] x1 + [0] [group3#1](x1) = [1] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [group3#2](x1, x2) = [1] x1 + [0] [nil] = [1] [group3#3](x1, x2, x3) = [1] x1 + [0] [tuple#3](x1, x2, x3) = [0] [zip3](x1, x2, x3) = [1] x1 + [1] x2 + [2] x3 + [0] [zip3#1](x1, x2, x3) = [1] x1 + [1] x2 + [2] x3 + [0] [zip3#2](x1, x2, x3, x4) = [1] x1 + [2] x2 + [1] x4 + [0] [zip3#3](x1, x2, x3, x4, x5) = [2] x1 + [1] x3 + [1] x5 + [0] This order satisfies following ordering constraints [group3(@l)] = [1] @l + [0] >= [1] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [1] @x + [1] @xs + [0] >= [1] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [1] >= [1] = [nil()] [group3#2(::(@y, @ys), @x)] = [1] @y + [1] @ys + [0] >= [1] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [1] >= [1] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [1] @z + [1] @zs + [0] >= [1] @zs + [0] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [1] >= [1] = [nil()] [zip3(@l1, @l2, @l3)] = [1] @l1 + [1] @l2 + [2] @l3 + [0] >= [1] @l1 + [1] @l2 + [2] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [1] @l2 + [2] @l3 + [1] @x + [1] @xs + [0] >= [1] @l2 + [2] @l3 + [1] @xs + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [1] @l2 + [2] @l3 + [1] >= [1] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [2] @l3 + [1] @xs + [1] @y + [1] @ys + [0] >= [2] @l3 + [1] @xs + [1] @ys + [0] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [2] @l3 + [1] @xs + [1] >= [1] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [1] @xs + [1] @ys + [2] @z + [2] @zs + [0] >= [1] @xs + [1] @ys + [2] @zs + [0] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [1] @xs + [1] @ys + [2] > [1] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) } Weak Trs: { group3#1(nil()) -> nil() , group3#2(nil(), @x) -> nil() , group3#3(nil(), @x, @y) -> nil() , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [2] x1 + [2] [group3#1](x1) = [2] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [2] [group3#2](x1, x2) = [2] x1 + [0] [nil] = [0] [group3#3](x1, x2, x3) = [2] x1 + [0] [tuple#3](x1, x2, x3) = [0] [zip3](x1, x2, x3) = [2] x3 + [2] [zip3#1](x1, x2, x3) = [2] x3 + [0] [zip3#2](x1, x2, x3, x4) = [2] x2 + [0] [zip3#3](x1, x2, x3, x4, x5) = [2] x1 + [0] This order satisfies following ordering constraints [group3(@l)] = [2] @l + [2] > [2] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [2] @x + [2] @xs + [4] > [2] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [0] >= [0] = [nil()] [group3#2(::(@y, @ys), @x)] = [2] @y + [2] @ys + [4] > [2] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [0] >= [0] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [2] @z + [2] @zs + [4] >= [2] @zs + [4] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [0] >= [0] = [nil()] [zip3(@l1, @l2, @l3)] = [2] @l3 + [2] > [2] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [2] @l3 + [0] >= [2] @l3 + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [2] @l3 + [0] >= [0] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [2] @l3 + [0] >= [2] @l3 + [0] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [2] @l3 + [0] >= [0] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @z + [2] @zs + [4] >= [2] @zs + [4] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [0] >= [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [2] x1 + [0] [group3#1](x1) = [2] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [2] [group3#2](x1, x2) = [2] x1 + [0] [nil] = [0] [group3#3](x1, x2, x3) = [2] x1 + [0] [tuple#3](x1, x2, x3) = [2] [zip3](x1, x2, x3) = [2] x1 + [2] x3 + [0] [zip3#1](x1, x2, x3) = [2] x1 + [2] x3 + [0] [zip3#2](x1, x2, x3, x4) = [2] x2 + [2] x4 + [0] [zip3#3](x1, x2, x3, x4, x5) = [2] x1 + [2] x3 + [0] This order satisfies following ordering constraints [group3(@l)] = [2] @l + [0] >= [2] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [2] @x + [2] @xs + [4] > [2] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [0] >= [0] = [nil()] [group3#2(::(@y, @ys), @x)] = [2] @y + [2] @ys + [4] > [2] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [0] >= [0] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [2] @z + [2] @zs + [4] >= [2] @zs + [4] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [0] >= [0] = [nil()] [zip3(@l1, @l2, @l3)] = [2] @l1 + [2] @l3 + [0] >= [2] @l1 + [2] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [2] @l3 + [2] @x + [2] @xs + [4] > [2] @l3 + [2] @xs + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [2] @l3 + [0] >= [0] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [2] @l3 + [2] @xs + [0] >= [2] @l3 + [2] @xs + [0] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [2] @l3 + [2] @xs + [0] >= [0] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @xs + [2] @z + [2] @zs + [4] >= [2] @xs + [2] @zs + [4] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [2] @xs + [0] >= [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@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() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [2] x1 + [1] [group3#1](x1) = [2] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [2] [group3#2](x1, x2) = [2] x1 + [0] [nil] = [0] [group3#3](x1, x2, x3) = [2] x1 + [0] [tuple#3](x1, x2, x3) = [0] [zip3](x1, x2, x3) = [2] x3 + [2] [zip3#1](x1, x2, x3) = [2] x3 + [0] [zip3#2](x1, x2, x3, x4) = [2] x2 + [0] [zip3#3](x1, x2, x3, x4, x5) = [2] x1 + [0] This order satisfies following ordering constraints [group3(@l)] = [2] @l + [1] > [2] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [2] @x + [2] @xs + [4] > [2] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [0] >= [0] = [nil()] [group3#2(::(@y, @ys), @x)] = [2] @y + [2] @ys + [4] > [2] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [0] >= [0] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [2] @z + [2] @zs + [4] > [2] @zs + [3] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [0] >= [0] = [nil()] [zip3(@l1, @l2, @l3)] = [2] @l3 + [2] > [2] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [2] @l3 + [0] >= [2] @l3 + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [2] @l3 + [0] >= [0] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [2] @l3 + [0] >= [2] @l3 + [0] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [2] @l3 + [0] >= [0] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @z + [2] @zs + [4] >= [2] @zs + [4] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [0] >= [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) } Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@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() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(::) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [group3](x1) = [2] x1 + [0] [group3#1](x1) = [2] x1 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [2] [group3#2](x1, x2) = [2] x1 + [0] [nil] = [0] [group3#3](x1, x2, x3) = [2] x1 + [0] [tuple#3](x1, x2, x3) = [1] [zip3](x1, x2, x3) = [2] x2 + [1] x3 + [0] [zip3#1](x1, x2, x3) = [2] x2 + [1] x3 + [0] [zip3#2](x1, x2, x3, x4) = [2] x1 + [1] x2 + [0] [zip3#3](x1, x2, x3, x4, x5) = [1] x1 + [2] x5 + [2] This order satisfies following ordering constraints [group3(@l)] = [2] @l + [0] >= [2] @l + [0] = [group3#1(@l)] [group3#1(::(@x, @xs))] = [2] @x + [2] @xs + [4] > [2] @xs + [0] = [group3#2(@xs, @x)] [group3#1(nil())] = [0] >= [0] = [nil()] [group3#2(::(@y, @ys), @x)] = [2] @y + [2] @ys + [4] > [2] @ys + [0] = [group3#3(@ys, @x, @y)] [group3#2(nil(), @x)] = [0] >= [0] = [nil()] [group3#3(::(@z, @zs), @x, @y)] = [2] @z + [2] @zs + [4] > [2] @zs + [3] = [::(tuple#3(@x, @y, @z), group3(@zs))] [group3#3(nil(), @x, @y)] = [0] >= [0] = [nil()] [zip3(@l1, @l2, @l3)] = [2] @l2 + [1] @l3 + [0] >= [2] @l2 + [1] @l3 + [0] = [zip3#1(@l1, @l2, @l3)] [zip3#1(::(@x, @xs), @l2, @l3)] = [2] @l2 + [1] @l3 + [0] >= [2] @l2 + [1] @l3 + [0] = [zip3#2(@l2, @l3, @x, @xs)] [zip3#1(nil(), @l2, @l3)] = [2] @l2 + [1] @l3 + [0] >= [0] = [nil()] [zip3#2(::(@y, @ys), @l3, @x, @xs)] = [1] @l3 + [2] @y + [2] @ys + [4] > [1] @l3 + [2] @ys + [2] = [zip3#3(@l3, @x, @xs, @y, @ys)] [zip3#2(nil(), @l3, @x, @xs)] = [1] @l3 + [0] >= [0] = [nil()] [zip3#3(::(@z, @zs), @x, @xs, @y, @ys)] = [2] @ys + [1] @z + [1] @zs + [4] > [2] @ys + [1] @zs + [3] = [::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))] [zip3#3(nil(), @x, @xs, @y, @ys)] = [2] @ys + [2] > [0] = [nil()] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { group3(@l) -> group3#1(@l) , group3#1(::(@x, @xs)) -> group3#2(@xs, @x) , group3#1(nil()) -> nil() , group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) , group3#2(nil(), @x) -> nil() , group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) , group3#3(nil(), @x, @y) -> nil() , zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) , zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) , zip3#1(nil(), @l2, @l3) -> nil() , zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) , zip3#2(nil(), @l3, @x, @xs) -> nil() , zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) , zip3#3(nil(), @x, @xs, @y, @ys) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))