1 include "delayed_updating/unwind/unwind2_rmap_closed.ma".
3 lemma pippo (o) (q) (n):
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/
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
31 /2 width=1 by nlt_succ_bi/
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
42 | <unwind2_rmap_L_dx <depth_L_dx
44 /2 width=1 by nle_succ_bi/
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)) [ // ]
56 | <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
57 /2 width=1 by nlt_succ_bi/