YES(?,O(n^2))

Problem:
 *(x,*(minus(y),y)) -> *(minus(*(y,y)),x)

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                 [1 1]     [1 1]     [4]
   [*](x0, x1) = [0 1]x0 + [0 1]x1 + [8],
   
                      [1]
   [minus](x0) = x0 + [3]
  orientation:
                        [1 1]    [2 4]    [23]    [1 1]    [2 4]    [20]                     
   *(x,*(minus(y),y)) = [0 1]x + [0 2]y + [19] >= [0 1]x + [0 2]y + [19] = *(minus(*(y,y)),x)
  problem:
   
  Qed