(* 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 ≘ f.
+lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ 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/
| /3 width=2 by frees_gref, ex_intro/
| #p #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
- elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT
+ elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
elim (sor_isfin_ex f1 (⫱f2))
/3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
| #I #V #T #HG #HL #HT destruct
(* Advanced main properties *************************************************)
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 ≘ 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 ≘ f.
+ â\88\80f1,L,V. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 →
+ â\88\80f. f1 â\8b\93 ⫱f2 â\89\98 f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85+â\9dªâ\93\91[p,I]V.Tâ\9d« ≘ f.
#f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
-elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0
+elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
elim (pn_split f2) * #g2 #H destruct
[ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct
(* 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 ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
+ â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9dªâ\93\91[p,I]V.Tâ\9d« ≘ f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ ⫱f2 ≘ 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
lemma frees_ind_void (Q:relation3 …):
(
- â\88\80f,L,s. ð\9d\90\88â¦\83fâ¦\84 → Q L (⋆s) f
+ â\88\80f,L,s. ð\9d\90\88â\9dªfâ\9d« → Q L (⋆s) f
) → (
- â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 → Q (⋆) (#i) (⫯*[i]↑f)
+ â\88\80f,i. ð\9d\90\88â\9dªfâ\9d« → Q (⋆) (#i) (⫯*[i]↑f)
) → (
∀f,I,L,V.
- L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f â\86\92 Q L V fâ\86\92 Q (L.â\93\91{I}V) (#O) (↑f)
+ L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f â\86\92 Q L V fâ\86\92 Q (L.â\93\91[I]V) (#O) (↑f)
) → (
- â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 Q (L.â\93¤{I}) (#O) (↑f)
+ â\88\80f,I,L. ð\9d\90\88â\9dªfâ\9d« â\86\92 Q (L.â\93¤[I]) (#O) (↑f)
) → (
∀f,I,L,i.
- L â\8a¢ ð\9d\90\85+â¦\83#iâ¦\84 â\89\98 f â\86\92 Q L (#i) f â\86\92 Q (L.â\93\98{I}) (#(↑i)) (⫯f)
+ L â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92 Q L (#i) f â\86\92 Q (L.â\93\98[I]) (#(↑i)) (⫯f)
) → (
- â\88\80f,L,l. ð\9d\90\88â¦\83fâ¦\84 → Q L (§l) f
+ â\88\80f,L,l. ð\9d\90\88â\9dªfâ\9d« → Q L (§l) f
) → (
∀f1,f2,f,p,I,L,V,T.
- L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â¦\83Tâ¦\84≘ f2 → f1 ⋓ ⫱f2 ≘ f →
- Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
+ L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«≘ 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 â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L â\8a¢ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 → f1 ⋓ f2 ≘ f →
- Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
+ L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L â\8a¢ð\9d\90\85+â\9dªTâ\9d« ≘ f2 → f1 ⋓ f2 ≘ f →
+ Q L V f1 → Q L T f2 → Q L (ⓕ[I]V.T) f
) →
- â\88\80L,T,f. L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f → Q L T f.
+ â\88\80L,T,f. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ 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