| 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 finite_pointwise_orders.pvs Sprache: PVS |
|||||||||
|
% pointwise orders on functions whose domain is finite
% their strict part preserves well-founded orders % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 finite_pointwise_orders[D, R: TYPE]: THEORY BEGIN ASSUMING domain_finiteness: ASSUMPTION is_finite_type[D] ENDASSUMING IMPORTING numbers_infinite, % to discharge a TCC of infinite_pigeonhole pointwise_orders[D, R], well_foundedness, infinite_pigeonhole[nat, D], integer_enumerations[nat] d: VAR D r: VAR R n: VAR nat rel: VAR (transitive?[R]) seq: VAR [nat -> [D -> R]] g: VAR (preserves[nat, nat](<, <)) % enumerates the subsequence indices % an infinite sequence of elements from the finite type D must contain % a mono-chromatic subsequence infinite_pigeonhole: LEMMA FORALL (f: [nat -> D]): EXISTS d, g: FORALL n: f(g(n)) = d descending_exists: LEMMA descending?(strictly_pointwise(rel))(seq) => EXISTS d: rel(seq(n + 1)(d), seq(n)(d)) descending_reflexive_closure: LEMMA descending?(strictly_pointwise(rel))(seq) => descending?[R](reflexive_closure[R](rel))(LAMBDA n: seq(n)(d)) pointwise_pigeonhole: LEMMA descending?(strictly_pointwise(rel))(seq) => EXISTS d, g: descending?(rel)(LAMBDA n: seq(g(n))(d)) strictly_pointwise_well_founded_order: JUDGEMENT strictly_pointwise(rel: (well_founded_order?[R])) HAS_TYPE (well_founded_order?[[D -> R]]) END finite_pointwise_orders ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28