X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fsex.ma;h=3fba7476ad0d087ac365539b8668024fc793e1ee;hp=49010d3305684e905ea643f6d35b3491c0780417;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma index 49010d330..3fba7476a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma @@ -32,6 +32,14 @@ inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝ interpretation "generic entrywise extension (local environment)" 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2). +definition sex_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. + definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → relation3 lenv bind bind → @@ -41,13 +49,14 @@ definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 → ∃∃I. R2 L1 I1 I & R1 L2 I2 I. -definition sex_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. +definition R_pw_replace3_sex: relation3 lenv bind bind → 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,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 → + ∀I. R2 L1 I1 I → R1 L2 I2 I. (* Basic inversion lemmas ***************************************************)