(RULES
  a -> b
  a -> f(a)
  b -> f(f(b))
  f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
  f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(
  b
  )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -> b
)
(COMMENT
  R_64 as defined in Section 4, [F12-RTA]
)