Problem:
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 bits(0()) -> 0()
 bits(s(x)) -> s(bits(half(s(x))))

Proof:
 Complexity Transformation Processor:
  strict:
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   bits(0()) -> 0()
   bits(s(x)) -> s(bits(half(s(x))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [bits](x0) = x0,
     
     [s](x0) = x0 + 8,
     
     [half](x0) = x0 + 8,
     
     [0] = 11
    orientation:
     half(0()) = 19 >= 11 = 0()
     
     half(s(0())) = 27 >= 11 = 0()
     
     half(s(s(x))) = x + 24 >= x + 16 = s(half(x))
     
     bits(0()) = 11 >= 11 = 0()
     
     bits(s(x)) = x + 8 >= x + 24 = s(bits(half(s(x))))
    problem:
     strict:
      bits(0()) -> 0()
      bits(s(x)) -> s(bits(half(s(x))))
     weak:
      half(0()) -> 0()
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [bits](x0) = x0 + 4,
       
       [s](x0) = x0 + 1,
       
       [half](x0) = x0,
       
       [0] = 0
      orientation:
       bits(0()) = 4 >= 0 = 0()
       
       bits(s(x)) = x + 5 >= x + 6 = s(bits(half(s(x))))
       
       half(0()) = 0 >= 0 = 0()
       
       half(s(0())) = 1 >= 0 = 0()
       
       half(s(s(x))) = x + 2 >= x + 1 = s(half(x))
      problem:
       strict:
        bits(s(x)) -> s(bits(half(s(x))))
       weak:
        bits(0()) -> 0()
        half(0()) -> 0()
        half(s(0())) -> 0()
        half(s(s(x))) -> s(half(x))
      Arctic Interpretation Processor:
       dimension: 3
       interpretation:
                     [0 0 0]  
        [bits](x0) = [0 3 3]x0
                     [0 2 2]  ,
        
                  [0  -& 0 ]  
        [s](x0) = [0  -& 3 ]x0
                  [3  1  0 ]  ,
        
                     [0  -& -&]  
        [half](x0) = [0  -& -&]x0
                     [0  -& -&]  ,
        
              [1 ]
        [0] = [-&]
              [1 ]
       orientation:
                     [3 1 3]     [2  -& 2 ]                       
        bits(s(x)) = [6 4 6]x >= [5  -& 5 ]x = s(bits(half(s(x))))
                     [5 3 5]     [4  -& 4 ]                       
        
                    [1]    [1 ]      
        bits(0()) = [4] >= [-&] = 0()
                    [3]    [1 ]      
        
                    [1]    [1 ]      
        half(0()) = [1] >= [-&] = 0()
                    [1]    [1 ]      
        
                       [1]    [1 ]      
        half(s(0())) = [1] >= [-&] = 0()
                       [1]    [1 ]      
        
                        [3 1 0]     [0  -& -&]              
        half(s(s(x))) = [3 1 0]x >= [3  -& -&]x = s(half(x))
                        [3 1 0]     [3  -& -&]              
       problem:
        strict:
         
        weak:
         bits(s(x)) -> s(bits(half(s(x))))
         bits(0()) -> 0()
         half(0()) -> 0()
         half(s(0())) -> 0()
         half(s(s(x))) -> s(half(x))
       Qed