X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=108da399f7e74507ffeede80cbdb4cf8703b1ea6;hb=43d727778aacdda8feb1228cf37860e7713930f2;hp=9bb35569b1636b1c915ff6605a3e7f50fc9f841e;hpb=7bedf1797ba168f0742194b2add69575e5d4a5cd;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 9bb35569b..108da399f 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -29,7 +29,7 @@
category | objects | |||||
sizes | files | 190 | bytes | 718106 | ||
propositions | theorems | 68 | lemmas | 859 | total | 927 |
concepts | declared | 40 | defined | 71 | total | 111 |
category | objects | |||||
sizes | files | 199 | bytes | 739801 | ||
propositions | theorems | 70 | lemmas | 880 | total | 950 |
concepts | declared | 40 | defined | 72 | total | 112 |
component | plane | files | ||||||||
dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift | snv_aaa | ||||||
equivalence | context-sensitive equivalence | lcpcs ( ? ⢠â¬* ? ) | lcpcs_aaa | lcpcs_lcprs | lcpcs_lcpcs | |||||
cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss | cpcs_delift | cpcs_ltpr | cpcs_cprs | cpcs_cpcs | |||||
conversion | context-sensitive conversion | lcpc ( ? ⢠⬠? ) | lcpc_lcpc | |||||||
cpc ( ? ⢠? ⬠? ) | cpc_cpc | |||||||||
computation | extended computation | xprs ( â¦?,?⦠⢠? â¸*[?] ? ) | xprs_lift | xprs_aaa | xprs_cprs | |||||
weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | ||||||||
strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | ||||||
csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift | csn_cpr | csn_lcpr | ||||||
context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs | ||||||
cprs (? ⢠? â¡* ?) | cprs_lift | cprs_delift | cprs_ltpr | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector | ||
context-free computation | ltprs ( ? â¡* ? ) | ltprs_alt ( ? â¡â¡* ? ) | ltprs_ldrop | ltprs_ltprs | ||||||
tprs ( ? â¡* ?) | tprs_lift | tprs_tprs | ||||||||
local env. ref. for abstract candidates of reducibility | lsubc ( ? â[?] ? ) | lsubc_ldrop | lsubc_ldrops | lsubc_lsuba | ||||||
support for abstract computation properties | acp | acp_cr ( â¦?,?⦠ϵ[?] ã?ã ) | acp_aaa | |||||||
reducibility | extended reduction | xpr ( â¦?,?⦠⢠? â¸[?] ? ) | xpr_lift | xpr_aaa | ||||||
context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift | cnf_cif | |||||||
context-sensitive reduction | lcpr ( ? ⢠⡠? ) | lcpr_aaa | lcpr_cpr | lcpr_lcpr | ||||||
cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpss | cpr_delift | cpr_ltpr | cpr_cpr | |||||
context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | ||||||
focalized reduction | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | |||||||||
fpr ( �,?⦠⡠�,?⦠) | ||||||||||
context-free normal forms | thnf ( ððâ¦?⦠) | |||||||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_ltpss_dx | ltpr_ltpss_sn | ltpr_aaa | ltpr_ltpr | |||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_delift | tpr_tpr | ||||||
unwind | ||||||||||
static typing | local env. ref. for stratified static type assignment | lsubss ( ? ââ ? ) | lsubss_ldrop | lsubss_ssta | lsubss_lsubss | |||||
stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift | ssta_ltpss_dx | ssta_ltpss_sn | ssta_aaa | ssta_ssta | ||||
local env. ref. for atomic arity assignment | lsuba ( ? ââ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | ||||||
atomic arity assignment | aaa ( ? ⢠? â ? ) | aaa_lift | aaa_lifts | aaa_ltpss_dx | aaa_ltpss_sn | aaa_aaa | ||||
parameters | sh | sd | ||||||||
unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop | thin_delift | ||||||
inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift | delift_tpss | delift_ltpss | delift_delift | ||||
partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_ldrop | ltpss_sn_tps | ltpss_sn_tpss | ltpss_sn_ltpss_sn | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | ||||
ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop | ltpss_dx_tps | ltpss_dx_tpss | ltpss_dx_ltpss_dx | ||||||
tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | |||||||
generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | ldrops_ldrop | ldrops_ldrops | |||||||
generic term relocation | lifts_vector ( â§*[?] ? â¡ ? ) | lifts_lift_vector | ||||||||
lifts ( â§*[?] ? â¡ ? ) | lifts_lift | lifts_lifts | ||||||||
support for generic relocation | gr2 ( @â¦?,?⦠⡠? ) | gr2_plus ( ? + ? ) | gr2_minus ( ? â ? â¡ ? ) | gr2_gr2 | ||||||
substitution | parallel substitution | tps ( ? ⢠? â¶[?,?] ? ) | tps_lift | tps_tps | ||||||
global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | ||||||||
basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_append | ldrop_lpx | ldrop_sfr | ldrop_ldrop | |||||
local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | |||||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | ||||||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | |||||||||
grammar | same head term form | tshf ( ? â ? ) | (tshf_tshf) | |||||||
same top term constructor | tstc ( ? â ? ) | tstc_tstc | tstc_vector | |||||||
closures | cl_shift ( ? @@ ? ) | cl_weight ( #{?,?} ) | ||||||||
internal syntax | genv | |||||||||
lenv | lenv_weight ( #{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) | lenv_px | lenv_px_bi | |||||
term | term_weight ( #{?} ) | term_simple ( ðâ¦?⦠) | term_vector | |||||||
item | ||||||||||
external syntax | aarity |
component | plane | files | |||||||||
dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift | snv_aaa | |||||||
equivalence | context-sensitive equivalence | lfpcs ( â¦?⦠â¬* â¦?⦠) | lfpcs_aaa | lfpcs_lfprs | lfpcs_lfpcs | ||||||
cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss | cpcs_delift | cpcs_aaa | cpcs_ltpr | cpcs_cprs | cpcs_cpcs | |||||
conversion | context-sensitive conversion | lfpc ( �⦠⬠�⦠) | lfpc_lfpc | ||||||||
cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||||||||
computation | extended computation | xprs ( â¦?,?⦠⢠? â¸*[?] ? ) | xprs_lift | xprs_aaa | xprs_cprs | ||||||
weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | |||||||||
strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | |||||||
csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift | csn_cpr | csn_lfpr | |||||||
context-sensitive computation | lfprs ( â¦?⦠â¡* â¦?⦠) | lfprs_aaa | lfprs_cprs | lfprs_lfprs | |||||||
cprs (? ⢠? â¡* ?) | cprs_lift | 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 | |||||||
tprs ( ? â¡* ?) | tprs_lift | tprs_tprs | |||||||||
local env. ref. for abstract candidates of reducibility | lsubc ( ? â[?] ? ) | lsubc_ldrop | lsubc_ldrops | lsubc_lsuba | |||||||
support for abstract computation properties | acp | acp_cr ( â¦?,?⦠ϵ[?] ã?ã ) | acp_aaa | ||||||||
reducibility | extended reduction | xpr ( â¦?,?⦠⢠? â¸[?] ? ) | xpr_lift | xpr_aaa | |||||||
context-sensitive focalized reduction | cfpr ( ? ⢠�,?⦠⡠�,?⦠) | cnfpr_ltpss | cfpr_aaa | cfpr_cpr | |||||||
context-free focalized reduction | lfpr ( â¦?⦠⡠â¦?⦠) | lfpr_aaa | lfpr_cpr | lfpr_fpr | lfpr_lfpr | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | |||||
fpr ( �,?⦠⡠�,?⦠) | fpr_cpr | ||||||||||
context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift | cnf_cif | ||||||||
context-sensitive reduction | cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_tpss | cpr_ltpss | cpr_delift | cpr_aaa | cpr_ltpr | cpr_cpr | |||
context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | |||||||
context-free normal forms | thnf ( ððâ¦?⦠) | ||||||||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_ltpss_dx | ltpr_ltpss_sn | ltpr_aaa | ltpr_ltpr | ||||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_delift | tpr_tpr | |||||||
unwind | |||||||||||
static typing | local env. ref. for stratified static type assignment | lsubss ( ? ââ ? ) | lsubss_ldrop | lsubss_ssta | lsubss_lsubss | ||||||
stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift | ssta_ltpss_dx | ssta_ltpss_sn | ssta_aaa | ssta_ssta | |||||
local env. ref. for atomic arity assignment | lsuba ( ? ââ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | |||||||
atomic arity assignment | aaa ( ? ⢠? â ? ) | aaa_lift | aaa_lifts | aaa_ltpss_dx | aaa_ltpss_sn | aaa_aaa | |||||
parameters | sh | sd | |||||||||
unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop | thin_delift | |||||||
inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift | delift_tpss | delift_ltpss | delift_delift | |||||
partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_ldrop | ltpss_sn_tps | ltpss_sn_tpss | ltpss_sn_ltpss_sn | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | |||||
ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop | ltpss_dx_tps | ltpss_dx_tpss | ltpss_dx_ltpss_dx | |||||||
tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | ||||||||
generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | ldrops_ldrop | ldrops_ldrops | ||||||||
generic term relocation | lifts_vector ( â§*[?] ? â¡ ? ) | lifts_lift_vector | |||||||||
lifts ( â§*[?] ? â¡ ? ) | lifts_lift | lifts_lifts | |||||||||
support for generic relocation | gr2 ( @â¦?,?⦠⡠? ) | gr2_plus ( ? + ? ) | gr2_minus ( ? â ? â¡ ? ) | gr2_gr2 | |||||||
substitution | parallel substitution | tps ( ? ⢠? â¶[?,?] ? ) | tps_lift | tps_tps | |||||||
global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | |||||||||
basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_append | ldrop_lpx | ldrop_sfr | ldrop_ldrop | ||||||
local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | ||||||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | |||||||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | ||||||||||
grammar | same head term form | tshf ( ? â ? ) | (tshf_tshf) | ||||||||
same top term constructor | tstc ( ? â ? ) | tstc_tstc | tstc_vector | ||||||||
closures | cl_shift ( ? @@ ? ) | cl_weight ( #{?,?} ) | |||||||||
internal syntax | genv | ||||||||||
lenv | lenv_weight ( #{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) | lenv_px | lenv_px_bi | ||||||
term | term_weight ( #{?} ) | term_simple ( ðâ¦?⦠) | term_vector | ||||||||
item | |||||||||||
external syntax | aarity |