]> matita.cs.unibo.it Git - helm.git/commitdiff
- some consequences of preservation added
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 8 Oct 2014 20:22:55 +0000 (20:22 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 8 Oct 2014 20:22:55 +0000 (20:22 +0000)
- some renaming and some notation updated

matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma
matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl

index b4b7fb2235c2cadf7ea2fe1c0610dc36b7d5b337..71ed202d7123d69afdd06c5132454d7a1513318e 100644 (file)
@@ -61,9 +61,9 @@ qed-.
 
 (* Advanced properties of "qrst" parallel computation on closures ***********)
 
-lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ →
-                       ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
-                       ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
+lemma fpbs_fpb_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ →
+                      ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
+                      ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
 #h #g #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_fpbg … H) -H
 [ #H12 #G2 #L2 #U2 #H2 elim (fleq_fpb_trans … H12 … H2) -F2 -K2 -T2
   /3 width=5 by fleq_fpbs, ex2_3_intro/
index 4d44edb46b9e6469a747d7c4090d3d81b45edf49..c8359a5498a3a4835ca0907358437411de7ab888 100644 (file)
@@ -31,17 +31,17 @@ interpretation
 (* Basic eliminators ********************************************************)
 
 lemma fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
-                      â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥[h,g] T1 → (
+                      â\88\80G1,L1,T1. â¦¥[h,g] â¦\83G1, L1, T1â¦\84 → (
                          ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
                       ) → R G1 L1 T1
                    ) →
-                   â\88\80G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T → R G L T.
+                   â\88\80G,L,T. â¦¥[h, g] â¦\83G, L, Tâ¦\84 → R G L T.
 #h #g #R #IH #G #L #T #H elim H -G -L -T
 /4 width=1 by fsb_intro/
 qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma fsb_inv_csx: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+lemma fsb_inv_csx: â\88\80h,g,G,L,T. â¦¥[h, g] â¦\83G, L, Tâ¦\84 → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/
 qed-.
index f8928c29854c97cad7f42882e0105ff6917e0bfb..6dff4c048ee6a71d1b55a33a92bd2aa33ca2cfeb 100644 (file)
@@ -21,34 +21,34 @@ include "basic_2/computation/fsb_csx.ma".
 (* Main properties **********************************************************)
 
 (* Note: this is the "big tree" theorem ("RST" version) *)
-theorem aaa_fsb: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T.
+theorem aaa_fsb: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦¥[h, g] â¦\83G, L, Tâ¦\84.
 /3 width=2 by aaa_csx, csx_fsb/ qed.
 
 (* Note: this is the "big tree" theorem ("QRST" version) *)
-theorem aaa_fsba: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¦¥â¦¥[h, g] T.
+theorem aaa_fsba: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦¥â¦¥[h, g] â¦\83G, L, Tâ¦\84.
 /3 width=2 by fsb_fsba, aaa_fsb/ qed.
 
 (* Advanced eliminators on atomica arity assignment for terms ***************)
 
-fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term.
-                       (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                     R G1 L1 T1
-                       ) →
-                       ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-#h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T
+fact aaa_ind_fpb_aux: ∀h,g. ∀R:relation3 genv lenv term.
+                      (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                    (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                    R G1 L1 T1
+                      ) →
+                      ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+#h #g #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
 #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
 #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1
 /2 width=2 by fpb_fpbs/
 qed-.
 
-lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
-                    (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                  (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                  R G1 L1 T1
-                    ) →
-                    ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-/4 width=4 by aaa_ind_fpbu_aux, aaa_csx/ qed-.
+lemma aaa_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term.
+                   (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                 R G1 L1 T1
+                   ) →
+                   ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
 
 fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term.
                        (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
index cf966232a7fc9e97df334d03af54a2cf7ac11afe..00fe4a67edbb0942b016ec1dadcfb1efbeba5ed3 100644 (file)
@@ -31,26 +31,26 @@ interpretation
 (* Basic eliminators ********************************************************)
 
 lemma fsba_ind_alt: ∀h,g. ∀R: relation3 …. (
-                       â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥â¦¥[h,g] T1 → (
+                       â\88\80G1,L1,T1. â¦¥â¦¥[h,g] â¦\83G1, L1, T1â¦\84 → (
                           ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
                        ) → R G1 L1 T1
                     ) →
-                    â\88\80G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¦¥â¦¥[h, g] T → R G L T.
+                    â\88\80G,L,T. â¦¥â¦¥[h, g] â¦\83G, L, Tâ¦\84 → R G L T.
 #h #g #R #IH #G #L #T #H elim H -G -L -T
 /4 width=1 by fsba_intro/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma fsba_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥â¦¥[h, g] T1 →
-                       â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ â¦¥â¦¥[h, g] T2.
+lemma fsba_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦¥â¦¥[h, g] â¦\83G1, L1, T1â¦\84 →
+                       â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦¥â¦¥[h, g] â¦\83G2, L2, T2â¦\84.
 #h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1
 /4 width=5 by fsba_intro, fpbs_fpbg_trans/
 qed-.
 
 (* Main properties **********************************************************)
 
-theorem fsb_fsba: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¦¥â¦¥[h, g] T.
+theorem fsb_fsba: â\88\80h,g,G,L,T. â¦¥[h, g] â¦\83G, L, Tâ¦\84  â\86\92 â¦¥â¦¥[h, g] â¦\83G, L, Tâ¦\84.
 #h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T
 #G1 #L1 #T1 #_ #IH @fsba_intro
 #G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/
@@ -58,25 +58,25 @@ qed.
 
 (* Main inversion lemmas ****************************************************)
 
-theorem fsba_inv_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¦¥â¦¥[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T.
+theorem fsba_inv_fsb: â\88\80h,g,G,L,T. â¦¥â¦¥[h, g] â¦\83G, L, Tâ¦\84 â\86\92 â¦¥[h, g] â¦\83G, L, Tâ¦\84.
 #h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T
 /4 width=1 by fsb_intro, fpb_fpbg/
 qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma fsb_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥[h, g] T1 →
-                      â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ â¦¥[h, g] T2.
+lemma fsb_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦¥[h, g] â¦\83G1, L1, T1â¦\84 →
+                      â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦¥[h, g] â¦\83G2, L2, T2â¦\84.
 /4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-.
 
 (* Advanced eliminators *****************************************************)
 
 lemma fsb_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
-                    (â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥[h, g] T1 →
+                    (â\88\80G1,L1,T1. â¦¥[h, g] â¦\83G1, L1, T1â¦\84 →
                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
                                 R G1 L1 T1
                     ) →
-                    â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ â¦¥[h, g] T1 → R G1 L1 T1.
+                    â\88\80G1,L1,T1. â¦¥[h, g] â¦\83G1, L1, T1â¦\84 → R G1 L1 T1.
 #h #g #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h g … G1 L1 T1)
 /3 width=1 by fsba_inv_fsb, fsb_fsba/
 qed-.
index 38cbe5c1657189de3705feace5ec62b4492fd2d6..54284a0b1e2dbeeeb1ccd1bd4ca7f566af9c88e1 100644 (file)
@@ -23,7 +23,7 @@ include "basic_2/computation/fsb_alt.ma".
 (* Advanced propreties on context-sensitive extended normalizing terms ******)
 
 lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
-                    â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ â¦¥[h, g] T2.
+                    â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦¥[h, g] â¦\83G2, L2, T2â¦\84.
 #h #g #G1 #L1 #T1 #H @(csx_ind … H) -T1
 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2
 #G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1
@@ -48,17 +48,17 @@ lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
 ]
 qed.
 
-lemma csx_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â¦¥[h, g] T.
+lemma csx_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] T â\86\92 â¦¥[h, g] â¦\83G, L, Tâ¦\84.
 /2 width=5 by csx_fsb_fpbs/ qed.
 
 (* Advanced eliminators *****************************************************)
 
-lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
-                    (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
-                                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                R G1 L1 T1
-                    ) →
-                    ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
+lemma csx_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term.
+                   (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+                               (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                               R G1 L1 T1
+                   ) →
+                   ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
 
 lemma csx_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
index 5f76fea80a0cbce0d4e3d71e0509c1bc13e5c18f..8376ac4c1df54bf0d72cd5aa7be5ede28b97876e 100644 (file)
@@ -59,3 +59,36 @@ lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
 #h #g #G #L1 #T1 #HT1 #T2 #H
 @(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
 qed-.
+
+lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                   ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+                   ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                      ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                      ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
+                      ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+                      ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
+                      ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
index 578937f4c84516861a887c849a8c5aa1365ea3b0..8da0347aaa3070bcce4ffa5fcfb1c801ec9e1b11 100644 (file)
@@ -1,10 +1,3 @@
-lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                   ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
-                   ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
-qed-.
-
 lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
                ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] →
                ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
@@ -23,32 +16,6 @@ elim (lstas_cpr_lpr  … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12
 /3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
 qed-.
 
-lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                      ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
-                      ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
-                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
-                      ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
-[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
-                      ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
-                      ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
-                      ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
-                      ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
-elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
-lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
-
 lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
                ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
                ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
@@ -82,3 +49,30 @@ lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
 elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
 qed-.
+
+(* Note: missing da_scpds_lpr, da_scpes *)
+
+lemma scpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                     ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 →
+                     ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                     ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G #L1 #T1 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (lstas_cpr_lpr … HTl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12
+lapply (da_cpr_lpr … HTl1 … HT12 … HL12) // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
+qed-.
+
+lemma scpes_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                     ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+                     ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+                     ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                     ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2.
+#h #g #G #L1 #T1 #HT1 #T2 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
+elim (scpds_cpr_lpr … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
+elim (scpds_cpr_lpr … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
+elim (cprs_conf … H1 … H2) -T0 /3 width=5 by scpds_div, scpds_cprs_trans/
+qed-.
+
+(* Note: missing lstas_scpds, scpes_le *)
index d6c4f425921df30f1937f49784b9c19460fc1137..207ba13bf278ab75c79776ba7f68df8a48d6e4b8 100644 (file)
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ â¦¥ break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( â¦¥ [ term 46 h, break term 46 g ] break â¦\83 term 46 G, break term 46 L, break term 46 T â¦\84 )"
    non associative with precedence 45
    for @{ 'BTSN $h $g $G $L $T }.
index 44976571b608f9bb04e54dfc71acb56844edb4ff..7c6d691205a58229b0495b269236b328d258e71b 100644 (file)
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ â¦¥ â¦¥ break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( â¦¥ â¦¥ [ term 46 h, break term 46 g ] break â¦\83 term 46 G, break term 46 L, break term 46 T â¦\84 )"
    non associative with precedence 45
    for @{ 'BTSNAlt $h $g $G $L $T }.
index 9ac05c7b6b5dd4e20ac461ab8192b42599e6f65f..1723a00052b6e7cca30d88c405538c221404abbc 100644 (file)
@@ -88,7 +88,7 @@ table {
           }
         ]
         [ { "strongly normalizing qrst-computation" * } {
-             [ "fsb ( â¦\83?,?â¦\84 â\8a¢ â¦¥[?,?] ? )" "fsb_alt ( â¦\83?,?â¦\84 â\8a¢ â¦¥â¦¥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
+             [ "fsb ( â¦¥[?,?] â¦\83?,?,?â¦\84 )" "fsb_alt ( â¦¥â¦¥[?,?] â¦\83?,?,?â¦\84 )" "fsb_aaa" + "fsb_csx" * ]
           }
         ]
         [ { "strongly normalizing rt-computation" * } {