X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind2_rmap_closed_2.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind2_rmap_closed_2.etc;h=58b1aab8d14474d29e4016a25d52b21dce0cda1b;hb=d108bcea8ebae11b03e8d8a155dfd3f2eb445127;hp=0000000000000000000000000000000000000000;hpb=4939d8280cb3467cd8fa648b1cea04f74d71e8b7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc
new file mode 100644
index 000000000..58b1aab8d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc
@@ -0,0 +1,57 @@
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
+
+lemma pippo (o) (q) (n):
+      (q◖𝗟) ϵ 𝐂❨o,n❩ →
+      (𝗟◗q) ϵ 𝐂❨o,n❩.
+#o #q elim q -q //
+* [ #k ] #q #IH #n #H0
+elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn
+[ elim (pcc_inv_d_dx … H0) -H0 #_ #H0
+  >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/
+| lapply (pcc_inv_m_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/
+| elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn
+  >Hn -Hn /4 width=1 by pcc_L_dx/
+| lapply (pcc_inv_A_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/
+| lapply (pcc_inv_S_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/
+]
+qed-.
+
+
+lemma pippo (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q＠⧣❨↑n❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+  <tr_compose_pap <tr_uni_pap //
+| <depth_L_dx <unwind2_rmap_L_dx
+  <tr_pap_push
+  /2 width=1 by nlt_succ_bi/
+]
+qed-.
+
+lemma pippo2 (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → ▶[f]q＠❨n❩ ≤ ♭q.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+  @(nle_trans … IH) -IH
+  <tr_compose_xap
+| <unwind2_rmap_L_dx <depth_L_dx
+  <tr_xap_push
+  /2 width=1 by nle_succ_bi/
+]
+qed-.
+
+lemma pippo (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → n < ▶[f]q＠⧣❨↑♭q❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+  <tr_compose_pap <tr_uni_pap
+  @(nlt_trans … (n+k)) [ // ]
+  @(nlt_trans … IH) -IH
+| <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
+  /2 width=1 by nlt_succ_bi/