]> matita.cs.unibo.it Git - helm.git/commit
we started to set up the strong normalization proof.
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 21 Feb 2011 19:05:11 +0000 (19:05 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 21 Feb 2011 19:05:11 +0000 (19:05 +0000)
commitef274cbe2b609a7fefc3efd3b1a2974ad81a55af
tree15c7e0be6d4b6fcafa2657cb6883778397e29ca4
parentcacbe3c6493ddce76c4c13379ade271d8dd172e8
we started to set up the strong normalization proof.
we plan to use saturated subsets of strongly normalizing terms
(see for instance D. Cescutti 2001, but a better citation is required)
rather than reducibility candidates.
The benefit is that reduction is not needed to define such subsets.
Also, this approach was never tried on a system with dependent types.
matita/matita/lib/lambda/rc.ma [new file with mode: 0644]
matita/matita/lib/lambda/sn.ma [new file with mode: 0644]