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/