YES(?,O(n^1))
TRS:
 {
        .(x, 1()) -> x,
        .(x, i x) -> 1(),
  .(y, .(i y, z)) -> z,
        .(1(), x) -> x,
        .(i x, x) -> 1(),
  .(i y, .(y, z)) -> z,
            i 1() -> 1(),
            i i x -> x
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
          .(x, 1()) -> x,
          .(x, i x) -> 1(),
    .(y, .(i y, z)) -> z,
          .(1(), x) -> x,
          .(i x, x) -> 1(),
    .(i y, .(y, z)) -> z,
              i 1() -> 1(),
              i i x -> x
   }
  Natural interpretation:
   Strict:
    {
           .(x, 1()) -> x,
           .(x, i x) -> 1(),
     .(y, .(i y, z)) -> z,
           .(1(), x) -> x,
           .(i x, x) -> 1(),
     .(i y, .(y, z)) -> z,
               i 1() -> 1(),
               i i x -> x
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [i](X0) = + 1*X0 + 6
   [1] = + 1
   [.](X1, X0) = + 1*X0 + 1*X1 + 0
   
   Qed