environ
vocabularies HIDDEN, POSET_2, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, STRUCT_0, FUNCT_1, FUNCT_2, NAT_1, TREES_2, LATTICE3, TARSKI, ORDERS_2, ORDINAL2, ARYTM_3, SEQM_3, LATTICES, YELLOW_0, POSET_1, NATTRA_1, MSAFREE1, ZFMISC_1, SUBSET_1, NUMBERS, CARD_1, XXREAL_0, ABIAN, PARTFUN1, MCART_1, YELLOW_3, ORDINAL1, WAYBEL_0, FINSET_1, TREES_1, PREFER_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, CARD_1, ORDERS_1, RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2, BINOP_1, FUNCOP_1, ORDINAL1, STRUCT_0, ORDERS_2, ORDERS_3, NUMBERS, NAT_1, XTUPLE_0, XXREAL_0, ABIAN, XCMPLX_0, FUNCT_3, POSET_1, LATTICES, YELLOW_2, YELLOW_3, LATTICE3, YELLOW_0, WAYBEL_0, LATTICE7, MCART_1;
definitions TARSKI, FUNCOP_1, XBOOLE_0, ABIAN, LATTICE3, RELAT_2, STRUCT_0, WAYBEL_0, POSET_1, SUBSET_1, YELLOW_3, FUNCT_3, MCART_1, ORDINAL1, XTUPLE_0, ORDERS_2, YELLOW_0, ORDERS_3;
theorems RELAT_1, RELSET_1, RELAT_2, ORDERS_2, TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, ORDERS_3, STRUCT_0, XREAL_1, LATTICE3, YELLOW_0, ABIAN, YELLOW_2, XTUPLE_0, POSET_1, XXREAL_0, ENUMSET1, YELLOW_3, FUNCT_3, MCART_1, NAT_1, LATTICE7, CARD_2;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FRAENKEL, STRUCT_0, ORDERS_2, ORDERS_3, FUNCOP_1, XREAL_0, NAT_1, NUMBERS, REAL_1, XXREAL_0, ARYTM_2, XCMPLX_0, RELAT_1, ORDERS_1, XBOOLEAN, KNASTER, LATTICE3, YELLOW_0, ABIAN, YELLOW_2, YELLOW_3, WAYBEL_0, WAYBEL10, WAYBEL24, POSET_1, YELLOW10, XTUPLE_0, ZFMISC_1, MCART_1, CARD_1, FINSET_1;
constructors HIDDEN, RELAT_2, PARTFUN1, ORDERS_2, ORDERS_3, FUNCOP_1, FUNCT_3, FINSET_1, LATTICE7, CARD_1, BINOP_1, FUNCT_4, NAT_1, REAL_1, DOMAIN_1, XXREAL_0, ARYTM_0, NUMBERS, XCMPLX_0, XREAL_0, ARYTM_1, ABIAN, XTUPLE_0, LATTICE3, YELLOW_0, YELLOW_2, YELLOW_3, POSET_1, RELSET_1, MCART_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ORDINAL1, POSET_1, RELSET_1, YELLOW_0, YELLOW_3, ORDERS_2, XTUPLE_0, MCART_1, FUNCT_2;
expansions POSET_1, ORDERS_2, YELLOW_0, FUNCT_2, FUNCT_3, ORDERS_3, RELAT_2, LATTICE3;
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 ) )
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 )
;
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:]
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 ) )
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
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 )
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
::
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:
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)
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
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:
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)
theorem Threcursive02:
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) )
theorem Threcursive03:
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) )
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)
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 ;
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:
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)
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
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:
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)
theorem Threcursive0201:
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) )
theorem Threcursive0301:
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) )
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) )
theorem Threcursive05:
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))] ) ) )
theorem
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 )
theorem
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))] ) )
theorem
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