| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 487 B |
|
Quelle booleans_are_finite.pvs Sprache: PVS |
|||||||||
|
% the booleans are a finite type.
% this theory is useful to discharge TCCs from finiteness proofs for % composed types such as set[T] = [T -> bool] % % Author: Alfons Geser, National Institute of Aerospace % Date: Jan 2005 booleans_are_finite: THEORY BEGIN bool_is_finite_type: LEMMA is_finite_type[bool] implies_is_total_order: JUDGEMENT IMPLIES HAS_TYPE (total_order?[bool]) IMPORTING finite_types[bool], finite_total_orders[bool, IMPLIES] END booleans_are_finite ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28