Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
int.pvs
Sprache: Unknown
|
%------------------------------------------------------------------------------
% 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.0 Sekunden
(vorverarbeitet)
]
|
|
