X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs.ma;h=291892f71d2a2ed2a5a8821a274fca586dd69b83;hp=a589666960aa5f6e3171ddd2495c3808fb8c09ff;hb=f7296f9cf2ee73465a374942c46b138f35c42ccb;hpb=e8971d3db8935436e6dddc27fe1ae168c7f3b315 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index a58966696..291892f71 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -36,16 +36,18 @@ definition R_pw_confluent2_lexs: relation3 lenv bind bind → relation3 lenv bin relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 rtmap lenv bind ≝ - λR1,R2,RN1,RP1,RN2,RP2,f,L0,T0. - ∀T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0. + ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 → ∀L1. L0 ⪤*[RN1, RP1, f] L1 → ∀L2. L0 ⪤*[RN2, RP2, f] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. - -definition lexs_transitive: relation5 (relation3 lenv bind bind) - (relation3 lenv bind bind) … ≝ - λR1,R2,R3,RN,RP. - ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⪤*[RN, RP, f] L2 → - ∀T2. R2 L2 T T2 → R3 L1 T1 T2. + ∃∃I. R2 L1 I1 I & R1 L2 I2 I. + +definition lexs_transitive: relation3 lenv bind bind → relation3 lenv bind bind → + relation3 lenv bind bind → + relation3 lenv bind bind → relation3 lenv bind bind → + relation3 rtmap lenv bind ≝ + λR1,R2,R3,RN,RP,f,L1,I1. + ∀I. R1 L1 I1 I → ∀L2. L1 ⪤*[RN, RP, f] L2 → + ∀I2. R2 L2 I I2 → R3 L1 I1 I2. (* Basic inversion lemmas ***************************************************)