:: HEYTING3 semantic presentation

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

for b₁, b₂ being Subset of F₁() st ( for b₃ being set holds
( b₃ in b₁ iff P₁[b₃] ) ) & ( for b₃ being set holds
( b₃ in b₂ iff P₁[b₃] ) ) holds
b₁ = b₂

proof end;

Lemma1: for b₁, b₂ being set holds [:b₁,{b₂}:] is Function

proof end;

registration

let c₁, c₂ be set ;
cluster [:a₁,{a₂}:] -> Function-like ;
coherence by Lemma1;

end;

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

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

1 = 0 + 1
;

then Lemma4: not 1 is even
by Lemma2, SCMFSA9A:1;

theorem Th1: :: HEYTING3:1

for b₁ being odd Nat holds 1 <= b₁

proof end;

theorem Th2: :: HEYTING3:2

canceled;

theorem Th3: :: HEYTING3:3

for b₁ being non empty finite Subset of NAT ex b₂ being Nat st b₁ c= (Seg b₂) \/ {0}

proof end;

theorem Th4: :: HEYTING3:4

for b₁ being finite Subset of NAT holds
not for b₂ being odd Nat holds b₂ in b₁

proof end;

theorem Th5: :: HEYTING3:5

for b₁ being Nat
for b₂ being non empty finite Subset of [:NAT ,{b₁}:] ex b₃ being non empty Nat st b₂ c= [:((Seg b₃) \/ {0}),{b₁}:]

proof end;

theorem Th6: :: HEYTING3:6

for b₁ being Nat
for b₂ being non empty finite Subset of [:NAT ,{b₁}:] holds
not for b₃ being non empty Nat holds [((2 * b₃) + 1),b₁] in b₂

proof end;

theorem Th7: :: HEYTING3:7

for b₁ being Nat
for b₂ being finite Subset of [:NAT ,{b₁}:] ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
not [b₄,b₁] in b₂

proof end;

theorem Th8: :: HEYTING3:8

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

proof end;

theorem Th9: :: HEYTING3:9

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

proof end;

theorem Th10: :: HEYTING3:10

canceled;

theorem Th11: :: HEYTING3:11

for b₁ being set
for b₂ being finite set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) st b₃ = {} & b₄ <> {} holds
b₄ =>> b₃ = {}

proof end;

theorem Th12: :: HEYTING3:12

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
SubstitutionSet b₁,b₃ c= SubstitutionSet b₂,b₄

proof end;

theorem Th13: :: HEYTING3:13

for b₁, b₂, b₃, b₄ being set
for b₅ being Element of Fin (PFuncs b₁,b₃)
for b₆ being Element of Fin (PFuncs b₂,b₄) st b₁ c= b₂ & b₃ c= b₄ & b₅ = b₆ holds
mi b₅ = mi b₆

proof end;

theorem Th14: :: HEYTING3:14

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
the L_join of (SubstLatt b₁,b₃) = the L_join of (SubstLatt b₂,b₄) || the carrier of (SubstLatt b₁,b₃)

proof end;

definition

let c₁, c₂ be set ;
func SubstPoset c₁,c₂ -> RelStr equals :: HEYTING3:def 1
LattPOSet (SubstLatt a₁,a₂);
coherence ;

end;

:: deftheorem Def1 defines SubstPoset HEYTING3:def 1 :

registration

let c₁, c₂ be set ;
cluster SubstPoset a₁,a₂ -> with_suprema with_infima ;
coherence ;

end;

registration

let c₁, c₂ be set ;
cluster SubstPoset a₁,a₂ -> reflexive transitive antisymmetric with_suprema with_infima ;
coherence ;

end;

Lemma11: for b₁, b₂ being set holds SubstitutionSet b₁,b₂ = the carrier of (SubstPoset b₁,b₂)
by SUBSTLAT:def 4;

theorem Th15: :: HEYTING3:15

for b₁, b₂ being set
for b₃, b₄ being Element of (SubstPoset b₁,b₂) holds
( b₃ <= b₄ iff for b₅ being set st b₅ in b₃ holds
ex b₆ being set st
( b₆ in b₄ & b₆ c= b₅ ) )

proof end;

theorem Th16: :: HEYTING3:16

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
SubstPoset b₁,b₃ is full SubRelStr of SubstPoset b₂,b₄

proof end;

definition

let c₁, c₂ be Nat;
func PFArt c₁,c₂ -> Element of PFuncs NAT ,{a₂} means :Def2: :: HEYTING3:def 2
for b₁ being set holds
( b₁ in a₃ iff ( ex b₂ being odd Nat st
( b₂ <= 2 * a₁ & [b₂,a₂] = b₁ ) or [(2 * a₁),a₂] = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :

registration

let c₁, c₂ be Nat;
cluster PFArt a₁,a₂ -> finite ;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
func PFCrt c₁,c₂ -> Element of PFuncs NAT ,{a₂} means :Def3: :: HEYTING3:def 3
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being odd Nat st
( b₂ <= (2 * a₁) + 1 & [b₂,a₂] = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :

registration

let c₁, c₂ be Nat;
cluster PFCrt a₁,a₂ -> finite ;
coherence

proof end;

end;

theorem Th17: :: HEYTING3:17

for b₁, b₂ being Nat holds [((2 * b₁) + 1),b₂] in PFCrt b₁,b₂

proof end;

theorem Th18: :: HEYTING3:18

for b₁, b₂ being Nat holds PFCrt b₁,b₂ misses {[((2 * b₁) + 3),b₂]}

proof end;

Lemma17: for b₁ being Nat holds (2 * b₁) + 1 <= (2 * (b₁ + 1)) + 1

proof end;

theorem Th19: :: HEYTING3:19

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

proof end;

Lemma19: for b₁, b₂ being Nat holds not PFCrt (b₁ + 1),b₂ c= PFCrt b₁,b₂

proof end;

theorem Th20: :: HEYTING3:20

for b₁, b₂ being Nat holds PFCrt b₁,b₂ c< PFCrt (b₁ + 1),b₂

proof end;

registration

let c₁, c₂ be Nat;
cluster PFArt a₁,a₂ -> non empty finite ;
coherence

proof end;

end;

theorem Th21: :: HEYTING3:21

for b₁, b₂, b₃ being Nat holds not PFArt b₁,b₂ c= PFCrt b₃,b₂

proof end;

Lemma22: for b₁, b₂ being Nat holds PFCrt b₁,b₂ c= PFCrt (b₁ + 1),b₂

proof end;

theorem Th22: :: HEYTING3:22

for b₁, b₂, b₃ being Nat st b₁ <= b₃ holds
PFCrt b₁,b₂ c= PFCrt b₃,b₂

proof end;

Lemma23: for b₁, b₂, b₃ being Nat st b₁ < b₃ holds
PFCrt b₁,b₂ c= PFArt b₃,b₂

proof end;

theorem Th23: :: HEYTING3:23

for b₁ being Nat holds PFArt 1,b₁ = {[1,b₁],[2,b₁]}

proof end;

definition

let c₁, c₂ be Nat;
func PFBrt c₁,c₂ -> Element of Fin (PFuncs NAT ,{a₂}) means :Def4: :: HEYTING3:def 4
for b₁ being set holds
( b₁ in a₃ iff ( ex b₂ being non empty Nat st
( b₂ <= a₁ & b₁ = PFArt b₂,a₂ ) or b₁ = PFCrt a₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :

theorem Th24: :: HEYTING3:24

for b₁, b₂ being Nat
for b₃ being set st b₃ in PFBrt (b₁ + 1),b₂ holds
ex b₄ being set st
( b₄ in PFBrt b₁,b₂ & b₄ c= b₃ )

proof end;

theorem Th25: :: HEYTING3:25

for b₁, b₂ being Nat holds not PFCrt b₁,b₂ in PFBrt (b₁ + 1),b₂

proof end;

Lemma25: for b₁, b₂ being Nat
for b₃ being set st b₃ in PFBrt b₁,b₂ holds
b₃ is finite

proof end;

theorem Th26: :: HEYTING3:26

for b₁, b₂, b₃ being Nat st PFArt b₁,b₂ c= PFArt b₃,b₂ holds
b₁ = b₃

proof end;

theorem Th27: :: HEYTING3:27

for b₁, b₂, b₃ being Nat holds
( PFCrt b₁,b₂ c= PFArt b₃,b₂ iff b₁ < b₃ )

proof end;

theorem Th28: :: HEYTING3:28

for b₁, b₂ being Nat holds PFBrt b₁,b₂ is Element of (SubstPoset NAT ,{b₂})

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :

theorem Th29: :: HEYTING3:29

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

proof end;

theorem Th30: :: HEYTING3:30

for b₁ being Nat holds PFBrt 1,b₁ <> {{} }

proof end;

registration

let c₁ be Nat;
cluster PFBrt 1,a₁ -> non empty ;
coherence

proof end;

end;

theorem Th31: :: HEYTING3:31

for b₁, b₂ being Nat holds {(PFArt b₁,b₂)} is Element of (SubstPoset NAT ,{b₂})

proof end;

theorem Th32: :: HEYTING3:32

for b₁ being Nat
for b₂, b₃ being set
for b₄ being Element of (SubstPoset b₂,{b₁}) st b₃ in b₄ holds
b₃ is finite Subset of [:b₂,{b₁}:]

proof end;

theorem Th33: :: HEYTING3:33

for b₁ being Nat
for b₂ being Element of (SubstPoset NAT ,{b₁}) st PFDrt b₁ is_>=_than b₂ holds
for b₃ being non empty set st b₃ in b₂ holds
ex b₄ being Nat st
( [b₄,b₁] in b₃ & b₄ is even )

proof end;

theorem Th34: :: HEYTING3:34

for b₁ being Nat
for b₂, b₃ being Element of (SubstPoset NAT ,{b₁})
for b₄ being Subset of (SubstPoset NAT ,{b₁}) st b₂ is_<=_than b₄ & b₃ is_<=_than b₄ holds
b₂ "\/" b₃ is_<=_than b₄

proof end;

registration

let c₁ be Nat;
cluster non empty Element of the carrier of (SubstPoset NAT ,{a₁});
existence

proof end;

end;

Lemma35: for b₁ being non empty set st b₁ <> {{} } & {} in b₁ holds
ex b₂ being set st
( b₂ in b₁ & b₂ <> {} )

proof end;

theorem Th35: :: HEYTING3:35

for b₁ being Nat
for b₂ being Element of (SubstPoset NAT ,{b₁}) st {} in b₂ holds
b₂ = {{} }

proof end;

theorem Th36: :: HEYTING3:36

for b₁ being Nat
for b₂ being non empty Element of (SubstPoset NAT ,{b₁}) st b₂ <> {{} } holds
ex b₃ being finite Function st
( b₃ in b₂ & b₃ <> {} )

proof end;

theorem Th37: :: HEYTING3:37

for b₁ being Nat
for b₂ being non empty Element of (SubstPoset NAT ,{b₁})
for b₃ being Element of Fin (PFuncs NAT ,{b₁}) st b₂ <> {{} } & b₂ = b₃ holds
Involved b₃ is non empty finite Subset of NAT

proof end;

theorem Th38: :: HEYTING3:38

for b₁ being Nat
for b₂ being Element of (SubstPoset NAT ,{b₁})
for b₃ being Element of Fin (PFuncs NAT ,{b₁})
for b₄ being non empty finite Subset of NAT st b₄ = Involved b₃ & b₃ = b₂ holds
for b₅ being set st b₅ in b₂ holds
for b₆ being Nat st b₆ > (max b₄) + 1 holds
not [b₆,b₁] in b₅

proof end;

theorem Th39: :: HEYTING3:39

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

proof end;

theorem Th40: :: HEYTING3:40

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

proof end;

theorem Th41: :: HEYTING3:41

for b₁ being Nat
for b₂, b₃ being Element of (SubstPoset NAT ,{b₁}) st b₂ <= b₃ & b₂ = {{} } holds
b₃ = {{} }

proof end;

theorem Th42: :: HEYTING3:42

for b₁ being Nat
for b₂, b₃ being Element of (SubstPoset NAT ,{b₁}) st b₂ <= b₃ & b₃ = {} holds
b₂ = {}

proof end;

theorem Th43: :: HEYTING3:43

for b₁ being Nat
for b₂ being Element of (SubstPoset NAT ,{b₁}) st PFDrt b₁ is_>=_than b₂ holds
b₂ <> {{} }

proof end;

Lemma45: for b₁ being Nat holds not SubstPoset NAT ,{b₁} is complete

proof end;

registration

let c₁ be Nat;
cluster SubstPoset NAT ,{a₁} -> reflexive transitive antisymmetric with_suprema with_infima non complete ;
coherence by Lemma45;

end;

registration

let c₁ be Nat;
cluster SubstLatt NAT ,{a₁} -> non complete ;
coherence

proof end;

end;