let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st a is_a_fixpoint_of f holds

( lfp f [= a & a [= gfp f )

let f be monotone UnOp of L; :: thesis: for a being Element of L st a is_a_fixpoint_of f holds

( lfp f [= a & a [= gfp f )

let a be Element of L; :: thesis: ( a is_a_fixpoint_of f implies ( lfp f [= a & a [= gfp f ) )

defpred S_{1}[ Ordinal] means (f,$1) +. (Bottom L) [= a;

then A8: f . a = a ;

then A10: S_{1}[ 0 ]
by LATTICES:16;

for O2 being Ordinal holds S_{1}[O2]
from ORDINAL2:sch 1(A10, A9, A1);

hence lfp f [= a ; :: thesis: a [= gfp f

defpred S_{2}[ Ordinal] means a [= (f,$1) -. (Top L);

then A19: S_{2}[ 0 ]
by LATTICES:19;

for O2 being Ordinal holds S_{2}[O2]
from ORDINAL2:sch 1(A19, A11, A12);

hence a [= gfp f ; :: thesis: verum

for a being Element of L st a is_a_fixpoint_of f holds

( lfp f [= a & a [= gfp f )

let f be monotone UnOp of L; :: thesis: for a being Element of L st a is_a_fixpoint_of f holds

( lfp f [= a & a [= gfp f )

let a be Element of L; :: thesis: ( a is_a_fixpoint_of f implies ( lfp f [= a & a [= gfp f ) )

defpred S

A1: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{1}[O2] ) holds

S_{1}[O1]

assume
a is_a_fixpoint_of f
; :: thesis: ( lfp f [= a & a [= gfp f )S

S

deffunc H_{1}( Ordinal) -> Element of L = (f,$1) +. (Bottom L);

let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{1}[O2] ) implies S_{1}[O1] )

assume that

A2: ( O1 <> 0 & O1 is limit_ordinal ) and

A3: for O2 being Ordinal st O2 in O1 holds

S_{1}[O2]
; :: thesis: S_{1}[O1]

consider L1 being Sequence such that

A4: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A5: rng L1 is_less_than a

hence S_{1}[O1]
by A5, LATTICE3:def 21; :: thesis: verum

end;let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S

assume that

A2: ( O1 <> 0 & O1 is limit_ordinal ) and

A3: for O2 being Ordinal st O2 in O1 holds

S

consider L1 being Sequence such that

A4: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H

A5: rng L1 is_less_than a

proof

(f,O1) +. (Bottom L) = "\/" ((rng L1),L)
by A2, A4, Th17;
let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= a )

assume q in rng L1 ; :: thesis: q [= a

then consider C being object such that

A6: C in dom L1 and

A7: q = L1 . C by FUNCT_1:def 3;

reconsider C = C as Ordinal by A6;

(f,C) +. (Bottom L) [= a by A3, A4, A6;

hence q [= a by A4, A6, A7; :: thesis: verum

end;assume q in rng L1 ; :: thesis: q [= a

then consider C being object such that

A6: C in dom L1 and

A7: q = L1 . C by FUNCT_1:def 3;

reconsider C = C as Ordinal by A6;

(f,C) +. (Bottom L) [= a by A3, A4, A6;

hence q [= a by A4, A6, A7; :: thesis: verum

hence S

then A8: f . a = a ;

A9: now :: thesis: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

(f,{}) +. (Bottom L) = Bottom L
by Th13;S

let O1 be Ordinal; :: thesis: ( S_{1}[O1] implies S_{1}[ succ O1] )

assume S_{1}[O1]
; :: thesis: S_{1}[ succ O1]

then f . ((f,O1) +. (Bottom L)) [= f . a by QUANTAL1:def 12;

hence S_{1}[ succ O1]
by A8, Th15; :: thesis: verum

end;assume S

then f . ((f,O1) +. (Bottom L)) [= f . a by QUANTAL1:def 12;

hence S

then A10: S

for O2 being Ordinal holds S

hence lfp f [= a ; :: thesis: a [= gfp f

defpred S

A11: now :: thesis: for O1 being Ordinal st S_{2}[O1] holds

S_{2}[ succ O1]

S

let O1 be Ordinal; :: thesis: ( S_{2}[O1] implies S_{2}[ succ O1] )

assume S_{2}[O1]
; :: thesis: S_{2}[ succ O1]

then f . a [= f . ((f,O1) -. (Top L)) by QUANTAL1:def 12;

hence S_{2}[ succ O1]
by A8, Th16; :: thesis: verum

end;assume S

then f . a [= f . ((f,O1) -. (Top L)) by QUANTAL1:def 12;

hence S

A12: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{2}[O2] ) holds

S_{2}[O1]

(f,{}) -. (Top L) = Top L
by Th14;S

S

deffunc H_{1}( Ordinal) -> Element of L = (f,$1) -. (Top L);

let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{2}[O2] ) implies S_{2}[O1] )

assume that

A13: ( O1 <> 0 & O1 is limit_ordinal ) and

A14: for O2 being Ordinal st O2 in O1 holds

S_{2}[O2]
; :: thesis: S_{2}[O1]

consider L1 being Sequence such that

A15: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A16: a is_less_than rng L1

hence S_{2}[O1]
by A16, LATTICE3:39; :: thesis: verum

end;let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S

assume that

A13: ( O1 <> 0 & O1 is limit_ordinal ) and

A14: for O2 being Ordinal st O2 in O1 holds

S

consider L1 being Sequence such that

A15: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H

A16: a is_less_than rng L1

proof

(f,O1) -. (Top L) = "/\" ((rng L1),L)
by A13, A15, Th18;
let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or a [= q )

assume q in rng L1 ; :: thesis: a [= q

then consider C being object such that

A17: C in dom L1 and

A18: q = L1 . C by FUNCT_1:def 3;

reconsider C = C as Ordinal by A17;

a [= (f,C) -. (Top L) by A14, A15, A17;

hence a [= q by A15, A17, A18; :: thesis: verum

end;assume q in rng L1 ; :: thesis: a [= q

then consider C being object such that

A17: C in dom L1 and

A18: q = L1 . C by FUNCT_1:def 3;

reconsider C = C as Ordinal by A17;

a [= (f,C) -. (Top L) by A14, A15, A17;

hence a [= q by A15, A17, A18; :: thesis: verum

hence S

then A19: S

for O2 being Ordinal holds S

hence a [= gfp f ; :: thesis: verum