Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: EquivClass.thy Sprache: Lisp

Original von: PVS^©

%-------------------------------------------------------------------------
%
%  Chain chains: chains of Ts ordered by inclusion.
%
%  For PVS version 3.2.  January 14, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), 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.53 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.