YES
Time: 0.002562
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:
  DP:
   {.#(.(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}
  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}
  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), .#(.(x, y), z) -> .#(y, z))
    (i# .(x, y) -> .#(i y, i x), .#(.(x, y), z) -> .#(x, .(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)
    (i# .(x, y) -> i# y, i# .(x, y) -> .#(i y, i x))
    (i# .(x, y) -> i# y, i# .(x, y) -> i# x)
    (i# .(x, y) -> i# y, i# .(x, y) -> i# y)
    (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(x, .(y, z)))
    (.#(.(x, y), z) -> .#(y, z), .#(.(x, y), z) -> .#(y, z))}
   SCCS (2):
    Scc:
     {i# .(x, y) -> i# x,
      i# .(x, y) -> i# y}
    Scc:
     {.#(.(x, y), z) -> .#(x, .(y, z)),
      .#(.(x, y), z) -> .#(y, z)}
    SCC (2):
     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 (1):
        Scc:
         {i# .(x, y) -> i# y}
        SCC (1):
         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 (2):
     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 (1):
        Scc:
         {.#(.(x, y), z) -> .#(y, z)}
        SCC (1):
         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