| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 962 B |
|
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 ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28