X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fllor.ma;h=4f3d948decd40b463a7cfdeb2ce5fcd95055ab10;hb=a2092f7ba4c7c566ea90653ff57e4623ab94d8d5;hp=df157a9902d9531e6f1482a144580feb914b0c52;hpb=4aa343ba8e1c807108203ece4e142c81b27d28e8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma index df157a990..4f3d948de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma @@ -23,7 +23,7 @@ definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → ∨∨ (∧∧ yinj i < d & I1 = I & V1 = V) | (∧∧ (L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ → ⊥) & I1 = I & V1 = V) | - (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V) + (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V) ). interpretation