From: Ferruccio Guidi Date: Sun, 5 May 2013 18:25:54 +0000 (+0000) Subject: partial update in basic_2 X-Git-Tag: make_still_working~1161 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b9d48c1a4433b3a2b17483bc207b2092f7ac4fd2;p=helm.git partial update in basic_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 078cbbeb2..25acf49f8 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 21 Apr 2013 17:53:32 +0200
+
Last update: Sun, 05 May 2013 20:24:23 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 11b277a34..736d0367c 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -74,7 +74,7 @@ files 5 characters - 5613 + 5790 nodes 9846 @@ -199,6 +199,6 @@

-
Last update: Sun, 21 Apr 2013 17:53:32 +0200
+
Last update: Sun, 05 May 2013 20:24:24 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3353e93a2..df81e0374 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,29 +159,29 @@ sizes files - 213 + 195 characters - 392008 + 365052 nodes - 1052979 + 984918 propositions theorems - 79 + 84 lemmas - 875 + 781 total - 954 + 865 concepts declared - 45 + 42 defined - 75 + 70 total - 120 + 112 @@ -294,9 +294,6 @@
- -
-
@@ -307,10 +304,7 @@ yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) yprs_yprs ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) - ygt_ygt - -
- + ygt_ygt @@ -322,9 +316,6 @@
- -
-
@@ -339,9 +330,6 @@
- -
-
@@ -356,9 +344,6 @@
- -
-
@@ -371,9 +356,6 @@
- -
-
@@ -390,9 +372,6 @@
- -
-
@@ -407,9 +386,6 @@
- -
-
@@ -424,9 +400,6 @@
- -
-
@@ -439,9 +412,6 @@
- -
-
@@ -458,9 +428,6 @@
- -
-
@@ -475,9 +442,6 @@
- -
-
@@ -490,9 +454,6 @@
- -
-
@@ -509,9 +470,6 @@
- -
-
@@ -526,9 +484,6 @@
- -
-
@@ -543,9 +498,6 @@
- -
-
@@ -560,9 +512,6 @@
- -
-
@@ -577,9 +526,6 @@ csn ( ? ⊢ ⬊* ? ) csn_alt ( ? ⊢ ⬊⬊* ? ) csn_lift csn_cpr csn_lfpr - -
-
@@ -589,29 +535,9 @@
context-sensitive computation - cprs (? ⊢ ? ➡* ?) - cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector - -
- - -
- - -
- - - - -
- - context-free computation - ltprs ( ? ➡* ? ) - ltprs_alt ( ? ➡➡* ? ) - ltprs_ldrop ltprs_ltprs - -
- + lprs ( ? ⊢ ➡* ? ) + lprs_alt ( ? ⊢ ➡➡* ? ) + lprs_ldrop lprs_aaa lprs_cprs lprs_lprs
@@ -623,11 +549,8 @@
- tprs ( ? ➡* ?) - tprs_lift tprs_tprs - -
- + cprs ( ? ⊢ ? ➡* ?) + cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_aaa cprs_lpr cprs_cprs cprs_tstc cprs_tstc_vector
@@ -645,9 +568,6 @@
- -
-
@@ -660,9 +580,6 @@ acp acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) acp_aaa - -
-
@@ -675,30 +592,6 @@
- -
- - -
- - - - -
- - -
- - chnf ( ? ⊢ 𝐇𝐍⦃?⦄ ) - -
- - -
- - -
-
@@ -713,9 +606,6 @@
- -
-
@@ -728,10 +618,7 @@
cpr ( ? ⊢ ? ➡ ? ) - lpr_tshf cpr_lift cpr_cif - -
- + cpr_lift cpr_cif
@@ -747,10 +634,7 @@ crf ( ? ⊢ 𝐑⦃?⦄ ) crf_append cif ( ? ⊢ 𝐈⦃?⦄ ) - cif_append - -
- + cif_append unfold @@ -760,9 +644,6 @@
- -
-
@@ -779,9 +660,6 @@
- -
-
@@ -798,9 +676,6 @@
- -
-
@@ -815,9 +690,6 @@
- -
-
@@ -830,9 +702,6 @@
- -
-
@@ -847,9 +716,6 @@
- -
-
@@ -864,9 +730,6 @@
- -
-
@@ -881,9 +744,6 @@
- -
-
@@ -896,9 +756,6 @@
- -
-
@@ -915,6 +772,17 @@
+ +
+ + + + +
+ + local env. ref. for substitution + lsubr ( ? ⊑ ? ) + lsubr_lsubr
@@ -932,9 +800,6 @@
- -
-
@@ -951,9 +816,6 @@
- -
-
@@ -968,9 +830,6 @@
- -
-
@@ -985,9 +844,6 @@
- -
-
@@ -1004,9 +860,6 @@
- -
-
@@ -1019,10 +872,7 @@ gr2 ( @⦃?,?⦄ ≡ ? ) gr2_plus ( ? + ? ) gr2_minus ( ? ▭ ? ≡ ? ) - gr2_gr2 - -
- + gr2_gr2 relocation @@ -1034,9 +884,6 @@
- -
-
@@ -1051,9 +898,6 @@
- -
-
@@ -1064,25 +908,7 @@ basic local env. slicing ldrop ( ⇩[?,?] ? ≡ ? ) - ldrop_append ldrop_lpx ldrop_lpx_sn ldrop_lbotr ldrop_ldrop - -
- - -
- - -
- - - - -
- - local env. ref. for substitution - lsubr ( ? ⊑[?,?] ? ) - (lsubr_lsubr) - lsubr_lbotr ( ⊒[?,?] ? ) + ldrop_append ldrop_lpx_sn ldrop_ldrop
@@ -1100,9 +926,6 @@
- -
-
@@ -1119,21 +942,15 @@
- -
-
grammar - same head term form - tshf ( ? ≈ ? ) - (tshf_tshf) - -
- + pointwise extension of a relation + lpx_sn + lpx_sn_tc lpx_sn_lpx_sn
@@ -1151,9 +968,6 @@
- -
-
@@ -1168,9 +982,6 @@
- -
-
@@ -1187,9 +998,6 @@
- -
-
@@ -1204,8 +1012,7 @@ lenv lenv_weight ( ♯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) - lenv_px lenv_px_sn lenv_px_bi + lenv_append ( ? @@ ? ) @@ -1217,10 +1024,7 @@ term term_weight ( ♯{?} ) term_simple ( 𝐒⦃?⦄ ) - term_vector - -
- + term_vector @@ -1236,9 +1040,6 @@
- -
-
@@ -1255,9 +1056,6 @@
- -
-
@@ -1296,6 +1094,6 @@

-
Last update: Sun, 21 Apr 2013 17:53:32 +0200
+
Last update: Sun, 05 May 2013 20:24:24 +0200