:: 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 b1 being Function of P,[:Q1,Q2:] st b1 = <:f1,f2:> holds
b1 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 b1 being Function of P,[:Q1,Q2:] st b1 = <:f1,f2:> holds
b1 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 b1 being non empty RelStr st b1 is discrete holds
b1 is reflexive by ORDERS_3:1;
end;

registration
cluster non empty trivial discrete -> non empty discrete flat for RelStr ;
coherence
for b1 being non empty discrete RelStr st b1 is trivial holds
b1 is flat
proof end;
end;

registration
cluster non empty strict total reflexive transitive antisymmetric flat for RelStr ;
existence
ex b1 being Poset st
( b1 is strict & not b1 is empty & b1 is flat )
proof end;
end;

registration
cluster flat -> reflexive transitive antisymmetric for RelStr ;
correctness
coherence
for b1 being RelStr st b1 is flat holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric );
proof end;
end;

registration
cluster non empty reflexive transitive antisymmetric flat -> non empty lower-bounded for RelStr ;
coherence
for b1 being non empty Poset st b1 is flat holds
b1 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 b1 being Poset st
( b1 is strict & not b1 is empty & b1 is flat & b1 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 b1 being Poset st not b1 is empty & b1 is flat holds
b1 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 b1 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 b1 being Function of (FlatPoset X),(FlatPoset Y) st
( b1 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b1 . x = f . x ) )
proof end;
uniqueness
for b1, b2 being Function of (FlatPoset X),(FlatPoset Y) st b1 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b1 . x = f . x ) & b2 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b2 . x = f . x ) holds
b1 = b2
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 b4 being Function of (FlatPoset X),(FlatPoset Y) holds
( b4 = Flatten f iff ( b4 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b4 . 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 b1 being Chain of L holds b1 is finite
proof end;
end;

registration
cluster non empty total reflexive transitive antisymmetric with_suprema with_infima lower-bounded flat for RelStr ;
existence
ex b1 being LATTICE st
( not b1 is empty & b1 is flat & b1 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 b1 being set st x in D & not x in D & x in X & y in Y holds
( b1 = I . x iff b1 = 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 b1 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
b1 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds
b1 = b2
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 b8 being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b8 = 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
b8 . 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 b1 being set st x in D & not x in D & x in X & y1 in Y & y2 in Y holds
( b1 = I . x iff b1 = 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 b1 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
b1 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D)
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) holds
b1 = b2
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 b10 being continuous Function of (FlatPoset X),(FlatPoset Y) holds
( b10 = 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
b10 . 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;