:: The Incompleteness of the Lattice of SubstitutionsPRE_CIRC,
:: by Adam Grabowski
::
:: Received July 17, 2000
:: Copyright (c) 2000 Association of Mizar Users
Lm1:
for A, x being set holds [:A,{x}:] is Function
Lm2:
( 0 = 2 * 0 & 2 = 2 * 1 )
;
1 = 0 + 1
;
then Lm3:
not 1 is even
by Lm2;
theorem Th1: :: HEYTING3:1
theorem :: HEYTING3:2
canceled;
theorem Th3: :: HEYTING3:3
theorem :: HEYTING3:4
theorem Th5: :: HEYTING3:5
theorem Th6: :: HEYTING3:6
theorem :: HEYTING3:7
theorem :: HEYTING3:8
theorem :: HEYTING3:9
theorem :: HEYTING3:10
canceled;
theorem :: HEYTING3:11
theorem Th12: :: HEYTING3:12
theorem Th13: :: HEYTING3:13
theorem :: HEYTING3:14
:: deftheorem defines SubstPoset HEYTING3:def 1 :
theorem Th15: :: HEYTING3:15
theorem :: HEYTING3:16
definition
let n,
k be
Element of
NAT ;
func PFArt n,
k -> Element of
PFuncs NAT ,
{k} means :
Def2:
:: HEYTING3:def 2
for
x being
set holds
(
x in it iff ( ex
m being
odd Element of
NAT st
(
m <= 2
* n &
[m,k] = x ) or
[(2 * n),k] = x ) );
existence
ex b1 being Element of PFuncs NAT ,{k} st
for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs NAT ,{k} st ( for x being set holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines PFArt HEYTING3:def 2 :
definition
let n,
k be
Element of
NAT ;
func PFCrt n,
k -> Element of
PFuncs NAT ,
{k} means :
Def3:
:: HEYTING3:def 3
for
x being
set holds
(
x in it iff ex
m being
odd Element of
NAT st
(
m <= (2 * n) + 1 &
[m,k] = x ) );
existence
ex b1 being Element of PFuncs NAT ,{k} st
for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs NAT ,{k} st ( for x being set holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in b2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :
theorem :: HEYTING3:17
theorem Th18: :: HEYTING3:18
Lm4:
for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1
theorem Th19: :: HEYTING3:19
Lm5:
for n, n' being Element of NAT holds not PFCrt (n + 1),n' c= PFCrt n,n'
theorem Th20: :: HEYTING3:20
theorem Th21: :: HEYTING3:21
Lm6:
for n, k being Element of NAT holds PFCrt n,k c= PFCrt (n + 1),k
theorem :: HEYTING3:22
Lm7:
for n, m, k being Element of NAT st n < k holds
PFCrt n,m c= PFArt k,m
theorem :: HEYTING3:23
definition
let n,
k be
Element of
NAT ;
func PFBrt n,
k -> Element of
Fin (PFuncs NAT ,{k}) means :
Def4:
:: HEYTING3:def 4
for
x being
set holds
(
x in it iff ( ex
m being non
empty Element of
NAT st
(
m <= n &
x = PFArt m,
k ) or
x = PFCrt n,
k ) );
existence
ex b1 being Element of Fin (PFuncs NAT ,{k}) st
for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) )
uniqueness
for b1, b2 being Element of Fin (PFuncs NAT ,{k}) st ( for x being set holds
( x in b1 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) ) ) & ( for x being set holds
( x in b2 iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :
theorem :: HEYTING3:24
theorem :: HEYTING3:25
Lm8:
for n, k being Element of NAT
for x being set st x in PFBrt n,k holds
x is finite
theorem Th26: :: HEYTING3:26
theorem Th27: :: HEYTING3:27
theorem Th28: :: HEYTING3:28
:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :
theorem :: HEYTING3:29
theorem Th30: :: HEYTING3:30
theorem Th31: :: HEYTING3:31
theorem Th32: :: HEYTING3:32
theorem Th33: :: HEYTING3:33
theorem Th34: :: HEYTING3:34
Lm9:
for a being non empty set st a <> {{} } & {} in a holds
ex b being set st
( b in a & b <> {} )
theorem Th35: :: HEYTING3:35
theorem Th36: :: HEYTING3:36
theorem Th37: :: HEYTING3:37
theorem Th38: :: HEYTING3:38
theorem Th39: :: HEYTING3:39
theorem Th40: :: HEYTING3:40
theorem Th41: :: HEYTING3:41
theorem Th42: :: HEYTING3:42
theorem Th43: :: HEYTING3:43
Lm10:
for m being Element of NAT holds not SubstPoset NAT ,{m} is complete