| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle chain_chain.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Chain chains: chains of Ts ordered by inclusion. % % For PVS version 3.2. January 14, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[subchain], orders[chain_chain], orders[subchain], % orders[T], relations[subchain], sets[subchain], sets[T] % orders: bounded_orders[subchain], chain[subchain,chain_incl], % chain[T,<=], chain_chain[T,<=], relations_extra[subchain] % %------------------------------------------------------------------------- chain_chain[T: TYPE, <=: (partial_order?[T])]: THEORY BEGIN % ========================================================================== % The lower level chains % ========================================================================== IMPORTING chain[T, <=] subchain: TYPE+ = chain[T, <=] subc1, subc2: VAR subchain % ========================================================================== % The higher level chains % ========================================================================== chain_incl(subc1, subc2): bool = subset?(subc1, subc2) chain_incl_partial_order: JUDGEMENT chain_incl HAS_TYPE (partial_order?[subchain]) IMPORTING bounded_orders[subchain], chain[subchain, chain_incl] chain_chain: TYPE+ = chain[subchain, chain_incl] C: VAR chain_chain chain_union(C): subchain = Union(extend[set[T], subchain, bool, FALSE](C)) chain_union_upper_bound: LEMMA FORALL (C: chain_chain): bounded_orders.upper_bound?(chain_union(C), C, chain_incl) END chain_chain ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28