YES

We show the termination of the TRS R:

  |:|(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

-- SCC decomposition.

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

  (no rules)

and R consists of:

r1: |:|(x,x) -> e()
r2: /(x,x) -> e()
r3: .(e(),x) -> x
r4: .(x,e()) -> x
r5: |:|(e(),x) -> x
r6: /(x,e()) -> x
r7: .(x,|:|(x,y)) -> y
r8: .(/(y,x),x) -> y
r9: |:|(x,.(x,y)) -> y
r10: /(.(y,x),x) -> y
r11: /(x,|:|(y,x)) -> y
r12: |:|(/(x,y),x) -> y

The estimated dependency graph contains the following SCCs:

  (no SCCs)