:: KNASTER semantic presentation

theorem Th1: :: KNASTER:1

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one & rng b₁ misses rng b₂ holds
b₁ +* b₂ is one-to-one

proof end;

theorem Th2: :: KNASTER:2

canceled;

theorem Th3: :: KNASTER:3

for b₁, b₂, b₃ being Function st b₁ = b₂ \/ b₃ & dom b₂ misses dom b₃ holds
( b₁ is one-to-one iff ( b₂ is one-to-one & b₃ is one-to-one & rng b₂ misses rng b₃ ) )

proof end;

theorem Th4: :: KNASTER:4

for b₁, b₂ being set
for b₃ being Nat
for b₄ being Function of b₁,b₁ st b₂ is_a_fixpoint_of iter b₄,b₃ holds
b₄ . b₂ is_a_fixpoint_of iter b₄,b₃

proof end;

theorem Th5: :: KNASTER:5

for b₁, b₂ being set
for b₃ being Function of b₁,b₁ st ex b₄ being Nat st
( b₂ is_a_fixpoint_of iter b₃,b₄ & ( for b₅ being set st b₅ is_a_fixpoint_of iter b₃,b₄ holds
b₂ = b₅ ) ) holds
b₂ is_a_fixpoint_of b₃

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
canceled;
canceled;
redefine attr c=-monotone as a₃ is c=-monotone means :Def3: :: KNASTER:def 3
for b₁, b₂ being Element of a₁ st b₁ c= b₂ holds
a₃ . b₁ c= a₃ . b₂;
compatibility

proof end;

end;

:: deftheorem Def1 KNASTER:def 1 :

:: deftheorem Def2 KNASTER:def 2 :

:: deftheorem Def3 defines c=-monotone KNASTER:def 3 :

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster c=-monotone Relation of a₁,a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be V71 Function of bool c₁, bool c₁;
func lfp c₁,c₂ -> Subset of a₁ equals :: KNASTER:def 4
meet { b₁ where B is Subset of a₁ : a₂ . b₁ c= b₁ } ;
coherence

proof end;

func gfp c₁,c₂ -> Subset of a₁ equals :: KNASTER:def 5
union { b₁ where B is Subset of a₁ : b₁ c= a₂ . b₁ } ;
coherence

proof end;

end;

:: deftheorem Def4 defines lfp KNASTER:def 4 :

:: deftheorem Def5 defines gfp KNASTER:def 5 :

theorem Th6: :: KNASTER:6

for b₁ being set
for b₂ being V71 Function of bool b₁, bool b₁ holds lfp b₁,b₂ is_a_fixpoint_of b₂

proof end;

theorem Th7: :: KNASTER:7

for b₁ being set
for b₂ being V71 Function of bool b₁, bool b₁ holds gfp b₁,b₂ is_a_fixpoint_of b₂

proof end;

theorem Th8: :: KNASTER:8

for b₁ being set
for b₂ being V71 Function of bool b₁, bool b₁
for b₃ being Subset of b₁ st b₂ . b₃ c= b₃ holds
lfp b₁,b₂ c= b₃

proof end;

theorem Th9: :: KNASTER:9

for b₁ being set
for b₂ being V71 Function of bool b₁, bool b₁
for b₃ being Subset of b₁ st b₃ c= b₂ . b₃ holds
b₃ c= gfp b₁,b₂

proof end;

theorem Th10: :: KNASTER:10

for b₁ being set
for b₂ being V71 Function of bool b₁, bool b₁
for b₃ being Subset of b₁ st b₃ is_a_fixpoint_of b₂ holds
( lfp b₁,b₂ c= b₃ & b₃ c= gfp b₁,b₂ )

proof end;

scheme :: KNASTER:sch 1
s1{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being set st
( F₂(b₁) = b₁ & b₁ c= F₁() )

provided

E9: for b₁, b₂ being set st b₁ c= b₂ holds
F₂(b₁) c= F₂(b₂) and
E10: F₂(F₁()) c= F₁()

proof end;

theorem Th11: :: KNASTER:11

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ ex b₅, b₆, b₇, b₈ being set st
( b₅ misses b₆ & b₇ misses b₈ & b₅ \/ b₆ = b₁ & b₇ \/ b₈ = b₂ & b₃ .: b₅ = b₇ & b₄ .: b₈ = b₆ )

proof end;

theorem Th12: :: KNASTER:12

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is one-to-one & b₄ is one-to-one holds
ex b₅ being Function of b₁,b₂ st b₅ is bijective

proof end;

theorem Th13: :: KNASTER:13

for b₁, b₂ being non empty set st ex b₃ being Function of b₂,b₁ st b₃ is bijective holds
b₂,b₁ are_equipotent

proof end;

theorem Th14: :: KNASTER:14

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is one-to-one & b₄ is one-to-one holds
b₁,b₂ are_equipotent

proof end;

definition

let c₁ be non empty LattStr ;
let c₂ be UnOp of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Function of the carrier of c₁,the carrier of c₁;
let c₃ be Element of c₁;
let c₄ be Ordinal;
func c₂,c₄ +. c₃ -> set means :Def6: :: KNASTER:def 6
ex b₁ being T-Sequence st
( a₅ = last b₁ & dom b₁ = succ a₄ & b₁ . {} = a₃ & ( for b₂ being Ordinal st succ b₂ in succ a₄ holds
b₁ . (succ b₂) = a₂ . (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₄ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = "\/" (rng (b₁ | b₂)),a₁ ) );
correctness

proof end;

func c₂,c₄ -. c₃ -> set means :Def7: :: KNASTER:def 7
ex b₁ being T-Sequence st
( a₅ = last b₁ & dom b₁ = succ a₄ & b₁ . {} = a₃ & ( for b₂ being Ordinal st succ b₂ in succ a₄ holds
b₁ . (succ b₂) = a₂ . (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₄ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = "/\" (rng (b₁ | b₂)),a₁ ) );
correctness

proof end;

end;

:: deftheorem Def6 defines +. KNASTER:def 6 :

:: deftheorem Def7 defines -. KNASTER:def 7 :

theorem Th15: :: KNASTER:15

canceled;

theorem Th16: :: KNASTER:16

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁ holds b₂,{} +. b₃ = b₃

proof end;

theorem Th17: :: KNASTER:17

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁ holds b₂,{} -. b₃ = b₃

proof end;

theorem Th18: :: KNASTER:18

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁
for b₄ being Ordinal holds b₂,(succ b₄) +. b₃ = b₂ . (b₂,b₄ +. b₃)

proof end;

theorem Th19: :: KNASTER:19

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁
for b₄ being Ordinal holds b₂,(succ b₄) -. b₃ = b₂ . (b₂,b₄ -. b₃)

proof end;

theorem Th20: :: KNASTER:20

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁
for b₄ being Ordinal
for b₅ being T-Sequence st b₄ <> {} & b₄ is_limit_ordinal & dom b₅ = b₄ & ( for b₆ being Ordinal st b₆ in b₄ holds
b₅ . b₆ = b₂,b₆ +. b₃ ) holds
b₂,b₄ +. b₃ = "\/" (rng b₅),b₁

proof end;

theorem Th21: :: KNASTER:21

for b₁ being Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁
for b₃ being Element of b₁
for b₄ being Ordinal
for b₅ being T-Sequence st b₄ <> {} & b₄ is_limit_ordinal & dom b₅ = b₄ & ( for b₆ being Ordinal st b₆ in b₄ holds
b₅ . b₆ = b₂,b₆ -. b₃ ) holds
b₂,b₄ -. b₃ = "/\" (rng b₅),b₁

proof end;

theorem Th22: :: KNASTER:22

for b₁ being Nat
for b₂ being Lattice
for b₃ being Function of the carrier of b₂,the carrier of b₂
for b₄ being Element of b₂ holds (iter b₃,b₁) . b₄ = b₃,b₁ +. b₄

proof end;

theorem Th23: :: KNASTER:23

for b₁ being Nat
for b₂ being Lattice
for b₃ being Function of the carrier of b₂,the carrier of b₂
for b₄ being Element of b₂ holds (iter b₃,b₁) . b₄ = b₃,b₁ -. b₄

proof end;

definition

let c₁ be Lattice;
let c₂ be UnOp of the carrier of c₁;
let c₃ be Element of c₁;
let c₄ be Ordinal;
redefine func +. as c₂,c₄ +. c₃ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be UnOp of the carrier of c₁;
let c₃ be Element of c₁;
let c₄ be Ordinal;
redefine func -. as c₂,c₄ -. c₃ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty LattStr ;
let c₂ be Subset of c₁;
attr a₂ is with_suprema means :Def8: :: KNASTER:def 8
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
ex b₃ being Element of a₁ st
( b₃ in a₂ & b₁ [= b₃ & b₂ [= b₃ & ( for b₄ being Element of a₁ st b₄ in a₂ & b₁ [= b₄ & b₂ [= b₄ holds
b₃ [= b₄ ) );
attr a₂ is with_infima means :Def9: :: KNASTER:def 9
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
ex b₃ being Element of a₁ st
( b₃ in a₂ & b₃ [= b₁ & b₃ [= b₂ & ( for b₄ being Element of a₁ st b₄ in a₂ & b₄ [= b₁ & b₄ [= b₂ holds
b₄ [= b₃ ) );

end;

:: deftheorem Def8 defines with_suprema KNASTER:def 8 :

:: deftheorem Def9 defines with_infima KNASTER:def 9 :

registration

let c₁ be Lattice;
cluster non empty with_suprema with_infima Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be non empty with_suprema with_infima Subset of c₁;
func latt c₂ -> strict Lattice means :Def10: :: KNASTER:def 10
( the carrier of a₃ = a₂ & ( for b₁, b₂ being Element of a₃ ex b₃, b₄ being Element of a₁ st
( b₁ = b₃ & b₂ = b₄ & ( b₁ [= b₂ implies b₃ [= b₄ ) & ( b₃ [= b₄ implies b₁ [= b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines latt KNASTER:def 10 :

registration

cluster complete -> bounded LattStr ;
coherence

proof end;

end;

theorem Th24: :: KNASTER:24

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ ex b₃ being Element of b₁ st b₃ is_a_fixpoint_of b₂

proof end;

theorem Th25: :: KNASTER:25

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ [= b₂ . b₃ holds
for b₄ being Ordinal holds b₃ [= b₂,b₄ +. b₃

proof end;

theorem Th26: :: KNASTER:26

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₂ . b₃ [= b₃ holds
for b₄ being Ordinal holds b₂,b₄ -. b₃ [= b₃

proof end;

theorem Th27: :: KNASTER:27

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ [= b₂ . b₃ holds
for b₄, b₅ being Ordinal st b₄ c= b₅ holds
b₂,b₄ +. b₃ [= b₂,b₅ +. b₃

proof end;

theorem Th28: :: KNASTER:28

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₂ . b₃ [= b₃ holds
for b₄, b₅ being Ordinal st b₄ c= b₅ holds
b₂,b₅ -. b₃ [= b₂,b₄ -. b₃

proof end;

theorem Th29: :: KNASTER:29

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ [= b₂ . b₃ holds
for b₄, b₅ being Ordinal st b₄ c< b₅ & not b₂,b₅ +. b₃ is_a_fixpoint_of b₂ holds
b₂,b₄ +. b₃ <> b₂,b₅ +. b₃

proof end;

theorem Th30: :: KNASTER:30

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₂ . b₃ [= b₃ holds
for b₄, b₅ being Ordinal st b₄ c< b₅ & not b₂,b₅ -. b₃ is_a_fixpoint_of b₂ holds
b₂,b₄ -. b₃ <> b₂,b₅ -. b₃

proof end;

theorem Th31: :: KNASTER:31

for b₁ being Ordinal
for b₂ being complete Lattice
for b₃ being monotone UnOp of b₂
for b₄ being Element of b₂ st b₄ [= b₃ . b₄ & b₃,b₁ +. b₄ is_a_fixpoint_of b₃ holds
for b₅ being Ordinal st b₁ c= b₅ holds
b₃,b₁ +. b₄ = b₃,b₅ +. b₄

proof end;

theorem Th32: :: KNASTER:32

for b₁ being Ordinal
for b₂ being complete Lattice
for b₃ being monotone UnOp of b₂
for b₄ being Element of b₂ st b₃ . b₄ [= b₄ & b₃,b₁ -. b₄ is_a_fixpoint_of b₃ holds
for b₅ being Ordinal st b₁ c= b₅ holds
b₃,b₁ -. b₄ = b₃,b₅ -. b₄

proof end;

Lemma32: for b₁, b₂ being Ordinal holds
( b₁ c< b₂ or b₁ = b₂ or b₂ c< b₁ )

proof end;

theorem Th33: :: KNASTER:33

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ [= b₂ . b₃ holds
ex b₄ being Ordinal st
( Card b₄ <=` Card the carrier of b₁ & b₂,b₄ +. b₃ is_a_fixpoint_of b₂ )

proof end;

theorem Th34: :: KNASTER:34

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₂ . b₃ [= b₃ holds
ex b₄ being Ordinal st
( Card b₄ <=` Card the carrier of b₁ & b₂,b₄ -. b₃ is_a_fixpoint_of b₂ )

proof end;

theorem Th35: :: KNASTER:35

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃, b₄ being Element of b₁ st b₃ is_a_fixpoint_of b₂ & b₄ is_a_fixpoint_of b₂ holds
ex b₅ being Ordinal st
( Card b₅ <=` Card the carrier of b₁ & b₂,b₅ +. (b₃ "\/" b₄) is_a_fixpoint_of b₂ & b₃ [= b₂,b₅ +. (b₃ "\/" b₄) & b₄ [= b₂,b₅ +. (b₃ "\/" b₄) )

proof end;

theorem Th36: :: KNASTER:36

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃, b₄ being Element of b₁ st b₃ is_a_fixpoint_of b₂ & b₄ is_a_fixpoint_of b₂ holds
ex b₅ being Ordinal st
( Card b₅ <=` Card the carrier of b₁ & b₂,b₅ -. (b₃ "/\" b₄) is_a_fixpoint_of b₂ & b₂,b₅ -. (b₃ "/\" b₄) [= b₃ & b₂,b₅ -. (b₃ "/\" b₄) [= b₄ )

proof end;

theorem Th37: :: KNASTER:37

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃, b₄ being Element of b₁ st b₃ [= b₂ . b₃ & b₃ [= b₄ & b₄ is_a_fixpoint_of b₂ holds
for b₅ being Ordinal holds b₂,b₅ +. b₃ [= b₄

proof end;

theorem Th38: :: KNASTER:38

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃, b₄ being Element of b₁ st b₂ . b₃ [= b₃ & b₄ [= b₃ & b₄ is_a_fixpoint_of b₂ holds
for b₅ being Ordinal holds b₄ [= b₂,b₅ -. b₃

proof end;

definition

let c₁ be complete Lattice;
let c₂ be UnOp of c₁;
assume E39: c₂ is monotone ;
func FixPoints c₂ -> strict Lattice means :Def11: :: KNASTER:def 11
ex b₁ being non empty with_suprema with_infima Subset of a₁ st
( b₁ = { b₂ where B is Element of a₁ : b₂ is_a_fixpoint_of a₂ } & a₃ = latt b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def11 defines FixPoints KNASTER:def 11 :

theorem Th39: :: KNASTER:39

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ holds the carrier of (FixPoints b₂) = { b₃ where B is Element of b₁ : b₃ is_a_fixpoint_of b₂ }

proof end;

theorem Th40: :: KNASTER:40

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ holds the carrier of (FixPoints b₂) c= the carrier of b₁

proof end;

theorem Th41: :: KNASTER:41

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ holds
( b₃ in the carrier of (FixPoints b₂) iff b₃ is_a_fixpoint_of b₂ )

proof end;

theorem Th42: :: KNASTER:42

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃, b₄ being Element of (FixPoints b₂)
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
( b₃ [= b₄ iff b₅ [= b₆ )

proof end;

theorem Th43: :: KNASTER:43

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ holds FixPoints b₂ is complete

proof end;

definition

let c₁ be complete Lattice;
let c₂ be monotone UnOp of c₁;
func lfp c₂ -> Element of a₁ equals :: KNASTER:def 12
a₂,(nextcard the carrier of a₁) +. (Bottom a₁);
coherence ;
func gfp c₂ -> Element of a₁ equals :: KNASTER:def 13
a₂,(nextcard the carrier of a₁) -. (Top a₁);
coherence ;

end;

:: deftheorem Def12 defines lfp KNASTER:def 12 :

:: deftheorem Def13 defines gfp KNASTER:def 13 :

theorem Th44: :: KNASTER:44

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ holds
( lfp b₂ is_a_fixpoint_of b₂ & ex b₃ being Ordinal st
( Card b₃ <=` Card the carrier of b₁ & b₂,b₃ +. (Bottom b₁) = lfp b₂ ) )

proof end;

theorem Th45: :: KNASTER:45

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁ holds
( gfp b₂ is_a_fixpoint_of b₂ & ex b₃ being Ordinal st
( Card b₃ <=` Card the carrier of b₁ & b₂,b₃ -. (Top b₁) = gfp b₂ ) )

proof end;

theorem Th46: :: KNASTER:46

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ is_a_fixpoint_of b₂ holds
( lfp b₂ [= b₃ & b₃ [= gfp b₂ )

proof end;

theorem Th47: :: KNASTER:47

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₂ . b₃ [= b₃ holds
lfp b₂ [= b₃

proof end;

theorem Th48: :: KNASTER:48

for b₁ being complete Lattice
for b₂ being monotone UnOp of b₁
for b₃ being Element of b₁ st b₃ [= b₂ . b₃ holds
b₃ [= gfp b₂

proof end;

registration

let c₁ be set ;
cluster BooleLatt a₁ -> complete ;
coherence by LATTICE3:25;

end;

theorem Th49: :: KNASTER:49

for b₁ being non empty set
for b₂ being UnOp of (BooleLatt b₁) holds
( b₂ is monotone iff b₂ is c=-monotone )

proof end;

theorem Th50: :: KNASTER:50

for b₁ being non empty set
for b₂ being monotone UnOp of (BooleLatt b₁) ex b₃ being V71 Function of bool b₁, bool b₁ st lfp b₁,b₃ = lfp b₂

proof end;

theorem Th51: :: KNASTER:51

for b₁ being non empty set
for b₂ being monotone UnOp of (BooleLatt b₁) ex b₃ being V71 Function of bool b₁, bool b₁ st gfp b₁,b₃ = gfp b₂

proof end;