]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / notes.txt
1 1) (⫯f)@(1) = 1
2 2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
3 3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k
Unnamed repository; edit this file 'description' to name the repository.