| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle partial_order_props.pvs Sprache: PVS |
|||||||||
|
% Properties and definitions for ordered sets.
partial_order_props[T:TYPE,<=:(partial_order?[T])]: THEORY BEGIN x,y,z: VAR T S: VAR set[T] XS: VAR setofsets[T] partial_order_reflexive: LEMMA x <= x partial_order_antisymmetric: LEMMA x <= y AND y <= x IMPLIES x = y partial_order_transitive: LEMMA x <= y AND y <= z IMPLIES x <= z AUTO_REWRITE+ partial_order_reflexive AUTO_REWRITE+ partial_order_antisymmetric AUTO_REWRITE+ partial_order_transitive lower_set?(S) :bool = FORALL x,y: member(x,S) AND y <= x IMPLIES member(y,S) upper_set?(S) :bool = FORALL x,y: member(x,S) AND x <= y IMPLIES member(y,S) lower_sets?(XS):bool = every(lower_set?,XS) upper_sets?(XS):bool = every(upper_set?,XS) lower_set: TYPE+ = (lower_set?) CONTAINING emptyset[T] upper_set: TYPE+ = (upper_set?) CONTAINING emptyset[T] lower_sets: TYPE+ = (lower_sets?) CONTAINING emptyset[set[T]] upper_sets: TYPE+ = (upper_sets?) CONTAINING emptyset[set[T]] L,L1,L2: VAR lower_set U,U1,U2: VAR upper_set LS: VAR lower_sets US: VAR upper_sets complement_lower_set: JUDGEMENT complement(L) HAS_TYPE upper_set complement_upper_set: JUDGEMENT complement(U) HAS_TYPE lower_set Complement_lower_sets: JUDGEMENT Complement(LS) HAS_TYPE upper_sets Complement_upper_sets: JUDGEMENT Complement(US) HAS_TYPE lower_sets down(x): lower_set = {y | y <= x} up(x): upper_set = {y | x <= y} down_subset: LEMMA x <= y IMPLIES subset?(down(x),down(y)) up_subset: LEMMA x <= y IMPLIES subset?(up(y),up(x)) lower_set_def: LEMMA lower_set?(S) IFF S = Union(image(down,S)) upper_set_def: LEMMA upper_set?(S) IFF S = Union(image(up,S)) Union_lower_set: JUDGEMENT Union(LS) HAS_TYPE lower_set Union_upper_set: JUDGEMENT Union(US) HAS_TYPE upper_set Intersection_lower_set: JUDGEMENT Intersection(LS) HAS_TYPE lower_set Intersection_upper_set: JUDGEMENT Intersection(US) HAS_TYPE upper_set union_lower_set: JUDGEMENT union(L1,L2) HAS_TYPE lower_set union_upper_set: JUDGEMENT union(U1,U2) HAS_TYPE upper_set intersection_lower_set: JUDGEMENT intersection(L1,L2) HAS_TYPE lower_set intersection_upper_set: JUDGEMENT intersection(U1,U2) HAS_TYPE upper_set END partial_order_props ¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28