% @(#)$Id: gcd.lsl,v 1.1 1999/04/11 23:15:51 leavens Exp $

gcd: trait
  includes Integer
  introduces
    __ \divides __: Int, Int -> Bool
    gcd: Int, Int -> Int
  asserts \forall x, y, n: Int
    x \neq 0 => (x \divides y = (mod(y,x) = 0));
    (x \neq 0 /\ y \neq 0)
      => ((gcd(x,y) \divides x) /\ (gcd(x,y) \divides y));
    (x \neq 0 /\ y \neq 0 /\ n \neq 0)
       => ((n \divides x /\ n \divides y)
           => (gcd(x,y) >= n));
    x \neq 0 => (gcd(x,0) = x);
    y \neq 0 => (gcd(0,y) = y);
  implies  \forall x, y, n: Int
    (x \neq 0) => (gcd(x,x) = abs(x));
    (x \neq 0 /\ y \neq 0) => (gcd(x,y) = gcd(y,x));
    (x \neq 0 /\ y \neq 0) => (gcd(x,y) = gcd(-x,y));
    (x \neq 0 /\ y \neq 0) => (gcd(x,y) = gcd(x-y,y));
    (x \neq 0 /\ y \neq 0 /\ n \neq 0)
       => ((n \divides x /\ n \divides y)
           => (n \divides gcd(x,y)));
    converts
      __ \divides __: Int, Int -> Bool,
      gcd: Int, Int -> Int
      exempting \forall y: Int
        0 \divides y, gcd(0, 0)

[Index]

HTML generated using lcpp2html.