:: HEYTING3 semantic presentation

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

end;

Lm2: ( 0 = 2 * 0 & 2 = 2 * 1 )
;

then Lm3: ( 0 is even & 2 is even )
by ABIAN:def 2;

1 = 0 + 1
;

then Lm4: not 1 is even
by Lm2, SCMFSA9A:1;

theorem Th1: :: HEYTING3:1

for n being odd Nat 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 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 Nat holds k in X

proof end;

theorem Th5: :: HEYTING3:5

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

proof end;

theorem Th6: :: HEYTING3:6

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

proof end;

theorem :: HEYTING3:7

for m being Nat
for X being finite Subset of [:NAT ,{m}:] ex k being Nat st
for l being 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 ;

end;

:: deftheorem defines SubstPoset HEYTING3:def 1 :

registration

let V, C be set ;
cluster SubstPoset V,C -> with_suprema with_infima ;
coherence ;

end;

registration

let V, C be set ;
cluster SubstPoset V,C -> reflexive transitive antisymmetric with_suprema with_infima ;
coherence ;

end;

Lm5: for V, C being set holds SubstitutionSet V,C = the carrier of (SubstPoset V,C)
by SUBSTLAT:def 4;

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 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 Nat st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :

registration

let n, k be Nat;
cluster PFArt n,k -> finite ;
coherence

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 set holds
( x in it iff ex m being odd Nat st
( m <= (2 * n) + 1 & [m,k] = x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :

registration

let n, k be Nat;
cluster PFCrt n,k -> finite ;
coherence

proof end;

end;

theorem Th17: :: HEYTING3:17

for n, k being Nat holds [((2 * n) + 1),k] in PFCrt n,k

proof end;

theorem Th18: :: HEYTING3:18

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

proof end;

Lm6: for n being Nat holds (2 * n) + 1 <= (2 * (n + 1)) + 1

proof end;

theorem Th19: :: HEYTING3:19

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

proof end;

Lm7: for n, n' being Nat holds not PFCrt (n + 1),n' c= PFCrt n,n'

proof end;

theorem Th20: :: HEYTING3:20

for n, k being Nat holds PFCrt n,k c< PFCrt (n + 1),k

proof end;

registration

let n, k be Nat;
cluster PFArt n,k -> non empty finite ;
coherence

proof end;

end;

theorem Th21: :: HEYTING3:21

for n, m, k being Nat holds not PFArt n,m c= PFCrt k,m

proof end;

Lm8: for n, k being Nat holds PFCrt n,k c= PFCrt (n + 1),k

proof end;

theorem :: HEYTING3:22

for n, m, k being Nat st n <= k holds
PFCrt n,m c= PFCrt k,m

proof end;

Lm9: for n, m, k being Nat st n < k holds
PFCrt n,m c= PFArt k,m

proof end;

theorem :: HEYTING3:23

for n being 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 set holds
( x in it iff ( ex m being non empty Nat st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :

theorem :: HEYTING3:24

for n, k being 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 Nat holds not PFCrt n,k in PFBrt (n + 1),k

proof end;

Lm10: for n, k being 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 Nat st PFArt n,m c= PFArt k,m holds
n = k

proof end;

theorem Th27: :: HEYTING3:27

for n, m, k being Nat holds
( PFCrt n,m c= PFArt k,m iff n < k )

proof end;

theorem Th28: :: HEYTING3:28

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

proof end;

definition

let k be 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 Nat st x = PFBrt n,k );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :

theorem :: HEYTING3:29

for k being Nat holds PFBrt 1,k = {(PFArt 1,k),(PFCrt 1,k)}

proof end;

theorem Th30: :: HEYTING3:30

for k being Nat holds PFBrt 1,k <> {{} }

proof end;

registration

let k be Nat;
cluster PFBrt 1,k -> non empty ;
coherence

proof end;

end;

theorem Th31: :: HEYTING3:31

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

proof end;

theorem Th32: :: HEYTING3:32

for k being 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 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 Nat st
( [n,m] in X & n is even )

proof end;

theorem Th34: :: HEYTING3:34

for k being 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 Nat;
cluster non empty Element of the carrier of (SubstPoset NAT ,{k});
existence

proof end;

end;

Lm11: 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 Nat
for a being Element of (SubstPoset NAT ,{n}) st {} in a holds
a = {{} }

proof end;

theorem Th36: :: HEYTING3:36

for k being 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 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 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 Nat st l > (max B) + 1 holds
not [l,k] in X

proof end;

theorem Th39: :: HEYTING3:39

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

proof end;

theorem Th40: :: HEYTING3:40

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

proof end;

theorem Th41: :: HEYTING3:41

for k being 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 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 Nat
for a being Element of (SubstPoset NAT ,{m}) st PFDrt m is_>=_than a holds
a <> {{} }

proof end;

Lm12: for m being Nat holds not SubstPoset NAT ,{m} is complete

proof end;

registration

let m be Nat;
cluster SubstPoset NAT ,{m} -> reflexive transitive antisymmetric with_suprema with_infima non complete ;
coherence by Lm12;

end;

registration

let m be Nat;
cluster SubstLatt NAT ,{m} -> non complete ;
coherence

proof end;

end;