From: Ferruccio Guidi Date: Fri, 21 Feb 2014 16:38:05 +0000 (+0000) Subject: update in basic_2 and ground_2 X-Git-Tag: make_still_working~974 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c713c14cb3c69b1e9a4c693aed382eedc04512c1;p=helm.git update in basic_2 and ground_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 3f0d5d427..b5bc15268 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Tue, 11 Feb 2014 22:11:38 +0100
+
Last update: Fri, 21 Feb 2014 17:37:37 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index a306d00ea..be978d3e6 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Tue, 11 Feb 2014 22:11:38 +0100
+
Last update: Fri, 21 Feb 2014 17:37:37 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index cf44a00e4..b6ba4f2be 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,29 +163,29 @@ sizes files - 337 + 327 characters - 575141 + 564871 nodes - 1625856 + 1606196 propositions theorems 105 lemmas - 1144 + 1107 total - 1249 + 1212 concepts declared - 51 + 52 defined - 79 + 76 total - 130 + 128 @@ -431,8 +431,24 @@
strongly normalizing extended computation - lsx ( ? ⊢ ⬊*[?,?,?] ? ) - lsx_cpxs lsx_csx + lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? ) + lcosx_cpxs + +
+ + +
+ + + + +
+ + +
+ + lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? ) + lsx_ldrop lsx_cpxs lsx_csx
@@ -565,7 +581,7 @@ context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? ) - lpxs_ldrop lpxs_cpye lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
@@ -578,7 +594,7 @@
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) - cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs + cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs
@@ -672,7 +688,7 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_cpys lpx_cpye lpx_lleq lpx_aaa + lpx_ldrop lpx_cpys lpx_lleq lpx_aaa
@@ -702,7 +718,7 @@ irreducible forms for context-sensitive extended reduction cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) - cix_append cix_lift + cix_lift
@@ -716,7 +732,7 @@ reducible forms for context-sensitive extended reduction crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) - crx_append crx_lift + crx_lift
@@ -774,7 +790,7 @@ irreducible forms for context-sensitive reduction cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) - cir_append cir_lift + cir_lift
@@ -788,7 +804,7 @@ reducible forms for context-sensitive reduction crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) - crr_append crr_lift + crr_lift
@@ -909,19 +925,7 @@ lazy equivalence for local environments lleq ( ? ⋕[?,?] ? ) lleq_alt ( ? ⋕⋕[?,?] ? ) - lleq_ldrop lleq_fqus lleq_cpye lleq_lleq lleq_ext - -
- - - - -
- - evaluation for contxt-sensitive extended substitution - cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ ) - cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ ) - cpye_lift cpye_cpye + lleq_ldrop lleq_fqus lleq_lleq lleq_ext
@@ -933,7 +937,7 @@ contxt-sensitive extended multiple substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) - cpys_lift cpys_cny cpys_cpys + cpys_lift cpys_cpys
@@ -1024,20 +1028,6 @@ relocation - normal forms for context-sensitive extended substitution - cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ ) - cny_lift - -
- - -
- - - - -
- contxt-sensitive extended ordinary substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_cpy @@ -1052,9 +1042,9 @@
- local env. ref. for extended substitution - lsuby ( ? ⊑×[?,?] ? ) - lsuby_lsuby + restricted local env. ref. + lsubr ( ? ⊑ ? ) + lsubr_lsubr
@@ -1066,9 +1056,9 @@
- restricted local env. ref. - lsubr ( ? ⊑ ? ) - lsubr_lsubr + local env. ref. for extended substitution + lsuby ( ? ⊑×[?,?] ? ) + lsuby_lsuby
@@ -1128,7 +1118,7 @@ basic local env. slicing ldrop ( ⇩[?,?,?] ? ≡ ? ) - ldrop_append ldrop_lpx_sn ldrop_ldrop + ldrop_lpx_sn ldrop_leq ldrop_ldrop
@@ -1168,6 +1158,20 @@ grammar + equivalence for local environments + leq ( ? ≃[?,?] ? ) + leq_leq + +
+ + +
+ + + + +
+ pointwise extension of a relation lpx_sn lpx_sn_tc lpx_sn_lpx_sn @@ -1197,8 +1201,8 @@
closures - cl_shift ( ? @@ ? ) - cl_weight ( ♯{?,?,?} ) + cl_weight ( ♯{?,?,?} ) + cl_restricted_weight ( ♯{?,?} )
@@ -1314,6 +1318,6 @@

-
Last update: Tue, 11 Feb 2014 22:11:38 +0100
+
Last update: Fri, 21 Feb 2014 17:37:37 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 45c5ad29b..468fa6578 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,20 +56,20 @@ sizes files - 31 + 29 characters - 71828 + 72188 nodes - 56616 + 57742 propositions theorems 2 lemmas - 168 + 171 total - 170 + 173 concepts @@ -234,6 +234,6 @@

-
Last update: Tue, 11 Feb 2014 22:11:38 +0100
+
Last update: Fri, 21 Feb 2014 17:37:37 +0100