% @(#)$Id: answer2.lsl,v 1.1 1995/09/18 05:25:19 leavens Exp $

% The order of fields in a tuple only matters for their construction.
% So one could have (rather perversely) ignored the traditional order
% and written the specification as follows.
% Note that none of the implications require the other order.

answer2: trait
  includes Integer(int for Int)
  Point tuple of y:int, x:int       % changed from answer1
  introduces
    origin: -> Point
    __+__: Point, Point -> Point
  asserts
    \forall i,j: int, p: Point
      origin == [0,0];
      [i,j] + p == [i+p.y, j+p.x];   % needs to be changed also
  implies
    \forall p,p1,p2:Point
      origin.x == 0;
      origin.y == 0;
      origin+p == p;
      (p1+p2).x == p1.x + p2.x;
      (p1+p2).y == p1.y + p2.y;