| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 641 B |
|
Quelle infinite_nat_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% infinite IFF injective map from the naturals. % % Author: David Lester, Manchester University % % Version 1.0 2/1/05 % Version 1.1 25/6/09 Dependency on other libraries removed %------------------------------------------------------------------------------ infinite_nat_def[T:TYPE]: THEORY BEGIN S,X: VAR set[T] infinite_def: THEOREM is_infinite(X) IFF (EXISTS (f:(injective?[nat,(X)])): TRUE) infinite_def2: LEMMA is_infinite(S) IFF (EXISTS (f:(surjective?[(S),nat])): TRUE) END infinite_nat_def ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28