|
%%-------------------** 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
%%
%%---------------------------------------------------------------------------
results_commutation[T : TYPE] : THEORY
BEGIN
IMPORTING noetherian[T]
R1, R2 : VAR PRED[[T, T]]
x, y, z, r : VAR T
%%------------------------** Commutation Lemma **---------------------------
%%
%%
%% - Local_Comu_and_Noeth: If -> and --> locally commute and (-> union -->)
%% is noetherian, then -> and --> commutes.
%%
%%
%% - commute_and_iterate_one: If -> and --> strongly commuting and
%% y *<- x --> z then exists r such that
%% y -->= r *<- z.
%%
%%
%% - commute_and_iterate_two: If -> and --> strongly commuting and
%% y *<- x -->* z then exists r such that
%% y -->* r *<- z.
%%
%%
%% - Comutation_Lemma: Two strongly commuting reductions commute.
%%
%%
%%---------------------------------------------------------------------------
Local_Comu_and_Noeth: THEOREM locally_commute?(R1,R2)
& noetherian?(union(R1, R2)) => commute?(R1,R2)
commute_and_iterate_one: LEMMA FORALL (n: nat): strong_commute?(R1,R2) &
iterate(R1, n)(x,y) & R2(x,z) =>
EXISTS r: RTC(R1)(z,r) & RC(R2)(y,r)
commute_and_iterate_two: LEMMA FORALL (n,m: nat): strong_commute?(R1,R2) &
iterate(R1, n)(x,y) & iterate(R2, m)(x,z) =>
EXISTS r: RTC(R2)(y,r) & RTC(R1)(z,r)
Comutation_Lemma: THEOREM strong_commute?(R1,R2) => commute?(R1,R2)
END results_commutation
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
