| products/sources/formale sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: contradiction.ml Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-------------------------------------------------------------------------
% % The converse of Zorn's lemma: if every chain has a lower bound, then % the set has a minimal element. % % For PVS version 3.2. January 17, 2005 % --------------------------------------------------------------------- % Author: Jerry James ([email protected]), University of Kansas % % EXPORTS % ------- % prelude: orders[T], relations[T], sets[T] % orders: bounded_orders[T], chain[T,<=], converse_zorn[T,<=], % minmax_orders[T], relations_extra[T] % %------------------------------------------------------------------------- converse_zorn[T: TYPE, <=: (partial_order?[T])]: THEORY EXPORTING ALL WITH orders[T], relations[T], sets[T], bounded_orders[T], chain[T, <=], minmax_orders[T], relations_extra[T] BEGIN IMPORTING minmax_orders[T], chain[T, <=] IMPORTING relation_converse_props[T], zorn[T, converse(<=)] % Proof only converse_zorn: THEOREM (FORALL (ch: chain[T, <=]): bounded_below?[T](ch, <=)) => (EXISTS (t: T): minimal?[T](t, fullset[T], <=)) END converse_zorn ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
