|
%%-------------------** 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
%%
%%---------------------------------------------------------------------------
newman_yokouchi[T : TYPE] : THEORY
BEGIN
IMPORTING results_confluence[T],
noetherian[T]
R, S : VAR PRED[[T, T]]
x, y, z : VAR T
%%----------------------** Newman and Yokouchi's Lemmas **--------------------%%
Newman_lemma: THEOREM noetherian?(R) => (confluent?(R) <=> locally_confluent?(R))
Yokouchi_lemma_ax1: LEMMA ( noetherian?(R) & confluent?(R) &
(FORALL x, y, z: ( S(x,y) & R(x,z) ) =>
( EXISTS (u: T): RTC(R)(y,u) & (RTC(R) o S o RTC(R))(z,u) )))
=> (FORALL x, y, z: ( S(x,y) & RTC(R)(x,z) ) =>
( EXISTS (w: T): RTC(R)(y,w) & (RTC(R) o S o RTC(R))(z,w) ))
Yokouchi_lemma: THEOREM (noetherian?(R) & confluent?(R) & diamond_property?(S)
& (FORALL x, y, z: ( S(x,y) & R(x,z) ) =>
( EXISTS (u: T): RTC(R)(y,u) & (RTC(R) o S o RTC(R))(z,u) )))
=> diamond_property?(RTC(R) o S o RTC(R))
end newman_yokouchi
¤ Dauer der Verarbeitung: 0.0 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.
|
