YES
TRS:
 {       .(x, 1()) -> x,
        .(x, i(x)) -> 1(),
  .(y, .(i(y), z)) -> z,
     .(.(x, y), z) -> .(x, .(y, z)),
         .(1(), x) -> x,
        .(i(x), x) -> 1(),
  .(i(y), .(y, z)) -> z,
        i(.(x, y)) -> .(i(y), i(x)),
            i(1()) -> 1(),
           i(i(x)) -> x}
 DP:
  Strict:
   {.#(.(x, y), z) -> .#(x, .(y, z)),
    .#(.(x, y), z) -> .#(y, z),
       i#(.(x, y)) -> .#(i(y), i(x)),
       i#(.(x, y)) -> i#(x),
       i#(.(x, y)) -> i#(y)}
  Weak:
  {       .(x, 1()) -> x,
         .(x, i(x)) -> 1(),
   .(y, .(i(y), z)) -> z,
      .(.(x, y), z) -> .(x, .(y, z)),
          .(1(), x) -> x,
         .(i(x), x) -> 1(),
   .(i(y), .(y, z)) -> z,
         i(.(x, y)) -> .(i(y), i(x)),
             i(1()) -> 1(),
            i(i(x)) -> x}
  EDG:
   {(.#(.(x, y), z) -> .#(x, .(y, z)), .#(.(x, y), z) -> .#(y, z))
    (.#(.(x, y), z) -> .#(x, .(y, z)), .#(.(x, y), z) -> .#(x, .(y, z)))
    (i#(.(x, y)) -> i#(y), i#(.(x, y)) -> i#(y))
    (i#(.(x, y)) -> i#(y), i#(.(x, y)) -> i#(x))
    (i#(.(x, y)) -> i#(y), i#(.(x, y)) -> .#(i(y), i(x)))
    (i#(.(x, y)) -> .#(i(y), i(x)), .#(.(x, y), z) -> .#(x, .(y, z)))
    (i#(.(x, y)) -> .#(i(y), i(x)), .#(.(x, y), z) -> .#(y, z))
    (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(x, .(y, z)))
    (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(y, z))
    (i#(.(x, y)) -> i#(x), i#(.(x, y)) -> .#(i(y), i(x)))
    (i#(.(x, y)) -> i#(x), i#(.(x, y)) -> i#(x))
    (i#(.(x, y)) -> i#(x), i#(.(x, y)) -> i#(y))}
   SCCS:
    Scc:
     {i#(.(x, y)) -> i#(x),
      i#(.(x, y)) -> i#(y)}
    Scc:
     {.#(.(x, y), z) -> .#(x, .(y, z)),
      .#(.(x, y), z) -> .#(y, z)}
    SCC:
     Strict:
      {i#(.(x, y)) -> i#(x),
       i#(.(x, y)) -> i#(y)}
     Weak:
     {       .(x, 1()) -> x,
            .(x, i(x)) -> 1(),
      .(y, .(i(y), z)) -> z,
         .(.(x, y), z) -> .(x, .(y, z)),
             .(1(), x) -> x,
            .(i(x), x) -> 1(),
      .(i(y), .(y, z)) -> z,
            i(.(x, y)) -> .(i(y), i(x)),
                i(1()) -> 1(),
               i(i(x)) -> x}
     SPSC:
      Simple Projection:
       pi(i#) = 0
      Strict:
       {i#(.(x, y)) -> i#(y)}
      EDG:
       {(i#(.(x, y)) -> i#(y), i#(.(x, y)) -> i#(y))}
       SCCS:
        Scc:
         {i#(.(x, y)) -> i#(y)}
        SCC:
         Strict:
          {i#(.(x, y)) -> i#(y)}
         Weak:
         {       .(x, 1()) -> x,
                .(x, i(x)) -> 1(),
          .(y, .(i(y), z)) -> z,
             .(.(x, y), z) -> .(x, .(y, z)),
                 .(1(), x) -> x,
                .(i(x), x) -> 1(),
          .(i(y), .(y, z)) -> z,
                i(.(x, y)) -> .(i(y), i(x)),
                    i(1()) -> 1(),
                   i(i(x)) -> x}
         SPSC:
          Simple Projection:
           pi(i#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {.#(.(x, y), z) -> .#(x, .(y, z)),
       .#(.(x, y), z) -> .#(y, z)}
     Weak:
     {       .(x, 1()) -> x,
            .(x, i(x)) -> 1(),
      .(y, .(i(y), z)) -> z,
         .(.(x, y), z) -> .(x, .(y, z)),
             .(1(), x) -> x,
            .(i(x), x) -> 1(),
      .(i(y), .(y, z)) -> z,
            i(.(x, y)) -> .(i(y), i(x)),
                i(1()) -> 1(),
               i(i(x)) -> x}
     SPSC:
      Simple Projection:
       pi(.#) = 0
      Strict:
       {.#(.(x, y), z) -> .#(y, z)}
      EDG:
       {(.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(y, z))}
       SCCS:
        Scc:
         {.#(.(x, y), z) -> .#(y, z)}
        SCC:
         Strict:
          {.#(.(x, y), z) -> .#(y, z)}
         Weak:
         {       .(x, 1()) -> x,
                .(x, i(x)) -> 1(),
          .(y, .(i(y), z)) -> z,
             .(.(x, y), z) -> .(x, .(y, z)),
                 .(1(), x) -> x,
                .(i(x), x) -> 1(),
          .(i(y), .(y, z)) -> z,
                i(.(x, y)) -> .(i(y), i(x)),
                    i(1()) -> 1(),
                   i(i(x)) -> x}
         SPSC:
          Simple Projection:
           pi(.#) = 0
          Strict:
           {}
          Qed