Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: well_foundedness.pvs Sprache: PVS

Original von: PVS^©

% 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.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.