Quelle directed_order_props.pvs Sprache: 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

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.