Quelle  lift_props.pvs

%------------------------------------------------------------------------------
% Properties of lift
%
%       Author: David Lester <dlester@cs.man.ac.uk> Manchester University
%
%       Version 1.0          03/30/06
%------------------------------------------------------------------------------

lift_props[T:TYPE]: THEORY

BEGIN

  x,x1,x2: VAR T
  y,y1,y2: VAR lift[T]

  down_up:    LEMMA down(up(x)) = x
  up_down:    LEMMA up?(y) IMPLIES up(down(y)) = y
  down_equal: LEMMA up?(y1) & up?(y2) IMPLIES (down(y1) = down(y2) IFF y1 = y2)
  up_equal:   LEMMA up(x1) = up(x2) IFF x1 = x2

END lift_props