| products/sources/formale Sprachen/Isabelle/HOL/HOLCF/IOA/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 202 B |
|
Quelle modulo_equivalence.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: October 15, 2008 %% %%--------------------------------------------------------------------------- modulo_equivalence[T : TYPE] : THEORY BEGIN IMPORTING noetherian[T] R, S : VAR PRED[[T, T]] Eq : VAR equivalence x, y, z, w, u, v : VAR T R_Eq(R, Eq) : PRED[[T, T]] = Eq o R o Eq SC_Eq(R, Eq) : PRED[[T, T]] = union(SC(R), Eq) Eq_Eq(R, Eq) : equivalence = EC(SC_Eq(R, Eq)) joinable_m?(R, Eq)(x,y) : bool = EXISTS u,v: RTC(R)(x,u) & Eq(u,v) & RTC(R)(y,v) church_rosser_m?(R, Eq) : bool = FORALL x, y: Eq_Eq(R, Eq)(x,y) => joinable_m?(R, Eq)(x,y) local_confluent_m?(R, Eq) : bool = FORALL x, y, z: R(x,y) & R(x,z) => joinable_m?(R, Eq)(y,z) confluent_m?(R, Eq) : bool = FORALL x, y, z, w: RTC(R)(x,z) & Eq(x,y) & RTC(R)(y,w) => joinable_m?(R, Eq)(z,w) has_unique_nf_m?(R, Eq) : bool = FORALL x, y, u, v: is_normal_form?(R)(u) & is_normal_form?(R)(v) & RTC(R)(x,u) & Eq_Eq(R, Eq)(x,y) & RTC(R)(y,v) => Eq(u,v) locally_coherent?(R, Eq, S) : bool = symmetric?(S) & FORALL x, y, z: R(x,y) & S(x,z) => joinable_m?(R, Eq)(y,z) noetherian_m?(R, Eq) : bool = well_founded?(converse(R o Eq)) %%-------------------------------------- van_oostrom94 : LEMMA diamond_property?(RTC(R) o Eq) => confluent_m?(R, Eq) newman_lemma_general : THEOREM noetherian?(R) => (local_confluent_m?(R, Eq) & locally_coherent?(R, Eq, Eq) <=> confluent_m?(R, Eq)) END modulo_equivalence ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28