|
%------------------------------------------------------------------------------
% Integer equivalence
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
int: THEORY
BEGIN
IMPORTING cauchy
p,m: VAR nat
n: VAR int
cauchy_int(n:int):cauchy_real = (LAMBDA p: n*2^p)
cauchy_nat(n:nat):cauchy_nnreal = (LAMBDA p: n*2^p)
int_lemma: LEMMA cauchy_prop(n, cauchy_int(n))
nat_lemma: LEMMA cauchy_prop(m, cauchy_nat(m))
END int
¤ Dauer der Verarbeitung: 0.15 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.
|
