- reconstruction of lfpx_frees.ma begins ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_fqup.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index c82690309a7b312ebb4e44ce193c4fac0adf41a3..d89aaaaae7a59b3c000ad58fddc29f5b5c8b06c2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/relocation/drops.ma".
 include "basic_2/s_computation/fqup_weight.ma".
 include "basic_2/static/frees.ma".
 
@@ -44,3 +45,59 @@ lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
   ]
 ]
 qed-.
+
+(* Properties with plus-iterated supclosure *********************************)
+
+lemma frees_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+                        ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
+                        ∀g1. ⫯g1 = ⫱*[n] f1 →
+                        ∃∃g2. L2 ⊢ 𝐅*⦃V2⦄ ≡ g2 & g2 ⊆ g1.
+#f1 #L1 #T1 #H elim H -f1 -L1 -T1
+[ #f1 #I1 #Hf1 #I2 #L2 #V2 #n #HL12
+  elim (drops_inv_atom1 … HL12) -HL12 #H destruct
+| #f1 #I1 #L1 #V1 #s #_ #IH #I2 #L2 #V2 *
+  [ -IH #_ #g1 #Hgf1 elim (discr_next_push … Hgf1)
+  | #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+    #HL12 #g1 <tls_xn #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+    /2 width=3 by ex2_intro/
+  ]
+| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
+  [ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+    #H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
+    /2 width=3 by sle_refl, ex2_intro/
+  | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+    #HL12 #g1 <tls_xn <tl_next_rew #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+    /2 width=3 by ex2_intro/
+  ]
+| #f1 #I1 #L1 #V1 #i #_ #IH #I2 #L2 #V2 *
+  [ -IH #_ #g1 #Hgf1 elim (discr_next_push … Hgf1)
+  | #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+    #HL12 #g1 <tls_xn #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+    /2 width=3 by ex2_intro/
+  ]
+| #f1 #I1 #L1 #V1 #l #_ #IH #I2 #L2 #V2 *
+  [ -IH #_ #g1 #Hgf1 elim (discr_next_push … Hgf1)
+  | #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+    #HL12 #g1 <tls_xn #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+    /2 width=3 by ex2_intro/
+  ]
+| #fV1 #fT1 #f1 #p #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
+  lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
+  elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
+  #gV1 #gT1 #Hg1
+  [ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
+    /3 width=6 by sor_sle_sn, ex2_intro/
+  | -IHV1 #_ >tls_xn #H2 elim (IHT1 … H2) -IHT1 -H2
+    /3 width=6 by drops_drop, sor_sle_dx, ex2_intro/
+  ]
+| #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
+  lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
+  elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
+  #gV1 #gT1 #Hg1
+  [ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
+    /3 width=6 by sor_sle_sn, ex2_intro/
+  | -IHV1 #_ #H2 elim (IHT1 … HL12 … H2) -IHT1 -HL12 -H2
+    /3 width=6 by sor_sle_dx, ex2_intro/
+  ]
+]
+qed-.