| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle lifted_orders.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Properties of Lifted Orders % % Author: David Lester <dlester@cs.man.ac.uk> Manchester University % % We define a lifting operator on relations, and show that this operation % preserves directed completeness and pointedness. % % Version 1.0 03/30/06 %------------------------------------------------------------------------------ lifted_orders[T:TYPE]: THEORY BEGIN rel: VAR pred[[T,T]] x,y: VAR lift[T] IMPORTING lift_props[T] lift(rel)(x,y):bool = (NOT up?(x)) OR (up?(y) AND rel(down(x),down(y))) lift_preserves_reflexive: JUDGEMENT lift(r:(reflexive?[T])) HAS_TYPE (reflexive?[lift[T]]) lift_preserves_transitive: JUDGEMENT lift(r:(transitive?[T])) HAS_TYPE (transitive?[lift[T]]) lift_preserves_antisymmetric: JUDGEMENT lift(r:(antisymmetric?[T])) HAS_TYPE (antisymmetric?[lift[T]]) lift_preserves_preorder: JUDGEMENT lift(r:(preorder?[T])) HAS_TYPE (preorder?[lift[T]]) lift_preserves_partial_order: JUDGEMENT lift(r:(partial_order?[T])) HAS_TYPE (partial_order?[lift[T]]) IMPORTING directed_orders[T], directed_orders[lift[T]] lift_lub_emptyset: LEMMA lub(lift(rel))(emptyset[lift[T]]) = bottom lift_lub_bounded: LEMMA FORALL (rel:(antisymmetric?[T]), S:(nonempty_least_bounded_above?(rel))): lub(lift(rel))(image[T,lift[T]](up,S)) = up(lub(rel)(S)) lift_preserves_directed_complete: JUDGEMENT lift(r:(directed_complete?[T])) HAS_TYPE (directed_complete?[lift[T]]) lift_preserves_directed_complete_partial_order: JUDGEMENT lift(r:(directed_complete_partial_order?[T])) HAS_TYPE (pointed_directed_complete_partial_order?[lift[T]]) END lifted_orders ¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28