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


begin

scheme :: HEYTING3:sch 1
SSubsetUniq{ F1() ->  1-sorted , P1[ set ] } :
 for A1, A2 being Subset of F1() st ( for x being set holds
( x in A1 iff P1[x] ) ) & ( for x being set holds
( x in A2 iff P1[x] ) ) holds
A1 = A2
proofend;

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

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 X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0}
proofend;

theorem :: HEYTING3:2
for X being finite Subset of NAT holds
not for k being odd Element of NAT holds k in X
proofend;

theorem Th3: :: HEYTING3:3
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}:]
proofend;

theorem Th4: :: HEYTING3:4
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
proofend;

theorem :: HEYTING3:5
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
proofend;

theorem :: HEYTING3:6
for L being upper-bounded Lattice holds Top L = Top (LattPOSet L)
proofend;

theorem :: HEYTING3:7
for L being lower-bounded Lattice holds Bottom L = Bottom (LattPOSet L)
proofend;

begin

theorem :: HEYTING3:8
for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) st A = {} &amp; B <> {} holds
B =>> A = {}
proofend;

theorem Th9: :: HEYTING3:9
for V, V9, C, C9 being set st V c= V9 &amp; C c= C9 holds
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
proofend;

theorem Th10: :: HEYTING3:10
for V, V9, C, C9 being set
for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 &amp; C c= C9 &amp; A = B holds
mi A = mi B
proofend;

theorem :: HEYTING3:11
for V, V9, C, C9 being set st V c= V9 &amp; C c= C9 holds
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))
proofend;

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 &amp; 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 &amp; SubstPoset (V,C) is antisymmetric &amp; SubstPoset (V,C) is transitive ) ;
end;

theorem Th12: :: HEYTING3:12
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 &amp; y c= x ) )
proofend;

theorem :: HEYTING3:13
for V, V9, C, C9 being set st V c= V9 &amp; C c= C9 holds
SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)
proofend;

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 &amp; [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 &amp; [m,k] = x ) or [(2 * n),k] = x ) )
proofend;
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 &amp; [m,k] = x ) or [(2 * n),k] = x ) ) ) &amp; ( for x being set holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n &amp; [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines PFArt HEYTING3:def_2_:_
 for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFArt (n,k) iff for x being set holds
( x in b3 iff ( ex m being odd Element of NAT st
( m <= 2 * n &amp; [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
proofend;
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 &amp; [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 &amp; [m,k] = x ) )
proofend;
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 &amp; [m,k] = x ) ) ) &amp; ( for x being set holds
( x in b2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 &amp; [m,k] = x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines PFCrt HEYTING3:def_3_:_
 for n, k being Element of NAT
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFCrt (n,k) iff for x being set holds
( x in b3 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 &amp; [m,k] = x ) ) );

registration
let n, k be Element of NAT ;
cluster PFCrt (n,k) ->  finite ;
coherence
 PFCrt (n,k) is finite
proofend;
end;

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

theorem Th15: :: HEYTING3:15
for n, k being Element of NAT holds PFCrt (n,k) misses {[((2 * n) + 3),k]}
proofend;

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

theorem Th16: :: HEYTING3:16
for n, k being Element of NAT holds PFCrt ((n + 1),k) = (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}
proofend;

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

theorem Th17: :: HEYTING3:17
for n, k being Element of NAT holds PFCrt (n,k) c< PFCrt ((n + 1),k)
proofend;

registration
let n, k be Element of NAT ;
cluster PFArt (n,k) ->  non empty ;
coherence
 not PFArt (n,k) is empty
proofend;
end;

theorem Th18: :: HEYTING3:18
for n, m, k being Element of NAT holds not PFArt (n,m) c= PFCrt (k,m)
proofend;

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

theorem :: HEYTING3:19
for n, m, k being Element of NAT st n <= k holds
PFCrt (n,m) c= PFCrt (k,m)
proofend;

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

theorem :: HEYTING3:20
for n being Element of NAT holds PFArt (1,n) = {[1,n],[2,n]}
proofend;

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 &amp; 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 &amp; x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
proofend;
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 &amp; x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( ex m being non empty Element of NAT st
( m <= n &amp; x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines PFBrt HEYTING3:def_4_:_
 for n, k being Element of NAT
for b3 being Element of Fin (PFuncs (NAT,{k})) holds
( b3 = PFBrt (n,k) iff for x being set holds
( x in b3 iff ( ex m being non empty Element of NAT st
( m <= n &amp; x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );

theorem :: HEYTING3:21
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) &amp; y c= x )
proofend;

theorem :: HEYTING3:22
for n, k being Element of NAT holds not PFCrt (n,k) in PFBrt ((n + 1),k)
proofend;

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

theorem Th23: :: HEYTING3:23
for n, m, k being Element of NAT st PFArt (n,m) c= PFArt (k,m) holds
n = k
proofend;

theorem Th24: :: HEYTING3:24
for n, m, k being Element of NAT holds
( PFCrt (n,m) c= PFArt (k,m) iff n < k )
proofend;

begin

theorem Th25: :: HEYTING3:25
for n, k being Element of NAT holds PFBrt (n,k) is Element of (SubstPoset (NAT,{k}))
proofend;

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 b1 being Subset of (SubstPoset (NAT,{k})) st
for x being set holds
( x in b1 iff ex n being non empty Element of NAT st x = PFBrt (n,k) )
proofend;
uniqueness
 for b1, b2 being Subset of (SubstPoset (NAT,{k})) st ( for x being set holds
( x in b1 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) &amp; ( for x being set holds
( x in b2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines PFDrt HEYTING3:def_5_:_
 for k being Element of NAT
for b2 being Subset of (SubstPoset (NAT,{k})) holds
( b2 = PFDrt k iff for x being set holds
( x in b2 iff ex n being non empty Element of NAT st x = PFBrt (n,k) ) );

theorem :: HEYTING3:26
for k being Element of NAT holds PFBrt (1,k) = {(PFArt (1,k)),(PFCrt (1,k))}
proofend;

theorem Th27: :: HEYTING3:27
for k being Element of NAT holds PFBrt (1,k) <> {{}}
proofend;

registration
let k be Element of NAT ;
cluster PFBrt (1,k) ->  non empty ;
coherence
 not PFBrt (1,k) is empty
proofend;
end;

theorem Th28: :: HEYTING3:28
for n, k being Element of NAT holds {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))
proofend;

theorem Th29: :: HEYTING3:29
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}:]
proofend;

theorem Th30: :: HEYTING3:30
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 &amp; not n is odd )
proofend;

theorem Th31: :: HEYTING3:31
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 &amp; b is_<=_than X holds
a "\/" b is_<=_than X
proofend;

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

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

theorem Th32: :: HEYTING3:32
for n being Element of NAT
for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}
proofend;

theorem Th33: :: HEYTING3:33
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 &amp; f <> {} )
proofend;

theorem Th34: :: HEYTING3:34
for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} &amp; a = a9 holds
Involved a9 is non empty finite Subset of NAT
proofend;

theorem Th35: :: HEYTING3:35
for k being Element of NAT
for a being Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 &amp; a9 = 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
proofend;

theorem Th36: :: HEYTING3:36
for k being Element of NAT holds Top (SubstPoset (NAT,{k})) = {{}}
proofend;

theorem Th37: :: HEYTING3:37
for k being Element of NAT holds Bottom (SubstPoset (NAT,{k})) = {}
proofend;

theorem Th38: :: HEYTING3:38
for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b &amp; a = {{}} holds
b = {{}}
proofend;

theorem Th39: :: HEYTING3:39
for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b &amp; b = {} holds
a = {}
proofend;

theorem Th40: :: HEYTING3:40
for m being Element of NAT
for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
a <> {{}}
proofend;

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

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
proofend;
end;