matita/matita/contribs/lambdadelta/basic_2/etc/scpds/scpds.etc

   1 (* these are superseded by confluence of cpms *)
   2
   3 lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 →
   4                           ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2.
   5 #h #o #G #L #T1 #T2 #d2 *
   6 #T0 #d1 #_ #_ #HT10 #HT02 #T #HT1
   7 lapply (lstas_mono … HT10 … HT1) #H destruct //
   8 qed-.
   9
  10 (* Main properties **********************************************************)
  11
  12 theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 →
  13                        ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 →
  14                        ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
  15 #h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2
  16 lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/
  17 qed-.