-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.