%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|