X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frex.ma;h=bfaf0cbce5d2b0cb831b246a216a7097384b359c;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=07ad9fe0587b434e67a5198c9ea22a2de3a7810b;hpb=db020b4218272e2e35641ce3bc3b0a9b3afda899;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma index 07ad9fe05..bfaf0cbce 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rex.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +include "ground_2/xoa/ex_1_2.ma". +include "ground_2/xoa/ex_3_4.ma". +include "ground_2/xoa/ex_4_4.ma". +include "ground_2/xoa/ex_4_5.ma". include "ground_2/relocation/rtmap_id.ma". include "static_2/notation/relations/relation_4.ma". include "static_2/syntax/cext2.ma". @@ -34,7 +38,7 @@ definition R_confluent2_rex: relation4 (relation3 lenv term term) ∃∃T. R2 L1 T1 T & R1 L2 T2 T. definition rex_confluent: relation … ≝ - λR1,R2. + λR1,R2. ∀K1,K,V1. K1 ⪤[R1,V1] K → ∀V. R1 K1 V1 V → ∀K2. K ⪤[R2,V] K2 → K ⪤[R2,V1] K2. @@ -319,7 +323,7 @@ lemma rex_isid (R1) (R2): /4 width=7 by sex_co_isid, ex2_intro/ qed-. -lemma rex_unit_sn (R1) (R2): +lemma rex_unit_sn (R1) (R2): ∀I,K1,L2. K1.ⓤ{I} ⪤[R1,#0] L2 → K1.ⓤ{I} ⪤[R2,#0] L2. #R1 #R2 #I #K1 #L2 #H elim (rex_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct @@ -327,8 +331,8 @@ elim (rex_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct qed-. (* Basic_2A1: removed theorems 9: - llpx_sn_skip llpx_sn_lref llpx_sn_free + llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_fwd_lref - llpx_sn_Y llpx_sn_ge_up llpx_sn_ge - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx + llpx_sn_Y llpx_sn_ge_up llpx_sn_ge + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx *)