YES

We show the termination of the TRS R:

  .(|1|(),x) -> x
  .(x,|1|()) -> x
  .(i(x),x) -> |1|()
  .(x,i(x)) -> |1|()
  i(|1|()) -> |1|()
  i(i(x)) -> x
  .(i(y),.(y,z)) -> z
  .(y,.(i(y),z)) -> z

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

  (no rules)

and R consists of:

r1: .(|1|(),x) -> x
r2: .(x,|1|()) -> x
r3: .(i(x),x) -> |1|()
r4: .(x,i(x)) -> |1|()
r5: i(|1|()) -> |1|()
r6: i(i(x)) -> x
r7: .(i(y),.(y,z)) -> z
r8: .(y,.(i(y),z)) -> z

The estimated dependency graph contains the following SCCs:

  (no SCCs)