X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_path_append.ma;h=8796ce86f860c08785d8e63c4d746ce4edeeda30;hb=e4328f6887dc0235d49d965a5ba44787b1754b80;hp=3114e9edd726515efca7a293a92dfe1959bca2ce;hpb=23e56dd2f1ff99613b69e1ed2a9f26e752304290;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
index 3114e9edd..8796ce86f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
@@ -19,20 +19,20 @@ include "ground/xoa/ex_4_2.ma".
 
 (* TAILED UNWIND FOR PATH ***************************************************)
 
-(* Constructions with inner condition for path ******************************)
+(* Constructions with pic ***************************************************)
 
-lemma unwind2_path_inner (f) (p):
+lemma unwind2_path_pic (f) (p):
       p ϵ 𝐈 → ⊗p = ▼[f]p.
 #f * // * // #k #q #Hq
 elim (pic_inv_d_dx … Hq)
 qed-.
 
-(* Constructions with append and inner condition for path *******************)
+(* Constructions with append and pic ****************************************)
 
-lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
+lemma unwind2_path_append_pic_sn (f) (p) (q): p ϵ 𝐈 →
       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
 #f #p * [ #Hp | * [ #k ] #q #_ ] //
-[ <(unwind2_path_inner … Hp) -Hp //
+[ <(unwind2_path_pic … Hp) -Hp //
 | <unwind2_path_d_dx <unwind2_path_d_dx
   /2 width=3 by trans_eq/
 | <unwind2_path_L_dx <unwind2_path_L_dx //
@@ -41,9 +41,9 @@ lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
 ]
 qed.
 
-(* Constructions with append and proper condition for path ******************)
+(* Constructions with append and ppc ****************************************)
 
-lemma unwind2_path_append_proper_dx (f) (p) (q): q ϵ 𝐏 →
+lemma unwind2_path_append_ppc_dx (f) (p) (q): q ϵ 𝐏 →
       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
 #f #p * [ #Hq | * [ #k ] #q #_ ] //
 [ elim (ppc_inv_empty … Hq)
@@ -63,47 +63,47 @@ lemma unwind2_path_d_empty (f) (k):
 
 lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
       ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
-#f #p #l #k <unwind2_path_append_proper_dx in ⊢ (???%); //
+#f #p #l #k <unwind2_path_append_ppc_dx in ⊢ (???%); //
 qed.
 
 lemma unwind2_path_m_sn (f) (p):
       ▼[f]p = ▼[f](𝗺◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_L_sn (f) (p):
       (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_A_sn (f) (p):
       (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_S_sn (f) (p):
       (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
-(* Destructions with inner condition for path *******************************)
+(* Destructions with pic ****************************************************)
 
-lemma unwind2_path_des_inner (f) (p):
+lemma unwind2_path_des_pic (f) (p):
       ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
 #f * // * [ #k ] #p //
 <unwind2_path_d_dx #H0
 elim (pic_inv_d_dx … H0)
 qed-.
 
-(* Destructions with append and inner condition for path ********************)
+(* Destructions with append and pic *****************************************)
 
-lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
+lemma unwind2_path_des_append_pic_sn (f) (p) (q1) (q2):
       q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
 [ <list_append_empty_sn #H0 destruct
-  lapply (unwind2_path_des_inner … Hq1) -Hq1 #Hp
-  <(unwind2_path_inner … Hp) -Hp
+  lapply (unwind2_path_des_pic … Hq1) -Hq1 #Hp
+  <(unwind2_path_pic … Hp) -Hp
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
   elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
@@ -112,24 +112,24 @@ lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_L_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_A_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_S_sn <Hr2 -Hr2 //
 ]
 qed-.
 
-(* Inversions with append and proper condition for path *********************)
+(* Inversions with append and ppc *******************************************)
 
-lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
+lemma unwind2_path_inv_append_ppc_dx (f) (p) (q1) (q2):
       q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
@@ -142,17 +142,17 @@ lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_L_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_A_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_S_sn <Hr2 -Hr2 //
 ]
 qed-.
@@ -167,7 +167,7 @@ lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
   elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
   /2 width=5 by ex4_2_intro/
 | >list_cons_comm #H0
-  elim (unwind2_path_inv_append_proper_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
+  elim (unwind2_path_inv_append_ppc_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
   elim (eq_inv_d_dx_structure … Hr1)
 ]
 qed-.
@@ -176,7 +176,7 @@ lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
       (𝗺◗q) = ▼[f]p → ⊥.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_m_dx_structure … Hr1)
 qed-.
@@ -186,11 +186,11 @@ lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_L_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/
@@ -201,11 +201,11 @@ lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_A_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/
@@ -216,11 +216,11 @@ lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_S_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/