confluence of parallel substitution (tps) started ...

[helm.git] / matita / matita / lib / lambda-delta / substitution / tps.ma

diff --git a/matita/matita/lib/lambda-delta/substitution/tps.ma b/matita/matita/lib/lambda-delta/substitution/tps.ma
index 9fe0c29e726370996a0acd6f1806cab5951f3b74..56d8f32118d77b893745692aa78b566470ab39c6 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/tps.ma
+++ b/matita/matita/lib/lambda-delta/substitution/tps.ma
@@ -91,6 +91,29 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
+lemma tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i →
+                         T2 = #i ∨ 
+                         ∃∃K,V1,V2,i. d ≤ i & i < d + e &
+                                      ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                      K ⊢ V1 [O, d + e - i - 1] ≫ V2 &
+                                      ↑[O, i + 1] V2 ≡ T2.
+#L #T1 #T2 #d #e * -L T1 T2 d e
+[ #L #k #d #e #i #H destruct
+| /2/
+| #L #K #V1 #V2 #T2 #i #d #e #Hdi #Hide #HLK #HV12 #HVT2 #j #H destruct -i /3 width=9/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+]
+qed.
+
+lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 →
+                     T2 = #i ∨ 
+                     ∃∃K,V1,V2,i. d ≤ i & i < d + e &
+                                  ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                  K ⊢ V1 [O, d + e - i - 1] ≫ V2 &
+                                  ↑[O, i + 1] V2 ≡ T2.
+/2/ qed.
+
 lemma tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
                          ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
                          ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &