Quelle  max.pvs

%------------------------------------------------------------------------------
% max of two reals
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

max: THEORY

BEGIN

  IMPORTING cauchy

  x,y:   VAR real
  cx,cy: VAR cauchy_real
  p:     VAR nat

  cauchy_max(cx,cy):cauchy_real = (LAMBDA p: max(cx(p),cy(p)))

  max_lemma: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cy) =>
                   cauchy_prop(max(x,y), cauchy_max(cx,cy))

END max