X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fllpx_sn_alt2.etc;h=5a87c0da3cd6fb347fc2874ab76ebe5ed73f332e;hb=3325b784763ae9e6bac4307463071bb38e5641c9;hp=888f83ef4cb50eaad1bd5d2754d75235f7d7f73f;hpb=a0d25627e80a3a2fe68da954b68f6d541c6dbc34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
index 888f83ef4..5a87c0da3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
@@ -15,104 +15,6 @@
 include "basic_2/substitution/cofrees_lift.ma".
 include "basic_2/substitution/llpx_sn_alt1.ma".
 
-lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
-#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
-qed-.
-
-lemma ldrop_fwd_length_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → |L1| ≤ d → |L2| = |L1|.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
-[ #I #L1 #L2 #V #e #_ #_ #H elim (le_plus_xSy_O_false … H)
-| /4 width=2 by le_plus_to_le_r, eq_f/
-]
-qed-.
-
-lemma ldrop_fwd_length_le_le: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → e ≤ |L1| - d → |L2| = |L1| - e.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
-[ /3 width=2 by le_plus_to_le_r/
-| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 >minus_plus_plus_l
-  #Hd #He lapply (le_plus_to_le_r … Hd) -Hd
-  #Hd >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/
-]
-qed-.
-
-lemma ldrop_fwd_length_le_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → |L1| - d ≤ e → |L2| = d.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e normalize
-[ /2 width=1 by le_n_O_to_eq/
-| #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
-| /3 width=2 by le_plus_to_le_r/
-| /4 width=2 by le_plus_to_le_r, eq_f/
-]
-qed-.
-
-lemma ldrop_O1_le: ∀s,e,L. e ≤ |L| → ∃K. ⇩[s, 0, e] L ≡ K.
-#s #e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
-#e #IHe *
-[ #H elim (le_plus_xSy_O_false … H)
-| #L #I #V normalize #H elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
-]
-qed-.
-
-lemma ldrop_O1_lt: ∀s,L,e. e < |L| → ∃∃I,K,V. ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
-#s #L elim L -L
-[ #e #H elim (lt_zero_false … H)
-| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
-  #e #_ normalize #H elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
-]
-qed-.
-
-lemma ldrop_O1_pair: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → e ≤ |L| → ∀I,V.
-                     ∃∃J,W. ⇩[s, 0, e] L.ⓑ{I}V ≡ K.ⓑ{J}W.
-#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize #He #I #V
-[ elim (ldrop_inv_atom1 … H) -H #H <(le_n_O_to_eq … He) -e
-  #Hs destruct /2 width=3 by ex1_2_intro/
-| elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK destruct /2 width=3 by ex1_2_intro/
-  elim (IHL … HLK … Z X) -IHL -HLK
-  /3 width=3 by ldrop_drop_lt, le_plus_to_minus, ex1_2_intro/
-]
-qed-.
-
-lemma ldrop_inv_O1_gt: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → |L| < e →
-                       s = Ⓣ ∧ K = ⋆.
-#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize in ⊢ (?%?→?); #H1e
-[ elim (ldrop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
-  #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (lt_zero_false … H1e)
-| elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HLK destruct
-  [ elim (lt_zero_false … H1e)
-  | elim (IHL … HLK) -IHL -HLK /2 width=1 by lt_plus_to_minus_r, conj/
-  ]
-]
-qed-.
-
-lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆.
-#L elim L -L [ #e #_ @ldrop_atom #H destruct ]
-#L #I #V #IHL #e @(nat_ind_plus … e) -e [ #H elim (le_plus_xSy_O_false … H) ]
-normalize /4 width=1 by ldrop_drop, monotonic_pred/
-qed.
-
-lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
-                   ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
-#L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
-[ #d #e2 #Hs #e1 #He12 @(ex2_intro … (⋆))
-  @ldrop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
-| #I #L1 #V #e1 #He1 lapply (le_n_O_to_eq … He1) -He1
-  #H destruct /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #e2 #HL12 #IHL12 #e1 @(nat_ind_plus … e1) -e1
-  [ /3 width=3 by ldrop_drop, ex2_intro/
-  | -HL12 #e1 #_ #He12 lapply (le_plus_to_le_r … He12) -He12
-    #He12 elim (IHL12 … He12) -IHL12 >minus_plus_plus_l
-    #L #HL1 #HL2 elim (lt_or_ge (|L1|) (e2-e1)) #H0
-    [ elim (ldrop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
-      elim (ldrop_inv_atom1 … HL2) -HL2 #H #_ destruct
-      @(ex2_intro … (⋆)) [ @ldrop_O1_ge normalize // ]
-      @ldrop_atom #H destruct
-    | elim (ldrop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by ldrop_drop, ex2_intro/
-    ]
-  ]
-| #I #L1 #L2 #V1 #V2 #d #e2 #_ #HV21 #IHL12 #e1 #He12 elim (IHL12 … He12) -IHL12
-  #L #HL1 #HL2 elim (lift_split … HV21 d e1) -HV21 /3 width=5 by ldrop_skip, ex2_intro/
-]
-qed-.
-
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
 (* alternative definition of llpx_sn (not recursive) *)