(* Advanced properties ******************************************************)
(* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: โL,T. โf. L โข ๐
*โฆTโฆ โ f.
+lemma frees_total: โL,T. โf. L โข ๐
+โชTโซ โ 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: โf1,L,V. L โข ๐
*โฆVโฆ โ f1 โ โf2,T. L.โง โข ๐
*โฆTโฆ โ f2 โ
- โf. f1 โ โซฑf2 โ f โ โp,I. L โข ๐
*โฆโ{p,I}V.Tโฆ โ f.
+theorem frees_bind_void:
+ โf1,L,V. L โข ๐
+โชVโซ โ f1 โ โf2,T. L.โง โข ๐
+โชTโซ โ f2 โ
+ โf. f1 โ โซฑf2 โ f โ โp,I. L โข ๐
+โชโ[p,I]V.Tโซ โ 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: โf,p,I,L,V,T. L โข ๐
*โฆโ{p,I}V.Tโฆ โ f โ
- โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L.โง โข ๐
*โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
+lemma frees_inv_bind_void:
+ โf,p,I,L,V,T. L โข ๐
+โชโ[p,I]V.Tโซ โ f โ
+ โโf1,f2. L โข ๐
+โชVโซ โ f1 & L.โง โข ๐
+โชTโซ โ 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
]
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.
+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