YES(?,O(n^3))

Problem:
 f(X) -> g()

Proof:
 RT Transformation Processor:
  strict:
   f(X) -> g()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 3
   interpretation:
          [0]
    [g] = [0]
          [0],
    
              [1 0 0]     [1]
    [f](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [0]
   orientation:
           [1 0 0]    [1]    [0]      
    f(X) = [0 0 0]X + [0] >= [0] = g()
           [0 0 0]    [0]    [0]      
   problem:
    strict:
     
    weak:
     f(X) -> g()
   Qed