matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc2.ma

   1
   2 include "basic_2/static/lfxs_lex.ma".
   3 include "basic_2/rt_transition/cpx_etc.ma".
   4 include "basic_2/rt_computation/lfpxs_lpxs.ma".
   5
   6 axiom fle_trans: ∀L1,L,T1,T. ⦃L1, T1⦄ ⊆ ⦃L, T⦄ →
   7                  ∀L2,T2. ⦃L, T⦄ ⊆ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄.
   8
   9 axiom pippo: ∀h,G,L1,T1,T2.  ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → ∀L. ⦃G, L1⦄ ⊢⬈[h] L →
  10              ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄.
  11 (*
  12 lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2.  ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
  13               ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄.
  14 #h #G #L1 #L #H
  15 lapply (lex_inv_ltc … H) -H // #H
  16 @(TC_star_ind ???????? H) -L //
  17 [ #T1 #T2 #H elim (pippo … H) -H /2 width=3 by conj/
  18 | #L #L0 #HL1 #HL0 #IH #T1 #T2 #HT12
  19   elim (IH … HT12) -IH #HT1 #HT21
  20   elim (pippo … T1 T1 … HL0) // #H1 #_ #_
  21   @conj
  22   [ @(fle_trans … H1) //
  23
  24 *)(*
  25 lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2.  ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
  26               ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄.
  27 #h #G #L1 #L #H
  28 lapply (lex_inv_ltc … H) -H // #H
  29 @(TC_star_ind_dx ???????? H) -L1 /2 width=5 by pippo/
  30 #L1 #L0 #HL10 #HL0 #IH #T1 #T2 #HT12
  31 elim (IH … HT12) -IH #HT1 #HT21 #H1T21
  32 @and3_intro
  33 [2:
  34 *)
  35
  36 axiom pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2.  ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
  37               ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & ⦃L, T2⦄ ⊆ ⦃L, T⦄.
  38
  39 lemma fle_tc_lfxs_trans: ∀h,G,L1,L2,T1. ⦃G, L1⦄ ⊢⬈*[h, T1] L2 →
  40                          ∀T2. ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄ → ⦃G, L1⦄ ⊢⬈* [h, T2] L2.
  41 #h #G #L1 #L2 #T1 #H
  42 @(TC_star_ind_dx ???????? H) -L1 /2 width=1 by tc_lfxs_refl, lfxs_refl/
  43 #L1 #L #HL1 #_ #IH #T2 #HT21
  44 lapply (fle_lfxs_trans … HT21 … HL1) -HL1 #HL1
  45 @(TC_strap … HL1) @IH -IH
  46
  47
  48 lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
  49 #h #G #L1 #T1 #T2 #HT12 #L2 #H
  50 lapply (cpx_fle_comp … HT12) -HT12 #HT21
  51
  52 elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
  53 @(lfpxs_lpxs_lfeq … HL1) -HL1
  54
  55
  56 @(fle_lfxs_trans
  57
  58 elim (pippos … HL1 … HT12) -HT12 #T #H #HT21
  59 @(lfpxs_lpxs_lfeq … HL1) -HL1
  60 @(fle_lfxs_trans … HL2) -HL2 //
  61 qed-.
  62
  63