(* *)
(**************************************************************************)
-include "basic_2/relocation/drops_ctc.ma".
+include "static_2/relocation/drops_ctc.ma".
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Advanced properties ******************************************************)
-lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
- â\88\80W2. â¬\86*[1] V2 â\89\98 W2 â\86\92 â¦\83G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
+lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 →
+ â\88\80W2. â\87§*[1] V2 â\89\98 W2 â\86\92 â¦\83G,K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
#h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
[ /3 width=3 by cpx_cpxs, cpx_delta/
| #V #V2 #_ #HV2 #IH #W2 #HVW2
]
qed.
-lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
- â\88\80U. â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
+lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G,K⦄ ⊢ #i ⬈*[h] T →
+ â\88\80U. â\87§*[1] T â\89\98 U â\86\92 â¦\83G,K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
#h #I #G #K #T #i #H @(cpxs_ind … H) -T
[ /3 width=3 by cpx_cpxs, cpx_lref/
| #T0 #T #_ #HT2 #IH #U #HTU
(* Basic_2A1: was: cpxs_delta *)
lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
- â¬\87*[i] L â\89\98 K.â\93\91{I}V1 â\86\92 â¦\83G, K⦄ ⊢ V1 ⬈*[h] V2 →
- â\88\80W2. â¬\86*[â\86\91i] V2 â\89\98 W2 â\86\92 â¦\83G, L⦄ ⊢ #i ⬈*[h] W2.
+ â\87©*[i] L â\89\98 K.â\93\91{I}V1 â\86\92 â¦\83G,K⦄ ⊢ V1 ⬈*[h] V2 →
+ â\88\80W2. â\87§*[â\86\91i] V2 â\89\98 W2 â\86\92 â¦\83G,L⦄ ⊢ #i ⬈*[h] W2.
#h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
[ /3 width=7 by cpx_cpxs, cpx_delta_drops/
| #V #V2 #_ #HV2 #IH #W2 #HVW2
(* Advanced inversion lemmas ************************************************)
-lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
+lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G,L⦄ ⊢ #0 ⬈*[h] T2 →
T2 = #0 ∨
- ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 & ⬆*[1] V2 ≘ T2 &
+ ∃∃I,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 & ⇧*[1] V2 ≘ T2 &
L = K.ⓑ{I}V1.
#h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
]
qed-.
-lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #↑i ⬈*[h] T2 →
+lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ⬈*[h] T2 →
T2 = #(↑i) ∨
- ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
+ ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬈*[h] T & ⇧*[1] T ≘ T2 & L = K.ⓘ{I}.
#h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
[ #H destruct
qed-.
(* Basic_2A1: was: cpxs_inv_lref1 *)
-lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 →
+lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G,L⦄ ⊢ #i ⬈*[h] T2 →
T2 = #i ∨
- â\88\83â\88\83I,K,V1,T1. â¬\87*[i] L â\89\98 K.â\93\91{I}V1 & â¦\83G, K⦄ ⊢ V1 ⬈*[h] T1 &
- â¬\86*[↑i] T1 ≘ T2.
+ â\88\83â\88\83I,K,V1,T1. â\87©*[i] L â\89\98 K.â\93\91{I}V1 & â¦\83G,K⦄ ⊢ V1 ⬈*[h] T1 &
+ â\87§*[↑i] T1 ≘ T2.
#h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
[ #H destruct