X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fnotes.txt;h=79d8698f97508071bcf21a0da735de3f464f9fd4;hb=d108bcea8ebae11b03e8d8a155dfd3f2eb445127;hp=47d6b3600521b427315fbef0aa2734f241798dbd;hpb=4939d8280cb3467cd8fa648b1cea04f74d71e8b7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
index 47d6b3600..79d8698f9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
@@ -1,8 +1,3 @@
-1) (⫯f)@(1) = 1
-2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
-3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k
-
-
 lemma pr_pat_after_uni_tls (i2) (i1):
       ∀f2. @❨i1, f2❩ ≘ i2 →
       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
@@ -13,3 +8,5 @@ lemma pr_pat_after_uni_tls (i2) (i1):
 266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;;
 266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;;
 266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;;
+
+include "ground/xoa/ex_6_5.ma".