Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: directed_order_props.pvs Sprache: PVS

Original von: PVS^©

directed_order_props[T:TYPE,(IMPORTING directed_orders[T])
                     <=:(directed_complete_partial_order?[T])]: THEORY

BEGIN

  IMPORTING partial_order_props[T,<=],
            bounded_order_props[T,<=]

  S: VAR (nonempty?[T])

  directed?(S):bool = directed?(<=)(S)

  directed: TYPE    = (directed?)

  x,y,z:   VAR T
  D:       VAR directed
  U:       VAR upper_set
  L,L1,L2: VAR lower_set

  directed_is_lub_set: JUDGEMENT directed     SUBTYPE_OF (lub_set?)
  directed_singleton:  JUDGEMENT singleton(x) HAS_TYPE directed

  intersection_directed_upper:
       LEMMA nonempty?(intersection(U,D)) IMPLIES directed?(intersection(U,D))

  split_directed_lower: LEMMA
       member(x,D) AND member(y,D) AND member(x,L) AND NOT member(y,L) IMPLIES
          EXISTS z: x <= z AND y <= z AND member(z,D) AND NOT member(z,L)

  directed_union_lower: LEMMA
    subset?(D,union(L1,L2)) IMPLIES (subset?(D,L1) OR subset?(D,L2))

END directed_order_props

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.