X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=d894aef118022e999a9e4dc83f9471358a811d31;hb=011cf6478141e69822a5b40933f2444d0522532f;hp=da3ebdad33ec3ffacbd26ac8d20ebad684ecc353;hpb=01d39f9b4feb6eba25f951c6fda8037840db88b4;p=helm.git diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index da3ebdad3..d894aef11 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -29,7 +29,7 @@
category | objects | |||||
propositions | theorems | 43 | lemmas | 422 | total | 465 |
concepts | declared | 32 | defined | 35 | total | 67 |
category | objects | |||||
volume | files | 112 | ||||
propositions | theorems | 45 | lemmas | 437 | total | 482 |
concepts | declared | 32 | defined | 38 | total | 70 |
component | plane | files | |||||
examples | |||||||
native typing | nty | ||||||
conversion | context-sensitive conversion | cpcs ( ? ⢠? â¬* ? ) | |||||
computation | strongly normalizing computation | csn_vector ( â¬* ? ) | csn_lcpr_vector | csn_aaa | |||
csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | |||
context-sensitive computation | cprs (? ⢠? â¡* ?) | cprs_lift | cprs_lcpr | cprs_cprs | cprs_tstc | cprs_tstc_vector | |
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 | context-sensitive normal forms | cnf ( ? ⢠ð[?] ) | cnf_lift | ||||
context-sensitive reduction | lcpr ( ? ⢠⡠? ) | lcpr_cpr | |||||
cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpss | cpr_ltpr | cpr_cpr | |||
context-free normal forms | twhnf ( ððð[?] ) | tnf ( ð[?] ) | tnf_tif | ||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ||||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_tpr | ||||
context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | |||||
static typing | static type assignment | sty | sty_lift | sty_sty | |||
local env. ref. for atomic arity assignment | lsuba ( ? ։ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | |||
atomic arity assignment | aaa ( ? ⢠? ÷ ? ) | aaa_lift | aaa_lifts | aaa_aaa | |||
parameters | sh | ||||||
unfold | term inverse relocation | delift ( ? ⢠? [?,?] ⡠? ) | delift_lift | ||||
partial unfold | ltpss ( ? [?,?] â¶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_ltpss | |||
tpss ( ? ⢠? [?,?] â¶* ? ) | tpss_lift | tpss_tpss | tpss_ltps | ||||
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 | ltps ( ? [?,?] ⶠ? ) | ltps_ldrop | ltps_tps | ltps_ltps | ||
tps ( ? ⢠? [?,?] ⶠ? ) | tps_lift | tps_tps | |||||
global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | |||||
basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_ldrop | |||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | |||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | ||||||
grammar | local env. ref. for substitution | lsubs ( ? [?,?] â¼ ? ) | lsubs_lsubs | ||||
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 ( |?| ) | |||||
term | term_weight ( #[?] ) | term_simple ( ð[?] ) | term_vector | ||||
item | |||||||
external syntax | aarity |
component | plane | files | ||||||
examples | ||||||||
native typing | nty | |||||||
equivalence | context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | ||||||
conversion | context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | |||||
computation | strongly normalizing computation | csn_vector ( â¬* ? ) | csn_lcpr_vector | csn_aaa | ||||
csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | ||||
context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_cprs | lcprs_lcprs | |||||
cprs (? ⢠? â¡* ?) | cprs_lift | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector | ||
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 | context-sensitive normal forms | cnf ( ? ⢠ð[?] ) | cnf_lift | |||||
context-sensitive reduction | lcpr ( ? ⢠⡠? ) | lcpr_cpr | ||||||
cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpss | cpr_ltpr | cpr_cpr | ||||
context-free normal forms | twhnf ( ððð[?] ) | tnf ( ð[?] ) | tnf_tif | |||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | |||||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_tpr | |||||
context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | ||||||
static typing | static type assignment | sty | sty_lift | sty_sty | ||||
local env. ref. for atomic arity assignment | lsuba ( ? ։ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | ||||
atomic arity assignment | aaa ( ? ⢠? ÷ ? ) | aaa_lift | aaa_lifts | aaa_aaa | ||||
parameters | sh | |||||||
unfold | term inverse relocation | delift ( ? ⢠? [?,?] ⡠? ) | delift_lift | |||||
partial unfold | ltpss ( ? [?,?] â¶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_ltpss | ||||
tpss ( ? ⢠? [?,?] â¶* ? ) | tpss_lift | tpss_tpss | tpss_ltps | |||||
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 | ltps ( ? [?,?] ⶠ? ) | ltps_ldrop | ltps_tps | ltps_ltps | |||
tps ( ? ⢠? [?,?] ⶠ? ) | tps_lift | tps_tps | ||||||
global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | ||||||
basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_ldrop | ||||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | ||||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | |||||||
grammar | local env. ref. for substitution | lsubs ( ? [?,?] â¼ ? ) | lsubs_lsubs | |||||
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 ( |?| ) | ||||||
term | term_weight ( #[?] ) | term_simple ( ð[?] ) | term_vector | |||||
item | ||||||||
external syntax | aarity |