% a characterization of well-foundedness by the absence of infinitely
% descending sequences; well-founded orders.
%
% Author: Alfons Geser ([email protected]), 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.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
