YES(?,O(n^1))

Problem:
 \(x,x) -> e()
 /(x,x) -> e()
 .(e(),x) -> x
 .(x,e()) -> x
 \(e(),x) -> x
 /(x,e()) -> x
 .(x,\(x,y)) -> y
 .(/(y,x),x) -> y
 \(x,.(x,y)) -> y
 /(.(y,x),x) -> y
 /(x,\(y,x)) -> y
 \(/(x,y),x) -> y

Proof:
 RT Transformation Processor:
  strict:
   \(x,x) -> e()
   /(x,x) -> e()
   .(e(),x) -> x
   .(x,e()) -> x
   \(e(),x) -> x
   /(x,e()) -> x
   .(x,\(x,y)) -> y
   .(/(y,x),x) -> y
   \(x,.(x,y)) -> y
   /(.(y,x),x) -> y
   /(x,\(y,x)) -> y
   \(/(x,y),x) -> y
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [.](x0, x1) = x0 + x1 + 5,
    
    [/](x0, x1) = x0 + x1 + 9,
    
    [e] = 1,
    
    [\](x0, x1) = x0 + x1 + 16
   orientation:
    \(x,x) = 2x + 16 >= 1 = e()
    
    /(x,x) = 2x + 9 >= 1 = e()
    
    .(e(),x) = x + 6 >= x = x
    
    .(x,e()) = x + 6 >= x = x
    
    \(e(),x) = x + 17 >= x = x
    
    /(x,e()) = x + 10 >= x = x
    
    .(x,\(x,y)) = 2x + y + 21 >= y = y
    
    .(/(y,x),x) = 2x + y + 14 >= y = y
    
    \(x,.(x,y)) = 2x + y + 21 >= y = y
    
    /(.(y,x),x) = 2x + y + 14 >= y = y
    
    /(x,\(y,x)) = 2x + y + 25 >= y = y
    
    \(/(x,y),x) = 2x + y + 25 >= y = y
   problem:
    strict:
     
    weak:
     \(x,x) -> e()
     /(x,x) -> e()
     .(e(),x) -> x
     .(x,e()) -> x
     \(e(),x) -> x
     /(x,e()) -> x
     .(x,\(x,y)) -> y
     .(/(y,x),x) -> y
     \(x,.(x,y)) -> y
     /(.(y,x),x) -> y
     /(x,\(y,x)) -> y
     \(/(x,y),x) -> y
   Qed