| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMRT/RobotRT/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 407 B |
|
SSL well_foundedness.pvs
Interaktion und |
|||||||||
|
% 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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.14Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28