:: The Incompleteness of the Lattice of Substitutions
::
:: Copyright (c) 2000-2021 Association of Mizar Users

scheme :: HEYTING3:sch 1
SSubsetUniq{ F1() -> 1-sorted , P1[ object ] } :
for A1, A2 being Subset of F1() st ( for x being object holds
( x in A1 iff P1[x] ) ) & ( for x being object holds
( x in A2 iff P1[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 ;
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) \/
proof end;

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

theorem Th3: :: HEYTING3:3
for k being Element of NAT
for X being non empty finite Subset of ex n being non zero Element of NAT st X c= [:((Seg n) \/ ),{k}:]
proof end;

theorem Th4: :: HEYTING3:4
for m being Element of NAT
for X being non empty finite Subset of holds
not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X
proof end;

theorem :: HEYTING3:5
for m being Element of NAT
for X being finite Subset of 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:6
for L being upper-bounded Lattice holds Top L = Top ()
proof end;

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

theorem :: HEYTING3:8
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 Th9: :: HEYTING3:9
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)
proof end;

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 & C c= C9 & A = B holds
mi A = mi B
proof end;

theorem :: HEYTING3:11
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || 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 ;
coherence
( SubstPoset (V,C) is with_suprema & SubstPoset (V,C) is with_infima )
;
end;

registration
let V, C be set ;
coherence
( SubstPoset (V,C) is reflexive & SubstPoset (V,C) is antisymmetric & 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 & y c= x ) )
proof end;

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

definition
let n, k be Nat;
func PFArt (n,k) -> Element of PFuncs (NAT,{k}) means :Def2: :: HEYTING3:def 2
for x being object 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 object holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
proof end;
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being object 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 object 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
proof end;
end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :
for n, k being Nat
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFArt (n,k) iff for x being object holds
( x in b3 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 Nat;
func PFCrt (n,k) -> Element of PFuncs (NAT,{k}) means :Def3: :: HEYTING3:def 3
for x being object 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 object holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) )
proof end;
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being object holds
( x in b1 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) & ( for x being object holds
( x in b2 iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :
for n, k being Nat
for b3 being Element of PFuncs (NAT,{k}) holds
( b3 = PFCrt (n,k) iff for x being object holds
( x in b3 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: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]}
proof end;

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

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

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

theorem Th17: :: HEYTING3:17
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 Th18: :: HEYTING3:18
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:19
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:20
for n being Element of NAT holds PFArt (1,n) = {[1,n],[2,n]}
proof end;

definition
let n, k be Nat;
func PFBrt (n,k) -> Element of Fin (PFuncs (NAT,{k})) means :Def4: :: HEYTING3:def 4
for x being object holds
( x in it iff ( ex m being non zero 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 object holds
( x in b1 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
proof end;
uniqueness
for b1, b2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being object holds
( x in b1 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being object holds
( x in b2 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :
for n, k being Nat
for b3 being Element of Fin (PFuncs (NAT,{k})) holds
( b3 = PFBrt (n,k) iff for x being object holds
( x in b3 iff ( ex m being non zero Element of NAT st
( m <= n & 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) & y c= x )
proof end;

theorem :: HEYTING3:22
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 Th23: :: HEYTING3:23
for n, m, k being Element of NAT st PFArt (n,m) c= PFArt (k,m) holds
n = k
proof end;

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

theorem Th25: :: HEYTING3:25
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 object holds
( x in it iff ex n being non zero Element of NAT st x = PFBrt (n,k) );
existence
ex b1 being Subset of (SubstPoset (NAT,{k})) st
for x being object holds
( x in b1 iff ex n being non zero Element of NAT st x = PFBrt (n,k) )
proof end;
uniqueness
for b1, b2 being Subset of (SubstPoset (NAT,{k})) st ( for x being object holds
( x in b1 iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) & ( for x being object holds
( x in b2 iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) holds
b1 = b2
proof end;
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 object holds
( x in b2 iff ex n being non zero 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))}
proof end;

theorem Th27: :: HEYTING3:27
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 Th28: :: HEYTING3:28
for n, k being Element of NAT holds {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))
proof end;

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}:]
proof end;

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 & not n is odd )
proof end;

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 & b is_<=_than X holds
a "\/" b is_<=_than X
proof end;

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
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 Th32: :: HEYTING3:32
for n being Element of NAT
for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a =
proof end;

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 & f <> {} )
proof end;

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 <> & a = a9 holds
Involved a9 is non empty finite Subset of NAT
proof end;

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 & 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
proof end;

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

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

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

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

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