X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2.ldw.xml;h=be3c16d738801109e4ab49ab78e61d0a3321a900;hb=bac74b5cff042d37e1abc9c961a6c41094b8a294;hp=a5c53bf3e17a212da07212849aec0276de36e8a5;hpb=31be09cc0d040577917783e050e1d38c0daa8f01;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index a5c53bf3e..be3c16d73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,8 +27,12 @@ Stage "B" + + Parametrized applicability condition + allows λδ-2B to generalize both λδ-2A and λδ-1B. + - Extended (λδ-2) and restricted (λδ-1) validity is decidable + Extended (λδ-2A) and restricted (λδ-1B) validity is decidable (anniversary milestone). @@ -37,7 +41,7 @@ (i.e. no induction on the degree). - Extended (λδ-2) and restricted (λδ-1) type rules justified. + Extended (λδ-2A) and restricted (λδ-1A) type rules justified. λδ-2A completed with