:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
registrations XBOOLE_0, ORDINAL1, SUBSET_1, RELSET_1, PARTFUN1, FUNCT_2,
STRUCT_0, ORDERS_2, ORDERS_3, XREAL_0, NAT_1, RELAT_1, YELLOW_0,
YELLOW_3, WAYBEL10, POSET_1, YELLOW10, XTUPLE_0, FINSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions YELLOW_0, ORDERS_3;
equalities ORDINAL1, POSET_1, YELLOW_0;
expansions POSET_1, ORDERS_2, YELLOW_0, FUNCT_2, ORDERS_3, RELAT_2, LATTICE3;
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;
begin :: Preliminaries
reserve a,Z1,Z2,Z3 for set,
x,y,z for object,
k for Nat;
LemSUM01:
a in (Z1 \/ Z2) \/ Z3 iff a in Z1 or a in Z2 or a in Z3
proof
a in (Z1 \/ Z2) \/ Z3 iff
a in Z1 \/ Z2 or a in Z3 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
LemMin01:
for S being non empty RelStr,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:
for P being lower-bounded non empty Poset,
p being Element of P
st p is_<=_than the carrier of P
holds p = Bottom P
proof
let P be lower-bounded non empty Poset;
let p be Element of P;
assume
A1: p is_<=_than the carrier of P;
A2: ex_sup_of {},P by YELLOW_0:42;
A3: {} is_<=_than p;
for a being Element of P st {} is_<=_than a holds p <= a by A1;
hence thesis by A2,A3,YELLOW_0:def 9;
end;
theorem Thsup01:
for P being chain-complete non empty Poset,
L being non empty Chain of P
for p being Element of P st p in L holds p <= sup L
proof
let P be chain-complete non empty Poset;
let L be non empty Chain of P;
let p be Element of P;
assume
A1: p in L;
A2: ex_sup_of L,P by POSET_1:def 1;
reconsider x = sup L as Element of P;
L is_<=_than x by YELLOW_0:def 9,A2;
hence thesis by A1;
end;
theorem Thsup02:
for P being chain-complete non empty Poset,
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
let P be chain-complete non empty Poset;
let L be non empty Chain of P;
let p1 be Element of P;
assume for p being Element of P st p in L holds p<=p1; then
A1: L is_<=_than p1;
ex_sup_of L,P by POSET_1:def 1;
hence thesis by YELLOW_0:def 9,A1;
end;
begin :: Product of Poset
theorem ThProdPoset01:
for P,Q being non empty RelStr,
x being object holds
x is Element of [:P,Q:]
iff ex p being Element of P,q being Element of Q st x = [p,q]
proof
let P,Q be non empty RelStr;
let x be object;
x in the carrier of [:P,Q:]
iff x in [:the carrier of P, the carrier of Q:] by YELLOW_3:def 2;
then x in the carrier of [:P,Q:] iff
ex p,q being object
st p in the carrier of P & q in the carrier of Q & x = [p,q]
by ZFMISC_1:def 2;
hence thesis;
end;
definition let P,Q be non empty Poset;
let L be non empty Chain of [:P,Q:];
redefine func proj1 L -> non empty Chain of P; :: redefines proj1 (XTUPLE_0, definition)
correctness
proof
set R = the InternalRel of [:P,Q:];
reconsider L as Relation of the carrier of P,the carrier of Q
by YELLOW_3:def 2;
reconsider L1 = dom L as Subset of P;
reconsider L2 = rng L as Subset of Q;
set R1 = the InternalRel of P;
x in L1 & y in L1 implies [x,y] in R1 or [y,x] in R1
proof
assume
B1: x in L1 & y in L1;
then reconsider x,y as Element of P;
consider q1 being object such that
B2: [x,q1] in L by XTUPLE_0:def 12,B1;
consider q2 being object such that
B3: [y,q2] in L by XTUPLE_0:def 12,B1;
q1 in L2 & q2 in L2 by B2,B3,XTUPLE_0:def 13;
then reconsider q1,q2 as Element of Q;
reconsider a = [x,q1] as Element of [:P,Q:];
reconsider b = [y,q2] as Element of [:P,Q:];
per cases by ORDERS_2:def 7,RELAT_2:def 7,B2,B3;
suppose a <= b;
then x <= y by YELLOW_3:11;
hence thesis;
end;
suppose b <= a;
then y <= x by YELLOW_3:11;
hence thesis;
end;
end;
hence thesis by ORDERS_2:def 7,RELAT_2:def 7;
end;
redefine func proj2 L -> non empty Chain of Q; :: redefines proj2 (XTUPLE_0, definition)
correctness
proof
set R = the InternalRel of [:P,Q:];
reconsider L as Relation of the carrier of P,the carrier of Q
by YELLOW_3:def 2;
reconsider L1 = dom L as Subset of P;
reconsider L2 = rng L as Subset of Q;
set R2 = the InternalRel of Q;
x in L2 & y in L2 implies [x,y] in R2 or [y,x] in R2
proof
assume
B1: x in L2 & y in L2;
then reconsider x,y as Element of Q;
consider p1 being object such that
B2: [p1,x] in L by XTUPLE_0:def 13,B1;
consider p2 being object such that
B3: [p2,y] in L by XTUPLE_0:def 13,B1;
p1 in L1 & p2 in L1 by B2,B3,XTUPLE_0:def 12;
then reconsider p1,p2 as Element of P;
reconsider a = [p1,x], b = [p2,y] as Element of [:P,Q:];
per cases by ORDERS_2:def 7,RELAT_2:def 7,B2,B3;
suppose a <= b;
then x <= y by YELLOW_3:11;
hence thesis;
end;
suppose b <= a;
then y <= x by YELLOW_3:11;
hence thesis;
end;
end;
hence thesis by ORDERS_2:def 7,RELAT_2:def 7;
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
proof
set f = <:f1,f2:>;
for x,y being Element of P st x <= y
for a,b being Element of [:Q1,Q2:] st a = f.x & b = f.y holds a <= b
proof
let x,y be Element of P such that
B1: x <= y;
let a,b be Element of [:Q1,Q2:] such that
B2: a = f.x & b = f.y;
dom f = the carrier of P by FUNCT_2:def 1; then
B3: a = [f1.x,f2.x] & b = [f1.y,f2.y] by FUNCT_3:def 7,B2;
f1.x <= f1.y & f2.x <= f2.y by B1,ORDERS_3:def 5;
hence thesis by YELLOW_3:11,B3;
end;
hence thesis;
end;
end;
:: Theorem for product of chain-complete Poset
LemProdPoset06:
for P,Q being chain-complete non empty Poset
for L being Chain of [:P,Q:]
st L is non empty holds ex_sup_of L,[:P,Q:]
proof
let P,Q be chain-complete non empty Poset;
let L be Chain of [:P,Q:];
set R = the InternalRel of [:P,Q:];
assume L is non empty;
then reconsider L as non empty Chain of [:P,Q:];
reconsider L1 = proj1 L as non empty Chain of P;
reconsider L2 = proj2 L as non empty Chain of Q;
reconsider z = [sup L1,sup L2] as Element of [:P,Q:];
a1: for x being Element of [:P,Q:] st x in L holds x <= z
proof
let x be Element of [:P,Q:] such that
B1: x in L;
consider p being Element of P,q being Element of Q such that
B2: x = [p,q] by ThProdPoset01;
p in L1 & q in L2 by XTUPLE_0:def 12,XTUPLE_0:def 13,B1,B2;
then p <= sup L1 & q <= sup L2 by Thsup01;
hence thesis by YELLOW_3:11,B2;
end;
for y being Element of [:P,Q:] st L is_<=_than y holds z <= y
proof
let y be Element of [:P,Q:];
consider p1 being Element of P,q1 being Element of Q such that
B1: y = [p1,q1] by ThProdPoset01;
L is_<=_than y implies z <= y
proof
assume
C1: L is_<=_than y;
C2: for p being Element of P st p in L1 holds p <= p1
proof
let p be Element of P;
assume p in L1;
then consider q0 being object such that
D1: [p,q0] in L by XTUPLE_0:def 12;
q0 in L2 by D1,XTUPLE_0:def 13;
then reconsider q0 as Element of Q;
reconsider b = [p,q0] as Element of [:P,Q:];
b <= y by C1,D1;
hence thesis by B1,YELLOW_3:11;
end;
for q being Element of Q st q in L2 holds q <= q1
proof
let q be Element of Q;
assume q in L2;
then consider p0 being object such that
D1: [p0,q] in L by XTUPLE_0:def 13;
p0 in L1 by D1,XTUPLE_0:def 12;
then reconsider p0 as Element of P;
reconsider b = [p0,q] as Element of [:P,Q:];
b <= y by C1,D1;
hence thesis by B1,YELLOW_3:11;
end;
then sup L1 <= p1 & sup L2 <= q1 by C2,Thsup02;
hence thesis by YELLOW_3:11,B1;
end;
hence thesis;
end;
hence thesis by a1,YELLOW_0:15,LATTICE3:def 9;
end;
registration
let P,Q be chain-complete non empty Poset;
cluster [:P,Q:] -> chain-complete;
correctness by LemProdPoset06;
end;
theorem
for P,Q being chain-complete non empty Poset,
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 strict chain-complete non empty 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
proof
reconsider f = <:f1,f2:> as monotone Function of P,[:Q1,Q2:]
by YELLOW_3:def 2;
for L being non empty Chain of P holds f.(sup L) <= sup (f.:L)
proof
let L be non empty Chain of P;
B0: f1.(sup L) = sup (f1.:L) & f2.(sup L) = sup (f2.:L) by POSET_1:6;
AA: dom f = the carrier of P by FUNCT_2:def 1; then
B1: f.(sup L) = [sup (f1.:L), sup (f2.:L)] by FUNCT_3:def 7,B0;
reconsider M = f.:L as non empty Chain of [:Q1,Q2:] by POSET_1:1;
B2: sup (f.:L) = [sup (proj1 M), sup (proj2 M)]
by YELLOW_3:46,LemProdPoset06;
B3: sup (f1.:L) <= sup (proj1 M)
proof
reconsider M1 = f1.:L as non empty Chain of Q1 by POSET_1:1;
set q1 = sup (proj1 M);
for q being Element of Q1 st q in M1 holds q <= q1
proof
let q be Element of Q1;
assume q in M1;
then consider p be Element of P such that
C1: p in L & q = f1.p by FUNCT_2:65;
reconsider a = f2.p as Element of Q2;
f.p = [q,a] by C1,FUNCT_3:def 7,AA;
then [q,a] in M by C1,FUNCT_2:35;
then q in proj1 M by XTUPLE_0:def 12;
hence thesis by Thsup01;
end;
hence thesis by Thsup02;
end;
sup (f2.:L) <= sup (proj2 M)
proof
reconsider M2 = f2.:L as non empty Chain of Q2 by POSET_1:1;
set q2 = sup (proj2 M);
for q being Element of Q2 st q in M2 holds q <= q2
proof
let q be Element of Q2;
assume q in M2;
then consider p be Element of P such that
C1: p in L & q = f2.p by FUNCT_2:65;
reconsider a = f1.p as Element of Q1;
f.p = [a,q] by C1,FUNCT_3:def 7,AA;
then [a,q] in M by C1,FUNCT_2:35;
then q in proj2 M by XTUPLE_0:def 13;
hence thesis by Thsup01;
end;
hence thesis by Thsup02;
end;
hence thesis by B1,B2,B3,YELLOW_3:11;
end;
hence thesis by POSET_1:8;
end;
end;
begin :: Flat Posets
definition let IT be RelStr;
attr IT is flat means :Defflat:
ex a being Element of IT st
for x,y being Element of IT holds (x <= y iff x = a or x = y);
end;
registration
cluster discrete -> reflexive for non empty RelStr;
coherence by ORDERS_3:1;
end;
registration
cluster trivial -> flat for discrete non empty RelStr;
coherence
proof
let IT be discrete non empty RelStr;
assume
A: IT is trivial;
ex a being Element of IT st
a is_<=_than the carrier of IT &
(for x,y being Element of IT holds (x <= y iff x = a or x = y))
proof
take a = the Element of IT;
for b being Element of IT st b in the carrier of IT holds a <= b
by A,STRUCT_0:def 10;
hence thesis by STRUCT_0:def 10,A;
end;
hence thesis;
end;
end;
registration
cluster strict non empty flat for Poset;
existence
proof
set A = {{}};
reconsider R = id A as Relation of A;
reconsider R as Order of A;
take IT = RelStr(#A,R#);
reconsider z = {} as Element of IT by TARSKI:def 1;
ex a being Element of IT st
a is_<=_than the carrier of IT &
(for x,y being Element of IT holds (x <= y iff x = a or x = y))
proof
b1: for x being Element of IT holds z<=x by TARSKI:def 1;
for x,y being Element of IT holds (x <= y iff x = z or x = y)
by TARSKI:def 1;
hence thesis by b1,LemMin01;
end;
hence thesis;
end;
end;
registration
cluster flat -> reflexive transitive antisymmetric for RelStr;
correctness
proof
let S be RelStr;
assume S is flat;
then consider a be Element of S such that
A1: for x,y being Element of S holds (x <= y iff x = a or x = y);
set R = the InternalRel of S;
set X = the carrier of S;
R is_reflexive_in X
proof
x in X implies [x,x] in R
proof
assume x in X;
then reconsider x as Element of S;
x <= x by A1;
hence thesis;
end;
hence thesis;
end;
hence S is reflexive;
R is_transitive_in X
proof
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
proof
assume
B1: x in X & y in X & z in X & [x,y] in R & [y,z] in R;
then reconsider x,y,z as Element of S;
x <= z
proof
x = a or x = y by B1,ORDERS_2:def 5,A1;
hence thesis by A1,B1;
end;
hence thesis;
end;
hence thesis;
end;
hence S is transitive;
R is_antisymmetric_in X
proof
x in X & y in X & [x,y] in R & [y,x] in R implies x = y
proof
assume
B1: x in X & y in X & [x,y] in R & [y,x] in R;
then reconsider x,y as Element of S;
x = a or x = y by B1,ORDERS_2:def 5,A1;
hence thesis by A1,B1,ORDERS_2:def 5;
end;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster flat -> lower-bounded for non empty Poset;
coherence
proof
let P be non empty Poset;
assume P is flat; then
consider a be Element of P such that
A1: for x,y being Element of P holds x <= y iff x = a or x = y;
take a;
thus thesis by A1;
end;
end;
reserve S for RelStr;
reserve P,Q for non empty flat Poset;
reserve p,p1,p2 for Element of P;
reserve K for non empty Chain of P;
Lemflat01:
p1 <= p2 iff p1 = Bottom P or p1 = p2
proof
consider a being Element of P such that
A1: for x,y being Element of P holds (x <= y iff x = a or x = y) by Defflat;
a = Bottom P
proof
for x being Element of P holds a <= x by A1;
hence thesis by ThMin02,LemMin01;
end;
hence thesis by A1;
end;
theorem Thflat01:
for P being non empty flat Poset,
K being non empty Chain of P holds
ex a being Element of P st K = {a} or K = {Bottom P, a}
proof
let P be non empty flat Poset,
K be non empty Chain of P;
set z = Bottom P;
per cases;
suppose ex a being Element of K st a <> z;
then consider a being Element of K such that B1:a <> z;
take a;
D1: x in K implies x = z or x = a
proof
assume
E1: x in K;
then reconsider x as Element of P;
x<=a or a<=x by E1,RELAT_2:def 7,ORDERS_2:def 7;
hence thesis by Lemflat01,B1;
end;
K = {a} or K = {z, a}
proof
per cases;
suppose
C1: z in K;
x = z or x = a implies x in K by C1;
hence thesis by D1,TARSKI:def 2;
end;
suppose
C2: not z in K;
D1: x in K implies x = a
proof
assume
E1: x in K;
reconsider x as Element of P by E1;
x<=a or a<=x by E1,RELAT_2:def 7,ORDERS_2:def 7;
hence thesis by B1,E1,C2,Lemflat01;
end;
for x st x = a holds x in K;
hence thesis by D1,TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose
A1: not ex a being Element of K st a <> z;
take z;
B1: x in K implies x = z by A1;
x = z implies x in K
proof
assume
C1: x = z;
the Element of K = z by A1;
hence thesis by C1;
end;
hence thesis by B1,TARSKI:def 1;
end;
end;
Lemflat02:
for K being Chain of P st K is non empty holds ex_sup_of K,P
proof
let K be Chain of P;
assume K is non empty;
then reconsider K as non empty Chain of P;
consider a being Element of P such that
A1: K = {a} or K = {Bottom P, a} by Thflat01;
take a;
per cases by A1;
suppose
B100: K = {a};
B101: for p st p in K holds p <= a by B100,TARSKI:def 1;
B2: for p st K is_<=_than p holds p >= a
proof
let p;
a in K by B100,TARSKI:def 1;
hence thesis;
end;
for p st (K is_<=_than p & for p1 st K is_<=_than p1 holds p1 >= p)
holds p = a
proof
let p;
assume that
C1: K is_<=_than p and
C2: for p1 st K is_<=_than p1 holds p1 >= p;
C3: p >= a by B2,C1;
a >= p by B101,C2,LATTICE3:def 9;
hence thesis by C3,ORDERS_2:2;
end;
hence thesis by B101,B2;
end;
suppose
A2:K = {Bottom P,a};
B101: for p st p in K holds p <= a
proof
let p;
assume p in K;
then p = Bottom P or p = a by A2,TARSKI:def 2;
hence thesis by YELLOW_0:44;
end;
B2: for p st K is_<=_than p holds p >= a
proof
let p;
a in K by A2,TARSKI:def 2;
hence thesis;
end;
for p st (K is_<=_than p &
for p1 st K is_<=_than p1 holds p1 >= p) holds p = a
proof
let p;
assume that
C1: K is_<=_than p and
C2: for p1 st K is_<=_than p1 holds p1 >= p;
C3: p >= a by B2,C1;
a >= p by B101,C2,LATTICE3:def 9;
hence thesis by C3,ORDERS_2:2;
end;
hence thesis by B101,B2;
end;
end;
theorem Thflat05:
for f being Function of P,Q holds
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
let f be Function of P,Q;
consider a being Element of P such that
A1: K = {a} or K = {Bottom P, a} by Thflat01;
take a;
set z = Bottom P;
A3: the carrier of P = dom f by FUNCT_2:def 1;
K = {a,a} or K = {Bottom P, a} by A1,ENUMSET1:29;
then (K = {a,a} & f.:K = {f.a,f.a}) or
(K = {Bottom P, a} & f.:K = {f.(Bottom P), f.a}) by A3,FUNCT_1:60;
hence thesis by ENUMSET1:29;
end;
theorem Thflat0501:
for f being Function of P,Q holds
f.(Bottom P) = Bottom Q implies f is monotone
proof
let f be Function of P,Q;
assume
A1: f.(Bottom P) = Bottom Q;
set z = Bottom P;
for p1,p2 being Element of P st p1 <= p2
for q1,q2 being Element of Q st q1 = f.p1 & q2 = f.p2
holds q1 <= q2
proof
let p1,p2 be Element of P;
assume p1 <= p2;
then p1 = z or p1 = p2 by Lemflat01;
hence thesis by A1,Lemflat01;
end;
hence thesis;
end;
theorem Thflat0502:
K = {Bottom P, p} implies sup K = p
proof
set z = Bottom P;
assume
A0: K = {z,p};
A1: ex_sup_of K,P by Lemflat02;
z <= p & p <= p by YELLOW_0:44; then
A2: K is_<=_than p by YELLOW_0:8,A0;
for p1 st K is_<=_than p1 holds p <= p1 by A0,YELLOW_0:8;
hence thesis by YELLOW_0:def 9,A1,A2;
end;
registration
cluster strict non empty flat chain-complete for Poset;
existence
proof
take the strict non empty flat Poset;
thus thesis by Lemflat02;
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 flat -> chain-complete for Poset;
correctness by Lemflat02;
end;
theorem Thflat07:
for P,Q being strict non empty chain-complete flat Poset,
f being Function of P,Q
st f.(Bottom P) = Bottom Q holds f is continuous
proof
let P,Q be strict non empty chain-complete flat Poset;
let f be Function of P,Q;
assume
A1: f.(Bottom P) = Bottom Q;
then reconsider f as monotone Function of P,Q by Thflat0501;
for K being non empty Chain of P holds f.(sup K) <= sup (f.:K)
proof
let K be non empty Chain of P;
reconsider M = f.:K as non empty Chain of Q by POSET_1:1;
consider a being Element of P such that
B1: (K = {a} & f.:K = {f.a}) or
(K = {Bottom P, a} & f.:K = {f.(Bottom P), f.a}) by Thflat05;
per cases by A1,B1;
suppose K = {a} & M = {f.a};
then sup K =a & sup M = f.a by YELLOW_0:39;
hence thesis;
end;
suppose K = {Bottom P, a} & M = {Bottom Q, f.a};
then sup K = a & sup M = f.a by Thflat0502;
hence thesis;
end;
end;
hence thesis by POSET_1:8;
end;
begin :: Primaries for existence theorem of recursive call using Flatten
reserve X,Y for non empty set;
definition
let X be non empty set;
func FlatRelat(X) -> Relation of succ(X),succ(X) equals
({[X,X]} \/ [:{X},X:]) \/ id X;
correctness
proof
set F = succ(X);
X in {X} by TARSKI:def 1;
then X in F by XBOOLE_0:def 3;
then reconsider R1 = {[X,X]} as Relation of F,F by RELSET_1:3;
A1: {X} c= F by XBOOLE_1:7;
A2: X c= F by XBOOLE_1:7;
[:{X},X:] c= [:{X},X:];
then reconsider R2 = [:{X},X:] as Relation of F,F by A1,A2,RELSET_1:7;
reconsider R3 = R1 \/ R2 as Relation of F,F;
reconsider R4 = id X as Relation of F,F by A2,RELSET_1:7;
R3 \/ R4 is Relation of F,F;
hence thesis;
end;
end;
LemFlatten01:
for x, y being Element of succ(X) st [x,y] in FlatRelat(X) holds
x = X or x = y
proof
let x, y be Element of succ(X);
set a = [x,y];
assume a in FlatRelat(X);
then a in {[X,X]} or a in [:{X},X:] or a in id X by LemSUM01;
then [x,y] = [X,X] or x = X or x = y
by TARSKI:def 1,ZFMISC_1:105,RELAT_1:def 10;
hence thesis by XTUPLE_0:1;
end;
LemFlatten02:
for x, y being Element of succ(X) st
(x = X or x = y) holds [x,y] in FlatRelat(X)
proof
let x, y be Element of succ(X);
assume
A1: x = X or x = y;
A2: x in {X} or x in X by XBOOLE_0:def 3;
A3: y in {X} or y in X by XBOOLE_0:def 3;
set a = [x,y];
per cases by A1;
suppose
B1: x = X;
per cases;
suppose y = X;
then a in {[X,X]} by B1,TARSKI:def 1;
hence thesis by LemSUM01;
end;
suppose y <> X;
then a in [:{X},X:] by B1,ZFMISC_1:105,A3,TARSKI:def 1;
hence thesis by LemSUM01;
end;
end;
suppose
B2: x = y;
per cases;
suppose x = X;
then a in {[X,X]} by B2,TARSKI:def 1;
hence thesis by LemSUM01;
end;
suppose x <> X;
then a in id X by B2,RELAT_1:def 10,A2,TARSKI:def 1;
hence thesis by LemSUM01;
end;
end;
end;
theorem
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) -> strict non empty chain-complete flat Poset equals
RelStr(#succ(X), FlatRelat(X)#);
correctness
proof
reconsider IT = RelStr(#succ(X), FlatRelat(X)#) as non empty RelStr;
X in {X} by TARSKI:def 1;
then reconsider X as Element of IT by XBOOLE_0:def 3;
IT is flat
proof
take X;
thus thesis by LemFlatten01,LemFlatten02;
end;
hence thesis;
end;
end;
theorem ThFlatten04:
for x, y being Element of FlatPoset(X) holds
x <= y iff x = X or x = y by LemFlatten01,LemFlatten02;
theorem LemFlatten05:
X is Element of FlatPoset(X)
proof
X in {X} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
registration
let X;
reduce Bottom FlatPoset(X) to X;
reducibility
proof
set F = FlatPoset(X);
reconsider X as Element of F by LemFlatten05;
for x being Element of F holds X <= x by LemFlatten02;
hence thesis by ThMin02,LemMin01;
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:
f.x if x in X otherwise Y;
correctness;
end;
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:
it.X = Y &
for x being Element of FlatPoset(X) st x <> X holds it.x = f.x;
existence
proof
set z = X;
set r = Y;
A0: not z in X & not r in Y;
set FX = FlatPoset(X);
set CX = succ(X);
z in {z} by TARSKI:def 1; then
A201: z in CX by XBOOLE_0:def 3;
set FY = FlatPoset(Y);
set CY = succ(Y);
r in {r} by TARSKI:def 1;
then
A401: r in CY by XBOOLE_0:def 3;
deffunc H(object) = Flatten(f,$1);
A5: for x st x in CX holds H(x) in CY
proof
let x;
assume x in CX;
per cases;
suppose
B2: x in X;
then C1:H(x) = f.x by DefFlatten01;
f.x in Y by B2,FUNCT_2:5;
hence thesis by C1,XBOOLE_0:def 3;
end;
suppose not x in X;
hence thesis by DefFlatten01,A401;
end;
end;
ex h being Function of CX,CY st for x st x in CX holds h.x = H(x)
from FUNCT_2:sch 2(A5);
then consider IT being Function of CX,CY such that
A6: for x st x in CX holds IT.x = H(x);
reconsider IT as Function of FX,FY;
A7: IT.z = H(z) by A201,A6 .= r by A0,DefFlatten01;
for x being Element of FX st x <> z holds IT.x = f.x
proof
let x be Element of FX;
assume
B1: x <> z;
B3: x in {z} or x in X by XBOOLE_0:def 3;
IT.x = H(x) by A6 .= f.x by DefFlatten01,B1,B3,TARSKI:def 1;
hence thesis;
end;
hence thesis by A7;
end;
uniqueness
proof
set FX = FlatPoset(X);
set FY = FlatPoset(Y);
set CX = succ(X);
set CY = succ(Y);
let IT1,IT2 be Function of FX,FY;
assume
B1: (IT1.X = Y & for x being Element of FX st x <> X holds IT1.x = f.x) &
(IT2.X = Y & for x being Element of FX st x <> X holds IT2.x = f.x);
reconsider IT1,IT2 as Function of CX,CY;
for x be Element of CX holds IT1.x = IT2.x
proof
let x be Element of CX;
per cases;
suppose x = X;
hence thesis by B1;
end;
suppose
C1: x <> X;
then IT1.x = f.x by B1.= IT2.x by C1,B1;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
let X,Y be non empty set;
let f be Function of X,Y;
cluster Flatten f -> continuous;
coherence
proof
(Flatten f).(Bottom FlatPoset(X)) = Bottom FlatPoset(Y) by DefFlatten04;
hence thesis by Thflat07;
end;
end;
theorem
for f being Function of X,Y st
x in X holds (Flatten f).x in Y
proof
let f be Function of X,Y;
assume
A1: x in X; then
reconsider xx = x as set;
A2: not xx in xx;
set FX = FlatPoset(X);
reconsider x as Element of FX by A1,XBOOLE_0:def 3;
f.x in Y by A1,FUNCT_2:5;
hence thesis by DefFlatten04,A1,A2;
end;
definition let X,Y;
func FlatConF(X,Y) -> strict chain-complete non empty Poset equals
ConPoset(FlatPoset(X),FlatPoset(Y));
coherence;
end;
registration let L be flat Poset;
cluster -> finite for Chain of L;
coherence
proof
let A be Chain of L;
per cases;
suppose
A1: A is non empty; then
reconsider LL = L as non empty Poset;
reconsider AA = A as non empty Chain of LL by A1;
ex a being Element of LL st
AA = {a} or AA = {Bottom LL, a} by Thflat01;
hence thesis;
end;
suppose A is empty;
hence thesis;
end;
end;
end;
registration
cluster non empty flat lower-bounded for LATTICE;
existence
proof
set A = {{}};
reconsider R = id A as Relation of A;
reconsider R as Order of A;
take IT = RelStr(#A,R#);
reconsider z = {} as Element of IT by TARSKI:def 1;
ex a being Element of IT st
a is_<=_than the carrier of IT &
(for x,y being Element of IT holds (x <= y iff x = a or x = y))
proof
b1: for x being Element of IT holds z<=x by TARSKI:def 1;
for x,y being Element of IT holds (x <= y iff x = z or x = y)
by TARSKI:def 1;
hence thesis by b1,LemMin01;
end;
hence thesis;
end;
end;
theorem CardA1:
for L being non empty LATTICE,
x being Element of L,
A being Chain of x,x holds
card A = 1
proof
let L be non empty LATTICE,
x be Element of L,
A be Chain of x,x;
for z being Element of L st z in A holds z in {x}
proof
let z be Element of L;
assume z in A; then
x <= z & z <= x by LATTICE7:def 2; then
z = x by ORDERS_2:2;
hence thesis by TARSKI:def 1;
end; then
A c= {x} by LATTICE7:def 1;
hence thesis by CARD_2:42,ZFMISC_1:33;
end;
theorem
for L being non empty flat lower-bounded LATTICE,
x being Element of L,
A being Chain of Bottom L, x holds
card A <= 2
proof
let L be non empty flat lower-bounded LATTICE,
x be Element of L,
A be Chain of Bottom L, x;
S0: Bottom L <= x by YELLOW_0:44;
per cases;
suppose
KK: Bottom L <> x;
consider b being Element of L such that
H1: A = {b} or A = {Bottom L, b} by Thflat01;
H2: x in A & Bottom L in A by LATTICE7:def 2,S0;
A <> {b}
proof
assume A = {b}; then
x = b & b = Bottom L by TARSKI:def 1,H2;
hence thesis by KK;
end;
hence card A <= 2 by CARD_2:50,H1;
end;
suppose Bottom L = x; then
card A = 1 by CardA1;
hence thesis;
end;
end;
theorem
for L being finite lower-bounded antisymmetric non empty LATTICE holds
L is flat iff for x being Element of L holds height x <= 2
proof
let L be finite lower-bounded antisymmetric non empty LATTICE;
hereby assume
A0: L is flat;
let x be Element of L;
S0: Bottom L <= x by YELLOW_0:44;
reconsider D = {Bottom L, x} as Chain of Bottom L, x
by LATTICE7:1,YELLOW_0:44;
per cases;
suppose
KK: Bottom L <> x; then
t1: card D = 2 by CARD_2:57;
for A be Chain of Bottom L, x holds card A <= 2
proof
let A be Chain of Bottom L, x;
consider b being Element of L such that
H1: A = {b} or A = {Bottom L, b} by Thflat01,A0;
H2: x in A & Bottom L in A by LATTICE7:def 2,S0;
A <> {b}
proof
assume A = {b}; then
x = b & b = Bottom L by TARSKI:def 1,H2;
hence thesis by KK;
end;
hence card A <= 2 by CARD_2:50,H1;
end;
hence height x <= 2 by LATTICE7:def 3,t1;
end;
suppose Bottom L = x; then
height x = 1 by LATTICE7:6;
hence height x <= 2;
end;
end;
assume
AA: for x being Element of L holds height x <= 2;
ex a being Element of L st
for x,y being Element of L holds x <= y iff x = a or x = y
proof
take a = Bottom L;
let x,y be Element of L;
hereby assume
AS: x <= y;
per cases;
suppose x = a & y = x;
hence x = a or x = y;
end;
suppose x <> a & y = x;
hence x = a or x = y;
end;
suppose
a1: x <> a & y <> x; then
a < x by YELLOW_0:44; then
height a < height x by LATTICE7:2; then
1 < height x by LATTICE7:6; then
y1: 1 + 1 <= height x by NAT_1:13;
x < y by a1,AS; then
Y2: height x < height y by LATTICE7:2;
height x <= 2 by AA; then
height x = 2 by y1,XXREAL_0:1;
hence x = a or x = y by AA,Y2;
end;
suppose x = a & y <> x;
hence x = a or x = y;
end;
end;
thus thesis by YELLOW_0:44;
end;
hence thesis;
end;
begin :: Existence theorem of recursive call for sigle-equation
reserve D for Subset of X;
reserve I for Function of X,Y;
reserve J for Function of [:X,Y:], Y;
reserve E for Function of X,X;
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
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;
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:
I.x if x in D,
J.[x,y] if (not x in D) & x in X & y in Y
otherwise Y;
correctness;
end;
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),
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
proof
set z = X;
set r = Y;
A0: not z in X & not r in Y;
set FX = FlatPoset(X);
set CX = succ(X);
z in {z} by TARSKI:def 1;
then reconsider z as Element of FX by XBOOLE_0:def 3;
set FY = FlatPoset(Y);
set CY = succ(Y);
r in {r} by TARSKI:def 1; then
A401: r in CY by XBOOLE_0:def 3;
reconsider h as continuous Function of FX,FY by A00;
defpred U[object,object] means
for x being set,
f being continuous Function of FX,FY
st x is Element of FlatPoset(X) & h = f & x = $1 holds
$2 = BaseFunc01(x,f.((Flatten E).x),I,J,D);
deffunc H(object) = BaseFunc01($1,h.((Flatten E).$1),I,J,D);
A5: for x0 being object st x0 in CX ex y being object st y in CY & U[x0,y]
proof
let x0 be object;
assume x0 in CX;
set x1 = h.((Flatten E).x0);
set y = H(x0);
B200: U[x0,y];
per cases;
suppose
B2: x0 in X;
y in CY
proof
per cases;
suppose
B3: x1 in Y; then
C0: [x0,x1] in [:X,Y:] by B2,ZFMISC_1:def 2;
per cases;
suppose x0 in D; then
C01: H(x0) = I.x0 by DefBaseFunc01;
I.x0 in Y by B2,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
suppose not x0 in D; then
C01: H(x0) = J.[x0,x1] by DefBaseFunc01,B2,B3;
J.[x0,x1] in Y by C0,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
end;
suppose
B3: not x1 in Y;
per cases;
suppose x0 in D; then
C01: H(x0) = I.x0 by DefBaseFunc01;
I.x0 in Y by B2,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
suppose not x0 in D;
hence thesis by B3,A401,DefBaseFunc01;
end;
end;
end;
hence thesis by B200;
end;
suppose not x0 in X;
then not (x0 in D or (x0 in X & x1 in Y));
then H(x0) = r by DefBaseFunc01;
hence thesis by A401,B200;
end;
end;
consider IT being Function of CX,CY such that
A6: for x st x in CX holds U[x,IT.x] from FUNCT_2:sch 1(A5);
reconsider IT as Function of FX,FY;
A601:not z in D by A0;
A7: IT.z = BaseFunc01(z,h.((Flatten E).z),I,J,D) by A6
.= r by A0,DefBaseFunc01,A601;
IT.(Bottom FX) = Bottom FY by A7;
then reconsider IT as continuous Function of FX,FY by Thflat07;
take IT;
thus thesis by A6;
end;
uniqueness
proof
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
reconsider h as continuous Function of FX,FY by A00;
for g1,g2 be continuous Function of FX,FY st
((for x being Element of FX,
f being continuous Function of FX,FY st h = f holds
g1.x = BaseFunc01(x,f.((Flatten E).x),I,J,D)) &
(for x being Element of FX,
f being continuous Function of FX,FY st h = f holds
g2.x = BaseFunc01(x,f.((Flatten E).x),I,J,D))) holds g1=g2
proof
let g1,g2 be continuous Function of FX,FY;
assume
B1: (for x being Element of FX,
f being continuous Function of FX,FY st h = f holds
g1.x = BaseFunc01(x,f.((Flatten E).x),I,J,D)) &
(for x being Element of FX,
f being continuous Function of FX,FY st h = f holds
g2.x = BaseFunc01(x,f.((Flatten E).x),I,J,D));
for x being Element of FX holds g1.x=g2.x
proof
let x be Element of FX;
g1.x = BaseFunc01(x,h.((Flatten E).x),I,J,D) by B1
.= g2.x by B1;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem Threcursive01:
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
set z = X;
set r = Y;
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
set FlatC = FlatConF(X,Y);
set CFXY = ConFuncs(FX,FY);
set CRFXY = ConRelat(FX,FY);
deffunc H(object) = RecFunc01($1,E,I,J,D);
::*** lemma A7
A7: for h being continuous Function of FX,FY holds h in CFXY
proof
let h be continuous Function of FX,FY;
h in Funcs(the carrier of FX,the carrier of FY) by FUNCT_2:8;
hence thesis;
end;
::*** lemma A8
A8: for h being set st h in CFXY holds h is continuous Function of FX,FY
proof
let h be set;
assume h in CFXY;
then consider x being Element of
Funcs(the carrier of FX,the carrier of FY) such that
B1: h = x & ex g be continuous Function of FX,FY st g=x;
thus thesis by B1;
end;
A9: for f being object st f in CFXY holds H(f) in CFXY by A7;
ex W being Function of CFXY,CFXY st
for f being object st f in CFXY holds W.f = H(f)
from FUNCT_2:sch 2(A9);
then consider IT being Function of CFXY,CFXY such that
A10:for f being object st f in CFXY holds IT.f = H(f);
IT is continuous Function of FlatC,FlatC
proof
::**preparation using lemma A7,A8
B2: for f being continuous Function of FX,FY holds
ex g being continuous Function of FX,FY st g = IT.f
proof
let f be continuous Function of FX,FY;
set g = IT.f;
f in CFXY by A7;
then reconsider g as continuous Function of FX,FY by A8,FUNCT_2:5;
take g;
thus thesis;
end;
B3: for f,g being continuous Function of FX,FY st g = IT.f holds
for x being Element of FX holds
g.x = BaseFunc01(x,f.((Flatten E).x),I,J,D)
proof
let f,g be continuous Function of FX,FY;
assume
C1: g = IT.f;
for x being Element of FX holds
g.x = BaseFunc01(x,f.((Flatten E).x),I,J,D)
proof
let x be Element of FX;
g.x = RecFunc01(f,E,I,J,D).x by A7,A10,C1
.= BaseFunc01(x,f.((Flatten E).x),I,J,D) by DefRecFunc01;
hence thesis;
end;
hence thesis;
end;
::** proof of continuity of IT as Function of CFXY,CFXY
::* so IT is Function of FlatC,FlatC
reconsider IT as Function of FlatC,FlatC;
IT is monotone
proof
for f1,f2 being Element of FlatC st f1 <= f2
for g1,g2 being Element of FlatC st g1 = IT.f1 & g2 = IT.f2
holds g1 <= g2
proof
let f1,f2 be Element of FlatC such that
C1: f1 <= f2;
let g1,g2 be Element of FlatC such that
C2: g1 = IT.f1 & g2 = IT.f2;
consider f10,f20 be Function of FX,FY such that
C401: f1 = f10 & f2 = f20 & f10 <= f20 by POSET_1:def 7,C1;
reconsider f10,f20 as continuous Function of FX,FY by C401,A8;
reconsider g10 = g1 as continuous Function of FX,FY by A8;
reconsider g20 = g2 as continuous Function of FX,FY by A8;
for x being Element of FX holds g10.x <= g20.x
proof
let x be Element of FX;
reconsider y = (Flatten E).x as Element of FX;
set y1 = f10.y;
set y2 = f20.y;
D1: g10.x = BaseFunc01(x,y1,I,J,D) by B3,C2,C401;
D2: g20.x = BaseFunc01(x,y2,I,J,D) by B3,C2,C401;
per cases by ThFlatten04,C401,YELLOW_2:9;
suppose y1 = r; then
D000: not y1 in Y;
per cases;
suppose
D001: x in D;
then g10.x = I.x by D1,DefBaseFunc01;
hence thesis by D2,D001,DefBaseFunc01;
end;
suppose not x in D;
then g10.x = r by D000,D1,DefBaseFunc01;
hence thesis by LemFlatten02;
end;
end;
suppose y1 = y2;
hence thesis by D1,B3,C2,C401;
end;
end;
then
g10 <= g20 by YELLOW_2:9;
hence thesis by POSET_1:def 7;
end;
hence thesis;
end;
then reconsider IT as monotone Function of FlatC,FlatC;
for F being non empty Chain of FlatC holds IT.(sup F) <= sup (IT.:F)
proof
let F be non empty Chain of FlatC;
reconsider G = IT.:F as non empty Chain of FlatC by POSET_1:1;
IT.(sup F) <= sup G
proof
reconsider F,G as non empty Chain of ConPoset(FX,FY);
set sf = sup F;
D1: sf = sup_func(F) by POSET_1:11;
then reconsider sf as continuous Function of FX,FY;
set sg = sup G;
D3: sg = sup_func(G) by POSET_1:11;
then reconsider sg as continuous Function of FX,FY;
consider g being continuous Function of FX,FY such that
D5: g = IT.sf by B2;
for x being Element of FX holds g.x <= sg.x
proof
let x be Element of FX;
reconsider x1 = (Flatten E).x as Element of FX;
reconsider M = F-image x1 as non empty Chain of FY;
consider a be Element of FY such that
D000: M = {a} or M = {Bottom FY, a} by Thflat01;
D001: sup M = a by D000,YELLOW_0:39,Thflat0502;
D002: g.x = BaseFunc01(x,sf.x1,I,J,D) by B3,D5
.= BaseFunc01(x,a,I,J,D) by D001,POSET_1:def 10,D1;
a in F-image x1 by TARSKI:def 1,TARSKI:def 2,D000;
then consider q1 be Element of FY such that
D003: q1 = a & ex f1 being continuous Function of FX,FY
st f1 in F & q1 =f1.x1;
consider f1 be continuous Function of FX,FY such that
D004: f1 in F & a =f1.x1 by D003;
reconsider f01 = f1 as Element of FlatC by A7;
reconsider g01 = IT.f01 as continuous Function of FX,FY by A8;
D005: g01.x = g.x by B3,D004,D002;
reconsider N = G-image x as non empty Chain of FY;
D006: sg.x = sup N by POSET_1:def 10,D3;
dom IT = CFXY by FUNCT_2:def 1;
then [f01,g01] in IT by FUNCT_1:def 2;
then g01 in IT.:F by RELAT_1:def 13,D004;
then g01.x in N;
hence thesis by D005,Thsup01,D006;
end; then
g <= sg by YELLOW_2:9;
hence thesis by D5,POSET_1:def 7;
end;
hence thesis;
end;
hence thesis by POSET_1:8;
end;
then reconsider IT as continuous Function of FlatC,FlatC;
for f being Element of CFXY holds IT.f = RecFunc01(f,E,I,J,D) by A10;
hence thesis;
end;
theorem Threcursive02:
ex f being set st f in ConFuncs(FlatPoset(X),FlatPoset(Y)) &
f = RecFunc01(f,E,I,J,D)
proof
set FX = FlatPoset(X);
set FY = FlatPoset(Y);
set FlatC = FlatConF(X,Y);
set CFXY = ConFuncs(FX,FY);
set CRFXY = ConRelat(FX,FY);
consider W be continuous Function of FlatC,FlatC such that
A4: for f being Element of CFXY
holds W.f = RecFunc01(f,E,I,J,D) by Threcursive01;
reconsider W as monotone Function of FlatC,FlatC;
reconsider f = least_fix_point(W) as Element of FlatC;
A5: f is_a_fixpoint_of W by POSET_1:def 5;
A6: f = W.f by A5,ABIAN:def 3;
take f;
thus thesis by A4,A6;
end;
theorem Threcursive03:
E is_well_founded_with_minimal_set D implies
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
set z = X;
set r = Y;
assume
A0: E is_well_founded_with_minimal_set D;
A1: not z in X & not r in Y;
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
consider f being set such that
A5: f in ConFuncs(FlatPoset(X),FlatPoset(Y)) &
f = RecFunc01(f,E,I,J,D) by Threcursive02;
reconsider f as continuous Function of FlatPoset(X),FlatPoset(Y) by A5;
consider l be Function of X,NAT such that
A6: for x0 being Element of X holds
(l.x0 <=0 implies x0 in D) &
(not x0 in D implies l.(E.x0) < l.x0) by A0;
defpred P[Nat] means
for x0 being Element of X st l.x0<=$1 holds
(f.x0 in Y & f.x0 = BaseFunc01(x0,f.(E.x0),I,J,D));
A7: P[0]
proof
let x0 be Element of X;
assume
b1:l.x0 <=0;
B2: x0 in X;
reconsider x0 as Element of FX by XBOOLE_0:def 3;
B3: x0 <> z by B2;
B5: f.x0 = BaseFunc01(x0,f.((Flatten E).x0),I,J,D) by DefRecFunc01,A5
.= BaseFunc01(x0,f.(E.x0),I,J,D) by B3,DefFlatten04;
then f.x0 = I.x0 by DefBaseFunc01,b1,A6;
hence thesis by B5,FUNCT_2:5;
end;
A8: for k st P[k] holds P[k + 1]
proof
let k;
assume
B0: P[k];
let x0 be Element of X;
assume
B1: l.x0 <=k+1;
reconsider x0 as Element of FX by XBOOLE_0:def 3;
B3: x0 <> z by A1;
reconsider x1 = E.x0 as Element of X by FUNCT_2:5;
B5: f.x0 = BaseFunc01(x0,f.((Flatten E).x0),I,J,D) by DefRecFunc01,A5
.= BaseFunc01(x0,f.x1,I,J,D) by B3,DefFlatten04;
per cases;
suppose x0 in D;
then f.x0 = I.x0 by DefBaseFunc01,B5;
hence thesis by FUNCT_2:5,B5;
end;
suppose
C0: not x0 in D;
reconsider x0 as Element of X;
l.x1 + 1 <= l.x0 by NAT_1:13,A6,C0;
then l.x1 + 1 <= k + 1 by B1,XXREAL_0:2;
then l.x1 <= k by XREAL_1:8; then
C1: f.x1 in Y by B0;
C4: [x0,f.x1] in [:X,Y:] by C1,ZFMISC_1:def 2;
J.[x0,f.x1] in Y by C4,FUNCT_2:5;
hence thesis by B5,DefBaseFunc01,C0,C1;
end;
end;
A9: for k being Nat holds P[k] from NAT_1:sch 2(A7,A8);
for x being Element of X holds
f.x in Y & f.x = BaseFunc01(x,f.(E.x),I,J,D)
proof
let x be Element of X;
reconsider k = l.x as Nat;
l.x <= k;
hence thesis by A9;
end;
hence thesis;
end;
:: Under these preparations, we get the following theorem.
::
:: If E is_well_founded_with_minimal_set D, there is a (unique) function f:X->Y and
:: f satisfies the recursive condition
:: f.x = I.x if x in D :: initial condition
:: = J.[x, f.(E.x)] otherwise :: recursive condition
::
:: Example of using this theorem:
:: let X = Y = NAT, D = {0}, I.0 = 1 , J.[x,y] = x*y.
:: let l(x) = x and E(x) = x if x = 0 otherwise x-1
:: then E is_well_founded_with_minimal_set D
:: then there exist function f such that f.0 = 1 and f.x = x*f(x-1) if x <>0.
:: this means there exist factorial function.
Lemrecursive04:
E is_well_founded_with_minimal_set D implies
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
assume
A1: E is_well_founded_with_minimal_set D;
set FX = FlatPoset(X);
set CX = succ(X);
A02:X c= CX by XBOOLE_1:7;
set FY = FlatPoset(Y);
set CY = succ(Y);
consider f1 being continuous Function of FX,FY such that
A3: for x being Element of X
holds (f1.x in Y & f1.x = BaseFunc01(x,f1.(E.x),I,J,D))
by A1,Threcursive03;
reconsider f1 as Function of CX,CY;
reconsider f = f1|X as Function of X,CY by A02,FUNCT_2:32;
for x being Element of X holds f.x in Y
proof
let x be Element of X;
f1.x in Y by A3;
hence thesis by FUNCT_1:49;
end;
then rng f c= Y by FUNCT_2:114;
then reconsider f as Function of X,Y by FUNCT_2:6;
for x being Element of X holds f.x = BaseFunc01(x,f.(E.x),I,J,D)
proof
let x be Element of X;
reconsider x1 = E.x as Element of X;
f.x = f1.x by FUNCT_1:49
.= BaseFunc01(x,f1.x1,I,J,D) by A3;
hence thesis by FUNCT_1:49;
end;
hence thesis;
end;
:: Existence
theorem
E is_well_founded_with_minimal_set D implies
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
assume E is_well_founded_with_minimal_set D;
then consider f being Function of X,Y such that
A1: for x being Element of X holds f.x = BaseFunc01(x,f.(E.x),I,J,D)
by Lemrecursive04;
take f;
let x be Element of X;
f.x = BaseFunc01(x,f.(E.x),I,J,D) by A1;
hence thesis by DefBaseFunc01;
end;
:: Uniqueness
theorem
for f1,f2 being Function of X,Y holds
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)]))
implies f1 = f2
proof
let f1,f2 be Function of X,Y;
assume
A0: 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)])); then
consider l be Function of X,NAT such that
A1: for x being Element of X holds
(l.x <= 0 implies x in D) &
(not x in D implies l.(E.x) < l.x);
defpred P[Nat] means
for x being Element of X st l.x<=$1 holds f1.x = f2.x;
A2: P[0]
proof
let x be Element of X;
assume b1: l.x <= 0; then
f1.x = I.x by A0,A1
.= f2.x by A0,b1,A1;
hence thesis;
end;
A3: for k st P[k] holds P[k + 1]
proof
let k;
assume
B0: P[k];
let x be Element of X;
assume
B1: l.x <=k+1;
per cases;
suppose
C0: x in D;
f1.x = I.x by A0,C0
.= f2.x by A0,C0;
hence thesis;
end;
suppose
C0: not x in D;
reconsider x1 = E.x as Element of X;
reconsider x as Element of X;
l.x1 + 1 <= l.x by NAT_1:13,A1,C0;
then c2: l.x1 + 1 <= k + 1 by B1,XXREAL_0:2;
f1.x = J.[x,f1.x1] by A0,C0
.= J.[x,f2.x1] by c2,B0,XREAL_1:8
.= f2.x by A0,C0;
hence thesis;
end;
end;
A4: for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
for x being Element of X holds f1.x = f2.x
proof
let x be Element of X;
reconsider k = l.x as Nat;
l.x <= k;
hence thesis by A4;
end;
hence thesis;
end;
begin :: Existence theorem of recursive calls for 2-equations
reserve D for Subset of X;
reserve I,I1,I2 for Function of X,Y;
reserve J,J1,J2 for Function of [:X,Y,Y:], Y;
reserve E1,E2 for Function of X,X;
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
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;
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:
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;
end;
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,
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
proof
set z = X;
set r = Y;
A0: not X in X & not Y in Y;
set FX = FlatPoset(X);
set CX = succ(X);
z in {z} by TARSKI:def 1;
then reconsider z as Element of FX by XBOOLE_0:def 3;
set FY = FlatPoset(Y);
set CY = succ(Y);
Y in {Y} by TARSKI:def 1; then
A401: Y in CY by XBOOLE_0:def 3;
reconsider h1,h2 as continuous Function of FX,FY by A00;
defpred U[object,object] means for x being set,
f1,f2 being continuous Function of FX,FY
st x is Element of FlatPoset(X) & h1 = f1 & h2 =f2 & x = $1
holds
$2 = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D);
deffunc H(object)
= BaseFunc02($1,h1.((Flatten E1).$1),h2.((Flatten E2).$1),I,J,D);
A5: for x0 being object st x0 in CX ex y st y in CY & U[x0,y]
proof
let x0 be object;
assume x0 in CX;
set x1 = h1.((Flatten E1).x0);
set x2 = h2.((Flatten E2).x0);
set y = H(x0);
B200: U[x0,y];
per cases;
suppose
B2: x0 in X;
y in CY
proof
per cases;
suppose
B3: x1 in Y & x2 in Y; then
C0: [x0,x1,x2] in [:X,Y,Y:] by B2,MCART_1:69;
per cases;
suppose x0 in D; then
C01: H(x0) = I.x0 by DefBaseFunc02;
I.x0 in Y by B2,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
suppose not x0 in D; then
C01: H(x0) = J.[x0,x1,x2] by DefBaseFunc02,B2,B3;
J.[x0,x1,x2] in Y by C0,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
end;
suppose
B3: not (x1 in Y & x2 in Y);
per cases;
suppose x0 in D; then
C01: H(x0) = I.x0 by DefBaseFunc02;
I.x0 in Y by B2,FUNCT_2:5;
hence thesis by C01,XBOOLE_0:def 3;
end;
suppose not x0 in D;
hence thesis by A401,DefBaseFunc02,B3;
end;
end;
end;
hence thesis by B200;
end;
suppose not x0 in X;
then not ((x0 in D) or (x0 in X & x1 in Y & x2 in Y));
then H(x0) = Y by DefBaseFunc02;
hence thesis by A401,B200;
end;
end;
consider IT being Function of CX,CY such that
A6: for x being object st x in CX holds U[x,IT.x] from FUNCT_2:sch 1(A5);
reconsider IT as Function of FX,FY;
A7: not z in D by A0;
A8: IT.z = BaseFunc02(z,h1.((Flatten E1).z),h2.((Flatten E2).z),I,J,D) by A6
.= r by A0,DefBaseFunc02,A7;
IT.(Bottom FX) = Bottom FY by A8;
then reconsider IT as continuous Function of FX,FY by Thflat07;
take IT;
thus thesis by A6;
end;
uniqueness
proof
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
reconsider h1,h2 as continuous Function of FX,FY by A00;
for g1,g2 be continuous Function of FX,FY st
((for x being Element of FX,
f1,f2 being continuous Function of FX,FY
st h1 = f1 & h2 = f2 holds
g1.x = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D)) &
(for x being Element of FX,
f1,f2 being continuous Function of FX,FY
st h1 = f1 & h2 = f2 holds
g2.x = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D)) )
holds g1=g2
proof
let g1,g2 be continuous Function of FX,FY;
assume
B1: (for x being Element of FX,
f1,f2 being continuous Function of FX,FY
st h1 = f1 & h2 = f2 holds
g1.x = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D)) &
(for x being Element of FX,
f1,f2 being continuous Function of FX,FY
st h1 = f1 & h2 = f2 holds
g2.x = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D));
for x being Element of FX holds g1.x=g2.x
proof
let x be Element of FX;
g1.x = BaseFunc02(x,h1.((Flatten E1).x),h2.((Flatten E2).x),I,J,D)
by B1
.= g2.x by B1;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem Threcursive0101:
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
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
set FlatC = FlatConF(X,Y);
set CFXY = ConFuncs(FX,FY);
set CRFXY = ConRelat(FX,FY);
set FlatC2 = [:FlatC,FlatC:];
set CFXY2 = [:CFXY,CFXY:];
set CRFXY2 = ["CRFXY,CRFXY"];
A6: the carrier of FlatC2 = CFXY2 &
the InternalRel of FlatC2 = CRFXY2 by YELLOW_3:def 2;
deffunc H(object) = RecFunc02($1`1,$1`2,E1,E2,I,J,D);
::*** lemma A7
A7: for h being continuous Function of FX,FY holds h in CFXY
proof
let h be continuous Function of FX,FY;
h in Funcs(the carrier of FX,the carrier of FY) by FUNCT_2:8;
hence thesis;
end;
::*** lemma A8
A8: for h being set st h in CFXY holds h is continuous Function of FX,FY
proof
let h be set;
assume h in CFXY;
then consider
x being Element of Funcs(the carrier of FX,the carrier of FY)
such that
B1: h = x & ex g be continuous Function of FX,FY st g=x;
thus thesis by B1;
end;
A801:for h being Element of FlatC2 holds
ex h1,h2 being continuous Function of FX,FY st h = [h1,h2]
proof
let h be Element of FlatC2;
B1:h is Element of CFXY2 by YELLOW_3:def 2;
reconsider h1 = h`1, h2 = h`2 as continuous Function of FX,FY by A8;
take h1,h2;
consider xx,y being object such that
hh: xx in CFXY & y in CFXY & h = [xx,y] by ZFMISC_1:def 2,B1;
thus thesis by hh;
end;
A9: for f being object st f in CFXY2 holds H(f) in CFXY by A7;
ex W being Function of CFXY2,CFXY st
for f being object st f in CFXY2 holds W.f = H(f) from FUNCT_2:sch 2(A9);
then consider IT being Function of CFXY2,CFXY such that
A10:for f being object st f in CFXY2 holds IT.f = H(f);
IT is continuous Function of FlatC2,FlatC
proof
::**preparation using lemma A7,A8
B1: for f1,f2 being continuous Function of FX,FY holds
IT.[f1,f2] = H([f1,f2])
proof
let f1,f2 be continuous Function of FX,FY;
set f = [f1,f2];
f1 in CFXY & f2 in CFXY by A7;
then f in CFXY2 by ZFMISC_1:def 2;
hence thesis by A10;
end;
B2: for f1,f2 being continuous Function of FX,FY holds
ex g being continuous Function of FX,FY st g = IT.[f1,f2]
proof
let f1,f2 be continuous Function of FX,FY;
set f = [f1,f2];
f1 in CFXY & f2 in CFXY by A7;
then C1:f in CFXY2 by ZFMISC_1:def 2;
reconsider g = IT.f as continuous Function of FX,FY
by A8,C1,FUNCT_2:5;
take g;
thus thesis;
end;
B3: for f1,f2 being continuous Function of FX,FY
for g being continuous Function of FX,FY st g = IT.[f1,f2] holds
for x being Element of FX holds
((g.x =
BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D))
&
(x in D implies g.x = I.x))
proof
let f1,f2 be continuous Function of FX,FY;
let g be continuous Function of FX,FY;
assume
C1: g = IT.[f1,f2];
let x be Element of FX;
[f1,f2]`1 = f1 & [f1,f2]`2 = f2; then
g.x= RecFunc02(f1,f2,E1,E2,I,J,D).x by B1,C1
.= BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D)
by DefRecFunc02;
hence thesis by DefBaseFunc02;
end;
::** proof of continuity of IT
::* IT being Function of CFXY2,CFXY,
::* so IT be considered as Function of FlatC2,FlatC
reconsider IT as Function of FlatC2,FlatC by A6;
IT is monotone
proof
let f1,f2 be Element of FlatC2 such that
C1: f1 <= f2;
let g1,g2 be Element of FlatC such that
C2: g1 = IT.f1 & g2 = IT.f2;
reconsider f101 = f1`1, f102 = f1`2, f201 = f2`1, f202 = f2`2
as Element of FlatC;
[f101,f201] in CRFXY by ORDERS_2:def 5,C1,YELLOW_3:12;
then consider f1011,f2011 be Function of FX,FY such that
C301:f101 = f1011 & f201 = f2011 &
f1011 <= f2011 by POSET_1:def 7;
reconsider f1011,f2011 as continuous Function of FX,FY by C301,A8;
[f102,f202] in CRFXY by ORDERS_2:def 5,C1,YELLOW_3:12;
then consider f1021,f2021 be Function of FX,FY such that
C401:f102 = f1021 & f202 = f2021 &
f1021 <= f2021 by POSET_1:def 7;
reconsider f1021,f2021 as continuous Function of FX,FY by C401,A8;
reconsider g10 = g1, g20 = g2 as continuous Function of FX,FY by A8;
for x being Element of FX holds g10.x <= g20.x
proof
let x be Element of FX;
reconsider y01 = (Flatten E1).x, y02 = (Flatten E2).x
as Element of FX;
set y1 = f1011.y01;
set y2 = f2011.y01;
set y3 = f1021.y02;
set y4 = f2021.y02;
f1 in the carrier of [:FlatC,FlatC:]; then
f1 in [:the carrier of FlatC,the carrier of FlatC:]
by YELLOW_3:def 2; then
consider xx,y being object such that
hh: xx in the carrier of FlatC & y in the carrier of FlatC &
f1 = [xx,y] by ZFMISC_1:def 2;
D1: g10 = IT.[f1011,f1021] by C2,C401,hh,C301;
D101: g10.x = BaseFunc02(x,y1,y3,I,J,D) by B3,C2,C401,hh,C301;
f2 in the carrier of [:FlatC,FlatC:]; then
f2 in [:the carrier of FlatC,the carrier of FlatC:]
by YELLOW_3:def 2; then
consider xx,y being object such that
hh: xx in the carrier of FlatC & y in the carrier of FlatC &
f2 = [xx,y] by ZFMISC_1:def 2;
D2: g20 = IT.[f2011,f2021] by C2,C401,C301,hh;
per cases by ThFlatten04,C301,YELLOW_2:9;
suppose y1 = Y; then
D301: not y1 in Y;
per cases;
suppose
D302: x in D;
then g10.x = I.x by D1,B3;
hence thesis by D2,B3,D302;
end;
suppose not x in D;
then g10.x = Y by D301,D101,DefBaseFunc02;
hence thesis by LemFlatten02;
end;
end;
suppose
D304: y1 = y2;
per cases by C401,YELLOW_2:9,ThFlatten04;
suppose y3 = Y; then
D305: not y3 in Y;
per cases;
suppose
D306: x in D;
then g10.x = I.x by D1,B3;
hence thesis by D2,B3,D306;
end;
suppose not x in D;
then g10.x = Y by D305,D101,DefBaseFunc02;
hence thesis by LemFlatten02;
end;
end;
suppose y3 = y4;
hence thesis by D101,C2,C401,C301,hh,B3,D304;
end;
end;
end; then
g10 <= g20 by YELLOW_2:9;
hence thesis by POSET_1:def 7;
end;
then reconsider IT as monotone Function of FlatC2,FlatC;
for F being non empty Chain of FlatC2 holds IT.(sup F) <= sup (IT.:F)
proof
let F be non empty Chain of FlatC2;
reconsider G = IT.:F as non empty Chain of FlatC by POSET_1:1;
IT.(sup F) <= sup G
proof
reconsider
F as non empty Chain of [:ConPoset(FX,FY),ConPoset(FX,FY):];
reconsider G as non empty Chain of ConPoset(FX,FY);
D101: sup (proj1 F) = sup_func(proj1 F) by POSET_1:11;
then reconsider sf1 = sup (proj1 F) as continuous Function of FX,FY;
D102: sup (proj2 F) = sup_func(proj2 F) by POSET_1:11;
then reconsider sf2 = sup (proj2 F) as continuous Function of FX,FY;
D103: sup F = [sf1, sf2] by YELLOW_3:46,LemProdPoset06;
set sg = sup G;
D3: sg = sup_func(G) by POSET_1:11;
then reconsider sg as continuous Function of FX,FY;
D4: for x being Element of FX st x in D holds sg.x = I.x
proof
let x be Element of FX;
assume
D401: x in D;
reconsider N = G-image x as non empty Chain of FY;
set h = the Element of G;
reconsider h as continuous Function of FX,FY by A8;
reconsider hx = h.x as Element of FY;
D402: hx in N;
consider f be Element of CFXY2 such that
D403: f in F & h = IT.f by FUNCT_2:65;
reconsider f as Element of FlatC2 by D403;
consider f1,f2 being continuous Function of FX,FY such that
D404: f =[f1,f2] by A801;
D405: hx = I.x by B3,D401,D403,D404;
then hx in Y by FUNCT_2:5,D401;
then hx <> Y;
then sup N = hx by ThFlatten04,D402,Thsup01;
hence thesis by D405,POSET_1:def 10,D3;
end;
consider g being continuous Function of FX,FY such that
D5: g = IT.[sf1,sf2] by B2;
for x being Element of FX holds g.x <= sg.x
proof::**************
let x be Element of FX;
reconsider x1 = (Flatten E1).x, x2 = (Flatten E2).x
as Element of FX;
reconsider M1 = proj1 F -image x1, M2 = proj2 F -image x2
as non empty Chain of FY;
consider a1 be Element of FY such that
E401: M1 = {a1} or M1 = {Bottom FY, a1} by Thflat01;
E402: sup M1 = a1
proof
per cases by E401;
suppose M1 = {a1};
hence thesis by YELLOW_0:39;
end;
suppose M1 = {Bottom FY,a1};
hence thesis by Thflat0502;
end;
end;
consider a2 be Element of FY such that
E403: M2 = {a2} or M2 = {Bottom FY, a2} by Thflat01;
E404: sup M2 = a2
proof
per cases by E403;
suppose M2 = {a2};
hence thesis by YELLOW_0:39;
end;
suppose M2 = {Bottom FY,a2};
hence thesis by Thflat0502;
end;
end;
E0: sf1.x1 = a1 & sf2.x2 = a2
by POSET_1:def 10,D101,D102,E402,E404;
E1: g.x = BaseFunc02(x,a1,a2,I,J,D) by B3,D5,E0;
E500: a1 in proj1 F-image x1 & a2 in proj2 F-image x2
by TARSKI:def 1,TARSKI:def 2,E401,E403;
consider q1 be Element of FY such that
E501: q1 = a1 & ex f1 being continuous Function of FX,FY
st f1 in proj1 F & q1 =f1.x1 by E500;
consider q2 be Element of FY such that
E502: q2 = a2 & ex f2 being continuous Function of FX,FY
st f2 in proj2 F & q2 =f2.x2 by E500;
per cases;
suppose
E503: not x in D;
per cases;
suppose
E504: a1 <> Y & a2 <> Y;
ex f1,f2 be continuous Function of FX,FY st
[f1,f2] in F & a1 =f1.x1 & a2 =f2.x2
proof
consider f1,f2 be continuous Function of FX,FY such that
E600: f1 in proj1 F & a1 =f1.x1 &
f2 in proj2 F & a2 =f2.x2 by E501,E502;
consider f12 be object such that
E601: [f1,f12] in F by E600,XTUPLE_0:def 12;
[f1,f12]`2 in CFXY by MCART_1:10,A6,E601;
then reconsider f12 as continuous Function of FX,FY by A8;
consider f21 be object such that
E602: [f21,f2] in F by E600,XTUPLE_0:def 13;
[f21,f2]`1 in CFXY by MCART_1:10,A6,E602;
then reconsider f21 as continuous Function of FX,FY by A8;
reconsider f1F = f1, f12F = f12, f2F = f2, f21F = f21
as Element of FlatC by A7;
reconsider h1 = [f1F,f12F], h2 = [f21F,f2F] as Element of F
by E601,E602;
reconsider h1,h2 as Element of FlatC2;
per cases by ORDERS_2:11;
suppose h1 <= h2;
then f1F <= f21F by YELLOW_3:11;
then consider f,g being Function of FX,FY such that
G001:f1=f & f21=g & f <= g by POSET_1:def 7;
take f21,f2;
thus thesis by E602,E600,E504,
ThFlatten04,YELLOW_2:9,G001;
end;
suppose h2 <= h1;
then f2F <= f12F by YELLOW_3:11;
then consider f,g being Function of FX,FY such that
G001:f2=f & f12=g & f <= g by POSET_1:def 7;
take f1,f12;
thus thesis by E601,E600,E504,ThFlatten04,
YELLOW_2:9,G001;
end;
end;
then consider f1,f2 be continuous Function of FX,FY such that
E6: [f1,f2] in F & a1 =f1.x1 & a2 =f2.x2;
f1 in CFXY & f2 in CFXY by A7;
then reconsider f01 = [f1,f2] as Element of FlatC2
by ZFMISC_1:def 2,A6;
reconsider g01 = IT.f01 as continuous Function of FX,FY
by A8;
E7: g01.x = g.x by B3,E6,E1;
reconsider N = G-image x as non empty Chain of FY;
E9: sg.x = sup N by POSET_1:def 10,D3;
dom IT = CFXY2 by FUNCT_2:def 1;
then [f01,g01] in IT by FUNCT_1:def 2,A6;
then g01 in IT.:F by RELAT_1:def 13,E6;
then g01.x in N;
hence thesis by E7,Thsup01,E9;
end;
suppose a1 = Y or a2 = Y;
then not (a1 in Y & a2 in Y);
then g.x = Y by E1,DefBaseFunc02,E503;
hence thesis by LemFlatten02;
end;
end;
suppose
E506: x in D;
then sg.x = I.x by D4 .= g.x by E506,B3,D5;
hence thesis;
end;
end;::***********g.x <= sg.x
then g <= sg by YELLOW_2:9;
hence thesis by D5,D103,POSET_1:def 7;
end;
hence thesis;
end;
hence thesis by POSET_1:8;
end;
then reconsider IT as continuous Function of FlatC2,FlatC;
for f being set st f in CFXY2
holds IT.f = RecFunc02(f`1,f`2,E1,E2,I,J,D) by A10;
hence thesis;
end;
theorem Threcursive0201:
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
set FX = FlatPoset(X);
set FY = FlatPoset(Y);
set FlatC = FlatConF(X,Y);
set CFXY = ConFuncs(FX,FY);
set CRFXY = ConRelat(FX,FY);
set FlatC2 = [:FlatC,FlatC:];
set CFXY2 = [:CFXY,CFXY:];
set CRFXY2 = ["CRFXY,CRFXY"];
A4: the carrier of FlatC2 = CFXY2 &
the InternalRel of FlatC2 = CRFXY2 by YELLOW_3:def 2;
consider W1 be continuous Function of FlatC2,FlatC such that
A5: for h being set st h in CFXY2
holds W1.h = RecFunc02(h`1,h`2,E1,E2,I1,J1,D)
by Threcursive0101;
consider W2 be continuous Function of FlatC2,FlatC such that
A6: for h being set st h in CFXY2
holds W2.h = RecFunc02(h`1,h`2,E1,E2,I2,J2,D)
by Threcursive0101;
reconsider W = <:W1,W2:> as continuous Function of FlatC2,FlatC2
by YELLOW_3:def 2;
reconsider h = least_fix_point(W) as Element of FlatC2;
h is_a_fixpoint_of W by POSET_1:def 5; then
A7: h = W.h by ABIAN:def 3;
A8: W1.h = RecFunc02(h`1,h`2,E1,E2,I1,J1,D) &
W2.h = RecFunc02(h`1,h`2,E1,E2,I2,J2,D) by A4,A5,A6;
consider f,g being Element of FlatC such that
A9: h = [f,g] by ThProdPoset01;
take f,g;
dom W = (the carrier of FlatC2) by FUNCT_2:def 1; then
[f,g] = [RecFunc02(f,g,E1,E2,I1,J1,D),
RecFunc02(f,g,E1,E2,I2,J2,D) ] by FUNCT_3:def 7,A7,A8,A9;
hence thesis by XTUPLE_0:1;
end;
theorem Threcursive0301:
E1,E2 is_well_founded_with_minimal_set D implies
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
assume
A1: E1,E2 is_well_founded_with_minimal_set D;
A2: not X in X & not Y in Y;
set FX = FlatPoset(X);
set CX = succ(X);
set FY = FlatPoset(Y);
set CY = succ(Y);
consider f,g being set such that
A7: 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) by Threcursive0201;
reconsider f,g as continuous Function of FlatPoset(X),FlatPoset(Y) by A7;
take f,g;
consider l be Function of X,NAT such that
A801: for x0 being Element of X holds
(l.x0 <=0 implies x0 in D) &
( not x0 in D implies l.(E1.x0) < l.x0 & l.(E2.x0) < l.x0) by A1;
defpred P[Nat] means
for x1,x2 being Element of X
st l.x1<=$1 & l.x2<=$1 holds
(f.x1 in Y & f.x1 = BaseFunc02(x1,f.(E1.x1),g.(E2.x1),I1,J1,D) &
g.x2 in Y & g.x2 = BaseFunc02(x2,f.(E1.x2),g.(E2.x2),I2,J2,D));
A9: P[0]
proof
let x1,x2 be Element of X;
assume b1: l.x1<= 0 & l.x2<= 0;
B2: x1 in X & x2 in X;
reconsider x1,x2 as Element of FX by XBOOLE_0:def 3;
x1 <> X & x2 <> X by B2; then
B4: f.((Flatten E1).x1) = f.(E1.x1) &
g.((Flatten E2).x1) = g.(E2.x1) &
f.((Flatten E1).x2) = f.(E1.x2) &
g.((Flatten E2).x2) = g.(E2.x2) by DefFlatten04;
f.x1 = BaseFunc02(x1,f.(E1.x1),g.(E2.x1),I1,J1,D) by A7,DefRecFunc02,B4;
then
B6: f.x1 = I1.x1 by DefBaseFunc02,b1,A801;
g.x2 = BaseFunc02(x2,f.(E1.x2),g.(E2.x2),I2,J2,D) by A7,DefRecFunc02,B4;
then g.x2 = I2.x2 by DefBaseFunc02,b1,A801;
hence thesis by A7,DefRecFunc02,B4,FUNCT_2:5,B6;
end;
A10: for k st P[k] holds P[k + 1]
proof
let k;
assume
B0: P[k];
let x01,x02 be Element of X;
assume
B1: l.x01 <=k+1 & l.x02 <=k+1;
reconsider x01,x02 as Element of FX by XBOOLE_0:def 3;
x01 <> X & x02 <> X by A2; then
B4: f.((Flatten E1).x01) = f.(E1.x01) &
g.((Flatten E2).x01) = g.(E2.x01) &
f.((Flatten E1).x02) = f.(E1.x02) &
g.((Flatten E2).x02) = g.(E2.x02) by DefFlatten04;
set x11 = E1.x01;
set x21 = E2.x01;
set x12 = E1.x02;
set x22 = E2.x02;
reconsider x11,x12,x21,x22 as Element of X by FUNCT_2:5;
B501: f.x01 = BaseFunc02(x01,f.x11,g.x21,I1,J1,D) by A7,DefRecFunc02,B4;
B502: g.x02 = BaseFunc02(x02,f.x12,g.x22,I2,J2,D) by A7,DefRecFunc02,B4;
reconsider x01,x02 as Element of X;
per cases;
suppose x01 in D; then
C2: f.x01 = I1.x01 by DefBaseFunc02,B501;
per cases;
suppose x02 in D;
then g.x02 = I2.x02 by DefBaseFunc02,B502;
hence thesis by C2,A7,DefRecFunc02,B4;
end;
suppose
C01: not x02 in D;
then l.x12 + 1 <= l.x02 & l.x22 + 1 <= l.x02
by NAT_1:13,A801;
then l.x12 + 1 <= k + 1 & l.x22 + 1 <= k + 1 by B1,XXREAL_0:2;
then l.x12 <= k & l.x22 <= k by XREAL_1:8;
then
C04: f.x12 in Y & g.x22 in Y by B0;
C06: g.x02 = J2.[x02,f.x12,g.x22] by B502,DefBaseFunc02,C01,C04;
[x02,f.x12,g.x22] in [:X,Y,Y:] by C04,MCART_1:69;
hence thesis by C2,C06,A7,DefRecFunc02,B4,FUNCT_2:5;
end;
end;
suppose
C1: not x01 in D;
then l.x11 + 1 <= l.x01 & l.x21 + 1 <= l.x01 by NAT_1:13,A801;
then l.x11 + 1 <= k + 1 & l.x21 + 1 <= k + 1 by B1,XXREAL_0:2;
then l.x11 <= k & l.x21 <= k by XREAL_1:8; then
C4: f.x11 in Y & g.x21 in Y by B0; then
C6: f.x01 = J1.[x01,f.x11,g.x21] by B501,DefBaseFunc02,C1;
C7: [x01,f.x11,g.x21] in [:X,Y,Y:] by C4,MCART_1:69;
per cases;
suppose x02 in D;
then g.x02 = I2.x02 by DefBaseFunc02,B502;
hence thesis by C6,C7,FUNCT_2:5,A7,DefRecFunc02,B4;
end;
suppose
C01: not x02 in D;
then l.x12 + 1 <= l.x02 & l.x22 + 1 <= l.x02 by NAT_1:13,A801;
then l.x12 + 1 <= k + 1 & l.x22 + 1 <= k + 1 by B1,XXREAL_0:2;
then l.x12 <= k & l.x22 <= k by XREAL_1:8;
then
C04: f.x12 in Y & g.x22 in Y by B0;
C06: g.x02 = J2.[x02,f.x12,g.x22] by B502,DefBaseFunc02,C01,C04;
[x02,f.x12,g.x22] in [:X,Y,Y:] by C04,MCART_1:69;
hence thesis by C6,C7,C06,A7,DefRecFunc02,B4,FUNCT_2:5;
end;
end;
end;
A11: for k being Nat holds P[k] from NAT_1:sch 2(A9,A10);
for x1,x2 being Element of X holds
f.x1 in Y & f.x1 = BaseFunc02(x1,f.(E1.x1),g.(E2.x1),I1,J1,D) &
g.x2 in Y & g.x2 = BaseFunc02(x2,f.(E1.x2),g.(E2.x2),I2,J2,D)
proof
let x1,x2 be Element of X;
reconsider k = l.x1 + l.x2 as Nat;
l.x1 <= k & l.x2 <= k by NAT_1:11;
hence thesis by A11;
end;
hence thesis;
end;
:: Under these preparations, we get the following theorem.
::
:: If E1,E2 is_well_founded_with_minimal_set D,there are only two functions
:: f,g:X->Y such that
:: f and g satisfy the recursive condition
:: f.x = I1.x if x in D ::initial condition
:: = J1.[x, f.(E1.x), g.(E2.x)] otherwise ::recursive condition
:: g.x = I2.x if x in D ::initial condition
:: = J2.[x, f.(E1.x), g.(E2.x)] otherwise ::recursive condition
::
:: Example:
:: Let X be the set of binary trees, and D be the set of leaf nodes.
:: For x be binary tree in X, let E1.x be the left side subtree of x,
:: E2.x be the right side sub tree of x, and
:: l(x) be the amount of nodes under x as the root node of tree.
:: Then E1,E2 is_well_founded_with_minimal_set D
:: Above theorem is used to define the evaluate functions f,g
:: for the binary tree(x), when the treatments of
:: E1.x and E2.x are different (i.e. f <> g).
Lemrecursive0401:
E1,E2 is_well_founded_with_minimal_set D implies
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
assume
A1: E1,E2 is_well_founded_with_minimal_set D;
set FX = FlatPoset(X);
set CX = succ(X);
A02:X c= CX by XBOOLE_1:7;
set FY = FlatPoset(Y);
set CY = succ(Y);
consider f,g being continuous Function of FX,FY such that
A3: 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))
by A1,Threcursive0301;
reconsider f,g as Function of CX,CY;
reconsider fX = f|X, gX = g|X as Function of X,CY by A02,FUNCT_2:32;
for x being Element of X holds fX.x in Y & gX.x in Y
proof
let x be Element of X;
f.x in Y & g.x in Y by A3;
hence thesis by FUNCT_1:49;
end;
then rng fX c= Y & rng gX c= Y by FUNCT_2:114;
then reconsider fX,gX as Function of X,Y by FUNCT_2:6;
take fX,gX;
let x be Element of X;
reconsider x1 = E1.x, x2 = E2.x as Element of X;
B2: fX.x1 = f.x1 & gX.x2 = g.x2 by FUNCT_1:49;
B3: fX.x = f.x by FUNCT_1:49
.= BaseFunc02(x,fX.x1,gX.x2,I1,J1,D) by A3,B2;
gX.x = g.x by FUNCT_1:49
.= BaseFunc02(x,f.x1,g.x2,I2,J2,D) by A3;
hence thesis by B2,B3;
end;
:: Existence
theorem Threcursive05:
E1,E2 is_well_founded_with_minimal_set D implies
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
assume E1,E2 is_well_founded_with_minimal_set D;
then consider f,g being Function of X,Y such that
A1: 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) by Lemrecursive0401;
take f,g;
let x be Element of X;
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) by A1;
hence thesis by DefBaseFunc02;
end;
:: Uniqueness
theorem
for f1,g1,f2,g2 being Function of X,Y holds
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)]) )
implies f1 = f2 & g1 = g2
proof
let f1,g1,f2,g2 be Function of X,Y;
assume
A0: 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)]) ); then
consider l be Function of X,NAT such that
A1: 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);
defpred P[Nat] means
for x being Element of X st l.x<=$1 holds f1.x = f2.x & g1.x = g2.x;
A2: P[0]
proof
let x be Element of X;
assume l.x <= 0; then
B1: x in D by A1;
B2: f1.x = I1.x by A0,B1
.= f2.x by A0,B1;
g1.x = I2.x by A0,B1
.= g2.x by A0,B1;
hence thesis by B2;
end;
A3: for k st P[k] holds P[k + 1]
proof
let k;
assume
B0: P[k];
let x be Element of X;
assume
B1: l.x <= k+1;
per cases;
suppose
C0: x in D;
C1: f1.x = I1.x by A0,C0
.= f2.x by A0,C0;
g1.x = I2.x by A0,C0
.= g2.x by A0,C0;
hence thesis by C1;
end;
suppose
C0: not x in D;
reconsider x1=E1.x,x2=E2.x as Element of X;
l.x1 + 1 <= l.x & l.x2 + 1 <= l.x by NAT_1:13,A1,C0;
then l.x1 + 1 <= k + 1 & l.x2 + 1 <= k + 1 by B1,XXREAL_0:2;
then
l.x1 <= k & l.x2 <= k by XREAL_1:8;
then C1:f1.x1 = f2.x1 & g1.x2 = g2.x2 by B0;
C2: f1.x = J1.[x,f2.x1,g2.x2] by A0,C0,C1
.= f2.x by A0,C0;
g1.x = J2.[x,f2.x1,g2.x2] by A0,C0,C1
.= g2.x by A0,C0;
hence thesis by C2;
end;
end;
A4: for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
for x being Element of X holds f1.x = f2.x & g1.x = g2.x
proof
let x be Element of X;
reconsider k = l.x as Nat;
l.x <= k;
hence thesis by A4;
end;
hence thesis;
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
E1,E2 is_well_founded_with_minimal_set D implies
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
assume E1,E2 is_well_founded_with_minimal_set D;
then consider f,g being Function of X,Y such that
A1: for x being Element of X holds
(x in D implies f.x = I.x & g.x = I.x) &
(not x in D implies f.x = J.[x,f.(E1.x),g.(E2.x)] &
g.x = J.[x,f.(E1.x),g.(E2.x)]) by Threcursive05;
for x being Element of X holds f.x = g.x
proof
let x be Element of X;
per cases;
suppose
C0: x in D; then
f.x = I.x by A1
.= g.x by A1,C0;
hence thesis;
end;
suppose
C0: not x in D; then
f.x = J.[x,f.(E1.x),g.(E2.x)] by A1
.= g.x by A1,C0;
hence thesis;
end;
end; then
f = g;
then 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)]) by A1;
hence thesis;
end;
:: Uniqueness
theorem
for f1,f2 being Function of X,Y holds
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)]))
implies f1 = f2
proof
let f1,f2 be Function of X,Y;
assume
A0: 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)])); then
consider l be Function of X,NAT such that
A1: 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);
defpred P[Nat] means
for x being Element of X st l.x<=$1 holds f1.x = f2.x;
A2: P[0]
proof
let x be Element of X;
assume b1: l.x <= 0; then
f1.x = I.x by A0,A1
.= f2.x by A0,b1,A1;
hence thesis;
end;
A3: for k st P[k] holds P[k + 1]
proof
let k;
assume
B0: P[k];
let x be Element of X;
assume
B1: l.x <= k+1;
per cases;
suppose
C0: x in D;
f1.x = I.x by A0,C0
.= f2.x by A0,C0;
hence thesis;
end;
suppose
C0: not x in D;
set x1 = E1.x, x2 = E2.x;
reconsider x as Element of X;
l.x1 + 1 <= l.x & l.x2 + 1 <= l.x by NAT_1:13,A1,C0;
then l.x1 + 1 <= k + 1 & l.x2 + 1 <= k + 1 by B1,XXREAL_0:2;
then
C2: f1.x1 = f2.x1 & f1.x2 = f2.x2 by B0,XREAL_1:8;
f1.x = J.[x,f1.x1,f1.x2] by A0,C0
.= f2.x by C2,A0,C0;
hence thesis;
end;
end;
A4: for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
for x being Element of X holds f1.x = f2.x
proof
let x be Element of X;
reconsider k = l.x as Nat;
l.x <= k;
hence thesis by A4;
end;
hence thesis;
end;