products/sources/formale Sprachen/PVS/summaries/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Road.vdmpp   Sprache: Isabelle

Original von: PVS©
%-------------------------------------------------------------------------
%
%  Properties of well-ordered relations on sets.
%
%  For PVS version 3.2.  February 28, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: relation_props2[T, T, T, T], sets[T]
%  orders: closure_ops[T], indexed_sets_extra, isomorphism,
%    monotone_functions[T,T], ordered_subset[T], relation_iterate[T],
%    relations_extra, well_ordered_props[T,<]
%
%-------------------------------------------------------------------------
well_ordered_props[T: TYPE, <: (well_ordered?[T])]: THEORY
 BEGIN

  IMPORTING ordered_subset[T], monotone_functions[T, T], isomorphism

  t, r: VAR T
  S, R: VAR set[T]

  initial_segment: TYPE = {pre: (prefix?(<)) | EXISTS t: NOT member(t, pre)}

  seg: VAR initial_segment

  induced_prefixes: LEMMA FORALL seg: EXISTS t: seg = below(t, <)

  increasing_well_ordered: LEMMA
    FORALL (f: (increasing?(<, <))), t: t < f(t) OR t = f(t)

  initial_segment_isomorphism: COROLLARY
    FORALL seg:
      NOT isomorphic?[T, (seg)]
              (<, restrict[[T, T], [(seg), (seg)], bool](<))

 END well_ordered_props

¤ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff