From: Ferruccio Guidi Date: Tue, 11 Feb 2014 21:12:19 +0000 (+0000) Subject: update in basic_2 and ground_2 X-Git-Tag: make_still_working~978 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93c509f03ffa0d622fa76e39addf32966a173147;p=helm.git update in basic_2 and ground_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 2d1bb0ec8..3f0d5d427 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Mon, 20 Jan 2014 17:00:19 +0100
+
Last update: Tue, 11 Feb 2014 22:11:38 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 14a742095..a306d00ea 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Mon, 20 Jan 2014 17:00:19 +0100
+
Last update: Tue, 11 Feb 2014 22:11:38 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 951778d1e..cf44a00e4 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -163,29 +163,29 @@ sizes files - 324 + 337 characters - 549104 + 575141 nodes - 1564238 + 1625856 propositions theorems - 103 + 105 lemmas - 1089 + 1144 total - 1192 + 1249 concepts declared - 50 + 51 defined - 77 + 79 total - 127 + 130 @@ -388,7 +388,7 @@ computation - context-sensitive extended evaluation + evaluation for context-sensitive extended reduction cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
@@ -404,7 +404,7 @@
- context-sensitive evaluation + evaluation for context-sensitive reduction cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) cpre_cpre @@ -565,7 +565,7 @@ context-sensitive extended computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? ) - lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + lpxs_ldrop lpxs_cpye lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
@@ -578,7 +578,7 @@
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) - cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs + cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
@@ -656,8 +656,8 @@
- context-sensitive extended normal forms - cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ ) + normal forms for context-sensitive extended reduction + cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) cnx_lift cnx_crx cnx_cix
@@ -672,7 +672,7 @@ context-sensitive extended reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_ldrop lpx_lleq lpx_aaa + lpx_ldrop lpx_cpys lpx_cpye lpx_lleq lpx_aaa
@@ -700,8 +700,8 @@
- context-sensitive extended irreducible forms - cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ ) + irreducible forms for context-sensitive extended reduction + cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) cix_append cix_lift
@@ -714,8 +714,8 @@
- context-sensitive extended reducible forms - crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ ) + reducible forms for context-sensitive extended reduction + crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) crx_append crx_lift
@@ -728,8 +728,8 @@
- context-sensitive normal forms - cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ ) + normal forms for context-sensitive reduction + cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ ) cnr_lift cnr_crr cnr_cir
@@ -772,8 +772,8 @@
- context-sensitive irreducible forms - cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ ) + irreducible forms for context-sensitive reduction + cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) cir_append cir_lift
@@ -786,8 +786,8 @@
- context-sensitive reducible forms - crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ ) + reducible forms for context-sensitive reduction + crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) crr_append crr_lift
@@ -909,7 +909,19 @@ lazy equivalence for local environments lleq ( ? ⋕[?,?] ? ) lleq_alt ( ? ⋕⋕[?,?] ? ) - lleq_ldrop lleq_fqus lleq_lleq lleq_ext + lleq_ldrop lleq_fqus lleq_cpye lleq_lleq lleq_ext + +
+ + + + +
+ + evaluation for contxt-sensitive extended substitution + cpye ( ⦃?,?⦄ ⊢ ? ▶*[?,?] 𝐍⦃?⦄ ) + cpye_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] 𝐍⦃?⦄ ) + cpye_lift cpye_cpye
@@ -919,9 +931,9 @@
contxt-sensitive extended multiple substitution - cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? ) - cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? ) - cpys_lift cpys_cpys + cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) + cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) + cpys_lift cpys_cny cpys_cpys
@@ -1012,8 +1024,22 @@ relocation + normal forms for context-sensitive extended substitution + cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ ) + cny_lift + +
+ + +
+ + + + +
+ contxt-sensitive extended ordinary substitution - cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? ) + cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_cpy
@@ -1288,6 +1314,6 @@

-
Last update: Mon, 20 Jan 2014 17:00:19 +0100
+
Last update: Tue, 11 Feb 2014 22:11:38 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 4dd340fa4..45c5ad29b 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,20 +56,20 @@ sizes files - 29 + 31 characters - 71585 + 71828 nodes - 58746 + 56616 propositions theorems 2 lemmas - 167 + 168 total - 169 + 170 concepts @@ -234,6 +234,6 @@

-
Last update: Mon, 20 Jan 2014 17:00:19 +0100
+
Last update: Tue, 11 Feb 2014 22:11:38 +0100