:: by Kazuhisa Ishida , Yasunari Shidama and Adam Grabowski

::

:: Received February 11, 2014

:: Copyright (c) 2014-2019 Association of Mizar Users

LemSUM01: for a, Z1, Z2, Z3 being set holds

( a in (Z1 \/ Z2) \/ Z3 iff ( a in Z1 or a in Z2 or a in Z3 ) )

proof end;

LemMin01: for S being non empty RelStr

for a being Element of S holds

( a is_<=_than the carrier of S iff for x being Element of S holds a <= x )

;

theorem ThMin02: :: POSET_2:1

for P being non empty lower-bounded Poset

for p being Element of P st p is_<=_than the carrier of P holds

p = Bottom P

for p being Element of P st p is_<=_than the carrier of P holds

p = Bottom P

proof end;

theorem Thsup01: :: POSET_2:2

for P being non empty chain-complete Poset

for L being non empty Chain of P

for p being Element of P st p in L holds

p <= sup L

for L being non empty Chain of P

for p being Element of P st p in L holds

p <= sup L

proof end;

theorem Thsup02: :: POSET_2:3

for P being non empty chain-complete Poset

for L being non empty Chain of P

for p1 being Element of P st ( for p being Element of P st p in L holds

p <= p1 ) holds

sup L <= p1

for L being non empty Chain of P

for p1 being Element of P st ( for p being Element of P st p in L holds

p <= p1 ) holds

sup L <= p1

proof end;

theorem ThProdPoset01: :: POSET_2:4

for P, Q being non empty RelStr

for x being object holds

( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] )

for x being object holds

( x is Element of [:P,Q:] iff ex p being Element of P ex q being Element of Q st x = [p,q] )

proof end;

definition

let P, Q be non empty Poset;

let L be non empty Chain of [:P,Q:];

:: original: dom

redefine func proj1 L -> non empty Chain of P;

correctness

coherence

dom L is non empty Chain of P;

redefine func proj2 L -> non empty Chain of Q;

correctness

coherence

rng L is non empty Chain of Q;

end;
let L be non empty Chain of [:P,Q:];

:: original: dom

redefine func proj1 L -> non empty Chain of P;

correctness

coherence

dom L is non empty Chain of P;

proof end;

:: original: rngredefine func proj2 L -> non empty Chain of Q;

correctness

coherence

rng L is non empty Chain of Q;

proof end;

:: Product of Function

registration

let P, Q1, Q2 be non empty Poset;

let f1 be monotone Function of P,Q1;

let f2 be monotone Function of P,Q2;

correctness

coherence

for b_{1} being Function of P,[:Q1,Q2:] st b_{1} = <:f1,f2:> holds

b_{1} is monotone ;

end;
let f1 be monotone Function of P,Q1;

let f2 be monotone Function of P,Q2;

correctness

coherence

for b

b

proof end;

LemProdPoset06: for P, Q being non empty chain-complete Poset

for L being Chain of [:P,Q:] st not L is empty holds

ex_sup_of L,[:P,Q:]

proof end;

registration

let P, Q be non empty chain-complete Poset;

correctness

coherence

[:P,Q:] is chain-complete ;

by LemProdPoset06;

end;
correctness

coherence

[:P,Q:] is chain-complete ;

by LemProdPoset06;

theorem :: POSET_2:5

registration

let P, Q1, Q2 be non empty strict chain-complete Poset;

let f1 be continuous Function of P,Q1;

let f2 be continuous Function of P,Q2;

correctness

coherence

for b_{1} being Function of P,[:Q1,Q2:] st b_{1} = <:f1,f2:> holds

b_{1} is continuous ;

end;
let f1 be continuous Function of P,Q1;

let f2 be continuous Function of P,Q2;

correctness

coherence

for b

b

proof end;

:: deftheorem Defflat defines flat POSET_2:def 1 :

for IT being RelStr holds

( IT is flat iff ex a being Element of IT st

for x, y being Element of IT holds

( x <= y iff ( x = a or x = y ) ) );

for IT being RelStr holds

( IT is flat iff ex a being Element of IT st

for x, y being Element of IT holds

( x <= y iff ( x = a or x = y ) ) );

registration

coherence

for b_{1} being non empty RelStr st b_{1} is discrete holds

b_{1} is reflexive
by ORDERS_3:1;

end;
for b

b

registration

coherence

for b_{1} being non empty discrete RelStr st b_{1} is trivial holds

b_{1} is flat

end;
for b

b

proof end;

registration

existence

ex b_{1} being Poset st

( b_{1} is strict & not b_{1} is empty & b_{1} is flat )

end;
ex b

( b

proof end;

registration

correctness

coherence

for b_{1} being RelStr st b_{1} is flat holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric );

end;
coherence

for b

( b

proof end;

registration
end;

Lemflat01: for P being non empty flat Poset

for p1, p2 being Element of P holds

( p1 <= p2 iff ( p1 = Bottom P or p1 = p2 ) )

proof end;

theorem Thflat01: :: POSET_2:6

for P being non empty flat Poset

for K being non empty Chain of P ex a being Element of P st

( K = {a} or K = {(Bottom P),a} )

for K being non empty Chain of P ex a being Element of P st

( K = {a} or K = {(Bottom P),a} )

proof end;

Lemflat02: for P being non empty flat Poset

for K being Chain of P st not K is empty holds

ex_sup_of K,P

proof end;

theorem Thflat05: :: POSET_2:7

for P, Q being non empty flat Poset

for K being non empty Chain of P

for f being Function of P,Q ex a being Element of P st

( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )

for K being non empty Chain of P

for f being Function of P,Q ex a being Element of P st

( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )

proof end;

theorem Thflat0501: :: POSET_2:8

for P, Q being non empty flat Poset

for f being Function of P,Q st f . (Bottom P) = Bottom Q holds

f is monotone

for f being Function of P,Q st f . (Bottom P) = Bottom Q holds

f is monotone

proof end;

theorem Thflat0502: :: POSET_2:9

for P being non empty flat Poset

for p being Element of P

for K being non empty Chain of P st K = {(Bottom P),p} holds

sup K = p

for p being Element of P

for K being non empty Chain of P st K = {(Bottom P),p} holds

sup K = p

proof end;

registration

existence

ex b_{1} being Poset st

( b_{1} is strict & not b_{1} is empty & b_{1} is flat & b_{1} is chain-complete )

end;
ex b

( b

proof end;

:: If P,Q is non empty flat RelStr, then P,Q is always chain-complete poset

:: and function f : P -> Q st f.(Bottom P) = Bottom Q is always continuous

:: (so, it is monotone too).

:: So, we can use every theorems for continuous function on the non empty

:: chain-complete poset such as fix point theorem (see POSET_1).

:: and function f : P -> Q st f.(Bottom P) = Bottom Q is always continuous

:: (so, it is monotone too).

:: So, we can use every theorems for continuous function on the non empty

:: chain-complete poset such as fix point theorem (see POSET_1).

registration

correctness

coherence

for b_{1} being Poset st not b_{1} is empty & b_{1} is flat holds

b_{1} is chain-complete ;

by Lemflat02;

end;
coherence

for b

b

by Lemflat02;

theorem Thflat07: :: POSET_2:10

for P, Q being non empty strict chain-complete flat Poset

for f being Function of P,Q st f . (Bottom P) = Bottom Q holds

f is continuous

for f being Function of P,Q st f . (Bottom P) = Bottom Q holds

f is continuous

proof end;

definition

let X be non empty set ;

coherence

({[X,X]} \/ [:{X},X:]) \/ (id X) is Relation of (succ X),(succ X);

end;
func FlatRelat X -> Relation of (succ X),(succ X) equals :: POSET_2:def 2

({[X,X]} \/ [:{X},X:]) \/ (id X);

correctness ({[X,X]} \/ [:{X},X:]) \/ (id X);

coherence

({[X,X]} \/ [:{X},X:]) \/ (id X) is Relation of (succ X),(succ X);

proof end;

:: deftheorem defines FlatRelat POSET_2:def 2 :

for X being non empty set holds FlatRelat X = ({[X,X]} \/ [:{X},X:]) \/ (id X);

for X being non empty set holds FlatRelat X = ({[X,X]} \/ [:{X},X:]) \/ (id X);

LemFlatten01: for X being non empty set

for x, y being Element of succ X holds

( not [x,y] in FlatRelat X or x = X or x = y )

proof end;

LemFlatten02: for X being non empty set

for x, y being Element of succ X st ( x = X or x = y ) holds

[x,y] in FlatRelat X

proof end;

theorem :: POSET_2:11

definition

let X be non empty set ;

coherence

RelStr(# (succ X),(FlatRelat X) #) is non empty strict chain-complete flat Poset;

end;
func FlatPoset X -> non empty strict chain-complete flat Poset equals :: POSET_2:def 3

RelStr(# (succ X),(FlatRelat X) #);

correctness RelStr(# (succ X),(FlatRelat X) #);

coherence

RelStr(# (succ X),(FlatRelat X) #) is non empty strict chain-complete flat Poset;

proof end;

:: deftheorem defines FlatPoset POSET_2:def 3 :

for X being non empty set holds FlatPoset X = RelStr(# (succ X),(FlatRelat X) #);

for X being non empty set holds FlatPoset X = RelStr(# (succ X),(FlatRelat X) #);

theorem ThFlatten04: :: POSET_2:12

for X being non empty set

for x, y being Element of (FlatPoset X) holds

( x <= y iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02;

for x, y being Element of (FlatPoset X) holds

( x <= y iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02;

definition

let x be object ;

let X, Y be non empty set ;

let f be Function of X,Y;

correctness

coherence

( ( x in X implies f . x is set ) & ( not x in X implies Y is set ) );

consistency

for b_{1} being set holds verum;

;

end;
let X, Y be non empty set ;

let f be Function of X,Y;

correctness

coherence

( ( x in X implies f . x is set ) & ( not x in X implies Y is set ) );

consistency

for b

;

:: deftheorem DefFlatten01 defines Flatten POSET_2:def 4 :

for x being object

for X, Y being non empty set

for f being Function of X,Y holds

( ( x in X implies Flatten (f,x) = f . x ) & ( not x in X implies Flatten (f,x) = Y ) );

for x being object

for X, Y being non empty set

for f being Function of X,Y holds

( ( x in X implies Flatten (f,x) = f . x ) & ( not x in X implies Flatten (f,x) = Y ) );

definition

let X, Y be non empty set ;

let f be Function of X,Y;

ex b_{1} being Function of (FlatPoset X),(FlatPoset Y) st

( b_{1} . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

b_{1} . x = f . x ) )

for b_{1}, b_{2} being Function of (FlatPoset X),(FlatPoset Y) st b_{1} . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

b_{1} . x = f . x ) & b_{2} . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

b_{2} . x = f . x ) holds

b_{1} = b_{2}

end;
let f be Function of X,Y;

func Flatten f -> Function of (FlatPoset X),(FlatPoset Y) means :DefFlatten04: :: POSET_2:def 5

( it . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

it . x = f . x ) );

existence ( it . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

it . x = f . x ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem DefFlatten04 defines Flatten POSET_2:def 5 :

for X, Y being non empty set

for f being Function of X,Y

for b_{4} being Function of (FlatPoset X),(FlatPoset Y) holds

( b_{4} = Flatten f iff ( b_{4} . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds

b_{4} . x = f . x ) ) );

for X, Y being non empty set

for f being Function of X,Y

for b

( b

b

registration
end;

theorem :: POSET_2:14

for x being object

for X, Y being non empty set

for f being Function of X,Y st x in X holds

(Flatten f) . x in Y

for X, Y being non empty set

for f being Function of X,Y st x in X holds

(Flatten f) . x in Y

proof end;

definition

let X, Y be non empty set ;

ConPoset ((FlatPoset X),(FlatPoset Y)) is non empty strict chain-complete Poset ;

end;
func FlatConF (X,Y) -> non empty strict chain-complete Poset equals :: POSET_2:def 6

ConPoset ((FlatPoset X),(FlatPoset Y));

coherence ConPoset ((FlatPoset X),(FlatPoset Y));

ConPoset ((FlatPoset X),(FlatPoset Y)) is non empty strict chain-complete Poset ;

:: deftheorem defines FlatConF POSET_2:def 6 :

for X, Y being non empty set holds FlatConF (X,Y) = ConPoset ((FlatPoset X),(FlatPoset Y));

for X, Y being non empty set holds FlatConF (X,Y) = ConPoset ((FlatPoset X),(FlatPoset Y));

registration
end;

registration

ex b_{1} being LATTICE st

( not b_{1} is empty & b_{1} is flat & b_{1} is lower-bounded )
end;

cluster non empty total reflexive transitive antisymmetric with_suprema with_infima lower-bounded non void flat for RelStr ;

existence ex b

( not b

proof end;

theorem :: POSET_2:16

for L being non empty lower-bounded flat LATTICE

for x being Element of L

for A being Chain of Bottom L,x holds card A <= 2

for x being Element of L

for A being Chain of Bottom L,x holds card A <= 2

proof end;

theorem :: POSET_2:17

for L being non empty finite lower-bounded LATTICE holds

( L is flat iff for x being Element of L holds height x <= 2 )

( L is flat iff for x being Element of L holds height x <= 2 )

proof end;

:: deftheorem defines is_well_founded_with_minimal_set POSET_2:def 7 :

for X being non empty set

for D being Subset of X

for E being Function of X,X holds

( E is_well_founded_with_minimal_set D iff ex l being Function of X,NAT st

for x being Element of X holds

( ( l . x <= 0 implies x in D ) & ( not x in D implies l . (E . x) < l . x ) ) );

for X being non empty set

for D being Subset of X

for E being Function of X,X holds

( E is_well_founded_with_minimal_set D iff ex l being Function of X,NAT st

for x being Element of X holds

( ( l . x <= 0 implies x in D ) & ( not x in D implies l . (E . x) < l . x ) ) );

definition

let X, Y be non empty set ;

let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y:],Y;

let x, y be object ;

coherence

( ( x in D implies I . x is set ) & ( not x in D & x in X & y in Y implies J . [x,y] is set ) & ( not x in D & ( x in D or not x in X or not y in Y ) implies Y is set ) );

consistency

for b_{1} being set st x in D & not x in D & x in X & y in Y holds

( b_{1} = I . x iff b_{1} = J . [x,y] );

;

end;
let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y:],Y;

let x, y be object ;

func BaseFunc01 (x,y,I,J,D) -> set equals :DefBaseFunc01: :: POSET_2:def 8

I . x if x in D

J . [x,y] if ( not x in D & x in X & y in Y )

otherwise Y;

correctness I . x if x in D

J . [x,y] if ( not x in D & x in X & y in Y )

otherwise Y;

coherence

( ( x in D implies I . x is set ) & ( not x in D & x in X & y in Y implies J . [x,y] is set ) & ( not x in D & ( x in D or not x in X or not y in Y ) implies Y is set ) );

consistency

for b

( b

;

:: deftheorem DefBaseFunc01 defines BaseFunc01 POSET_2:def 8 :

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for x, y being object holds

( ( x in D implies BaseFunc01 (x,y,I,J,D) = I . x ) & ( not x in D & x in X & y in Y implies BaseFunc01 (x,y,I,J,D) = J . [x,y] ) & ( not x in D & ( x in D or not x in X or not y in Y ) implies BaseFunc01 (x,y,I,J,D) = Y ) );

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for x, y being object holds

( ( x in D implies BaseFunc01 (x,y,I,J,D) = I . x ) & ( not x in D & x in X & y in Y implies BaseFunc01 (x,y,I,J,D) = J . [x,y] ) & ( not x in D & ( x in D or not x in X or not y in Y ) implies BaseFunc01 (x,y,I,J,D) = Y ) );

definition

let X, Y be non empty set ;

let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y:],Y;

let E be Function of X,X;

let h be object ;

assume A00: h is continuous Function of (FlatPoset X),(FlatPoset Y) ;

ex b_{1} being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b_{1} . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)

for b_{1}, b_{2} being continuous Function of (FlatPoset X),(FlatPoset Y) st ( for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b_{1} . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b_{2} . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds

b_{1} = b_{2}

end;
let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y:],Y;

let E be Function of X,X;

let h be object ;

assume A00: h is continuous Function of (FlatPoset X),(FlatPoset Y) ;

func RecFunc01 (h,E,I,J,D) -> continuous Function of (FlatPoset X),(FlatPoset Y) means :DefRecFunc01: :: POSET_2:def 9

for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

it . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D);

existence for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

it . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D);

ex b

for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b

proof end;

uniqueness for b

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b

b

proof end;

:: deftheorem DefRecFunc01 defines RecFunc01 POSET_2:def 9 :

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X

for h being object st h is continuous Function of (FlatPoset X),(FlatPoset Y) holds

for b_{8} being continuous Function of (FlatPoset X),(FlatPoset Y) holds

( b_{8} = RecFunc01 (h,E,I,J,D) iff for x being Element of (FlatPoset X)

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b_{8} . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) );

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X

for h being object st h is continuous Function of (FlatPoset X),(FlatPoset Y) holds

for b

( b

for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds

b

theorem Threcursive01: :: POSET_2:18

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X ex W being continuous Function of (FlatConF (X,Y)),(FlatConF (X,Y)) st

for f being Element of ConFuncs ((FlatPoset X),(FlatPoset Y)) holds W . f = RecFunc01 (f,E,I,J,D)

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X ex W being continuous Function of (FlatConF (X,Y)),(FlatConF (X,Y)) st

for f being Element of ConFuncs ((FlatPoset X),(FlatPoset Y)) holds W . f = RecFunc01 (f,E,I,J,D)

proof end;

theorem Threcursive02: :: POSET_2:19

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X ex f being set st

( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X ex f being set st

( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc01 (f,E,I,J,D) )

proof end;

theorem Threcursive03: :: POSET_2:20

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X st E is_well_founded_with_minimal_set D holds

ex f being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of X holds

( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X st E is_well_founded_with_minimal_set D holds

ex f being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of X holds

( f . x in Y & f . x = BaseFunc01 (x,(f . (E . x)),I,J,D) )

proof end;

Lemrecursive04: for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X st E is_well_founded_with_minimal_set D holds

ex f being Function of X,Y st

for x being Element of X holds f . x = BaseFunc01 (x,(f . (E . x)),I,J,D)

proof end;

:: Existence

theorem :: POSET_2:21

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X st E is_well_founded_with_minimal_set D holds

ex f being Function of X,Y st

for x being Element of X holds

( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E . x))] ) )

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X st E is_well_founded_with_minimal_set D holds

ex f being Function of X,Y st

for x being Element of X holds

( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E . x))] ) )

proof end;

:: Uniqueness

theorem :: POSET_2:22

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X

for f1, f2 being Function of X,Y st E is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies f1 . x = I . x ) & ( not x in D implies f1 . x = J . [x,(f1 . (E . x))] ) ) ) & ( for x being Element of X holds

( ( x in D implies f2 . x = I . x ) & ( not x in D implies f2 . x = J . [x,(f2 . (E . x))] ) ) ) holds

f1 = f2

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y:],Y

for E being Function of X,X

for f1, f2 being Function of X,Y st E is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies f1 . x = I . x ) & ( not x in D implies f1 . x = J . [x,(f1 . (E . x))] ) ) ) & ( for x being Element of X holds

( ( x in D implies f2 . x = I . x ) & ( not x in D implies f2 . x = J . [x,(f2 . (E . x))] ) ) ) holds

f1 = f2

proof end;

:: deftheorem defines is_well_founded_with_minimal_set POSET_2:def 10 :

for X being non empty set

for D being Subset of X

for E1, E2 being Function of X,X holds

( E1,E2 is_well_founded_with_minimal_set D iff ex l being Function of X,NAT st

for x being Element of X holds

( ( l . x <= 0 implies x in D ) & ( not x in D implies ( l . (E1 . x) < l . x & l . (E2 . x) < l . x ) ) ) );

for X being non empty set

for D being Subset of X

for E1, E2 being Function of X,X holds

( E1,E2 is_well_founded_with_minimal_set D iff ex l being Function of X,NAT st

for x being Element of X holds

( ( l . x <= 0 implies x in D ) & ( not x in D implies ( l . (E1 . x) < l . x & l . (E2 . x) < l . x ) ) ) );

definition

let X, Y be non empty set ;

let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y,Y:],Y;

let x, y1, y2 be object ;

coherence

( ( x in D implies I . x is set ) & ( not x in D & x in X & y1 in Y & y2 in Y implies J . [x,y1,y2] is set ) & ( not x in D & ( x in D or not x in X or not y1 in Y or not y2 in Y ) implies Y is set ) );

consistency

for b_{1} being set st x in D & not x in D & x in X & y1 in Y & y2 in Y holds

( b_{1} = I . x iff b_{1} = J . [x,y1,y2] );

;

end;
let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y,Y:],Y;

let x, y1, y2 be object ;

func BaseFunc02 (x,y1,y2,I,J,D) -> set equals :DefBaseFunc02: :: POSET_2:def 11

I . x if x in D

J . [x,y1,y2] if ( not x in D & x in X & y1 in Y & y2 in Y )

otherwise Y;

correctness I . x if x in D

J . [x,y1,y2] if ( not x in D & x in X & y1 in Y & y2 in Y )

otherwise Y;

coherence

( ( x in D implies I . x is set ) & ( not x in D & x in X & y1 in Y & y2 in Y implies J . [x,y1,y2] is set ) & ( not x in D & ( x in D or not x in X or not y1 in Y or not y2 in Y ) implies Y is set ) );

consistency

for b

( b

;

:: deftheorem DefBaseFunc02 defines BaseFunc02 POSET_2:def 11 :

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for x, y1, y2 being object holds

( ( x in D implies BaseFunc02 (x,y1,y2,I,J,D) = I . x ) & ( not x in D & x in X & y1 in Y & y2 in Y implies BaseFunc02 (x,y1,y2,I,J,D) = J . [x,y1,y2] ) & ( not x in D & ( x in D or not x in X or not y1 in Y or not y2 in Y ) implies BaseFunc02 (x,y1,y2,I,J,D) = Y ) );

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for x, y1, y2 being object holds

( ( x in D implies BaseFunc02 (x,y1,y2,I,J,D) = I . x ) & ( not x in D & x in X & y1 in Y & y2 in Y implies BaseFunc02 (x,y1,y2,I,J,D) = J . [x,y1,y2] ) & ( not x in D & ( x in D or not x in X or not y1 in Y or not y2 in Y ) implies BaseFunc02 (x,y1,y2,I,J,D) = Y ) );

definition

let X, Y be non empty set ;

let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y,Y:],Y;

let E1, E2 be Function of X,X;

let h1, h2 be object ;

assume A00: ( h1 is continuous Function of (FlatPoset X),(FlatPoset Y) & h2 is continuous Function of (FlatPoset X),(FlatPoset Y) ) ;

ex b_{1} being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b_{1} . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D)

for b_{1}, b_{2} being continuous Function of (FlatPoset X),(FlatPoset Y) st ( for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b_{1} . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b_{2} . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) holds

b_{1} = b_{2}

end;
let D be Subset of X;

let I be Function of X,Y;

let J be Function of [:X,Y,Y:],Y;

let E1, E2 be Function of X,X;

let h1, h2 be object ;

assume A00: ( h1 is continuous Function of (FlatPoset X),(FlatPoset Y) & h2 is continuous Function of (FlatPoset X),(FlatPoset Y) ) ;

func RecFunc02 (h1,h2,E1,E2,I,J,D) -> continuous Function of (FlatPoset X),(FlatPoset Y) means :DefRecFunc02: :: POSET_2:def 12

for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

it . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D);

existence for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

it . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D);

ex b

for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b

proof end;

uniqueness for b

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b

b

proof end;

:: deftheorem DefRecFunc02 defines RecFunc02 POSET_2:def 12 :

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for h1, h2 being object st h1 is continuous Function of (FlatPoset X),(FlatPoset Y) & h2 is continuous Function of (FlatPoset X),(FlatPoset Y) holds

for b_{10} being continuous Function of (FlatPoset X),(FlatPoset Y) holds

( b_{10} = RecFunc02 (h1,h2,E1,E2,I,J,D) iff for x being Element of (FlatPoset X)

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b_{10} . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) );

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for h1, h2 being object st h1 is continuous Function of (FlatPoset X),(FlatPoset Y) & h2 is continuous Function of (FlatPoset X),(FlatPoset Y) holds

for b

( b

for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds

b

theorem Threcursive0101: :: POSET_2:23

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X ex W being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) st

for f being set st f in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds

W . f = RecFunc02 ((f `1),(f `2),E1,E2,I,J,D)

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X ex W being continuous Function of [:(FlatConF (X,Y)),(FlatConF (X,Y)):],(FlatConF (X,Y)) st

for f being set st f in [:(ConFuncs ((FlatPoset X),(FlatPoset Y))),(ConFuncs ((FlatPoset X),(FlatPoset Y))):] holds

W . f = RecFunc02 ((f `1),(f `2),E1,E2,I,J,D)

proof end;

theorem Threcursive0201: :: POSET_2:24

for X, Y being non empty set

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X ex f, g being set st

( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X ex f, g being set st

( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) )

proof end;

theorem Threcursive0301: :: POSET_2:25

for X, Y being non empty set

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f, g being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of X holds

( f . x in Y & f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x in Y & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) )

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f, g being continuous Function of (FlatPoset X),(FlatPoset Y) st

for x being Element of X holds

( f . x in Y & f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x in Y & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) )

proof end;

Lemrecursive0401: for X, Y being non empty set

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f, g being Function of X,Y st

for x being Element of X holds

( f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) )

proof end;

:: Existence

theorem Threcursive05: :: POSET_2:26

for X, Y being non empty set

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f, g being Function of X,Y st

for x being Element of X holds

( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f, g being Function of X,Y st

for x being Element of X holds

( ( x in D implies ( f . x = I1 . x & g . x = I2 . x ) ) & ( not x in D implies ( f . x = J1 . [x,(f . (E1 . x)),(g . (E2 . x))] & g . x = J2 . [x,(f . (E1 . x)),(g . (E2 . x))] ) ) )

proof end;

:: Uniqueness

theorem :: POSET_2:27

for X, Y being non empty set

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds

( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds

( f1 = f2 & g1 = g2 )

for D being Subset of X

for I1, I2 being Function of X,Y

for J1, J2 being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds

( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds

( f1 = f2 & g1 = g2 )

proof end;

:: In the case of I1 = I2 (=I) and J1 = J2 (=J), we get the following theorems.

:: For example, they are used to define the evaluate function for the binary tree(x) ,

:: when the treatments of the left side sub tree(E1.x) and the right side sub tree(E2.x) are same.

:: Existence

:: For example, they are used to define the evaluate function for the binary tree(x) ,

:: when the treatments of the left side sub tree(E1.x) and the right side sub tree(E2.x) are same.

:: Existence

theorem :: POSET_2:28

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f being Function of X,Y st

for x being Element of X holds

( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E1 . x)),(f . (E2 . x))] ) )

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X st E1,E2 is_well_founded_with_minimal_set D holds

ex f being Function of X,Y st

for x being Element of X holds

( ( x in D implies f . x = I . x ) & ( not x in D implies f . x = J . [x,(f . (E1 . x)),(f . (E2 . x))] ) )

proof end;

:: Uniqueness

theorem :: POSET_2:29

for X, Y being non empty set

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for f1, f2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies f1 . x = I . x ) & ( not x in D implies f1 . x = J . [x,(f1 . (E1 . x)),(f1 . (E2 . x))] ) ) ) & ( for x being Element of X holds

( ( x in D implies f2 . x = I . x ) & ( not x in D implies f2 . x = J . [x,(f2 . (E1 . x)),(f2 . (E2 . x))] ) ) ) holds

f1 = f2

for D being Subset of X

for I being Function of X,Y

for J being Function of [:X,Y,Y:],Y

for E1, E2 being Function of X,X

for f1, f2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds

( ( x in D implies f1 . x = I . x ) & ( not x in D implies f1 . x = J . [x,(f1 . (E1 . x)),(f1 . (E2 . x))] ) ) ) & ( for x being Element of X holds

( ( x in D implies f2 . x = I . x ) & ( not x in D implies f2 . x = J . [x,(f2 . (E1 . x)),(f2 . (E2 . x))] ) ) ) holds

f1 = f2

proof end;