(* 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/
(* 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
lapply (lsubr_lsubf โฆ Hf2 โฆ Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
(* 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