| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/scott/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle dual_fixpoints.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Dual Fixpoint Induction % % All references are to BA Davey and HA Priestly "Introduction to Lattices and % Orders", CUP, 1990 % % Author: David Lester, Manchester University, NIA, Université Perpignan % % Version 1.0 25/12/07 Initial Version %------------------------------------------------------------------------------ dual_fixpoints[T1,T2:TYPE+, (IMPORTING orders@directed_orders) le1:(pointed_directed_complete_partial_order?[T1]), le2:(pointed_directed_complete_partial_order?[T2])]: THEORY BEGIN IMPORTING orders@product_orders[T1,T2], fixpoints[T1,le1], fixpoints[T2,le2], fixpoints[[T1,T2],(le1*le2)], admissible[[T1,T2],(le1*le2)] x: VAR T1 y: VAR T2 phi: VAR (increasing?[T1,T1,le1,le1]) psi: VAR (increasing?[T2,T2,le2,le2]) D: VAR directed[[T1,T2],(le1*le2)] IMPORTING scott_continuity[[T1,T2],bool,(le1*le2),when] p: VAR admissible_pred[[T1,T2],(le1*le2)] dual_fixpoint_induction: LEMMA (FORALL x,y: p(x,y) IMPLIES p(phi(x),psi(y))) IMPLIES p(fix(phi),fix(psi)) END dual_fixpoints ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28