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/notation/relations/dpconvstar_8.ma".
16 include "basic_2/computation/scpds.ma".
18 (* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
20 definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
22 ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T.
24 interpretation "stratified decomposed parallel equivalence (term)"
25 'DPConvStar h g l1 l2 G L T1 T2 = (scpes h g l1 l2 G L T1 T2).
27 (* Basic properties *********************************************************)
29 lemma scpds_div: ∀h,g,G,L,T1,T2,T,l1,l2.
30 ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T →
31 ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
32 /2 width=3 by ex2_intro/ qed.
34 lemma scpes_refl_O_O: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
35 ⦃G, L⦄ ⊢ T •*⬌*[h, g, 0, 0] T.
36 /3 width=3 by scpds_refl, scpds_div/ qed.
38 lemma scpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
39 ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
40 #h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by scpds_div/