products/sources/formale Sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: mtac2.nix   Sprache: PVS

%------------------------------------------------------------------------------
% 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

[ Verzeichnis aufwärts0.13unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]