| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle noetherian.pvs Sprache: PVS |
|||||||||
|
%%-------------------** Abstract Reduction System (ARS) **-------------------
%% %% Authors : Andre Luiz Galdino %% Universidade Federal de Goiás - Brasil %% %% and %% %% Mauricio Ayala Rincon %% Universidade de Brasília - Brasil %% %% Last Modified On: December 02, 2006 %% %%--------------------------------------------------------------------------- noetherian[T : TYPE] : THEORY BEGIN IMPORTING ars_terminology[T], orders@well_foundedness[T] P : VAR PRED[T] R : VAR PRED[[T, T]] x, y : VAR T %%------------------------** Termination (Noetherian) **-------------------- %% %% A reduction -> (relation R) is %% %% - noetherian (terminating) iff there is no infinite %% descending chain a0 -> a1 -> .... In other words, a relation -> is %% noetherian if the inverse (converse) relation of -> is well founded. %% %% - convergent if is confluent and noetherian. %% %% - R_is_Noet_iff_TC_is: ->+ is terminating iff -> is. %% %% %% - noetherian_induction: To prove P(x) for all x, it suffices to prove P(x) %% under the assunption that P(y) holds for all %% successors y of x. %% %%-------------------------------------------------------------------------- noetherian?(R): bool = well_founded?(converse(R)) noetherian: TYPE = (noetherian?) convergent?(R): bool = confluent?(R) & noetherian?(R) R_is_Noet_iff_TC_is: LEMMA noetherian?(R) <=> noetherian?(TC(R)) noetherian_induction: LEMMA (FORALL (R: noetherian, P): (FORALL x: (FORALL y: TC(R)(x, y) IMPLIES P(y)) IMPLIES P(x)) IMPLIES (FORALL x: P(x))) END noetherian ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28