(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-inductive tpr: term → term → Prop ≝
+(* Basic-1: includes: pr0_delta1 *)
+inductive tpr: relation term ≝
| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
/2/ qed.
+(* Basic-1: was by definition: pr0_refl *)
lemma tpr_refl: ∀T. T ⇒ T.
#T elim T -T //
#I elim I -I /2/
]
qed.
+(* Basic-1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
/2/ qed.
∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
/2/ qed.
+(* Basic-1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
(∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
| (U0 ⇒ U2 ∧ I = Cast).
/2/ qed.
+(* Basic-1: was pr0_gen_appl *)
lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
U2 = 𝕔{Appl} V2. T2
elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
qed.
+(* Basic-1: was: pr0_gen_cast *)
lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
(∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
∨ T1 ⇒ U2.
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
/2/ qed.
+
+(* Basic-1: removed theorems 3:
+ pr0_subst0_back pr0_subst0_fwd pr0_subst0
+ Basic-1: removed local theorems: 1: pr0_delta_tau
+*)