include "static_2/s_computation/fqus.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
(* Properties with extended supclosure **************************************)
-lemma csx_fqu_conf (h) (b):
- â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 â\86\92 â¦\83G2,L2â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T2â¦\84.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+lemma csx_fqu_conf (b):
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G2,L2,T2â\9d© →
+ â\9d¨G1,L1â\9d© â\8a¢ â¬\88*ð\9d\90\92 T1 â\86\92 â\9d¨G2,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T2.
+#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/
| /2 width=3 by csx_fwd_pair_sn/
| /2 width=2 by csx_fwd_bind_dx/
]
qed-.
-lemma csx_fquq_conf (h) (b):
- â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82⸮[b] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 â\86\92 â¦\83G2,L2â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T2â¦\84.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
+lemma csx_fquq_conf (b):
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82⸮[b] â\9d¨G2,L2,T2â\9d© →
+ â\9d¨G1,L1â\9d© â\8a¢ â¬\88*ð\9d\90\92 T1 â\86\92 â\9d¨G2,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T2.
+#b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
* #HG #HL #HT destruct //
qed-.
-lemma csx_fqup_conf (h) (b):
- â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82+[b] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 â\86\92 â¦\83G2,L2â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T2â¦\84.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+lemma csx_fqup_conf (b):
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82+[b] â\9d¨G2,L2,T2â\9d© →
+ â\9d¨G1,L1â\9d© â\8a¢ â¬\88*ð\9d\90\92 T1 â\86\92 â\9d¨G2,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T2.
+#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
/3 width=6 by csx_fqu_conf/
qed-.
-lemma csx_fqus_conf (h) (b):
- â\88\80G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 â\86\92 â¦\83G2,L2â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T2â¦\84.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
+lemma csx_fqus_conf (b):
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+ â\9d¨G1,L1â\9d© â\8a¢ â¬\88*ð\9d\90\92 T1 â\86\92 â\9d¨G2,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T2.
+#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
/3 width=6 by csx_fquq_conf/
qed-.