X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=8e5745e167831a675faa3ae35b90f89649ebba45;hb=645b62762e9c86e343d4741541a2ddccfed8ebc7;hp=71e132de8f0fb11d83df8203928b836cc46e16d9;hpb=4aa343ba8e1c807108203ece4e142c81b27d28e8;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 71e132de8..8e5745e16 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -58,20 +58,20 @@ sizes files - 354 + 361 characters - 639332 + 652919 nodes - 1776063 + 1828390 propositions theorems - 117 + 121 lemmas - 1271 + 1299 total - 1388 + 1420 concepts @@ -94,16 +94,23 @@ + @@ -229,7 +236,7 @@ dynamic typing local env. ref. for stratified native validity lsubsv ( ? ⊢ ? ¡⫃[?,?] ? ) - lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv + lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv
@@ -243,7 +250,7 @@ stratified native validity snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) - snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs + snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve
@@ -352,7 +359,7 @@ lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? ) - lsx_ldrop lsx_lpx lsx_lpxs llsx_csx + lsx_drop lsx_lpx lsx_lpxs llsx_csx
@@ -392,7 +399,7 @@
"big tree" parallel computation - fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ ) + fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) fpbg_lift fpbg_fleq fpbg_fpbg
@@ -408,7 +415,7 @@
- fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ ) + fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ ) fpbc_fleq fpbc_fpbs
@@ -465,7 +472,7 @@ context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) - lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
@@ -495,7 +502,7 @@ context-sensitive computation lprs ( ⦃?,?⦄ ⊢ ➡* ? ) - lprs_ldrop lprs_cprs lprs_lprs + lprs_drop lprs_cprs lprs_lprs
@@ -525,7 +532,7 @@ local env. ref. for abstract candidates of reducibility lsubc ( ? ⊢ ? ⫃[?] ? ) - lsubc_ldrop lsubc_ldrops lsubc_lsuba + lsubc_drop lsubc_drops lsubc_lsuba
@@ -577,7 +584,7 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_frees + lpx_drop lpx_frees lpx_lleq lpx_aaa
@@ -647,7 +654,7 @@ context-sensitive reduction lpr ( ⦃?,?⦄ ⊢ ➡ ? ) - lpr_ldrop lpr_lpr + lpr_drop lpr_lpr
@@ -718,18 +725,18 @@
iterated static type assignment - lsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? ) - lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? ) - lsstas_lift lsstas_aaa lsstas_lsstas + lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? ) + lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? ) + lstas_lift lstas_aaa lstas_da lstas_lstas
static typing - local env. ref. for atomic arity assignment - lsuba ( ? ⊢ ? ⁝⫃ ? ) - lsuba_ldrop lsuba_aaa lsuba_lsuba + local env. ref. for degree assignment + lsubd ( ? ⊢ ? ▪⫃ ? ) + lsubd_da lsubd_lsubd
@@ -741,9 +748,9 @@
- atomic arity assignment - aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_da aaa_ssta aaa_aaa + degree assignment + da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) + da_lift da_aaa da_sta da_da
@@ -755,9 +762,9 @@
- stratified static type assignment - ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) - ssta_lift ssta_lpx_sn ssta_ssta + static type assignment + sta ( ⦃?,?⦄ ⊢ ? •[?] ? ) + sta_lift sta_lpx_sn sta_aaa sta_sta
@@ -769,9 +776,9 @@
- local env. ref. for degree assignment - lsubd ( ? ⊢ ? ▪⫃ ? ) - lsubd_da lsubd_lsubd + parameters + sh + sd
@@ -783,9 +790,9 @@
- degree assignment - da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) - da_lift da_da + local env. ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⁝⫃ ? ) + lsuba_aaa lsuba_lsuba
@@ -797,9 +804,9 @@
- parameters - sh - sd + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
@@ -824,7 +831,7 @@ multiple substitution lazy equivalence - fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ ) + fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) fleq_fleq
@@ -840,8 +847,8 @@
- lleq ( ? ⋕[?,?] ? ) - lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleq + lleq ( ? ≡[?,?] ? ) + lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq
@@ -855,7 +862,7 @@ lazy pointwise extension of a relation llpx_sn - llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor + llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor
@@ -869,7 +876,7 @@ pointwise union for local environments llor ( ? ⩖[?,?] ? ≡ ? ) - llor_ldrop + llor_alt llor_drop
@@ -883,7 +890,7 @@ context-sensitive exclusion from free variables frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ ) - frees_leq frees_lift + frees_append frees_leq frees_lift
@@ -938,8 +945,8 @@
iterated local env. slicing - ldrops ( ⇩*[?,?] ? ≡ ? ) - ldrops_ldrop ldrops_ldrops + drops ( ⇩*[?,?] ? ≡ ? ) + drops_drop drops_drops
@@ -1065,7 +1072,7 @@ pointwise extension of a relation lpx_sn - lpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn + lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
@@ -1078,8 +1085,8 @@
basic local env. slicing - ldrop ( ⇩[?,?,?] ? ≡ ? ) - ldrop_leq ldrop_ldrop + drop ( ⇩[?,?,?] ? ≡ ? ) + drop_append drop_leq drop_drop
@@ -1120,7 +1127,7 @@ grammar equivalence for local environments - leq ( ? ≃[?,?] ? ) + leq ( ? ⩬[?,?] ? ) leq_leq
@@ -1134,7 +1141,7 @@
same top term constructor - tstc ( ? ≃ ? ) + tstc ( ? ≂ ? ) tstc_tstc tstc_vector
@@ -1265,6 +1272,6 @@

-
Last update: Sat, 07 Jun 2014 21:44:26 +0200
+
Last update: Sat, 28 Jun 2014 20:29:31 +0200