- bugfixed "aacr" allows to remove historical eta-conversions

  in the apparatus for strong normalization
- minor bugfixes in annotations
- xhtbl tables updated for the bugfixed stylesheets

diff --git a/matita/matita/contribs/BTM/web/chc_45.tbl b/matita/matita/contribs/BTM/web/chc_45.tbl
index a822c986fdd5114899a9b75f8abfd4101b3b7a83..187b82e7a2f0d6fde1755425d786681bc12de828 100644 (file)
--- a/matita/matita/contribs/BTM/web/chc_45.tbl
+++ b/matita/matita/contribs/BTM/web/chc_45.tbl
@@ -14,8 +14,6 @@ table {
 }
 
 
-class "component" { 0 }
+class "capitalize italic" { 0 }
 
-class "text" { 1 }
-
-class "number" { 2 * }
+class "right italic" { 2 * }

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 5dc025fc3c5edde3b610fb1d65139098bc075ef5..e985b7e59501f8d5c7c412cd0ee35e0556c88f1a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -200,30 +200,30 @@ define SUMMARY_TEMPLATE
 
   $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt
        @printf '  SUMMARY $(1)\n'
-       @printf 'name "$$(basename $$(@F))"\n\n'                >  $$@
-       @printf 'table {\n'                                     >> $$@
-       @printf '   class "gray"   [ "category"\n'              >> $$@
-       @printf '      [ "objects" * ]\n'                       >> $$@
-       @printf '   ]\n'                                        >> $$@
-       @printf '   class "cyan"   [ "sizes"\n'                 >> $$@
-       @printf '      [ "files"      "$$(S4)" ]\n'             >> $$@
-       @printf '      [ "characters" "$$(word 1, $$(S1))" ]\n' >> $$@
-       @printf '      [ "nodes"      "$$(word 3, $$(S0))" ]\n' >> $$@
-       @printf '   ]\n'                                        >> $$@  
-       @printf '   class "green"  [ "propositions"\n'          >> $$@
-       @printf '      [ "theorems" "$$(P1)" ]\n'               >> $$@
-       @printf '      [ "lemmas"   "$$(P2)" ]\n'               >> $$@
-       @printf '      [ "total"    "$$(P3)" ]\n'               >> $$@
-       @printf '   ]\n'                                        >> $$@
-       @printf '   class "yellow" [ "concepts"\n'              >> $$@
-       @printf '      [ "declared" "$$(C1)" ]\n'               >> $$@
-       @printf '      [ "defined"  "$$(C2)" ]\n'               >> $$@
-       @printf '      [ "total"    "$$(C3)" ]\n'               >> $$@
-       @printf '   ]\n'                                        >> $$@
-       @printf '}\n\n'                                         >> $$@
-       @printf 'class "component" { 0 }\n\n'                   >> $$@
-       @printf 'class "plane"     { 1 } { 3 } { 5 }\n\n'       >> $$@
-       @printf 'class "number"    { 2 } { 4 } { 6 }\n'         >> $$@
+       @printf 'name "$$(basename $$(@F))"\n\n'                  >  $$@
+       @printf 'table {\n'                                       >> $$@
+       @printf '   class "gray"   [ "category"\n'                >> $$@
+       @printf '      [ "objects" * ]\n'                         >> $$@
+       @printf '   ]\n'                                          >> $$@
+       @printf '   class "cyan"   [ "sizes"\n'                   >> $$@
+       @printf '      [ "files"      "$$(S4)" ]\n'               >> $$@
+       @printf '      [ "characters" "$$(word 1, $$(S1))" ]\n'   >> $$@
+       @printf '      [ "nodes"      "$$(word 3, $$(S0))" ]\n'   >> $$@
+       @printf '   ]\n'                                          >> $$@        
+       @printf '   class "green"  [ "propositions"\n'            >> $$@
+       @printf '      [ "theorems" "$$(P1)" ]\n'                 >> $$@
+       @printf '      [ "lemmas"   "$$(P2)" ]\n'                 >> $$@
+       @printf '      [ "total"    "$$(P3)" ]\n'                 >> $$@
+       @printf '   ]\n'                                          >> $$@
+       @printf '   class "yellow" [ "concepts"\n'                >> $$@
+       @printf '      [ "declared" "$$(C1)" ]\n'                 >> $$@
+       @printf '      [ "defined"  "$$(C2)" ]\n'                 >> $$@
+       @printf '      [ "total"    "$$(C3)" ]\n'                 >> $$@
+       @printf '   ]\n'                                          >> $$@
+       @printf '}\n\n'                                           >> $$@
+       @printf 'class "capitalize italic" { 0 }\n\n'             >> $$@
+       @printf 'class "italic"            { 1 } { 3 } { 5 }\n\n' >> $$@
+       @printf 'class "right italic"      { 2 } { 4 } { 6 }\n'   >> $$@
 
 .PHONY: $$(SUM_$(1))
 endef

diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
index f854d14eab6fa744fb1435ae7f7dde8699d7e888..29d687e7f494b147524581219dd6e12af79cc169 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
@@ -33,8 +33,8 @@ table {
    ]
 }
 
-class "component" { 0 }
+class "top"               { * }
 
-class "plane" { 1 }
+class "capitalize italic" { 0 }
 
-class "file" { 2 * }
+class "italic"            { 1 }

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
index 0d054da39e51417de00ed28354993be77101fbf2..6bcbfe4c7982511c4688364c154cfd64d72849e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
@@ -17,6 +17,8 @@ include "basic_2/multiple/drops.ma".
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
 
+definition candidate: Type[0] ≝ relation3 genv lenv term.
+
 definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                  ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T →
                  ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
@@ -29,11 +31,11 @@ definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
 definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                  ∀G,L. ∃k. NF … (RR G L) RS (⋆k).
 
-definition CP2 ≝ λRP:relation3 genv lenv term.
+definition CP2 ≝ λRP:candidate.
                  ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
 
 (* requirements for abstract computation properties *)
-record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 genv lenv term) : Prop ≝
+record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
 { cp0: CP0 RR RS;
   cp1: CP1 RR RS;
   cp2: CP2 RP

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
index b95885d7f196b2d7e7afdfd154c68ce5e673b1b4..be5351c2b9f9fffb4bcacc62b90bc0e472babb7d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
@@ -24,7 +24,7 @@ include "basic_2/computation/lsubc_drops.ma".
 
 (* Basic_1: was: sc3_arity_csubc *)
 theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
-                              acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+                              acp RR RS RP → acr RR RS RP RP →
                               ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 →
                               ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
                               ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
@@ -81,11 +81,11 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
 qed.
 
 (* Basic_1: was: sc3_arity *)
-lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
                 ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
 /2 width=8 by drops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed.
 
-lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
                ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
 #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
 lapply (aacr_acr … H1RP H2RP A) #HA

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
index f5b3f6a05bf8803f81066371314b567049ab9a0d..1537d175c1d50af2c9cafe55f3f9b3807a8cb9a4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
@@ -21,43 +21,43 @@ include "basic_2/computation/acp.ma".
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
 
-definition S0 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e.
+definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e.
                 C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
 
-definition S0s ≝ λC:relation3 genv lenv term.
+definition S0s ≝ λC:candidate.
                  ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 →
                  ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2.
 
 (* Note: this is Girard's CR1 *)
-definition S1 ≝ λRP,C:relation3 genv lenv term.
+definition S1 ≝ λRP,C:candidate.
                 ∀G,L,T. C G L T → RP G L T.
 
 (* Note: this is Tait's iii, or Girard's CR4 *)
-definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:relation3 genv lenv term.
+definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate.
                 ∀G,L,Vs. all … (RP G L) Vs →
                 ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T).
 
 (* Note: this generalizes Tait's ii *)
-definition S3 ≝ λC:relation3 genv lenv term.
+definition S3 ≝ λC:candidate.
                 ∀a,G,L,Vs,V,T,W.
                 C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T).
 
-definition S4 ≝ λRP,C:relation3 genv lenv term.
+definition S4 ≝ λRP,C:candidate.
                 ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k).
 
-definition S5 ≝ λC:relation3 genv lenv term. ∀I,G,L,K,Vs,V1,V2,i.
+definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
                 C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 →
                 ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
 
-definition S6 ≝ λRP,C:relation3 genv lenv term.
+definition S6 ≝ λRP,C:candidate.
                 ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                 ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T).
 
-definition S7 ≝ λC:relation3 genv lenv term.
+definition S7 ≝ λC:candidate.
                 ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
 
 (* properties of the abstract candidate of reducibility *)
-record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3 genv lenv term) : Prop ≝
+record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
 { s0: S0 C;
   s1: S1 RP C;
   s2: S2 RR RS RP C;
@@ -68,13 +68,16 @@ record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3
   s7: S7 C
 }.
 
-(* the abstract candidate of reducibility associated to an atomic arity *)
-let rec aacr (RP:relation3 genv lenv term) (A:aarity) (G:genv) (L:lenv) on A: predicate term ≝
-λT. match A with
-[ AAtom     ⇒ RP G L T
-| APair B A ⇒ ∀L0,V0,T0,des.
-              aacr RP B G L0 V0 → ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] T ≡ T0 →
-              aacr RP A G L0 (ⓐV0.T0)
+(* the functional construction for candidates *)
+definition cfun: candidate → candidate → candidate ≝
+                 λC1,C2,G,K,T. ∀L,V,U,des.
+                 ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U).
+
+(* the candidate associated to an atomic arity *)
+let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝
+match A with
+[ AAtom     ⇒ RP
+| APair B A ⇒ cfun (aacr RP B) (aacr RP A)
 ].
 
 interpretation
@@ -92,7 +95,7 @@ lemma acr_lifts: ∀C. S0 C → S0s C.
 ]
 qed.
 
-lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
+lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP RP →
                 ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 →
                 RP G L V → RP G L0 V0.
 #RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV
@@ -101,7 +104,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
 qed.
 
 (* Basic_1: was only: sns3_lifts1 *)
-lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
+lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP RP →
                      ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s →
                      all … (RP G L) Vs → all … (RP G L0) V0s.
 #RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize //
@@ -111,7 +114,7 @@ qed.
 (* Basic_1: was:
    sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
 *)
-lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
                 ∀A. acr RR RS RP (aacr RP A).
 #RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
 #B #A #IHB #IHA @mk_acr normalize
@@ -119,26 +122,26 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 
 | #G #L #T #H
   elim (cp1 … H1RP G L) #k #HK
   lapply (H ? (⋆k) ? (⟠) ? ? ?) -H
-  [1,3: // |2,4: skip
+  [3,5: // |2,4: skip
   | @(s2 … IHB … (◊)) //
   | #H @(cp2 … H1RP … k) @(s1 … IHA) //
   ]
-| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
+| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
   lapply (s1 … IHB … HB) #HV0
   @(s2 … IHA … (V0 @ V0s))
   /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/
-| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
+| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
   @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H
+| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   >(lifts_inv_sort1 … HY) -Y
   lapply (s1 … IHB … HB) #HV0
   @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
-| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
   elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
@@ -148,32 +151,32 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 
   elim (lifts_lift_trans  … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
   >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
   @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
-| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
+| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
   elim (lift_total V10 0 1) #V20 #HV120
   elim (liftv_total 0 1 V10s) #V20s #HV120s
   @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
   @(HA … (des + 1)) /2 width=2 by drops_skip/
-  [ @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
-  | @lifts_applv //
+  [ @lifts_applv //
     elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
     >(liftv_mono … HV12s … HV10s) -V1s //
+  | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
   ]
-| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
+| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
   @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
 ]
 qed.
 
-lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
                  ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
-                    ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
+                    ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
                                    ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
                  ) →
                  ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
+#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB
 lapply (aacr_acr … H1RP H2RP A) #HCA
 lapply (aacr_acr … H1RP H2RP B) #HCB
 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index a8eb52ab50dc467bb522c133e4e26d7a3265e42e..e4c5460d09769a3c0285211a191baf0845baf0da 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -140,5 +140,5 @@ qed-.
    pr1_head_1 pr1_head_2 pr1_comp
    clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
-   pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind
+   pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
index bb225f6c7967103b2ae6961458a31abdaf56e39b..becbd624d463d01b6c002d79b1029e13948299d7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
@@ -20,7 +20,7 @@ include "basic_2/computation/cpxs_tstc.ma".
 
 (* Vector form of forward lemmas involving same top term constructor ********)
 
-(* Basic_1: was just: nf2_iso_applv_lref *)
+(* Basic_1: was just: nf2_iso_appls_lref *)
 lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T.  𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
                            ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U.
 #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
@@ -60,7 +60,7 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 
-(* Basic_1: was just: pr3_iso_applv_beta *)
+(* Basic_1: was just: pr3_iso_appls_beta *)
 lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
                             ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U.
 #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
@@ -109,7 +109,7 @@ elim (cpxs_inv_appl1 … H) -H *
 ]
 qed-.
 
-(* Basic_1: was just: pr3_iso_applv_abbr *)
+(* Basic_1: was just: pr3_iso_appls_abbr *)
 lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                              ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
                              ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
@@ -158,7 +158,7 @@ elim (cpxs_inv_appl1 … H) -H *
 ]
 qed-.
 
-(* Basic_1: was just: pr3_iso_applv_cast *)
+(* Basic_1: was just: pr3_iso_appls_cast *)
 lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
                             ∨∨ ⒶVs. ⓝW. T ≂ U
                              | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
index 426ae47fa4e96a62ed301b72f3fed6f9ca99e8b3..cd28a524b295703cb4cfb2308b214d9a82333433 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
@@ -129,5 +129,5 @@ lemma csx_fwd_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T →
             sn3_cdelta
             sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change
             sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
-            sn3_appl_applv sn3_bind sn3_appl_bind sn3_applv_bind
+            sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
 *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index 736b21f3bf141ba7817942c0dda7c07343deae46..9573d288b5575797205aff208b9aca2569f5ea99 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -21,7 +21,7 @@ include "basic_2/computation/csx_vector.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Basic_1: was just: sn3_applv_lref *)
+(* Basic_1: was just: sn3_appls_lref *)
 lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
                      ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
 #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
@@ -48,7 +48,7 @@ elim (cpxs_fwd_sort_vector … H) -H #H
 ]
 qed.
 
-(* Basic_1: was just: sn3_applv_beta *)
+(* Basic_1: was just: sn3_appls_beta *)
 lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
 #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
@@ -80,7 +80,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
 ]
 qed.
 
-(* Basic_1: was just: sn3_applv_abbr *)
+(* Basic_1: was just: sn3_appls_abbr *)
 lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                        ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
                        ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
@@ -99,7 +99,7 @@ elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -
 ]
 qed.
 
-(* Basic_1: was just: sn3_applv_cast *)
+(* Basic_1: was just: sn3_appls_cast *)
 lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
                       ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
 #h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
@@ -116,7 +116,7 @@ elim (cpxs_fwd_cast_vector … H) -H #H
 ]
 qed.
 
-theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
+theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g).
 #h #g @mk_acr //
 [ /2 width=8 by csx_lift/
 | /3 width=1 by csx_applv_cnx/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
index f45319f6746524afa959f9dd70a37bd6a25a11ac..7c0a785ca8c24ceee050044412c74fb017108b07 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma
@@ -50,8 +50,8 @@ fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 =
                                       L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
 #RP #G #L1 #L2 * -L1 -L2
 [ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10/
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/
 ]
 qed-.
 
@@ -82,8 +82,8 @@ fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 =
                                     L1 = K1.ⓓⓝW.V & I = Abst.
 #RP #G #L1 #L2 * -L1 -L2
 [ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8/
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/
 ]
 qed-.
 
@@ -99,7 +99,7 @@ lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
 
 (* Basic_1: was just: csubc_refl *)
 lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L.
-#RP #G #L elim L -L // /2 width=1/
+#RP #G #L elim L -L /2 width=1 by lsubc_pair/
 qed.
 
 (* Basic_1: removed theorems 3:

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma
index 5f75a2d9b316f960fdb8324fa0c8a693cd262e3d..9b46f01f0e6856817af2cbbf92d7b5807ef33116 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma
@@ -42,7 +42,7 @@ qed-.
 
 (* Basic_1: was: csubc_drop_conf_rev *)
 lemma drop_lsubc_trans: ∀RR,RS,RP.
-                        acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+                        acp RR RS RP → acr RR RS RP RP →
                         ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2.
 #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
index 90a7aa04184f6924f316a3028db1732e25a484bc..5685fd1ef9bcc7338d20dd1f80870a8b6c73634b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma
@@ -20,7 +20,7 @@ include "basic_2/computation/lsubc_drop.ma".
 
 (* Basic_1: was: csubc_drop1_conf_rev *)
 lemma drops_lsubc_trans: ∀RR,RS,RP.
-                         acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+                         acp RR RS RP → acr RR RS RP RP →
                          ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
                          ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2.
 #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma
index 06666965b9a03222314c49730f7c1a7832f21810..d8dcf0e8d96598d2caed9b959986086161886868 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma
@@ -19,8 +19,8 @@ include "basic_2/computation/acp_aaa.ma".
 
 (* properties concerning lenv refinement for atomic arity assignment ********)
 
-lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
+lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
                    ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.
-#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4/
+#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/
+#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by aacr_aaa, lsubc_beta/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 328d64e87918fd179eaf2659c81f6ce566346d34..583105a8d8738d649cbeb7710089e44e35033dfc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -52,13 +52,14 @@ n: native type annotation
 
 NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
 
-- first letter
+- prefix and first letter
 
 b: bi contex-sensitive for local environments
 c: contex-sensitive for terms
 f: context-freee for closures
 l: sn contex-sensitive for local environments
 r: dx contex-sensitive for local environments
+s: stratified (prefix) 
 t: context-free for terms
 
 - second letter

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl
index 7d5f0649b0acc47b0a0938d75fd587bc182b7cd2..cbcbb50669a3dd11047dcf6a899081e9c0feb7a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl
@@ -47,6 +47,6 @@ table {
    } ]
 }
 
-class "text" { 0 } { 2 * }
+class "top"    { * }
 
-class "plane" { 1 }
+class "italic" { 1 }

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 55e58114b9467ec9df2c2bdacc1d90bc59febac5..81cd8e41dbc7c1dcb61037f41c25f7c51bedefaf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -101,7 +101,7 @@ table {
         [ { "\"big tree\" parallel computation" * } {
              [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ]
              [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ]
-             [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ]
+             [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ]
              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ]
           }
         ]
@@ -140,7 +140,7 @@ table {
           }
         ]
         [ { "context-sensitive extended reduction" * } {
-             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" "lpx_lleq" + "lpx_aaa" * ]
+             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
@@ -321,8 +321,8 @@ table {
    ]
 }
 
-class "component" { 0 }
+class "top"               { * }
 
-class "plane" { 1 }
+class "capitalize italic" { 0 }
 
-class "file" { 2 * }
+class "italic"            { 1 }

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index c5e65b0b59b45d1fefa343a3871f80cf7100a557..6d8d7435c2d659c4e9a4230dd36d945092654bb6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -26,6 +26,6 @@ table {
    ]
 }
 
-class "plane" { 0 }
+class "top"    { * }
 
-class "file" { 1 * }
+class "italic" { 0 }