| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 461 B |
|
Quelle function_image_nonempty.pvs Sprache: PVS |
|||||||||
|
% to be added to Jerry James's function_image_aux theory in the prelude
function_image_nonempty[D: TYPE, R: TYPE]: THEORY BEGIN f: VAR [D -> R] S: VAR set[D] nonempty_image: JUDGEMENT image(f, (S: (nonempty?[D]))) HAS_TYPE (nonempty?[R]) nonempty_finite_image: JUDGEMENT image(f, (S: non_empty_finite_set[D])) HAS_TYPE non_empty_finite_set[R] % image_witness: JUDGEMENT % f(x: (S)) HAS_TYPE (image?(f, S)) END function_image_nonempty ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28