1 lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
3 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
4 [ elim (drop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
5 #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (ylt_yle_false … H1m) -H1m //
6 | elim (drop_inv_O1_pair1 … H) -H * #H2m #HLK destruct
7 [ elim (ylt_yle_false … H1m) -H1m //
8 | elim (IHL … HLK) -IHL -HLK /2 width=1 by ylt_pred, conj/
13 lemma drop_O1_le: ∀s,m,L. m ≤ |L| → ∃K. ⬇[s, 0, m] L ≡ K.
14 #s #m @(ynat_ind … m) -m /2 width=2 by ex_intro/
16 [ #H elim (ylt_yle_false … H) -H //
17 | #L #I #V #H elim (IHm L) -IHm /3 width=2 by drop_drop, yle_inv_succ, ex_intro/
19 | #L #H elim (ylt_yle_false … H) -H //
23 lemma drop_O1_lt: ∀s,L,m. m < |L| → ∃∃I,K,V. ⬇[s, 0, m] L ≡ K.ⓑ{I}V.
25 [ #m #H elim (ylt_yle_false … H) -H //
26 | #L #I #V #IHL #m @(ynat_ind … m) -m /2 width=4 by drop_pair, ex1_3_intro/
27 [ #m #_#H elim (IHL m) -IHL /3 width=4 by drop_drop, ylt_inv_succ, ex1_3_intro/
28 | #H elim (ylt_yle_false … H) -H //
33 lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → m ≤ |L| → ∀I,V.
34 ∃∃J,W. ⬇[s, 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W.
35 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H #Hm #I #V
36 [ elim (drop_inv_atom1 … H) -H #H >(yle_inv_O2 … Hm) -m
37 #Hs destruct /2 width=3 by ex1_2_intro/
38 | elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK destruct /2 width=3 by ex1_2_intro/
39 elim (IHL … HLK … Z X) -IHL -HLK
40 /3 width=3 by yle_pred, drop_drop_lt, ex1_2_intro/
44 lemma drop_O1_ge: ∀L,m. |L| ≤ m → ⬇[Ⓣ, 0, m] L ≡ ⋆.
45 #L elim L -L [ #m #_ @drop_atom #H destruct ]
46 #L #I #V #IHL #m @(ynat_ind … m) -m //
47 [ #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/
48 | /4 width=1 by drop_drop, yle_inv_succ/
52 lemma drop_O1_eq: ∀L,s. ⬇[s, 0, |L|] L ≡ ⋆.
53 #L elim L -L /2 width=1 by drop_drop/
56 lemma drop_fwd_length_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → |L1| ≤ l → |L2| = |L1|.
57 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
58 [ #I #L1 #L2 #V #m #_ #_ #H elim (ylt_yle_false … H) -H //
59 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IH #H
60 lapply (yle_inv_succ … H) -H #H
61 >length_pair >length_pair /3 width=1 by eq_f/
65 lemma drop_fwd_length_le_le: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 →
66 ∀l0. l + m + l0 = |L1| → |L2| = l + l0.
67 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
68 [ #l #m #Hm #l0 #H elim (yplus_inv_O … H) -H
69 #H #H0 elim (yplus_inv_O … H) -H
71 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1 #IH #l0
72 /3 width=1 by ysucc_inv_inj/
73 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 #l0 >yplus_succ1 >yplus_succ1 #H
74 lapply (ysucc_inv_inj … H) -H #Hl1
75 >yplus_succ1 /3 width=1 by eq_f/
79 lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| ≤ l + m → |L2| = l.
80 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m
81 [ #l #m #_ #H #_ /2 width=1 by yle_inv_O2/
82 | #I #L #V #_ #H elim (ylt_yle_false … H) -H //
83 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1
84 /3 width=1 by yle_inv_succ/
85 | #I #L1 #L2 #V1 #v2 #l #m #_ #_ #IH
87 /4 width=1 by yle_inv_succ, eq_f/
91 lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
92 #L #K #s #l #m #i #HLK #HK #Hl elim (ylt_split i (|L|)) //
93 #HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
94 elim (ylt_inv_plus_sn … Hl) -Hl #l0 #H0
95 elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0
96 #K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1
97 #H elim (ylt_yle_false … H) -H //
100 lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
101 ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
102 #K2 #i @(ynat_ind … i) -i
103 [ /3 width=3 by lreq_O2, ex2_intro/
104 | #i #IHi #Y >yplus_succ2 #Hi
105 elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
106 #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
107 >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
108 #HL1K2 elim (IHi L1) -IHi // -HL1K2
109 /3 width=5 by lreq_pair, drop_drop, ex2_intro/
110 | #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //