|
%------------------------------------------------------------------------------
% Negation
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
neg: THEORY
BEGIN
IMPORTING cauchy
cx: VAR cauchy_real
x: VAR real
p: VAR nat
nzcx: VAR cauchy_nzreal
pcx: VAR cauchy_posreal
ncx: VAR cauchy_negreal
cauchy_neg(cx): cauchy_real = (LAMBDA p: -cx(p))
neg_lemma: LEMMA cauchy_prop(x,cx) IFF cauchy_prop(-x, cauchy_neg(cx))
neg_cauchy_nzreal_is_cauchy_nzreal:
JUDGEMENT cauchy_neg(nzcx) HAS_TYPE cauchy_nzreal
neg_cauchy_posreal_is_cauchy_negreal:
JUDGEMENT cauchy_neg(pcx) HAS_TYPE cauchy_negreal
neg_cauchy_negreal_is_cauchy_posreal:
JUDGEMENT cauchy_neg(ncx) HAS_TYPE cauchy_posreal
END neg
¤ Dauer der Verarbeitung: 0.23 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.
|
