Quelle  int.pvs   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