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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.