- confluence of context-free reduction on terms (tpr) closed!

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / reduction / tpr.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
index fdfc4f08b8d499bd868ffacf80691ae7cc0c9178..6f90fd90791ac80f2f5f4ed28b1d1899890d8a99 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
@@ -16,6 +16,7 @@ include "Basic-2/substitution/tps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
+(* Basic-1: includes: pr0_delta1 *)
 inductive tpr: term → term → Prop ≝
 | tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
@@ -44,6 +45,7 @@ lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ 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/
@@ -63,6 +65,7 @@ fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒
 ]
 qed.
 
+(* Basic-1: was: pr0_gen_sort pr0_gen_lref *)
 lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
 /2/ qed.
 
@@ -91,6 +94,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
                      ∃∃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 &
@@ -139,6 +143,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
                       |                     (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
@@ -153,6 +158,7 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
 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.
@@ -185,30 +191,8 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
                                   T1 = 𝕔{Abbr} V. T
                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
 /2/ qed.
-(*
-pr0/fwd pr0_gen_sort
-pr0/fwd pr0_gen_lref
-pr0/fwd pr0_gen_abst
-pr0/fwd pr0_gen_appl
-pr0/fwd pr0_gen_cast
-pr0/fwd pr0_gen_abbr
-pr0/fwd pr0_gen_void
-pr0/fwd pr0_gen_lift
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
-pr0/pr0 pr0_confluence__pr0_cong_delta
-pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
-pr0/pr0 pr0_confluence__pr0_delta_delta
-pr0/pr0 pr0_confluence__pr0_delta_tau
-pr0/pr0 pr0_confluence
-pr0/props pr0_lift
-pr0/props pr0_subst0_back
-pr0/props pr0_subst0_fwd
-pr0/props pr0_subst0
-pr0/subst1 pr0_delta1
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr0/subst1 pr0_subst1
-*)
\ No newline at end of file
+
+(* Basic-1: removed theorems 3:
+            pr0_subst0_back pr0_subst0_fwd pr0_subst0
+   Basic-1: removed local theorems: 1: pr0_delta_tau
+*)