LOCAL GCD.

Gcd(i, j, d) <-
  CommonDivisor(i, j, d) &
  ~ SOME [e] (CommonDivisor(i, j, e) & e > d).

CommonDivisor(i, j, d) <-
  IF (i = 0 \/ j = 0)
  THEN
  d = Max(Abs(i), Abs(j))
  ELSE
  1 =< d =< Min(Abs(i), Abs(j)) &
  i Mod d = 0 &
  j Mod d = 0.