X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=71e25ea8f394b1559e18e5d251bdd3db67c25438;hb=bcab3f92c6f815098ecc24eff06bfd3d232eb497;hp=a24c6e00767a5f5bc725f9d9a696a9ff2e347df2;hpb=41441a27e7dc2afcd20ffd6159015ee77f37a3d8;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index a24c6e007..71e25ea8f 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -58,29 +58,29 @@
| sizes |
files |
- 360 |
+ 363 |
characters |
- 646465 |
+ 652617 |
nodes |
- 1812003 |
+ 1820917 |
| propositions |
theorems |
- 117 |
+ 122 |
lemmas |
- 1283 |
+ 1295 |
total |
- 1400 |
+ 1417 |
| concepts |
declared |
- 54 |
+ 55 |
defined |
81 |
total |
- 135 |
+ 136 |
@@ -236,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 |
|
@@ -250,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 |
|
@@ -399,7 +399,7 @@
"big tree" parallel computation |
- fpbg ( â¦?,?,?⦠>â[?,?] â¦?,?,?⦠) |
+ fpbg ( â¦?,?,?⦠>â¡[?,?] â¦?,?,?⦠) |
fpbg_lift fpbg_fleq fpbg_fpbg |
@@ -415,7 +415,7 @@
|
|
- fpbc ( â¦?,?,?⦠â»â[?,?] â¦?,?,?⦠) |
+ fpbc ( â¦?,?,?⦠â»â¡[?,?] â¦?,?,?⦠) |
fpbc_fleq fpbc_fpbs |
@@ -725,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 |
|
@@ -748,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 |
|
@@ -762,9 +762,9 @@
|
- stratified static type assignment |
- ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) |
- ssta_lift ssta_lpx_sn ssta_ssta |
+ stratified equivalence |
+ steq ( ? â¡[?,?] ? ) |
+ steq_steq |
|
@@ -776,9 +776,9 @@
|
- local env. ref. for degree assignment |
- lsubd ( ? ⢠? âªâ« ? ) |
- lsubd_da lsubd_lsubd |
+ static type assignment |
+ sta ( â¦?,?⦠⢠? â¢[?] ? ) |
+ sta_lift sta_lpx_sn sta_aaa sta_sta |
|
@@ -790,9 +790,9 @@
|
- degree assignment |
- da ( â¦?,?⦠⢠? âª[?,?] ? ) |
- da_lift da_da |
+ parameters |
+ sh |
+ sd |
|
@@ -804,9 +804,23 @@
|
- parameters |
- sh |
- sd |
+ local env. ref. for atomic arity assignment |
+ lsuba ( ? ⢠? ââ« ? ) |
+ lsuba_aaa lsuba_lsuba |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ atomic arity assignment |
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa |
|
@@ -831,7 +845,7 @@
| multiple substitution |
lazy equivalence |
- fleq ( â¦?,?,?⦠â[?] â¦?,?,?⦠) |
+ fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠) |
fleq_fleq |
@@ -847,7 +861,7 @@
|
|
- lleq ( ? â[?,?] ? ) |
+ lleq ( ? â¡[?,?] ? ) |
lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleq |
@@ -1272,6 +1286,6 @@
- Last update: Mon, 09 Jun 2014 22:16:19 +0200
+ Last update: Sun, 15 Jun 2014 16:14:12 +0200
|