X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2fd65b8cd1e980dca197760d1c519ce671381393;hb=8913001064f595c21ed4234884e7c370be2afb52;hp=16bb892ad42f9c5997426a51a76f306821d03259;hpb=f5c6d4c41cbbdabdf998be0c4a8242849a790f1b;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 16bb892ad..2fd65b8cd 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,29 +163,29 @@ sizes files - 265 + 268 characters - 399415 + 407502 nodes - 1201927 + 1213911 propositions theorems - 81 + 83 lemmas - 806 + 826 total - 887 + 909 concepts declared 44 defined - 79 + 81 total - 123 + 125 @@ -411,8 +411,8 @@
strongly normalizing computation - csn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csn_tstc_vector csn_aaa + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) + csx_tstc_vector csx_aaa
@@ -427,9 +427,9 @@
- csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) - csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) - csn_lift csn_lpx + csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) + csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) + csx_lift csx_lpx
@@ -439,8 +439,8 @@
"big tree" parallel computation - ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) - ygt_lift ygt_ygt + fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) + fpbg_lift fpbg_fpbg
@@ -455,11 +455,9 @@
- yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) - yprs_lift yprs_yprs - -
- + fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) + fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) + fpbs_lift fpbs_fpbs
@@ -563,8 +561,24 @@ reduction "big tree" parallel reduction - ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) - ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) + fpbc_lift + +
+ + +
+ + + + +
+ + +
+ + fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) + fpb_lift
@@ -841,8 +855,8 @@
iterated structural successor for closures - fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) - fsups_fsups + fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) + fqus_fqus
@@ -857,8 +871,8 @@
- fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) - fsupp_fsupp + fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) + fqup_fqup
@@ -923,9 +937,9 @@ relocation structural successor for closures - fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) - fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) - fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) + fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) + fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )
@@ -1136,6 +1150,6 @@

-
Last update: Fri, 04 Oct 2013 17:03:32 +0200
+
Last update: Sat, 12 Oct 2013 19:38:34 +0200