From: Ferruccio Guidi Date: Wed, 7 Aug 2013 21:42:41 +0000 (+0000) Subject: milestone in basic_2 X-Git-Tag: make_still_working~1116 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b2c1a95861424ba23e491e2b258f7413efbc1fba;p=helm.git milestone in basic_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 8f9e8123f..07f9063ec 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sat, 27 Jul 2013 18:11:40 +0200
+
Last update: Wed, 07 Aug 2013 23:40:05 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 07f0e3cc9..b3301124a 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sat, 27 Jul 2013 18:25:25 +0200
+
Last update: Wed, 07 Aug 2013 23:40:05 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index a14edca67..c543bb9d2 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -165,9 +165,9 @@ files 247 characters - 350287 + 366699 nodes - 1035865 + 1091471 propositions @@ -206,7 +206,7 @@ @@ -317,9 +317,9 @@ dynamic typing "big tree" parallel computation - yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) + yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) yprs_yprs - ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) + ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ ) ygt_ygt @@ -327,8 +327,8 @@
"big tree" parallel reduction - ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) - ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) + ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) + ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )
@@ -341,7 +341,7 @@
local env. ref. for stratified native validity - lsubsv ( ? ⊢ ? ¡⊑[?] ? ) + lsubsv ( ? ⊢ ? ¡⊑[?,?] ? ) lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv
@@ -355,7 +355,7 @@
stratified native validity - snv ( ⦃?,?⦄ ⊢ ? ¡[?] ) + snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) snv_lift snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs
@@ -367,7 +367,7 @@ equivalence context-sensitive equivalence - cpcs ( ? ⊢ ? ⬌* ? ) + cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) cpcs_aaa cpcs_cprs cpcs_cpcs
@@ -379,7 +379,7 @@ conversion context-sensitive conversion - cpc ( ? ⊢ ? ⬌ ? ) + cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) cpc_cpc
@@ -391,7 +391,7 @@ computation context-sensitive extended evaluation - cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ ) + cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
@@ -407,7 +407,7 @@
context-sensitive evaluation - cpre ( ? ⊢ ➡* 𝐍⦃?⦄ ) + cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) cpre_cpre
@@ -421,7 +421,7 @@
strongly normalizing computation - csn_vector ( ? ⊢ ⬊* ? ) + csn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) csn_tstc_vector csn_aaa
@@ -437,8 +437,8 @@
- csn ( ? ⊢ ⬊* ? ) - csn_alt ( ? ⊢ ⬊⬊* ? ) + csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) + csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) csn_lift csn_lpx
@@ -449,7 +449,7 @@
decomposed extended computation - dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) + dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? ) dxprs_lift dxprs_aaa dxprs_dxprs
@@ -463,8 +463,8 @@
context-sensitive extended computation - lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? ) - lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? ) + lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) + lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? ) lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs
@@ -477,7 +477,7 @@
- cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? ) + cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs
@@ -491,8 +491,8 @@
context-sensitive computation - lprs ( ? ⊢ ➡* ? ) - lprs_alt ( ? ⊢ ➡➡* ? ) + lprs ( ⦃?,?⦄ ⊢ ➡* ? ) + lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? ) lprs_ldrop lprs_cprs lprs_lprs
@@ -505,7 +505,7 @@
- cprs ( ? ⊢ ? ➡* ?) + cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) cprs_lift cprs_cprs
@@ -519,7 +519,7 @@
local env. ref. for abstract candidates of reducibility - lsubc ( ? ⊑[?] ? ) + lsubc ( ? ⊢ ? ⊑[?] ? ) lsubc_ldrop lsubc_ldrops lsubc_lsuba
@@ -534,7 +534,7 @@ support for abstract computation properties acp - acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) + acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) acp_aaa
@@ -543,7 +543,7 @@ reduction context-sensitive extended normal forms - cnx ( ⦃?,?⦄ ⊢ 𝐍[?]⦃?⦄ ) + cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ ) cnx_lift cnx_crx cnx_cix
@@ -557,7 +557,7 @@
context-sensitive extended reduction - lpx ( ⦃?,?⦄ ⊢ ➡[?] ? ) + lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) lpx_ldrop lpx_aaa
@@ -573,7 +573,7 @@
- cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) cpx_lift cpx_cix
@@ -587,7 +587,7 @@
context-sensitive extended irreducible forms - cix ( ⦃?,?⦄ ⊢ 𝐈[?]⦃?⦄ ) + cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ ) cix_append cix_lift
@@ -601,7 +601,7 @@
context-sensitive extended reducible forms - crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ ) + crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ ) crx_append crx_lift
@@ -615,7 +615,7 @@
context-sensitive normal forms - cnr ( ? ⊢ 𝐍⦃?⦄ ) + cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ ) cnr_lift cnr_crr cnr_cir
@@ -629,7 +629,7 @@
context-sensitive reduction - lpr ( ? ⊢ ➡ ? ) + lpr ( ⦃?,?⦄ ⊢ ➡ ? ) lpr_ldrop lpr_lpr
@@ -645,7 +645,7 @@
- cpr ( ? ⊢ ? ➡ ? ) + cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) cpr_lift cpr_cir
@@ -659,7 +659,7 @@
context-sensitive irreducible forms - cir ( ? ⊢ 𝐈⦃?⦄ ) + cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ ) cir_append cir_lift
@@ -673,7 +673,7 @@
context-sensitive reducible forms - crr ( ? ⊢ 𝐑⦃?⦄ ) + crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ ) crr_append crr_lift
@@ -685,7 +685,7 @@ unfold unfold - unfold ( ? ⊢ ? ⧫* ? ) + unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )
@@ -713,7 +713,7 @@ static typing stratified static type assignment - ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) + ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ⦃?,?⦄ ) ssta_lift ssta_aaa ssta_ssta
@@ -727,7 +727,7 @@
local env. ref. for atomic arity assignment - lsuba ( ? ⁝⊑ ? ) + lsuba ( ? ⊢ ? ⁝⊑ ? ) lsuba_ldrop lsuba_aaa lsuba_lsuba
@@ -741,7 +741,7 @@
atomic arity assignment - aaa ( ? ⊢ ? ⁝ ? ) + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) aaa_lift aaa_lifts aaa_aaa
@@ -781,7 +781,7 @@
iterated structural successor for closures - fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ ) + fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) fsups_fsups
@@ -797,7 +797,7 @@
- fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ ) + fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) fsupp_fsupp
@@ -863,9 +863,9 @@ relocation structural successor for closures - fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) - fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ ) - fsupq_alt + fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) + fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) + fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )
@@ -960,7 +960,7 @@ closures cl_shift ( ? @@ ? ) - cl_weight ( ♯{?,?} ) + cl_weight ( ♯{?,?,?} )
@@ -1076,6 +1076,6 @@

-
Last update: Sat, 27 Jul 2013 18:22:47 +0200
+
Last update: Wed, 07 Aug 2013 23:40:05 +0200