Problem:
 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()

Proof:
 Complexity Transformation Processor:
  strict:
   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()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [zip3#3](x0, x1, x2, x3, x4) = x0 + x1 + x2 + x3 + x4 + 1,
     
     [zip3#2](x0, x1, x2, x3) = x0 + x1 + x2 + x3,
     
     [zip3#1](x0, x1, x2) = x0 + x1 + x2,
     
     [zip3](x0, x1, x2) = x0 + x1 + x2,
     
     [tuple#3](x0, x1, x2) = x0 + x1 + x2,
     
     [group3#3](x0, x1, x2) = x0 + x1 + x2,
     
     [nil] = 12,
     
     [group3#2](x0, x1) = x0 + x1,
     
     [::](x0, x1) = x0 + x1,
     
     [group3#1](x0) = x0 + 4,
     
     [group3](x0) = x0
    orientation:
     group3(@l) = @l >= @l + 4 = group3#1(@l)
     
     group3#1(::(@x,@xs)) = @x + @xs + 4 >= @x + @xs = group3#2(@xs,@x)
     
     group3#1(nil()) = 16 >= 12 = nil()
     
     group3#2(::(@y,@ys),@x) = @x + @y + @ys >= @x + @y + @ys = group3#3(@ys,@x,@y)
     
     group3#2(nil(),@x) = @x + 12 >= 12 = nil()
     
     group3#3(::(@z,@zs),@x,@y) = @x + @y + @z + @zs >= @x + @y + @z + @zs = ::(tuple#3(@x,@y,@z),group3(@zs))
     
     group3#3(nil(),@x,@y) = @x + @y + 12 >= 12 = nil()
     
     zip3(@l1,@l2,@l3) = @l1 + @l2 + @l3 >= @l1 + @l2 + @l3 = zip3#1(@l1,@l2,@l3)
     
     zip3#1(::(@x,@xs),@l2,@l3) = @l2 + @l3 + @x + @xs >= @l2 + @l3 + @x + @xs = zip3#2(@l2,@l3,@x,@xs)
     
     zip3#1(nil(),@l2,@l3) = @l2 + @l3 + 12 >= 12 = nil()
     
     zip3#2(::(@y,@ys),@l3,@x,@xs) = @l3 + @x + @xs + @y + @ys >= @l3 + @x + @xs + @y + @ys + 1 = zip3#3(@l3,@x,@xs,@y,@ys)
     
     zip3#2(nil(),@l3,@x,@xs) = @l3 + @x + @xs + 12 >= 12 = nil()
     
     zip3#3(::(@z,@zs),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + @z + @zs + 1 >= @x + @xs + @y + @ys + @z + @zs = ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs))
     
     zip3#3(nil(),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + 13 >= 12 = nil()
    problem:
     strict:
      group3(@l) -> group3#1(@l)
      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()
     weak:
      group3#1(::(@x,@xs)) -> group3#2(@xs,@x)
      group3#1(nil()) -> 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()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [zip3#3](x0, x1, x2, x3, x4) = x0 + x1 + x2 + x3 + x4 + 5,
       
       [zip3#2](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 8,
       
       [zip3#1](x0, x1, x2) = x0 + x1 + x2 + 6,
       
       [zip3](x0, x1, x2) = x0 + x1 + x2,
       
       [tuple#3](x0, x1, x2) = x0 + x1 + x2 + 4,
       
       [group3#3](x0, x1, x2) = x0 + x1 + x2,
       
       [nil] = 0,
       
       [group3#2](x0, x1) = x0 + x1 + 4,
       
       [::](x0, x1) = x0 + x1 + 4,
       
       [group3#1](x0) = x0,
       
       [group3](x0) = x0 + 9
      orientation:
       group3(@l) = @l + 9 >= @l = group3#1(@l)
       
       group3#2(::(@y,@ys),@x) = @x + @y + @ys + 8 >= @x + @y + @ys = group3#3(@ys,@x,@y)
       
       group3#2(nil(),@x) = @x + 4 >= 0 = nil()
       
       group3#3(::(@z,@zs),@x,@y) = @x + @y + @z + @zs + 4 >= @x + @y + @z + @zs + 17 = ::(tuple#3(@x,@y,@z),group3(@zs))
       
       group3#3(nil(),@x,@y) = @x + @y >= 0 = nil()
       
       zip3(@l1,@l2,@l3) = @l1 + @l2 + @l3 >= @l1 + @l2 + @l3 + 6 = zip3#1(@l1,@l2,@l3)
       
       zip3#1(::(@x,@xs),@l2,@l3) = @l2 + @l3 + @x + @xs + 10 >= @l2 + @l3 + @x + @xs + 8 = zip3#2(@l2,@l3,@x,@xs)
       
       zip3#1(nil(),@l2,@l3) = @l2 + @l3 + 6 >= 0 = nil()
       
       zip3#2(::(@y,@ys),@l3,@x,@xs) = @l3 + @x + @xs + @y + @ys + 12 >= @l3 + @x + @xs + @y + @ys + 5 = zip3#3(@l3,@x,@xs,@y,@ys)
       
       zip3#2(nil(),@l3,@x,@xs) = @l3 + @x + @xs + 8 >= 0 = nil()
       
       group3#1(::(@x,@xs)) = @x + @xs + 4 >= @x + @xs + 4 = group3#2(@xs,@x)
       
       group3#1(nil()) = 0 >= 0 = nil()
       
       zip3#3(::(@z,@zs),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + @z + @zs + 9 >= @x + @xs + @y + @ys + @z + @zs + 8 = ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs))
       
       zip3#3(nil(),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + 5 >= 0 = nil()
      problem:
       strict:
        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)
       weak:
        group3(@l) -> group3#1(@l)
        group3#2(::(@y,@ys),@x) -> group3#3(@ys,@x,@y)
        group3#2(nil(),@x) -> nil()
        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()
        group3#1(::(@x,@xs)) -> group3#2(@xs,@x)
        group3#1(nil()) -> 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()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [zip3#3](x0, x1, x2, x3, x4) = x0 + x1 + x2 + x3 + x4 + 1,
         
         [zip3#2](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 3,
         
         [zip3#1](x0, x1, x2) = x0 + x1 + x2,
         
         [zip3](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [tuple#3](x0, x1, x2) = x0 + x1 + x2,
         
         [group3#3](x0, x1, x2) = x0 + x1 + x2 + 4,
         
         [nil] = 2,
         
         [group3#2](x0, x1) = x0 + x1,
         
         [::](x0, x1) = x0 + x1 + 4,
         
         [group3#1](x0) = x0 + 7,
         
         [group3](x0) = x0 + 7
        orientation:
         group3#3(::(@z,@zs),@x,@y) = @x + @y + @z + @zs + 8 >= @x + @y + @z + @zs + 11 = ::(tuple#3(@x,@y,@z),group3(@zs))
         
         group3#3(nil(),@x,@y) = @x + @y + 6 >= 2 = nil()
         
         zip3(@l1,@l2,@l3) = @l1 + @l2 + @l3 + 1 >= @l1 + @l2 + @l3 = zip3#1(@l1,@l2,@l3)
         
         group3(@l) = @l + 7 >= @l + 7 = group3#1(@l)
         
         group3#2(::(@y,@ys),@x) = @x + @y + @ys + 4 >= @x + @y + @ys + 4 = group3#3(@ys,@x,@y)
         
         group3#2(nil(),@x) = @x + 2 >= 2 = nil()
         
         zip3#1(::(@x,@xs),@l2,@l3) = @l2 + @l3 + @x + @xs + 4 >= @l2 + @l3 + @x + @xs + 3 = zip3#2(@l2,@l3,@x,@xs)
         
         zip3#1(nil(),@l2,@l3) = @l2 + @l3 + 2 >= 2 = nil()
         
         zip3#2(::(@y,@ys),@l3,@x,@xs) = @l3 + @x + @xs + @y + @ys + 7 >= @l3 + @x + @xs + @y + @ys + 1 = zip3#3(@l3,@x,@xs,@y,@ys)
         
         zip3#2(nil(),@l3,@x,@xs) = @l3 + @x + @xs + 5 >= 2 = nil()
         
         group3#1(::(@x,@xs)) = @x + @xs + 11 >= @x + @xs = group3#2(@xs,@x)
         
         group3#1(nil()) = 9 >= 2 = nil()
         
         zip3#3(::(@z,@zs),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + @z + @zs + 5 >= @x + @xs + @y + @ys + @z + @zs + 5 = ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs))
         
         zip3#3(nil(),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + 3 >= 2 = nil()
        problem:
         strict:
          group3#3(::(@z,@zs),@x,@y) -> ::(tuple#3(@x,@y,@z),group3(@zs))
         weak:
          group3#3(nil(),@x,@y) -> nil()
          zip3(@l1,@l2,@l3) -> zip3#1(@l1,@l2,@l3)
          group3(@l) -> group3#1(@l)
          group3#2(::(@y,@ys),@x) -> group3#3(@ys,@x,@y)
          group3#2(nil(),@x) -> nil()
          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()
          group3#1(::(@x,@xs)) -> group3#2(@xs,@x)
          group3#1(nil()) -> 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()
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [zip3#3](x0, x1, x2, x3, x4) = x0 + x1 + x2 + x3 + x4,
           
           [zip3#2](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 6,
           
           [zip3#1](x0, x1, x2) = x0 + x1 + x2,
           
           [zip3](x0, x1, x2) = x0 + x1 + x2,
           
           [tuple#3](x0, x1, x2) = x0 + x1 + x2,
           
           [group3#3](x0, x1, x2) = x0 + x1 + x2 + 8,
           
           [nil] = 14,
           
           [group3#2](x0, x1) = x0 + x1 + 8,
           
           [::](x0, x1) = x0 + x1 + 11,
           
           [group3#1](x0) = x0 + 4,
           
           [group3](x0) = x0 + 7
          orientation:
           group3#3(::(@z,@zs),@x,@y) = @x + @y + @z + @zs + 19 >= @x + @y + @z + @zs + 18 = ::(tuple#3(@x,@y,@z),group3(@zs))
           
           group3#3(nil(),@x,@y) = @x + @y + 22 >= 14 = nil()
           
           zip3(@l1,@l2,@l3) = @l1 + @l2 + @l3 >= @l1 + @l2 + @l3 = zip3#1(@l1,@l2,@l3)
           
           group3(@l) = @l + 7 >= @l + 4 = group3#1(@l)
           
           group3#2(::(@y,@ys),@x) = @x + @y + @ys + 19 >= @x + @y + @ys + 8 = group3#3(@ys,@x,@y)
           
           group3#2(nil(),@x) = @x + 22 >= 14 = nil()
           
           zip3#1(::(@x,@xs),@l2,@l3) = @l2 + @l3 + @x + @xs + 11 >= @l2 + @l3 + @x + @xs + 6 = zip3#2(@l2,@l3,@x,@xs)
           
           zip3#1(nil(),@l2,@l3) = @l2 + @l3 + 14 >= 14 = nil()
           
           zip3#2(::(@y,@ys),@l3,@x,@xs) = @l3 + @x + @xs + @y + @ys + 17 >= @l3 + @x + @xs + @y + @ys = zip3#3(@l3,@x,@xs,@y,@ys)
           
           zip3#2(nil(),@l3,@x,@xs) = @l3 + @x + @xs + 20 >= 14 = nil()
           
           group3#1(::(@x,@xs)) = @x + @xs + 15 >= @x + @xs + 8 = group3#2(@xs,@x)
           
           group3#1(nil()) = 18 >= 14 = nil()
           
           zip3#3(::(@z,@zs),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + @z + @zs + 11 >= @x + @xs + @y + @ys + @z + @zs + 11 = ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs))
           
           zip3#3(nil(),@x,@xs,@y,@ys) = @x + @xs + @y + @ys + 14 >= 14 = nil()
          problem:
           strict:
            
           weak:
            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)
            group3(@l) -> group3#1(@l)
            group3#2(::(@y,@ys),@x) -> group3#3(@ys,@x,@y)
            group3#2(nil(),@x) -> nil()
            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()
            group3#1(::(@x,@xs)) -> group3#2(@xs,@x)
            group3#1(nil()) -> 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()
          Qed