1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/computation/scpds_scpds.ma".
16 include "basic_2/equivalence/scpes.ma".
18 (* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
20 (* Advanced inversion lemmas ************************************************)
22 lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 →
23 ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
24 ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T.
25 #h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H
26 elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
29 (* Advanced properties ******************************************************)
31 lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 →
32 ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
33 ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2.
34 #h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 *
35 /3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
37 (* Properties on parallel computation for terms *****************************)
39 lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T →
40 ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d →
41 ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
42 ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2.
43 #h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0)
44 #X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1
45 /3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/
48 (* Main properties **********************************************************)
50 theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
51 ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
52 #h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2
53 elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/
56 theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 →
57 ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
58 /3 width=4 by scpes_trans, scpes_sym/ qed-.
60 theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
61 ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
62 /3 width=4 by scpes_trans, scpes_sym/ qed-.