matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc

   1 include "delayed_updating/unwind/unwind2_rmap_closed.ma".
   2
   3 lemma pippo (o) (q) (n):
   4       (q◖𝗟) ϵ 𝐂❨o,n❩ →
   5       (𝗟◗q) ϵ 𝐂❨o,n❩.
   6 #o #q elim q -q //
   7 * [ #k ] #q #IH #n #H0
   8 elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn
   9 [ elim (pcc_inv_d_dx … H0) -H0 #_ #H0
  10   >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/
  11 | lapply (pcc_inv_m_dx … H0) -H0 #H0
  12   >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/
  13 | elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn
  14   >Hn -Hn /4 width=1 by pcc_L_dx/
  15 | lapply (pcc_inv_A_dx … H0) -H0 #H0
  16   >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/
  17 | lapply (pcc_inv_S_dx … H0) -H0 #H0
  18   >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/
  19 ]
  20 qed-.
  21
  22
  23 lemma pippo (o) (f) (q) (n):
  24       q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q＠⧣❨↑n❩.
  25 #o #f #q #n #H0 elim H0 -q -n //
  26 #q #n [ #k #_ ] #_ #IH
  27 [ <depth_d_dx <unwind2_rmap_d_dx
  28   <tr_compose_pap <tr_uni_pap //
  29 | <depth_L_dx <unwind2_rmap_L_dx
  30   <tr_pap_push
  31   /2 width=1 by nlt_succ_bi/
  32 ]
  33 qed-.
  34
  35 lemma pippo2 (o) (f) (q) (n):
  36       q ϵ 𝐂❨o,n❩ → ▶[f]q＠❨n❩ ≤ ♭q.
  37 #o #f #q #n #H0 elim H0 -q -n //
  38 #q #n [ #k #_ ] #_ #IH
  39 [ <unwind2_rmap_d_dx <depth_d_dx
  40   @(nle_trans … IH) -IH
  41   <tr_compose_xap
  42 | <unwind2_rmap_L_dx <depth_L_dx
  43   <tr_xap_push
  44   /2 width=1 by nle_succ_bi/
  45 ]
  46 qed-.
  47
  48 lemma pippo (o) (f) (q) (n):
  49       q ϵ 𝐂❨o,n❩ → n < ▶[f]q＠⧣❨↑♭q❩.
  50 #o #f #q #n #H0 elim H0 -q -n //
  51 #q #n [ #k #_ ] #_ #IH
  52 [ <unwind2_rmap_d_dx <depth_d_dx
  53   <tr_compose_pap <tr_uni_pap
  54   @(nlt_trans … (n+k)) [ // ]
  55   @(nlt_trans … IH) -IH
  56 | <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
  57   /2 width=1 by nlt_succ_bi/