(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps.ma".
+include "basic_2/substitution/tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
| tpr_beta : ∀V1,V2,W,T1,T2.
tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
| tpr_delta: ∀I,V1,V2,T1,T2,T.
- tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
+ tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T →
tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
-| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93£V. T1) T2
+| tpr_tau : â\88\80V,T1,T2. tpr T1 T2 â\86\92 tpr (â\93\9dV. T1) T2
.
interpretation
(* Basic properties *********************************************************)
-lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
- ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
+lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. ⓓV2 ⊢ T2 [0, 1] ▶ T &
+ ⋆. ⓓV2 ⊢ T2 ▶ [0, 1] T &
U2 = ⓓV2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
U = ⓐV2. T2.
#V1 #T1 #U #H #HT1
qed-.
(* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93£V1. T1 ➡ U2 →
- (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93£V2. T2)
+lemma tpr_inv_cast1: â\88\80V1,T1,U2. â\93\9dV1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93\9dV2. T2)
∨ T1 ➡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=5/
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
T1 = ⓓV. T
- | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93\9dV. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3: