]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d833e40) | patch
- main proof for strong normalization closed! ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 Jan 2012 21:05:57 +0000 (21:05 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 21 Jan 2012 21:05:57 +0000 (21:05 +0000)
commit30f9071732ef8d6957deac4179f39799eddda267
treeb343ca9c82bf5de30b5df7a10c963e88be6b8789tree | snapshot
parentd833e40ce45e301a01ddd9ea66c29fb2b34bb685commit | diff
- main proof for strong normalization closed! ...
- bug fix in lenv refinement for abstract candidates of reducibility (lsubc)
- lenv refinement for atomic arity assignment defined (lsuba) and relation
with lsubc proved
matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/Basic_2/notation.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.