:: The Incompleteness of the Lattice of SubstitutionsPRE_CIRC,
:: by Adam Grabowski
::
:: Received July 17, 2000
:: Copyright (c) 2000 Association of Mizar Users

registration

cluster natural odd set ;
existence
ex b₁ being number st
( not b₁ is even & b₁ is natural )

proof end;

cluster natural even set ;
existence
ex b₁ being number st
( b₁ is even & b₁ is natural )

proof end;

end;

scheme :: HEYTING3:sch 1
SSubsetUniq{ F₁() -> RelStr , P₁[ set ] } :

for A1, A2 being Subset of F₁() st ( for x being set holds
( x in A1 iff P₁[x] ) ) & ( for x being set holds
( x in A2 iff P₁[x] ) ) holds
A1 = A2

proof end;

Lm1: for A, x being set holds [:A,{x}:] is Function

proof end;

registration

let A, x be set ;
cluster [:A,{x}:] -> Function-like ;
coherence
[:A,{x}:] is Function-like by Lm1;

end;

Lm2: 0 = 2 * 0
;

Lm3: 1 = 0 + 1
;

theorem Th1: :: HEYTING3:1

for n being natural odd number holds 1 <= n

proof end;

theorem :: HEYTING3:2

canceled;

theorem Th3: :: HEYTING3:3

for X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0 }

proof end;

theorem :: HEYTING3:4

for X being finite Subset of NAT holds
not for k being odd Element of NAT holds k in X

proof end;

theorem Th5: :: HEYTING3:5

for k being Element of NAT
for X being non empty finite Subset of [:NAT ,{k}:] ex n being non empty Element of NAT st X c= [:((Seg n) \/ {0 }),{k}:]

proof end;

theorem Th6: :: HEYTING3:6

for m being Element of NAT
for X being non empty finite Subset of [:NAT ,{m}:] holds
not for k being non empty Element of NAT holds [((2 * k) + 1),m] in X

proof end;

theorem :: HEYTING3:7

for m being Element of NAT
for X being finite Subset of [:NAT ,{m}:] ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X

proof end;

theorem :: HEYTING3:8

for L being upper-bounded Lattice holds Top L = Top (LattPOSet L)

proof end;

theorem :: HEYTING3:9

for L being lower-bounded Lattice holds Bottom L = Bottom (LattPOSet L)

proof end;

theorem :: HEYTING3:10

canceled;

theorem :: HEYTING3:11

for V being set
for C being finite set
for A, B being Element of Fin (PFuncs V,C) st A = {} & B <> {} holds
B =>> A = {}

proof end;

theorem Th12: :: HEYTING3:12

for V, V', C, C' being set st V c= V' & C c= C' holds
SubstitutionSet V,C c= SubstitutionSet V',C'

proof end;

theorem Th13: :: HEYTING3:13

for V, V', C, C' being set
for A being Element of Fin (PFuncs V,C)
for B being Element of Fin (PFuncs V',C') st V c= V' & C c= C' & A = B holds
mi A = mi B

proof end;

theorem :: HEYTING3:14

for V, V', C, C' being set st V c= V' & C c= C' holds
the L_join of (SubstLatt V,C) = the L_join of (SubstLatt V',C') || the carrier of (SubstLatt V,C)

proof end;

definition

let V, C be set ;
func SubstPoset V,C -> RelStr equals :: HEYTING3:def 1
LattPOSet (SubstLatt V,C);
coherence
LattPOSet (SubstLatt V,C) is RelStr ;

end;

:: deftheorem defines SubstPoset HEYTING3:def 1 :

for V, C being set holds SubstPoset V,C = LattPOSet (SubstLatt V,C);

registration

let V, C be set ;
cluster SubstPoset V,C -> with_suprema with_infima ;
coherence
( SubstPoset V,C is with_suprema & SubstPoset V,C is with_infima ) ;

end;

registration

let V, C be set ;
cluster SubstPoset V,C -> reflexive transitive antisymmetric ;
coherence
( SubstPoset V,C is reflexive & SubstPoset V,C is antisymmetric & SubstPoset V,C is transitive ) ;

end;

theorem Th15: :: HEYTING3:15

for V, C being set
for a, b being Element of (SubstPoset V,C) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )

proof end;

theorem :: HEYTING3:16

for V, V', C, C' being set st V c= V' & C c= C' holds
SubstPoset V,C is full SubRelStr of SubstPoset V',C'

proof end;

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 b₁ being Element of PFuncs NAT ,{k} st
for x being set holds
( x in b₁ iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )

proof end;

uniqueness
for b₁, b₂ being Element of PFuncs NAT ,{k} st ( for x being set holds
( x in b₁ 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 b₂ iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :

for n, k being Element of NAT
for b₃ being Element of PFuncs NAT ,{k} holds
( b₃ = PFArt n,k iff for x being set holds
( x in b₃ iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );

registration

let n, k be Element of NAT ;
cluster PFArt n,k -> finite ;
coherence
PFArt n,k is finite

proof end;

end;

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 b₁ being Element of PFuncs NAT ,{k} st
for x being set holds
( x in b₁ iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )

proof end;

uniqueness
for b₁, b₂ being Element of PFuncs NAT ,{k} st ( for x being set holds
( x in b₁ iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being set holds
( x in b₂ iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :

for n, k being Element of NAT
for b₃ being Element of PFuncs NAT ,{k} holds
( b₃ = PFCrt n,k iff for x being set holds
( x in b₃ iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) );

registration

let n, k be Element of NAT ;
cluster PFCrt n,k -> finite ;
coherence
PFCrt n,k is finite

proof end;

end;

theorem :: HEYTING3:17

for n, k being Element of NAT holds [((2 * n) + 1),k] in PFCrt n,k by Def3;

theorem Th18: :: HEYTING3:18

for n, k being Element of NAT holds PFCrt n,k misses {[((2 * n) + 3),k]}

proof end;

Lm4: for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1

proof end;

theorem Th19: :: HEYTING3:19

for n, k being Element of NAT holds PFCrt (n + 1),k = (PFCrt n,k) \/ {[((2 * n) + 3),k]}

proof end;

Lm5: for n, n' being Element of NAT holds not PFCrt (n + 1),n' c= PFCrt n,n'

proof end;

theorem Th20: :: HEYTING3:20

for n, k being Element of NAT holds PFCrt n,k c< PFCrt (n + 1),k

proof end;

registration

let n, k be Element of NAT ;
cluster PFArt n,k -> non empty ;
coherence
not PFArt n,k is empty

proof end;

end;

theorem Th21: :: HEYTING3:21

for n, m, k being Element of NAT holds not PFArt n,m c= PFCrt k,m

proof end;

Lm6: for n, k being Element of NAT holds PFCrt n,k c= PFCrt (n + 1),k

proof end;

theorem :: HEYTING3:22

for n, m, k being Element of NAT st n <= k holds
PFCrt n,m c= PFCrt k,m

proof end;

Lm7: for n, m, k being Element of NAT st n < k holds
PFCrt n,m c= PFArt k,m

proof end;

theorem :: HEYTING3:23

for n being Element of NAT holds PFArt 1,n = {[1,n],[2,n]}

proof end;

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 b₁ being Element of Fin (PFuncs NAT ,{k}) st
for x being set holds
( x in b₁ iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) )

proof end;

uniqueness
for b₁, b₂ being Element of Fin (PFuncs NAT ,{k}) st ( for x being set holds
( x in b₁ 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 b₂ iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :

for n, k being Element of NAT
for b₃ being Element of Fin (PFuncs NAT ,{k}) holds
( b₃ = PFBrt n,k iff for x being set holds
( x in b₃ iff ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) ) );

theorem :: HEYTING3:24

for n, k being Element of NAT
for x being set st x in PFBrt (n + 1),k holds
ex y being set st
( y in PFBrt n,k & y c= x )

proof end;

theorem :: HEYTING3:25

for n, k being Element of NAT holds not PFCrt n,k in PFBrt (n + 1),k

proof end;

Lm8: for n, k being Element of NAT
for x being set st x in PFBrt n,k holds
x is finite

proof end;

theorem Th26: :: HEYTING3:26

for n, m, k being Element of NAT st PFArt n,m c= PFArt k,m holds
n = k

proof end;

theorem Th27: :: HEYTING3:27

for n, m, k being Element of NAT holds
( PFCrt n,m c= PFArt k,m iff n < k )

proof end;

theorem Th28: :: HEYTING3:28

for n, k being Element of NAT holds PFBrt n,k is Element of (SubstPoset NAT ,{k})

proof end;

definition

let k be Element of NAT ;
func PFDrt k -> Subset of (SubstPoset NAT ,{k}) means :Def5: :: HEYTING3:def 5
for x being set holds
( x in it iff ex n being non empty Element of NAT st x = PFBrt n,k );
existence
ex b₁ being Subset of (SubstPoset NAT ,{k}) st
for x being set holds
( x in b₁ iff ex n being non empty Element of NAT st x = PFBrt n,k )

proof end;

uniqueness
for b₁, b₂ being Subset of (SubstPoset NAT ,{k}) st ( for x being set holds
( x in b₁ iff ex n being non empty Element of NAT st x = PFBrt n,k ) ) & ( for x being set holds
( x in b₂ iff ex n being non empty Element of NAT st x = PFBrt n,k ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :

for k being Element of NAT
for b₂ being Subset of (SubstPoset NAT ,{k}) holds
( b₂ = PFDrt k iff for x being set holds
( x in b₂ iff ex n being non empty Element of NAT st x = PFBrt n,k ) );

theorem :: HEYTING3:29

for k being Element of NAT holds PFBrt 1,k = {(PFArt 1,k),(PFCrt 1,k)}

proof end;

theorem Th30: :: HEYTING3:30

for k being Element of NAT holds PFBrt 1,k <> {{} }

proof end;

registration

let k be Element of NAT ;
cluster PFBrt 1,k -> non empty ;
coherence
not PFBrt 1,k is empty

proof end;

end;

theorem Th31: :: HEYTING3:31

for n, k being Element of NAT holds {(PFArt n,k)} is Element of (SubstPoset NAT ,{k})

proof end;

theorem Th32: :: HEYTING3:32

for k being Element of NAT
for V, X being set
for a being Element of (SubstPoset V,{k}) st X in a holds
X is finite Subset of [:V,{k}:]

proof end;

theorem Th33: :: HEYTING3:33

for m being Element of NAT
for a being Element of (SubstPoset NAT ,{m}) st PFDrt m is_>=_than a holds
for X being non empty set st X in a holds
ex n being Element of NAT st
( [n,m] in X & n is even )

proof end;

theorem Th34: :: HEYTING3:34

for k being Element of NAT
for a, b being Element of (SubstPoset NAT ,{k})
for X being Subset of (SubstPoset NAT ,{k}) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X

proof end;

registration

let k be Element of NAT ;
cluster non empty Element of the carrier of (SubstPoset NAT ,{k});
existence
not for b₁ being Element of (SubstPoset NAT ,{k}) holds b₁ is empty

proof end;

end;

Lm9: for a being non empty set st a <> {{} } & {} in a holds
ex b being set st
( b in a & b <> {} )

proof end;

theorem Th35: :: HEYTING3:35

for n being Element of NAT
for a being Element of (SubstPoset NAT ,{n}) st {} in a holds
a = {{} }

proof end;

theorem Th36: :: HEYTING3:36

for k being Element of NAT
for a being non empty Element of (SubstPoset NAT ,{k}) st a <> {{} } holds
ex f being finite Function st
( f in a & f <> {} )

proof end;

theorem Th37: :: HEYTING3:37

for k being Element of NAT
for a being non empty Element of (SubstPoset NAT ,{k})
for a' being Element of Fin (PFuncs NAT ,{k}) st a <> {{} } & a = a' holds
Involved a' is non empty finite Subset of NAT

proof end;

theorem Th38: :: HEYTING3:38

for k being Element of NAT
for a being Element of (SubstPoset NAT ,{k})
for a' being Element of Fin (PFuncs NAT ,{k})
for B being non empty finite Subset of NAT st B = Involved a' & a' = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X

proof end;

theorem Th39: :: HEYTING3:39

for k being Element of NAT holds Top (SubstPoset NAT ,{k}) = {{} }

proof end;

theorem Th40: :: HEYTING3:40

for k being Element of NAT holds Bottom (SubstPoset NAT ,{k}) = {}

proof end;

theorem Th41: :: HEYTING3:41

for k being Element of NAT
for a, b being Element of (SubstPoset NAT ,{k}) st a <= b & a = {{} } holds
b = {{} }

proof end;

theorem Th42: :: HEYTING3:42

for k being Element of NAT
for a, b being Element of (SubstPoset NAT ,{k}) st a <= b & b = {} holds
a = {}

proof end;

theorem Th43: :: HEYTING3:43

for m being Element of NAT
for a being Element of (SubstPoset NAT ,{m}) st PFDrt m is_>=_than a holds
a <> {{} }

proof end;

Lm10: for m being Element of NAT holds not SubstPoset NAT ,{m} is complete

proof end;

registration

let m be Element of NAT ;
cluster SubstPoset NAT ,{m} -> non complete ;
coherence
not SubstPoset NAT ,{m} is complete by Lm10;

end;

registration

let m be Element of NAT ;
cluster SubstLatt NAT ,{m} -> non complete ;
coherence
not SubstLatt NAT ,{m} is complete

proof end;

end;