(* Advanced properties ******************************************************)
(* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f.
+lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f.
#L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
#G0 #L0 #T0 #IH #G #L * *
[ /3 width=2 by frees_sort, ex_intro/
(* Advanced main properties *************************************************)
-theorem frees_bind_void: â\88\80f1,L,V. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 →
- â\88\80f. f1 â\8b\93 ⫱f2 â\89¡ f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f.
+theorem frees_bind_void: â\88\80f1,L,V. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 →
+ â\88\80f. f1 â\8b\93 ⫱f2 â\89\98 f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 f.
#f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
- lapply (sor_sym … Hz) -Hz #Hz
+ lapply (sor_comm … Hz) -Hz #Hz
lapply (sor_mono … f Hz ?) // -Hz #H
lapply (sor_inv_sle_sn … Hf) -Hf #Hf
- lapply (frees_eq_repl_back â\80¦ Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
+ lapply (frees_eq_repl_back â\80¦ Hf0 (â\86\91f) ?) /2 width=5 by eq_next/ -z #Hf0
@(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
/2 width=1 by sor_sle_dx/
]
(* Advanced inversion lemmas ************************************************)
-lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.
#f #p #I #L #V #T #H
elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
elim (frees_total (L.ⓧ) T) #f0 #Hf0
lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
@(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
- /2 width=3 by sor_trans2_idem/
+ /2 width=3 by sor_comm_23_idem/
+]
+qed-.
+
+lemma frees_ind_void: ∀Q:relation3 ….
+ (
+ ∀f,L,s. 𝐈⦃f⦄ → Q L (⋆s) f
+ ) → (
+ ∀f,i. 𝐈⦃f⦄ → Q (⋆) (#i) (⫯*[i]↑f)
+ ) → (
+ ∀f,I,L,V.
+ L ⊢ 𝐅*⦃V⦄ ≘ f → Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f)
+ ) → (
+ ∀f,I,L. 𝐈⦃f⦄ → Q (L.ⓤ{I}) (#O) (↑f)
+ ) → (
+ ∀f,I,L,i.
+ L ⊢ 𝐅*⦃#i⦄ ≘ f → Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f)
+ ) → (
+ ∀f,L,l. 𝐈⦃f⦄ → Q L (§l) f
+ ) → (
+ ∀f1,f2,f,p,I,L,V,T.
+ L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f →
+ Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
+ ) → (
+ ∀f1,f2,f,I,L,V,T.
+ L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f →
+ Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
+ ) →
+ ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → Q L T f.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
+@(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
+[ #s #HG #HL #HT #f #H destruct -IH
+ lapply (frees_inv_sort … H) -H /2 width=1 by/
+| cases L -L
+ [ #i #HG #HL #HT #f #H destruct -IH
+ elim (frees_inv_atom … H) -H #g #Hg #H destruct /2 width=1 by/
+ | #L #I * [ cases I -I #I [ | #V ] | #i ] #HG #HL #HT #f #H destruct
+ [ elim (frees_inv_unit … H) -H #g #Hg #H destruct /2 width=1 by/
+ | elim (frees_inv_pair … H) -H #g #Hg #H destruct
+ /4 width=2 by fqu_fqup, fqu_lref_O/
+ | elim (frees_inv_lref … H) -H #g #Hg #H destruct
+ /4 width=2 by fqu_fqup/
+ ]
+ ]
+| #l #HG #HL #HT #f #H destruct -IH
+ lapply (frees_inv_gref … H) -H /2 width=1 by/
+| #p #I #V #T #HG #HL #HT #f #H destruct
+ elim (frees_inv_bind_void … H) -H /3 width=7 by/
+| #I #V #T #HG #HL #HT #f #H destruct
+ elim (frees_inv_flat … H) -H /3 width=7 by/
]
qed-.