Quelle  add.pvs

%------------------------------------------------------------------------------
% Addition
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

add: THEORY

BEGIN

  IMPORTING appendix,
            cauchy

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

  cauchy_add(cx,cy): cauchy_real
           = (LAMBDA p: round((cx(p+2) + cy(p+2))/4))

  add_lemma: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cy) =>
                   cauchy_prop(x+y, cauchy_add(cx,cy))

END add