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 "static_2/s_computation/fqus.ma".
16 include "basic_2/rt_computation/csx_lsubr.ma".
18 (* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
20 (* Properties with extended supclosure **************************************)
22 lemma csx_fqu_conf (h) (b):
23 ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ →
24 ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
25 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
26 [ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/
27 | /2 width=3 by csx_fwd_pair_sn/
28 | /2 width=2 by csx_fwd_bind_dx/
29 | /2 width=4 by csx_fwd_bind_dx_unit/
30 | /2 width=3 by csx_fwd_flat_dx/
31 | /4 width=7 by csx_inv_lifts, drops_refl, drops_drop/
35 lemma csx_fquq_conf (h) (b):
36 ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ →
37 ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
38 #h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
39 * #HG #HL #HT destruct //
42 lemma csx_fqup_conf (h) (b):
43 ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ →
44 ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
45 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
46 /3 width=6 by csx_fqu_conf/
49 lemma csx_fqus_conf (h) (b):
50 ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
51 ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
52 #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
53 /3 width=6 by csx_fquq_conf/