]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2bc0ba9) | patch
update in delayed_updating
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Tue, 4 Jan 2022 12:09:51 +0000 (13:09 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Tue, 4 Jan 2022 12:09:51 +0000 (13:09 +0100)
commit8db3579bec4d9a97af526f95a179587a2fbfe3e3
tree204e24f807422b67e268b9e26bc8d4d55063e521tree | snapshot
parent2bc0ba993e26ab77a792b38ba39da7a3dd03ad43commit | diff
update in delayed_updating

+ immediate reduction defined
+ some lemmas with lift simplified
matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma [deleted file] blob | history
matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma diff | blob | history
matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma [deleted file] blob | history
Unnamed repository; edit this file 'description' to name the repository.