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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [.](x0, x1) = x0 + x1,
     
     [/](x0, x1) = x0 + x1,
     
     [e] = 0,
     
     [\](x0, x1) = x0 + x1 + 1
    orientation:
     \(x,x) = 2x + 1 >= 0 = e()
     
     /(x,x) = 2x >= 0 = e()
     
     .(e(),x) = x >= x = x
     
     .(x,e()) = x >= x = x
     
     \(e(),x) = x + 1 >= x = x
     
     /(x,e()) = x >= x = x
     
     .(x,\(x,y)) = 2x + y + 1 >= y = y
     
     .(/(y,x),x) = 2x + y >= y = y
     
     \(x,.(x,y)) = 2x + y + 1 >= y = y
     
     /(.(y,x),x) = 2x + y >= y = y
     
     /(x,\(y,x)) = 2x + y + 1 >= y = y
     
     \(/(x,y),x) = 2x + y + 1 >= y = y
    problem:
     strict:
      /(x,x) -> e()
      .(e(),x) -> x
      .(x,e()) -> x
      /(x,e()) -> x
      .(/(y,x),x) -> y
      /(.(y,x),x) -> y
     weak:
      \(x,x) -> e()
      \(e(),x) -> x
      .(x,\(x,y)) -> y
      \(x,.(x,y)) -> y
      /(x,\(y,x)) -> y
      \(/(x,y),x) -> y
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [.](x0, x1) = x0 + x1,
       
       [/](x0, x1) = x0 + x1 + 1,
       
       [e] = 0,
       
       [\](x0, x1) = x0 + x1
      orientation:
       /(x,x) = 2x + 1 >= 0 = e()
       
       .(e(),x) = x >= x = x
       
       .(x,e()) = x >= x = x
       
       /(x,e()) = x + 1 >= x = x
       
       .(/(y,x),x) = 2x + y + 1 >= y = y
       
       /(.(y,x),x) = 2x + y + 1 >= y = y
       
       \(x,x) = 2x >= 0 = e()
       
       \(e(),x) = x >= x = x
       
       .(x,\(x,y)) = 2x + y >= y = y
       
       \(x,.(x,y)) = 2x + y >= y = y
       
       /(x,\(y,x)) = 2x + y + 1 >= y = y
       
       \(/(x,y),x) = 2x + y + 1 >= y = y
      problem:
       strict:
        .(e(),x) -> x
        .(x,e()) -> x
       weak:
        /(x,x) -> e()
        /(x,e()) -> x
        .(/(y,x),x) -> y
        /(.(y,x),x) -> y
        \(x,x) -> e()
        \(e(),x) -> x
        .(x,\(x,y)) -> y
        \(x,.(x,y)) -> y
        /(x,\(y,x)) -> y
        \(/(x,y),x) -> y
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [.](x0, x1) = x0 + x1 + 1,
         
         [/](x0, x1) = x0 + x1,
         
         [e] = 0,
         
         [\](x0, x1) = x0 + x1
        orientation:
         .(e(),x) = x + 1 >= x = x
         
         .(x,e()) = x + 1 >= x = x
         
         /(x,x) = 2x >= 0 = e()
         
         /(x,e()) = x >= x = x
         
         .(/(y,x),x) = 2x + y + 1 >= y = y
         
         /(.(y,x),x) = 2x + y + 1 >= y = y
         
         \(x,x) = 2x >= 0 = e()
         
         \(e(),x) = x >= x = x
         
         .(x,\(x,y)) = 2x + y + 1 >= y = y
         
         \(x,.(x,y)) = 2x + y + 1 >= y = y
         
         /(x,\(y,x)) = 2x + y >= y = y
         
         \(/(x,y),x) = 2x + y >= y = y
        problem:
         strict:
          
         weak:
          .(e(),x) -> x
          .(x,e()) -> x
          /(x,x) -> e()
          /(x,e()) -> x
          .(/(y,x),x) -> y
          /(.(y,x),x) -> y
          \(x,x) -> e()
          \(e(),x) -> x
          .(x,\(x,y)) -> y
          \(x,.(x,y)) -> y
          /(x,\(y,x)) -> y
          \(/(x,y),x) -> y
        Qed