:: Definition of Flat Poset and Existence Theorems for Recursive Call
:: by Kazuhisa Ishida , Yasunari Shidama and Adam Grabowski
::
:: Received February 11, 2014
:: Copyright (c) 2014-2021 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

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

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

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] )

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;

proof end;

:: original: rng
redefine func proj2 L -> non empty Chain of Q;
correctness
coherence
rng L is non empty Chain of Q;

proof end;

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;

cluster <:f1,f2:> -> monotone for Function of P,[:Q1,Q2:];

correctness
coherence
for b₁ being Function of P,[:Q1,Q2:] st b₁ = <:f1,f2:> holds
b₁ is monotone ;

proof end;

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;

cluster [:P,Q:] -> chain-complete ;

correctness
coherence
[:P,Q:] is chain-complete ;
by LemProdPoset06;

end;

theorem :: POSET_2:5

for P, Q being non empty chain-complete Poset
for L being non empty Chain of [:P,Q:] holds sup L = [(sup (proj1 L)),(sup (proj2 L))] by YELLOW_3:46, LemProdPoset06;

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;

cluster <:f1,f2:> -> continuous for Function of P,[:Q1,Q2:];

correctness
coherence
for b₁ being Function of P,[:Q1,Q2:] st b₁ = <:f1,f2:> holds
b₁ is continuous ;

proof end;

end;

definition

let IT be RelStr ;

attr IT is flat means :Defflat: :: POSET_2:def 1
ex a being Element of IT st
for x, y being Element of IT holds
( x <= y iff ( x = a or x = y ) );

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 ) ) );

registration

cluster non empty discrete -> non empty reflexive for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is discrete holds
b₁ is reflexive by ORDERS_3:1;

end;

registration

cluster non empty trivial discrete -> non empty discrete flat for RelStr ;

coherence
for b₁ being non empty discrete RelStr st b₁ is trivial holds
b₁ is flat

proof end;

end;

registration

cluster non empty strict total reflexive transitive antisymmetric flat for RelStr ;

existence
ex b₁ being Poset st
( b₁ is strict & not b₁ is empty & b₁ is flat )

proof end;

end;

registration

cluster flat -> reflexive transitive antisymmetric for RelStr ;

correctness
coherence
for b₁ being RelStr st b₁ is flat holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric );

proof end;

end;

registration

cluster non empty reflexive transitive antisymmetric flat -> non empty lower-bounded for RelStr ;

coherence
for b₁ being non empty Poset st b₁ is flat holds
b₁ is lower-bounded

proof end;

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} )

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)} ) )

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

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

proof end;

registration

cluster non empty strict total reflexive transitive antisymmetric chain-complete flat for RelStr ;

existence
ex b₁ being Poset st
( b₁ is strict & not b₁ is empty & b₁ is flat & b₁ is chain-complete )

proof end;

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).

registration

cluster non empty reflexive transitive antisymmetric flat -> chain-complete for RelStr ;

correctness
coherence
for b₁ being Poset st not b₁ is empty & b₁ is flat holds
b₁ is chain-complete ;
by Lemflat02;

end;

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

proof end;

definition

let X be non empty set ;

func FlatRelat X -> Relation of (succ X),(succ X) equals :: POSET_2:def 2
({[X,X]} \/ [:{X},X:]) \/ (id X);

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

proof end;

end;

:: deftheorem defines FlatRelat POSET_2:def 2 :
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

for X being non empty set
for x, y being Element of succ X holds
( [x,y] in FlatRelat X iff ( x = X or x = y ) ) by LemFlatten01, LemFlatten02;

definition

let X be non empty set ;

func FlatPoset X -> non empty strict chain-complete flat Poset equals :: POSET_2:def 3
RelStr(# (succ X),(FlatRelat X) #);

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

proof end;

end;

:: deftheorem defines FlatPoset POSET_2:def 3 :
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;

theorem LemFlatten05: :: POSET_2:13

for X being non empty set holds X is Element of (FlatPoset X)

proof end;

registration

let X be non empty set ;

reduce Bottom (FlatPoset X) to X;

reducibility
Bottom (FlatPoset X) = X

proof end;

end;

definition

let x be object ;
let X, Y be non empty set ;
let f be Function of X,Y;

func Flatten (f,x) -> set equals :DefFlatten01: :: POSET_2:def 4
f . x if x in X
otherwise Y;

correctness
coherence
( ( x in X implies f . x is set ) & ( not x in X implies Y is set ) );
consistency
for b₁ being set holds verum;
;

end;

:: 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 ) );

definition

let X, Y be non empty set ;
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
ex b₁ being Function of (FlatPoset X),(FlatPoset Y) st
( b₁ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₁ . x = f . x ) )

proof end;

uniqueness
for b₁, b₂ being Function of (FlatPoset X),(FlatPoset Y) st b₁ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₁ . x = f . x ) & b₂ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₂ . x = f . x ) holds
b₁ = b₂

proof end;

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₄ being Function of (FlatPoset X),(FlatPoset Y) holds
( b₄ = Flatten f iff ( b₄ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₄ . x = f . x ) ) );

registration

let X, Y be non empty set ;
let f be Function of X,Y;

cluster Flatten f -> continuous ;

coherence
Flatten f is continuous

proof end;

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

proof end;

definition

let X, Y be non empty set ;

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)) is non empty strict chain-complete Poset ;

end;

:: deftheorem defines FlatConF POSET_2:def 6 :
for X, Y being non empty set holds FlatConF (X,Y) = ConPoset ((FlatPoset X),(FlatPoset Y));

registration

let L be flat Poset;

cluster strongly_connected -> finite for Element of bool the carrier of L;

coherence
for b₁ being Chain of L holds b₁ is finite

proof end;

end;

registration

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

existence
ex b₁ being LATTICE st
( not b₁ is empty & b₁ is flat & b₁ is lower-bounded )

proof end;

end;

theorem CardA1: :: POSET_2:15

for L being non empty LATTICE
for x being Element of L
for A being Chain of x,x holds card A = 1

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

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 )

proof end;

definition

let X be non empty set ;
let D be Subset of X;
let E be Function of X,X;

pred E is_well_founded_with_minimal_set D means :: POSET_2:def 7
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 ) );

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 ) ) );

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 ;

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
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₁ being set st x in D & not x in D & x in X & y in Y holds
( b₁ = I . x iff b₁ = J . [x,y] );
;

end;

:: 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 ) );

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) ;

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
ex b₁ 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₁ . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)

proof end;

uniqueness
for b₁, b₂ 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₁ . 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₂ . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds
b₁ = b₂

proof end;

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₈ being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b₈ = 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₈ . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) );

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)

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) )

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) )

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))] ) )

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

proof end;

definition

let X be non empty set ;
let D be Subset of X;
let E1, E2 be Function of X,X;

pred E1,E2 is_well_founded_with_minimal_set D means :: POSET_2:def 10
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 ) ) );

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 ) ) ) );

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 ;

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
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₁ being set st x in D & not x in D & x in X & y1 in Y & y2 in Y holds
( b₁ = I . x iff b₁ = J . [x,y1,y2] );
;

end;

:: 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 ) );

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) ) ;

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
ex b₁ 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₁ . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D)

proof end;

uniqueness
for b₁, b₂ 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₁ . 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₂ . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) holds
b₁ = b₂

proof end;

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₁₀ being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b₁₀ = 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₁₀ . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) );

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)

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) )

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) )

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))] ) ) )

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 )

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

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))] ) )

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

proof end;