| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
SSL product_orders.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Pointwise Ordering in Product Types % % Author: David Lester <dlester@cs.man.ac.uk> Manchester University % % Version 1.0 03/30/06 %------------------------------------------------------------------------------ product_orders[T1,T2:TYPE]: THEORY BEGIN rel1: VAR pred[[T1,T1]] rel2: VAR pred[[T2,T2]] x,y: VAR [[T1,T2]] ; % syntax *(rel1,rel2)(x,y):bool = rel1(x`1,y`1) AND rel2(x`2,y`2) product_preserves_reflexive: JUDGEMENT *(r1:(reflexive?[T1]),r2:(reflexive?[T2])) HAS_TYPE (reflexive?[[T1,T2]]) product_preserves_transitive: JUDGEMENT *(r1:(transitive?[T1]),r2:(transitive?[T2])) HAS_TYPE (transitive?[[T1,T2]]) product_preserves_antisymmetric: JUDGEMENT *(r1:(antisymmetric?[T1]),r2:(antisymmetric?[T2])) HAS_TYPE (antisymmetric?[[T1,T2]]) product_preserves_preorder: JUDGEMENT *(r1:(preorder?[T1]),r2:(preorder?[T2])) HAS_TYPE (preorder?[[T1,T2]]) product_preserves_partial_order: JUDGEMENT *(r1:(partial_order?[T1]),r2:(partial_order?[T2])) HAS_TYPE (partial_order?[[T1,T2]]) IMPORTING directed_orders[T1], directed_orders[T2], directed_orders[[T1,T2]] product_preserves_directed_complete: JUDGEMENT *(r1:(directed_complete?[T1]),r2:(directed_complete?[T2])) HAS_TYPE (directed_complete?[[T1,T2]]) product_preserves_directed_complete_partial_order: JUDGEMENT *(r1:(directed_complete_partial_order?[T1]), r2:(directed_complete_partial_order?[T2])) HAS_TYPE (directed_complete_partial_order?[[T1,T2]]) product_lub: LEMMA FORALL (r1:(directed_complete_partial_order?[T1]), r2:(directed_complete_partial_order?[T2]), D :(directed?(r1*r2))): lub(r1*r2)(D) = (lub(r1)({x:T1| EXISTS (z:(D)): z`1=x}), lub(r2)({y:T2| EXISTS (z:(D)): z`2=y})) product_preserves_has_least: LEMMA has_least?(rel1)(fullset[T1]) AND has_least?(rel2)(fullset[T2]) IMPLIES has_least?(*(rel1,rel2))(fullset[[T1,T2]]) product_preserves_pointed_directed_complete_partial_order: JUDGEMENT *(r1:(pointed_directed_complete_partial_order?[T1]), r2:(pointed_directed_complete_partial_order?[T2])) HAS_TYPE (pointed_directed_complete_partial_order?[[T1,T2]]) product_least: LEMMA FORALL (r1:(pointed_directed_complete_partial_order?[T1]), r2:(pointed_directed_complete_partial_order?[T2])): least(r1*r2)(fullset[[T1,T2]]) = (least(r1)(fullset[T1]),least(r2)(fullset[T2])) END product_orders ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28