(* forward lemmas with finite colength assignment ***************************)
lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
- â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & |L1| = |L2| + n.
+ â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & |L1| = |L2| + n.
#f #L1 #L2 #H elim H -f -L1 -L2
[ /4 width=3 by pr_fcla_isi, ex2_intro/
| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/
qed-.
(* Basic_2A1: includes: drop_fwd_length *)
-lemma drops_fcla_fwd: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n →
+lemma drops_fcla_fwd: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n →
|L1| = |L2| + n.
#f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
- â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & n ≤ |L1|.
+ â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & n ≤ |L1|.
#f #L1 #L2 #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
qed-.
(* Basic_2A1: includes: drop_fwd_length_le2 *)
-lemma drops_fcla_fwd_le2: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n →
+lemma drops_fcla_fwd_le2: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n →
n ≤ |L1|.
#f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] →
- â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & n < |L1|.
+ â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & n < |L1|.
#f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
#n #Hf #H >H -L1 /3 width=3 by nle_succ_bi, ex2_intro/
qed-.
(* Basic_2A1: includes: drop_fwd_length_lt2 *)
lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
- â\87©*[â\93\89,f] L1 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n →
+ â\87©*[â\93\89,f] L1 â\89\98 K2.â\93\98[I2] â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n →
n < |L1|.
#f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
(* Basic_2A1: includes: drop_fwd_length_lt4 *)
-lemma drops_fcla_fwd_lt4: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n → 0 < n →
+lemma drops_fcla_fwd_lt4: â\88\80f,L1,L2,n. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n → 0 < n →
|L2| < |L1|.
#f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
/2 width=1 by nlt_inv_minus_dx/ qed-.
(* Basic_2A1: includes: drop_inv_length_eq *)
-lemma drops_inv_length_eq: â\88\80f,L1,L2. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 |L1| = |L2| â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma drops_inv_length_eq: â\88\80f,L1,L2. â\87©*[â\93\89,f] L1 â\89\98 L2 â\86\92 |L1| = |L2| â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
#f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H
#n #Hn <HL12 -L2 #H lapply (nplus_refl_sn … H) -H
/2 width=3 by pr_fcla_inv_zero/
qed-.
theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 →
- â\88\83â\88\83n. ð\9d\90\82â\9dªf1â\9d« â\89\98 n & ð\9d\90\82â\9dªf2â\9d« ≘ n.
+ â\88\83â\88\83n. ð\9d\90\82â\9d¨f1â\9d© â\89\98 n & ð\9d\90\82â\9d¨f2â\9d© ≘ n.
#f1 #f2 #L1 #L2 #H1 #H2
elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
qed-.
theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2.
- â\87©*[â\93\89,f1] L1 â\89\98 L2 â\86\92 â\87©*[â\93\89,f2] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9dªf1â\9d« â\89\98 n1 â\86\92 ð\9d\90\82â\9dªf2â\9d« ≘ n2 →
+ â\87©*[â\93\89,f1] L1 â\89\98 L2 â\86\92 â\87©*[â\93\89,f2] L1 â\89\98 L2 â\86\92 ð\9d\90\82â\9d¨f1â\9d© â\89\98 n1 â\86\92 ð\9d\90\82â\9d¨f2â\9d© ≘ n2 →
n1 = n2.
#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1