| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/topology/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle prelude_sets_aux.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Various odds & ends for prelude libraries % % Author: David Lester, Manchester University, NIA, Université Perpignan % % Version 1.0 9/06/06 Initial Version %------------------------------------------------------------------------------ prelude_sets_aux[T:TYPE]: THEORY BEGIN finite_setofsets_is_setofsets: JUDGEMENT finite_set[set[T]] SUBTYPE_OF setofsets[T] x: VAR T A: VAR setofsets[T] a,b: VAR set[T] F: VAR finite_set[set[T]] P: VAR [set[T]->bool] complement_difference: LEMMA complement(difference(a,b)) = union(complement(a),b) Intersection_member: LEMMA member(x,Intersection(A)) IFF (FORALL (a:(A)): member(x,a)) Intersection_split: LEMMA nonempty?(A) => (Intersection(A) = intersection(choose(A),Intersection(rest(A)))) Intersection_finite: LEMMA P(fullset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND (FORALL (a,b:set[T]): P(a) AND P(b) => P(intersection(a,b))) => P(Intersection(A)) Union_member: LEMMA member(x,Union(A)) IFF (EXISTS (a:(A)): member(x,a)) Union_split: LEMMA nonempty?(A) => (Union(A) = union(choose(A),Union(rest(A)))) Union_finite: LEMMA P(emptyset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND (FORALL (a,b:set[T]): P(a) AND P(b) => P(union(a,b))) => P(Union(A)) finite_Complement: LEMMA is_finite(Complement(F)) END prelude_sets_aux ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28