|
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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
