include "basic_2/rt_computation/cpxs_theq_vector.ma".
include "basic_2/rt_computation/csx_simple_theq.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
include "basic_2/rt_computation/csx_vector.ma".
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
(* Advanced properties ************************************* ****************)
qed.
lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
- â\88\80V2. â¬\86*[⫯i] V1 ≘ V2 →
+ â\88\80V2. â¬\86*[â\86\91i] V1 ≘ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄.
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/
lapply (csx_fwd_pair_sn … H) #HW1
lapply (csx_fwd_flat_dx … H) #H1
@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … o … (V2@V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
+elim (cpxs_fwd_theta_vector … o … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
[ -H #H elim H2 -H2 //
| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]