X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=09ff142bf7dc510b68bf194cc9faedd44e4ebd42;hb=68a413ec8a20ef0d73fcd5810be7db659abe6f92;hp=65cc576272074a037687a069d7ee017e89958ad5;hpb=e5077c96c584933ad1467e8066780b46d7b0468c;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 65cc57627..09ff142bf 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,29 +159,29 @@ sizes files - 169 + 173 characters - 345703 + 363812 nodes - 964553 + 1057233 propositions theorems 75 lemmas - 710 + 750 total - 785 + 825 concepts declared - 42 + 43 defined - 66 + 68 total - 108 + 111 @@ -496,6 +496,36 @@ reduction + context-sensitive extended reduction + lpx ( ⦃?,?⦄ ⊢ ➡[?] ? ) + lpx_ldrop lpx_aaa + +
+ + +
+ + + + +
+ + +
+ + cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpx_lift + +
+ + +
+ + + + +
+ context-sensitive normal forms cnf ( ? ⊢ 𝐍⦃?⦄ ) cnf_liftt cnf_crf cnf_cif @@ -512,7 +542,7 @@ context-sensitive reduction lpr ( ? ⊢ ➡ ? ) - lpr_ldrop lpr_lpss lpr_aaa lpr_lpr + lpr_ldrop lpr_lpss lpr_lpr
@@ -788,9 +818,7 @@ relocation structural successor for closures fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) - -
- + fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ )
@@ -1004,6 +1032,6 @@

-
Last update: Mon, 03 Jun 2013 16:24:28 +0200
+
Last update: Sat, 08 Jun 2013 22:22:33 +0200