X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=8507922549e11f63c891184bf90cde259161f908;hb=0c7129d74ba0bfbdf7f71ffcf46a8c8c93e7df14;hp=0ac117159aa947b5dca92fc7a97e369bb893493b;hpb=cb5ca7ea4e826e9331eabeaea44353caab00071e;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0ac117159..850792254 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -58,29 +58,29 @@ sizes files - 332 + 361 characters - 558713 + 651755 nodes - 1519426 + 1819305 propositions theorems - 107 + 121 lemmas - 1136 + 1293 total - 1243 + 1414 concepts declared - 50 + 54 defined - 79 + 81 total - 129 + 135 @@ -94,16 +94,23 @@ + @@ -228,8 +235,8 @@ 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 ( ? ⊢ ? ¡⫃[?,?] ? ) + 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
@@ -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,8 +472,10 @@ context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) - lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? ) lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + +
+
@@ -493,8 +502,10 @@ context-sensitive computation lprs ( ⦃?,?⦄ ⊢ ➡* ? ) - lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? ) lprs_ldrop lprs_cprs lprs_lprs + +
+
@@ -520,7 +531,7 @@
local env. ref. for abstract candidates of reducibility - lsubc ( ? ⊢ ? ⊑[?] ? ) + lsubc ( ? ⊢ ? ⫃[?] ? ) lsubc_ldrop lsubc_ldrops lsubc_lsuba
@@ -573,10 +584,8 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_lleq lpx_aaa - -
- + lpx_ldrop lpx_frees + lpx_lleq lpx_aaa
@@ -716,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
@@ -739,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
@@ -753,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
@@ -767,9 +776,9 @@
- local env. ref. for degree assignment - lsubd ( ? ⊢ ? ▪⊑ ? ) - lsubd_da lsubd_lsubd + parameters + sh + sd
@@ -781,9 +790,9 @@
- degree assignment - da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) - da_lift da_da + local env. ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⁝⫃ ? ) + lsuba_aaa lsuba_lsuba
@@ -795,9 +804,9 @@
- parameters - sh - sd + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
@@ -810,7 +819,7 @@
restricted local env. ref. - lsubr ( ? ⊑ ? ) + lsubr ( ? ⫃ ? ) lsubr_lsubr
@@ -820,9 +829,9 @@ - substitution + multiple substitution lazy equivalence - fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ ) + fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) fleq_fleq
@@ -838,8 +847,50 @@
- lleq ( ? ⋕[?,?] ? ) - lleq_alt lleq_leq lleq_ldrop lleq_fqus lleq_lleq + lleq ( ? ≡[?,?] ? ) + lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleq + +
+ + +
+ + + + +
+ + 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 + +
+ + +
+ + + + +
+ + pointwise union for local environments + llor ( ? ⩖[?,?] ? ≡ ? ) + llor_alt llor_ldrop + +
+ + +
+ + + + +
+ + context-sensitive exclusion from free variables + frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ ) + frees_append frees_leq frees_lift
@@ -847,12 +898,24 @@
+ + +
+ + contxt-sensitive extended multiple substitution + cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) + cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) + cpys_lift cpys_cpys + +
+ +
iterated structural successor for closures - fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) + fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) fqus_alt fqus_fqus
@@ -868,7 +931,7 @@
- fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) fqup_fqup
@@ -932,10 +995,10 @@ gr2_gr2 - relocation + substitution structural successor for closures - fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) - fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) + fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
@@ -950,7 +1013,7 @@
- fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
@@ -966,8 +1029,8 @@
global env. slicing - gdrop ( ⇩[?] ? ≡ ? ) - gdrop_gdrop + gget ( ⇩[?] ? ≡ ? ) + gget_gget
@@ -979,11 +1042,9 @@
- pointwise union for local environments - llor ( ? ⩖[?] ? ≡ ? ) - -
- + contxt-sensitive extended ordinary substitution + cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) + cpy_lift cpy_nlift cpy_cpy
@@ -995,9 +1056,9 @@
- pointwise extension of a relation - llpx_sn - llpx_sn_alt llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn + local env. ref. for extended substitution + lsuby ( ? ⊑×[?,?] ? ) + lsuby_lsuby
@@ -1009,9 +1070,7 @@
- -
- + pointwise extension of a relation lpx_sn lpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn @@ -1027,7 +1086,7 @@ basic local env. slicing ldrop ( ⇩[?,?,?] ? ≡ ? ) - ldrop_leq ldrop_ldrop + ldrop_append ldrop_leq ldrop_ldrop
@@ -1213,6 +1272,6 @@

-
Last update: Wed, 16 Apr 2014 18:29:12 +0200
+
Last update: Wed, 18 Jun 2014 17:05:27 +0200