| 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 well_foundedness.pvs Sprache: PVS |
|||||||||
|
% a characterization of well-foundedness by the absence of infinitely
% descending sequences; well-founded orders. % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 / Jan 2005 well_foundedness[T: TYPE]: THEORY BEGIN IMPORTING orders[T], monotone_sequences[T], skolemization, closure_ops[T] n: VAR nat x, y: VAR T rel: VAR pred[[T, T]] seq: VAR sequence[T] no_infinite_descending_sequence: THEOREM well_founded?(rel) <=> empty?[sequence[T]](descending?(rel)) well_founded_is_irreflexive: JUDGEMENT (well_founded?) SUBTYPE_OF (irreflexive?[T]) well_founded_order?(rel): bool = well_founded?[T](rel) & transitive?[T](rel) well_order_is_well_founded_order: JUDGEMENT (well_ordered?[T]) SUBTYPE_OF (well_founded_order?) well_founded_order_is_well_founded: JUDGEMENT (well_founded_order?) SUBTYPE_OF (well_founded?) well_founded_order_is_strict_order: JUDGEMENT (well_founded_order?) SUBTYPE_OF (strict_order?) transitive_closure_preserves_well_foundedness: JUDGEMENT transitive_closure(rel: (well_founded?[T])) HAS_TYPE (well_founded_order?) END well_foundedness ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28