update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / notes.txt

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
index d70abbe43d82e43071a06d02922002a614dc8c4b..079d44d8d9b0eef3f7789fd27d10432a6656e23c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
@@ -1,3 +1,10 @@
-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.
+
+. replace.sh . "/substitution/" "/unwind/"
+. replace.sh . ↑ ▼ 
+
+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;;;;