YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
               [1 1]     [1]
   [log](x0) = [0 1]x0 + [0],
   
             [1 1]     [0]
   [s](x0) = [0 1]x0 + [8],
   
                     [2]
   [half](x0) = x0 + [0],
   
         [0]
   [0] = [0]
  orientation:
               [2]    [0]      
   half(0()) = [0] >= [0] = 0()
   
                   [1 2]    [10]    [1 1]    [2]             
   half(s(s(x))) = [0 1]x + [16] >= [0 1]x + [8] = s(half(x))
   
                 [9]    [0]      
   log(s(0())) = [8] >= [0] = 0()
   
                  [1 3]    [25]    [1 3]    [19]                     
   log(s(s(x))) = [0 1]x + [16] >= [0 1]x + [16] = s(log(s(half(x))))
  problem:
   
  Qed