milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fsb_csx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index 203f60b8aad1f66d6e47f8b5b4959fac9f9116a1..1839df0f8a3d800c1237a3c5a005fe2ddefccad8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -21,15 +21,17 @@ include "basic_2/rt_computation/fsb_fpbg.ma".
 
 (* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
 
-lemma fsb_inv_csx: ∀h,G,L,T. ≥[h] 𝐒❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
-#h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
+lemma fsb_inv_csx:
+      ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
+#G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
 qed-.
 
 (* Propreties with context-sensitive stringly rt-normalizing terms **********)
 
-lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
-                    ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫.
-#h #G1 #L1 #T1 #H @(csx_ind … H) -T1
+lemma csx_fsb_fpbs:
+      ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+      ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
+#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 (fpbs_csx_conf … H10) // -HT1 #HT0
@@ -56,23 +58,26 @@ generalize in match IHu; -IHu generalize in match H10; -H10
 ]
 qed.
 
-lemma csx_fsb: ∀h,G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ≥[h] 𝐒❪G,L,T❫.
+lemma csx_fsb:
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → ≥𝐒 ❪G,L,T❫.
 /2 width=5 by csx_fsb_fpbs/ qed.
 
 (* Advanced eliminators *****************************************************)
 
-lemma csx_ind_fpb: ∀h. ∀Q:relation3 genv lenv term.
-                   (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
-                               (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
-                               Q G1 L1 T1
-                   ) →
-                   ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ →  Q G L T.
+lemma csx_ind_fpb (Q:relation3 …):
+      (∀G1,L1,T1.
+        ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+        (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) →
+        Q G1 L1 T1
+      ) →
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
 
-lemma csx_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term.
-                    (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
-                                (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) →
-                                Q G1 L1 T1
-                    ) →
-                    ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ →  Q G L T.
+lemma csx_ind_fpbg (Q:relation3 …):
+      (∀G1,L1,T1.
+        ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+        (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
+        Q G1 L1 T1
+      ) →
+      ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.