]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc21a7a) | patch
- confluence of context-free reduction on terms (tpr) closed!
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 6 Sep 2011 16:30:41 +0000 (16:30 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 6 Sep 2011 16:30:41 +0000 (16:30 +0000)
commit0466f6387b02f1d0644fb74eacca237e30589111
tree5d1bc91362a85c31158972ddd9ccd317a79183bctree | snapshot
parentdc21a7ae8ac838b0967db8d65ca30724ae556a47commit | diff
- confluence of context-free reduction on terms (tpr) closed!
- substitution lemma for tpr closed!
- so-called "substitution lemma" closed!
- some annotating
matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma diff | blob | history
matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma diff | blob | history
matita/matita/contribs/lambda-delta/Makefile diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.