include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/jsx_rsx.ma".
-(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+(* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
(* Forward lemmas with strongly rt-normalizing terms ************************)
-fact rsx_fwd_lref_pair_csx_aux (h) (G):
- โL. G โข โฌ*๐[h,#0] L โ
- โI,K,V. L = K.โ[I]V โ โชG,Kโซ โข โฌ*๐[h] V.
-#h #G #L #H
+fact rsx_fwd_lref_pair_csx_aux (G):
+ โL. G โข โฌ*๐[#0] L โ
+ โI,K,V. L = K.โ[I]V โ โชG,Kโซ โข โฌ*๐ V.
+#G #L #H
@(rsx_ind โฆ H) -L #L #_ #IH #I #K #V1 #H destruct
@csx_intro #V2 #HV12 #HnV12
@(IH โฆ I) -IH [1,4: // | -HnV12 | -G #H ]
]
qed-.
-lemma rsx_fwd_lref_pair_csx (h) (G):
- โI,K,V. G โข โฌ*๐[h,#0] K.โ[I]V โ โชG,Kโซ โข โฌ*๐[h] V.
+lemma rsx_fwd_lref_pair_csx (G):
+ โI,K,V. G โข โฌ*๐[#0] K.โ[I]V โ โชG,Kโซ โข โฌ*๐ V.
/2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-.
-lemma rsx_fwd_lref_pair_csx_drops (h) (G):
- โI,K,V,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[h,#i] L โ โชG,Kโซ โข โฌ*๐[h] V.
-#h #G #I #K #V #i elim i -i
+lemma rsx_fwd_lref_pair_csx_drops (G):
+ โI,K,V,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[#i] L โ โชG,Kโซ โข โฌ*๐ V.
+#G #I #K #V #i elim i -i
[ #L #H >(drops_fwd_isid โฆ H) -H
/2 width=2 by rsx_fwd_lref_pair_csx/
| #i #IH #L #H1 #H2
(* Inversion lemmas with strongly rt-normalizing terms **********************)
-lemma rsx_inv_lref_pair (h) (G):
- โI,K,V. G โข โฌ*๐[h,#0] K.โ[I]V โ
- โงโง โชG,Kโซ โข โฌ*๐[h] V & G โข โฌ*๐[h,V] K.
+lemma rsx_inv_lref_pair (G):
+ โI,K,V. G โข โฌ*๐[#0] K.โ[I]V โ
+ โงโง โชG,Kโซ โข โฌ*๐ V & G โข โฌ*๐[V] K.
/3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-.
-lemma rsx_inv_lref_pair_drops (h) (G):
- โI,K,V,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[h,#i] L โ
- โงโง โชG,Kโซ โข โฌ*๐[h] V & G โข โฌ*๐[h,V] K.
+lemma rsx_inv_lref_pair_drops (G):
+ โI,K,V,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[#i] L โ
+ โงโง โชG,Kโซ โข โฌ*๐ V & G โข โฌ*๐[V] K.
/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
-lemma rsx_inv_lref_drops (h) (G):
- โL,i. G โข โฌ*๐[h,#i] L โ
+lemma rsx_inv_lref_drops (G):
+ โL,i. G โข โฌ*๐[#i] L โ
โจโจ โฉ*[โป,๐โจiโฉ] L โ โ
| โโI,K. โฉ[i] L โ K.โค[I]
- | โโI,K,V. โฉ[i] L โ K.โ[I]V & โชG,Kโซ โข โฌ*๐[h] V & G โข โฌ*๐[h,V] K.
-#h #G #L #i #H elim (drops_F_uni L i)
+ | โโI,K,V. โฉ[i] L โ K.โ[I]V & โชG,Kโซ โข โฌ*๐ V & G โข โฌ*๐[V] K.
+#G #L #i #H elim (drops_F_uni L i)
[ /2 width=1 by or3_intro0/
| * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
]
(* Note: swapping the eliminations to avoid rsx_cpx_trans: no solution found *)
(* Basic_2A1: uses: lsx_lref_be_lpxs *)
-lemma rsx_lref_pair_lpxs (h) (G):
- โK1,V. โชG,K1โซ โข โฌ*๐[h] V โ
- โK2. G โข โฌ*๐[h,V] K2 โ โชG,K1โซ โข โฌ*[h] K2 โ
- โI. G โข โฌ*๐[h,#0] K2.โ[I]V.
-#h #G #K1 #V #H
+lemma rsx_lref_pair_lpxs (G):
+ โK1,V. โชG,K1โซ โข โฌ*๐ V โ
+ โK2. G โข โฌ*๐[V] K2 โ โชG,K1โซ โข โฌ* K2 โ
+ โI. G โข โฌ*๐[#0] K2.โ[I]V.
+#G #K1 #V #H
@(csx_ind_cpxs โฆ H) -V #V0 #_ #IHV0 #K2 #H
@(rsx_ind โฆ H) -K2 #K0 #HK0 #IHK0 #HK10 #I
@rsx_intro #Y #HY #HnY
]
qed.
-lemma rsx_lref_pair (h) (G):
- โK,V. โชG,Kโซ โข โฌ*๐[h] V โ G โข โฌ*๐[h,V] K โ โI. G โข โฌ*๐[h,#0] K.โ[I]V.
+lemma rsx_lref_pair (G):
+ โK,V. โชG,Kโซ โข โฌ*๐ V โ G โข โฌ*๐[V] K โ โI. G โข โฌ*๐[#0] K.โ[I]V.
/2 width=3 by rsx_lref_pair_lpxs/ qed.
(* Basic_2A1: uses: lsx_lref_be *)
-lemma rsx_lref_pair_drops (h) (G):
- โK,V. โชG,Kโซ โข โฌ*๐[h] V โ G โข โฌ*๐[h,V] K โ
- โI,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[h,#i] L.
-#h #G #K #V #HV #HK #I #i elim i -i
+lemma rsx_lref_pair_drops (G):
+ โK,V. โชG,Kโซ โข โฌ*๐ V โ G โข โฌ*๐[V] K โ
+ โI,i,L. โฉ[i] L โ K.โ[I]V โ G โข โฌ*๐[#i] L.
+#G #K #V #HV #HK #I #i elim i -i
[ #L #H >(drops_fwd_isid โฆ H) -H /2 width=1 by rsx_lref_pair/
| #i #IH #L #H
elim (drops_inv_bind2_isuni_next โฆ H) -H // #J #Y #HY #H destruct
(* Main properties with strongly rt-normalizing terms ***********************)
(* Basic_2A1: uses: csx_lsx *)
-theorem csx_rsx (h) (G):
- โL,T. โชG,Lโซ โข โฌ*๐[h] T โ G โข โฌ*๐[h,T] L.
-#h #G #L #T @(fqup_wf_ind_eq (โ) โฆ G L T) -G -L -T
+theorem csx_rsx (G):
+ โL,T. โชG,Lโซ โข โฌ*๐ T โ G โข โฌ*๐[T] L.
+#G #L #T @(fqup_wf_ind_eq (โ) โฆ G L T) -G -L -T
#Z #Y #X #IH #G #L * *
[ //
| #i #HG #HL #HT #H destruct