(CONDITIONTYPE ORIENTED)
(VAR x y z)
(RULES
  gcd(z, y) -> gcd(x, y) | iadd(z) == tp2(x, y)
  gcd(y, z) -> gcd(x, y) | iadd(z) == tp2(x, y)
  gcd(x, 0) -> x
  gcd(0, x) -> x
  iadd(y) -> tp2(0, y)
  iadd(s(z)) -> u1(iadd(z))
  u1(tp2(x, y)) -> tp2(s(x), y)
  iadd(add(x, y)) -> tp2(x, y)
)
(COMMENT
  \cite{N04}, System R_29, p. 139
  http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf
)