lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / ygt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index 3b55fca9920e66a6a8be3f1a163cae1097a237c0..b593d637de03bb4cb7676417d5716a902a0920a8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/btpredstarproper_6.ma".
 include "basic_2/dynamic/ysc.ma".
 include "basic_2/dynamic/yprs.ma".
 
@@ -20,7 +21,7 @@ include "basic_2/dynamic/yprs.ma".
 inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝
 | ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ →
             ygt h g L1 T1 L2 T2
-| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T
+| ygt_step: â\88\80L,L2,T. ygt h g L1 T1 L T â\86\92 L â\8a¢ â\9e¡ L2 â\86\92 ygt h g L1 T1 L2 T
 .
 
 interpretation "'big tree' proper parallel computation (closure)"
@@ -31,7 +32,7 @@ interpretation "'big tree' proper parallel computation (closure)"
 lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ →
                     h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
 #h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2
-/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/
+/3 width=4 by yprs_strap1, ysc_ypr, ypr_lpr/
 qed-.
 
 (* Basic properties *********************************************************)
@@ -65,8 +66,9 @@ lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
 /3 width=4 by ygt_strap2/
 qed-.
 
-lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
+lemma fsupp_ygt: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+qed.
 
 lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
                 h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.