:: The Semantics of MML Query -- Ordering
:: by Grzegorz Bancerek
::
:: Received December 1, 2012
:: Copyright (c) 2012 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 MMLQUER2, RELAT_1, XBOOLE_0, SUBSET_1, AOFA_000, RELAT_2, TARSKI,
FUNCT_1, NUMBERS, MMLQUERY, ARYTM_3, ORDINAL1, PARTFUN1, ORDERS_1,
ORDINAL4, ZFMISC_1, XXREAL_0, FINSEQ_1, FINSEQ_4, SETFAM_1, CARD_1,
NAT_1, FUNCT_7, WELLORD1, REWRITE1, FINSET_1, PEPIN, AFINSQ_1, WELLORD2,
ORDINAL2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, AOFA_000,
RELAT_2, FUNCT_1, FINSET_1, FINSEQ_1, CARD_1, NAT_1, MEMBERED, ORDERS_1,
ORDINAL1, NUMBERS, PARTFUN1, FUNCT_2, MMLQUERY, ORDINAL2, ORDINAL4,
AFINSQ_1, XXREAL_0, XCMPLX_0, WELLORD1, FUNCT_7, RELSET_1, REWRITE1,
WELLORD2, TOLER_1;
constructors TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, MMLQUERY, XXREAL_0,
ORDINAL1, VALUED_0, ORDERS_1, FINSEQ_4, XCMPLX_0, FUNCT_1, FUNCT_7,
ZFMISC_1, WELLORD2, PARTFUN1, FUNCT_2, NUMBERS, NAT_1, REWRITE1,
MEMBERED, RELSET_1, WELLORD1, TOLER_1, ORDINAL2, ORDINAL3, ORDINAL4;
registrations RELAT_1, RELSET_1, ARMSTRNG, VALUED_0, ARROW, FINSEQ_1,
XXREAL_0, CARD_1, SUBSET_1, XCMPLX_0, ORDINAL1, NAT_1, FUNCT_7, MEMBERED,
FINSET_1, XBOOLE_0, AFINSQ_1;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, WELLORD1, FUNCT_1, PARTFUN1,
REWRITE1, MMLQUERY;
equalities RELAT_1, CARD_1;
expansions XBOOLE_0, RELAT_2, WELLORD1, FUNCT_1, REWRITE1, MMLQUERY;
theorems XBOOLE_0, XBOOLE_1, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_1, MMLQUERY,
NAT_1, XXREAL_0, SETFAM_1, AFINSQ_1, ORDINAL3, ORDINAL1, FUNCT_1, CARD_2,
TARSKI, FINSEQ_3, FUNCT_7, RELSET_1, FUNCT_2, AFINSQ_2, RELSET_2,
WELLORD1, WELLORD2, PARTFUN1, CARD_1, ORDINAL4, XTUPLE_0;
schemes NAT_1, RELAT_1, RECDEF_1, FINSET_1, FUNCT_1;
begin :: Preliminaries
reserve X for set, R,R1,R2 for Relation;
reserve x,y,z for set;
reserve n,m,k for Nat;
theorem
for R being Relation of X holds field R c= X
proof
let R be Relation of X;
dom R c= X & rng R c= X;
hence field R c= X by XBOOLE_1:8;
end;
theorem Lm2:
for R being Relation of X st x,y in R holds x in X & y in X
proof
let R be Relation of X;
assume [x,y] in R;
hence thesis by ZFMISC_1:87;
end;
theorem Lm3:
for X,Y being set holds (id X).:Y = X /\ Y
proof let X,Y be set;
thus (id X).:Y c= X /\ Y
proof let x be element; assume x in (id X).:Y; then
consider y be element such that
A1: [y,x] in id X & y in Y by RELAT_1:def 13;
x = y & y in X by A1,RELAT_1:def 10;
hence thesis by A1,XBOOLE_0:def 4;
end;
let x be element; assume x in X /\ Y; then
A2: x in X & x in Y by XBOOLE_0:def 4; then
[x,x] in id X by RELAT_1:def 10;
hence thesis by A2,RELAT_1:def 13;
end;
theorem Lm4:
[x,y] in R |_2 X iff x in X & y in X & [x,y] in R
proof
R |_2 X = X|`(R|X) by WELLORD1:11; then
[x,y] in R |_2 X iff y in X & [x,y] in R|X by RELAT_1:def 12;
hence thesis by RELAT_1:def 11;
end;
theorem
dom(X|`R) c= dom R
proof
let x be element; assume x in dom(X|`R); then
consider y be element such that
A1: [x,y] in X|`R by XTUPLE_0:def 12;
[x,y] in R by A1,RELAT_1:def 12;
hence thesis by XTUPLE_0:def 12;
end;
theorem Lm5:
for R being total reflexive Relation of X
for S being Subset of X holds
R |_2 S is total reflexive Relation of S
proof
let R be total reflexive Relation of X;
let S be Subset of X;
set Q = R |_2 S;
dom Q = S
proof
thus dom Q c= S;
let x be element; assume
A1: x in S; then x in X; then
x in field R & R is_reflexive_in field R
by RELAT_2:def 9,ORDERS_1:12; then
[x,x] in R; then
[x,x] in Q by A1,Lm4;
hence thesis by XTUPLE_0:def 12;
end;
hence R |_2 S is total reflexive Relation of S
by PARTFUN1:def 2,WELLORD1:15;
end;
theorem Lm8: ::: AFINSQ_1:26 generalized
for f,g being Sequence holds rng(f^g) = rng f \/ rng g
proof
let f,g be Sequence;
A0: dom(f^g) = dom f+^dom g by ORDINAL4:def 1;
thus rng(f^g) c= rng f \/ rng g
proof
let y be element;
assume y in rng(f^g); then
consider x be element such that
A1: x in dom(f^g) & y = (f^g).x by FUNCT_1:def 3;
per cases by A0,A1,ORDINAL3:38;
suppose
A2: x in dom f; then y = f.x by A1,ORDINAL4:def 1; then
y in rng f by A2,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex a being Ordinal st a in dom g & x = dom f+^a; then
consider a being Ordinal such that
A3: a in dom g & x = dom f+^a;
y = g.a by A1,A3,ORDINAL4:def 1; then
y in rng g by A3,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be element; assume
A4: x in rng f \/ rng g;
per cases by A4,XBOOLE_0:def 3;
suppose
x in rng f; then
consider y be element such that
A5: y in dom f & x = f.y by FUNCT_1:def 3;
x = (f^g).y & y in dom(f^g) by A0,A5,ORDINAL4:def 1,ORDINAL3:25;
hence thesis by FUNCT_1:def 3;
end;
suppose
x in rng g; then
consider y be element such that
A5: y in dom g & x = g.y by FUNCT_1:def 3;
reconsider y as Ordinal by A5;
x = (f^g).(dom f+^y) & dom f+^y in dom(f^g)
by A0,A5,ORDINAL4:def 1,ORDINAL3:17;
hence thesis by FUNCT_1:def 3;
end;
end;
definition
let R;
redefine attr R is transitive means :TRANS:
x,y in R & y,z in R implies x,z in R;
compatibility
proof
thus R is transitive implies
for x,y,z be set holds x,y in R & y,z in R implies x,z in R
proof
assume R is transitive; then
A: for x,y,z be element st [x,y] in R & [y,z] in R holds [x,z] in R
by RELAT_2:31;
let x,y,z be set; assume
x,y in R & y,z in R; then
[x,y] in R & [y,z] in R;
hence [x,z] in R by A;
end;
assume
A3: x,y in R & y,z in R implies x,z in R;
let x,y,z be element;
reconsider xx = x, yy = y, zz = z as set by TARSKI:1;
assume
x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R; then
xx,yy in R & yy,zz in R;
hence thesis by A3,MMLQUERY:def 1;
end;
redefine attr R is antisymmetric means :ANTIS:
x,y in R & y,x in R implies x = y;
compatibility
proof
thus R is antisymmetric implies for x,y st x,y in R & y,x in R holds x = y
proof
assume
A1: for x,y be element st x in field R & y in field R &
[x,y] in R & [y,x] in R holds x = y;
let x,y be set;
assume
A2: [x,y] in R & [y,x] in R; then
x in field R & y in field R by RELAT_1:15;
hence thesis by A1,A2;
end;
assume
A3: for x,y be set st x,y in R & y,x in R holds x = y;
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
assume
x in field R & y in field R & [x,y] in R & [y,x] in R; then
xx,yy in R & yy,xx in R;
hence thesis by A3;
end;
end;
theorem
for X being non empty set
for R being total connected Relation of X
for x,y being Element of X st x <> y holds x,y in R or y,x in R
proof
let X be non empty set;
let R be total connected Relation of X;
let x,y be Element of X;
field R = X by ORDERS_1:12; then
x <> y implies [x,y] in R or [y,x] in R by RELAT_2:def 6,def 14;
hence thesis;
end;
begin :: Composition of orders
definition
let R1,R2 be Relation;
func R1\,R2 -> Relation equals
R1 \/ (R2 \ R1~);
coherence;
end;
theorem Th1:
x,y in R1\,R2 iff x,y in R1 or y,x nin R1 & x,y in R2
proof
set R={[a,b] where a,b is Element of field R2: b,a nin R1 & a,b in R2};
thus x,y in R1\,R2 implies x,y in R1 or y,x nin R1 & x,y in R2
proof
assume [x,y] in R1\,R2; then
[x,y] in R1 or [x,y] in (R2 \ R1~) by XBOOLE_0:def 3; then
[x,y] in R1 or ([x,y] in R2 & not [x,y] in R1~) by XBOOLE_0:def 5; then
S: [x,y] in R1 or ([x,y] in R2 & not [y,x] in R1) by RELAT_1:def 7;
reconsider xx=x, yy=y as set;
xx,yy in R1 or (xx,yy in R2 & not yy,xx in R1)
by S;
hence thesis;
end;
assume x,y in R1 or y,x nin R1 & x,y in R2; then
[x,y] in R1 or [x,y] in R2 & not [y,x] in R1; then
[x,y] in R1 or [x,y] in R2 & not [x,y] in R1~ by RELAT_1:def 7; then
[x,y] in R1 or [x,y] in R2 \ R1~ by XBOOLE_0:def 5;
hence [x,y] in R1\,R2 by XBOOLE_0:def 3;
end;
theorem Th2:
field (R1\,R2) = field R1 \/ field R2
proof
thus field (R1\,R2) c= field R1 \/ field R2
proof
let z be element; assume z in field (R1\,R2); then
z in dom (R1\,R2) or z in rng (R1\,R2) by XBOOLE_0:def 3; then
consider y be element such that
A1: [z,y] in R1\,R2 or [y,z] in R1\,R2 by XTUPLE_0:def 12,def 13;
reconsider zz = z, y as set by TARSKI:1;
zz,y in R1\,R2 or y,zz in R1\,R2 by A1; then
zz,y in R1 or y,zz in R1 or zz,y in R2 or y,zz in R2 by Th1; then
[z,y] in R1 or [y,z] in R1 or [z,y] in R2 or [y,z] in R2; then
z in field R1 or z in field R2 by RELAT_1:15;
hence thesis by XBOOLE_0:def 3;
end;
let z be element;
assume z in field R1 \/ field R2; then
z in field R1 or z in field R2 by XBOOLE_0:def 3; then
z in dom R1 or z in rng R1 or z in dom R2 or z in rng R2 by XBOOLE_0:def 3;
then
consider y be element such that
A2: [z,y] in R1 or [y,z] in R1 or [z,y] in R2 or [y,z] in R2
by XTUPLE_0:def 12,def 13;
reconsider zz = z, y as set by TARSKI:1;
zz,y in R1 or y,zz in R1 or zz,y in R2 & y,zz nin R1 or y,zz in R1 or
y,zz in R2 & zz,y nin R1 or zz,y in R1 by A2; then
zz,y in R1\,R2 or y,zz in R1\,R2 by Th1; then
[z,y] in R1\,R2 or [y,z] in R1\,R2;
hence thesis by RELAT_1:15;
end;
theorem Th3:
R1\,R2 c= R1 \/ R2
proof
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
assume [x,y] in R1\,R2; then
xx,yy in R1\,R2; then
xx,yy in R1 or xx,yy in R2 by Th1; then
[x,y] in R1 or [x,y] in R2;
hence thesis by XBOOLE_0:def 3;
end;
definition
let X be set;
let R1,R2 be Relation of X;
redefine func R1\,R2 -> Relation of X;
coherence
proof
R1\,R2 c= R1 \/ R2 by Th3;
hence thesis by XBOOLE_1:1;
end;
end;
registration
let R1,R2 be reflexive Relation;
cluster R1\,R2 -> reflexive;
coherence
proof
let z be element; assume z in field(R1\,R2); then
z in field R1 \/ field R2 by Th2; then
z in field R1 or z in field R2 by XBOOLE_0:def 3; then
A1: [z,z] in R1 or [z,z] in R2 & [z,z] nin R1 by RELAT_2:def 1,def 9;
reconsider zz = z as set by TARSKI:1;
zz,zz in R1 or zz,zz in R2 & zz,zz nin R1 by A1; then
zz,zz in R1\,R2 by Th1;
hence thesis;
end;
end;
registration
let R1,R2 be antisymmetric Relation;
cluster R1\,R2 -> antisymmetric;
coherence
proof
let z,y;
assume
A2: [z,y] in R1\,R2 & [y,z] in R1\,R2;
z,y in R1\,R2 & y,z in R1\,R2 by A2; then
(z,y in R1 or y,z nin R1 & z,y in R2) &
(y,z in R1 or z,y nin R1 & y,z in R2) by Th1; then
[z,y] in R1 & [y,z] in R1 or [z,y] in R2 & [y,z] in R2; then
[z,y] in R1 & [y,z] in R1 & y in field R1 & z in field R1 or
[z,y] in R2 & [y,z] in R2 & y in field R2 & z in field R2 by RELAT_1:15;
hence y = z by RELAT_2:def 4,def 12;
end;
end;
definition
let X be set;
let R be Relation of X;
attr R is beta-transitive means :SEGM:
for x,y being Element of X st x,y nin R
for z being Element of X holds (x,z in R implies y,z in R);
end;
registration
let X be set;
cluster connected total transitive -> beta-transitive for Relation of X;
coherence
proof
let R be Relation of X;
assume
A1: R is connected total transitive; then
field R = X by ORDERS_1:12; then
A3: R is_connected_in X by A1;
let x,y be Element of X;
assume
A4: x,y nin R;
let z be Element of X;
assume
A5: [x,z] in R; then
x in X by ZFMISC_1:87; then
x <> y implies [x,y] in R or [y,x] in R by A3; then
(x = y or y,x in R) & x,z in R by A4,A5;
hence y,z in R by A1;
end;
end;
registration
let X be set;
cluster connected for Order of X;
existence
proof
set R = the connected Order of X;
take R; thus thesis;
end;
end;
registration
let X be set;
let R1 be beta-transitive transitive Relation of X;
let R2 be transitive Relation of X;
cluster R1\,R2 -> transitive;
coherence
proof
let x,y,z be set;
assume
A1: x,y in R1\,R2 & y,z in R1\,R2; then
[x,y] in R1\,R2 & [y,z] in R1\,R2; then
reconsider x,y,z as Element of X by ZFMISC_1:87;
per cases by A1,Th1;
suppose
x,y in R1 & y,z in R1 or z,x nin R1 & x,y in R2 & y,z in R2; then
x,z in R1 or z,x nin R1 & x,z in R2 by TRANS;
hence thesis by Th1;
end;
suppose y,x nin R1 & z,y nin R1 & z,x in R1;
hence thesis by SEGM;
end;
suppose
A3: x,y in R1 & z,y nin R1 & y,z in R2;
assume not thesis; then
x,z nin R1 by Th1;
hence contradiction by A3,SEGM;
end;
suppose
A4: y,z in R1 & y,x nin R1 & x,y in R2;
assume not thesis; then
x,z nin R1 by Th1;
hence contradiction by A4,SEGM;
end;
end;
end;
registration
let X be set;
let R1 be Relation of X;
let R2 be total reflexive Relation of X;
cluster R1\,R2 -> total reflexive for Relation of X;
coherence
proof
field R2 = X by ORDERS_1:12; then
A3: R2 is_reflexive_in X by RELAT_2:def 9;
let R be Relation of X; assume
Z1: R = R1\,R2;
thus
A6: R is total
proof
thus dom R c= X;
let x be element; assume
A2: x in X; then
reconsider x as Element of X;
[x,x] in R2 by A2,A3; then
x,x in R1 or not x,x in R1 & x,x in R2; then
x,x in R by Z1,Th1; then
[x,x] in R;
hence thesis by XTUPLE_0:def 12;
end; then
A5: field R = X by ORDERS_1:12;
let x be element; assume
A4: x in field R; then
reconsider x as Element of X by A6,ORDERS_1:12;
[x,x] in R2 by A4,A5,A3; then
x,x in R1 or not x,x in R1 & x,x in R2; then
x,x in R by Z1,Th1;
hence thesis;
end;
end;
registration
let X be set;
let R1 be Relation of X;
let R2 be total connected reflexive Relation of X;
cluster R1\,R2 -> connected;
coherence
proof
set R = R1\,R2;
A0: field R = X & field R2 = X by ORDERS_1:12; then
A1: R2 is_connected_in X by RELAT_2:def 14;
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
assume x in field R & y in field R & x <> y; then
[x,y] in R2 or [y,x] in R2 by A0,A1; then
xx,yy in R1 or yy,xx nin R1 & xx,yy in R2 or yy,xx in R1 or xx,yy nin R1
& yy,xx in R2;
then xx,yy in R or yy,xx in R by Th1;
hence thesis;
end;
end;
theorem
(R\,R1)\,R2 = R\,(R1\,R2)
proof
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
thus [x,y] in (R\,R1)\,R2 implies [x,y] in R\,(R1\,R2)
proof
assume [x,y] in (R\,R1)\,R2; then
xx,yy in (R\,R1)\,R2; then
xx,yy in R\,R1 or yy,xx nin R\,R1 & xx,yy in R2 by Th1; then
xx,yy in R or yy,xx nin R & xx,yy in R1 or
yy,xx nin R & (xx,yy in R or yy,xx nin R1) & xx,yy in R2 by Th1; then
xx,yy in R or yy,xx nin R & xx,yy in R1\,R2 by Th1; then
xx,yy in R\,(R1\,R2) by Th1;
hence thesis;
end;
assume [x,y] in R\,(R1\,R2); then
xx,yy in R\,(R1\,R2); then
xx,yy in R or yy,xx nin R & xx,yy in R1\,R2 by Th1; then
xx,yy in R or yy,xx nin R & (xx,yy in R1 or yy,xx nin R1 &
xx,yy in R2) by Th1;then
xx,yy in R\,R1 or yy,xx nin R\,R1 & xx,yy in R2 by Th1; then
xx,yy in (R\,R1)\,R2 by Th1;
hence thesis;
end;
theorem
for R being connected reflexive total Relation of X
for R2 being Relation of X holds R\,R2 = R
proof
let R be connected reflexive total Relation of X;
let R2 be Relation of X;
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
hereby assume [x,y] in R\,R2; then xx,yy in R\,R2; then
xx,yy in R or yy,xx nin R & xx,yy in R2 by Th1; then
[x,y] in R or [y,x] nin R & x in X & y in X & field R = X &
R is_connected_in field R & R is_reflexive_in field R & (x = y or x <> y)
by Lm2,RELAT_2:def 9,def 14,ORDERS_1:12;
hence [x,y] in R;
end;
assume [x,y] in R; then
xx,yy in R; then
xx,yy in R\,R2 by Th1;
hence thesis;
end;
begin :: "number of" ordering
definition
let X be set;
let f be Function of X,NAT;
func value_of(f) -> Relation of X means :VAL:
x,y in it iff x in X & y in X & f.x < f.y;
existence
proof
defpred P[element,element] means f.$1 < f.$2;
consider R being Relation such that
A1: for x,y be element holds
[x,y] in R iff x in X & y in X & P[x,y] from RELAT_1:sch 1;
R c= [:X,X:]
proof
let x,y be element; assume [x,y] in R; then
x in X & y in X by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87;
end; then
reconsider R as Relation of X;
take R;
let x,y;
thus thesis by A1;
end;
uniqueness
proof let R1,R2 be Relation of X such that
A1: x,y in R1 iff x in X & y in X & f.x < f.y and
A2: x,y in R2 iff x in X & y in X & f.x < f.y;
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
[x,y] in R1 iff xx,yy in R1; then
[x,y] in R1 iff x in X & y in X & f.x < f.y by A1; then
[x,y] in R1 iff xx,yy in R2 by A2;
hence thesis;
end;
end;
registration
let X be set;
let f be Function of X,NAT;
cluster value_of f -> antisymmetric transitive beta-transitive;
coherence
proof
set R = value_of f;
thus R is antisymmetric
proof
let x,y; assume x,y in R & y,x in R; then
f.x < f.y & f.y < f.x by VAL;
hence thesis;
end;
thus R is transitive
proof
let x,y,z; assume x,y in R & y,z in R; then
A1: x in X & z in X & f.x < f.y & f.y < f.z by VAL; then
f.x < f.z by XXREAL_0:2;
hence thesis by A1,VAL;
end;
let x,y be Element of X such that
A2: x,y nin R;
let z be Element of X; assume
x,z in R; then
A3: x in X & f.x < f.z by VAL; then
f.x >= f.y by A2,VAL; then
f.y < f.z by A3,XXREAL_0:2;
hence y,z in R by A3,VAL;
end;
end;
definition
let X be finite set;
let O be Operation of X;
func number_of O -> Function of X,NAT means :NUM:
for x being Element of X holds it.x = card (x.O);
existence
proof
deffunc F(element) = card Im(O,$1);
consider f being Function such that
A1: dom f = X & for x be element st x in X holds f.x = F(x)
from FUNCT_1:sch 3;
rng f c= NAT
proof
let y be element; assume y in rng f; then
consider x be element such that
A2: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Element of X by A1,A2;
y = card(x.O) by A1,A2;
hence thesis;
end; then
reconsider f as Function of X,NAT by A1,FUNCT_2:2;
take f; let x be Element of X;
per cases;
suppose X = {}; then
f.x = 0 & x.O = {} by A1,FUNCT_1:def 2;
hence thesis;
end;
suppose X <> {};
hence thesis by A1;
end;
end;
uniqueness
proof
let f1,f2 be Function of X,NAT such that
A1: for x being Element of X holds f1.x = card (x.O) and
A2: for x being Element of X holds f2.x = card (x.O);
A3: dom f1 = X & dom f2 = X by FUNCT_2:def 1;
now let x be element; assume x in X; then
reconsider y = x as Element of X;
thus f1.x = card(y.O) by A1 .= f2.x by A2;
end;
hence thesis by A3;
end;
end;
theorem
for X being finite set
for O being Operation of X, x,y being Element of X holds
x,y in value_of number_of O iff card(x.O) < card(y.O)
proof
let X be finite set;
let O be Operation of X;
let x,y be Element of X;
hereby
assume x,y in value_of number_of O; then
(number_of O).x < (number_of O).y by VAL; then
card(x.O) < (number_of O).y by NUM;
hence card(x.O) < card(y.O) by NUM;
end;
assume Z1: card(x.O) < card(y.O);
0 <= card(x.O) by NAT_1:2; then
y.O <> {} by Z1; then
y in dom O & (number_of O).x = card(x.O) & (number_of O).y = card(y.O)
by NUM,RELAT_1:170;
hence x,y in value_of number_of O by Z1,VAL;
end;
definition
let X;
let O be Operation of X;
func first O -> Relation of X means :FIRST:
for x,y being Element of X holds x,y in it iff x.O <> {} & y.O = {};
existence
proof
defpred P[element,element] means Im(O,$1) <> {} & Im(O,$2) = {};
consider R such that
A1: for x,y be element holds
[x,y] in R iff x in X & y in X & P[x,y] from RELAT_1:sch 1;
R c= [:X,X:]
proof
let x,y be element; assume [x,y] in R; then
x in X & y in X by A1;
hence thesis by ZFMISC_1:87;
end; then
reconsider R as Relation of X;
take R;
let x,y be Element of X;
A2: x.O <> {} iff x in dom O by RELAT_1:170;
thus thesis by A1,A2;
end;
uniqueness
proof let R1,R2 be Relation of X such that
A1: for x,y being Element of X holds x,y in R1 iff x.O <> {} & y.O = {} and
A2: for x,y being Element of X holds x,y in R2 iff x.O <> {} & y.O = {};
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
thus [x,y] in R1 implies [x,y] in R2
proof assume
A7: [x,y] in R1;
then reconsider x,y as Element of X by ZFMISC_1:87;
x,y in R1 by A7; then
x.O <> {} & y.O = {} by A1;
hence thesis by A2,MMLQUERY:def 1;
end;
assume
A7: [x,y] in R2;
then reconsider x,y as Element of X by ZFMISC_1:87;
x,y in R2 by A7; then
x.O <> {} & y.O = {} by A2;
hence thesis by A1,MMLQUERY:def 1;
end;
end;
registration
let X;
let O be Operation of X;
cluster first O -> antisymmetric transitive beta-transitive;
coherence
proof set R = first O;
thus first O is antisymmetric
proof
let x,y; assume
A1: x,y in R & y,x in R; then
reconsider x,y as Element of X by Lm2;
y = y; then
x.O <> {} & x.O = {} by A1,FIRST;
hence thesis;
end;
thus first O is transitive
proof
let x,y,z; assume
A1: x,y in R & y,z in R; then
reconsider x,y,z as Element of X by Lm2;
x = x & z = z; then
y.O <> {} & y.O = {} by A1,FIRST;
hence thesis;
end;
let x,y be Element of X such that
A2: x,y nin R;
let z be Element of X; assume
x,z in R; then
A3: x.O <> {} & z.O = {} by FIRST; then
y.O <> {} by A2,FIRST;
hence y,z in R by A3,FIRST;
end;
end;
begin :: Ordering by resources
definition
let A be FinSequence;
let x be element;
func A <- x -> set equals meet (A"{x});
coherence;
end;
registration
let A be FinSequence;
let x;
cluster A <- x -> natural;
coherence
proof
per cases;
suppose A"{x} = {};
hence thesis by SETFAM_1:def 1;
end;
suppose A"{x} <> {}; then
consider y be element such that
A1: y in A"{x} by XBOOLE_0:def 1;
A2: A"{x} c= dom A by RELAT_1:132; then
y in dom A by A1; then
reconsider y as Element of NAT;
A3: A<-x is Ordinal by A2,XBOOLE_1:1,ORDINAL3:11;
A<-x c= y by A1,SETFAM_1:3;
hence thesis by A3;
end;
end;
end;
theorem
for A being FinSequence st x nin rng A holds A <- x = 0
proof
let A be FinSequence;
assume x nin rng A; then
A"{x} = {} by FUNCT_1:72;
hence A <- x = 0 by SETFAM_1:def 1;
end;
theorem Th22:
for A being FinSequence st x in rng A holds A <- x in dom A & x = A.(A <- x)
proof
let A be FinSequence;
assume x in rng A; then A"{x} <> {} by FUNCT_1:72; then
consider y be element such that
A1: y in A"{x} by XBOOLE_0:def 1;
A2: A"{x} c= dom A by RELAT_1:132; then
y in dom A by A1; then
reconsider y as Element of NAT;
defpred P[Nat] means $1 in A"{x};
y = y; then
A3: ex n st P[n] by A1;
consider n such that
A4: P[n] & for m st P[m] holds n <= m from NAT_1:sch 5(A3);
A5: A<-x c= n by A4,SETFAM_1:3;
for z st z in A"{x} holds n c= z by A2,A4,NAT_1:39; then
n c= A<-x by A1,SETFAM_1:5; then
A7: A<-x = n by A5;
hence A <- x in dom A by A4,FUNCT_1:def 7;
A.(A<-x) in {x} by A4,A7,FUNCT_1:def 7;
hence x = A.(A <- x) by TARSKI:def 1;
end;
theorem
for A being FinSequence st A <- x = 0 holds x nin rng A
proof
let A be FinSequence;
assume A <- x = 0 & x in rng A; then
0 in dom A by Th22;
hence thesis by FINSEQ_3:24;
end;
definition
let X;
let A be FinSequence;
let f be Function;
func resource(X,A,f) -> Relation of X means :RES:
x,y in it iff x in X & y in X &
A <- (f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0);
existence
proof
defpred P[element,element] means
A <- (f.$1) <> 0 & (A <- (f.$1) < A <- (f.$2) or A <- (f.$2) = 0);
consider R such that
A1: for x,y be element holds
[x,y] in R iff x in X & y in X & P[x,y] from RELAT_1:sch 1;
R c= [:X,X:]
proof
let x,y be element; assume [x,y] in R; then
x in X & y in X by A1;
hence thesis by ZFMISC_1:87;
end; then
reconsider R as Relation of X;
take R;
let x,y;
thus thesis by A1;
end;
uniqueness
proof let R1,R2 be Relation of X such that
A1: x,y in R1 iff x in X & y in X &
A<-(f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0) and
A2: x,y in R2 iff x in X & y in X &
A<-(f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0);
let x,y be element;
reconsider xx = x, yy = y as set by TARSKI:1;
[x,y] in R1 iff xx,yy in R1; then
[x,y] in R1 iff x in X & y in X &
A<-(f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0) by A1; then
[x,y] in R1 iff xx,yy in R2 by A2;
hence thesis;
end;
end;
registration
let X;
let A be FinSequence;
let f be Function;
cluster resource(X,A,f) -> antisymmetric transitive beta-transitive;
coherence
proof set R = resource(X,A,f);
thus R is antisymmetric
proof
let x,y; assume x,y in R & y,x in R; then
A <- (f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0) &
A <- (f.y) <> 0 & (A <- (f.y) < A <- (f.x) or A <- (f.x) = 0) by RES;
hence thesis;
end;
thus R is transitive
proof
let x,y,z; assume
x,y in R & y,z in R; then
A2: x in X & y in X & A <- (f.x) <> 0 & (A <- (f.x) < A <- (f.y) or
A <- (f.y) = 0) & z in X & A <- (f.y) <> 0 &
(A <- (f.y) < A <- (f.z) or A <- (f.z) = 0) by RES;then
A <- (f.x) < A <- (f.z) or A <- (f.z) = 0 by XXREAL_0:2;
hence thesis by A2,RES;
end;
let x,y be Element of X such that
A2: x,y nin R;
let z be Element of X; assume x,z in R; then
A3: x in X & z in X & A <- (f.x) <> 0 &
(A <- (f.x) < A <- (f.z) or A <- (f.z) = 0) &
not (x in X & y in X & A <- (f.x) <> 0 & (A <- (f.x) < A <- (f.y) or
A <- (f.y) = 0)) by A2,RES; then
A <- (f.y) <> 0 & (A <- (f.y) < A <- (f.z) or A <- (f.z) = 0)
by XXREAL_0:2;
hence y,z in R by A3,RES;
end;
end;
begin :: Ordering by number of iteration
definition
let X;
let R be Relation of X;
let n be Nat;
redefine func iter(R,n) -> Relation of X;
coherence
proof
consider p being Function of NAT, bool [:field R,field R:] such that
A1: p.n = iter(R,n) & p.0 = id(field R) and
A2: for k being Nat holds p.(k+1) = R*p.k by FUNCT_7:def 11;
defpred P[Nat] means p.$1 is Relation of X;
field R c= X \/ X by RELSET_1:8; then
dom id(field R) c= X & rng id(field R) c= X; then
A3: P[0] by A1,RELSET_1:4;
A4: for m being Nat holds P[m] implies P[m+1]
proof let m be Nat;
assume P[m]; then
reconsider g = p.m as Relation of X;
p.(m+1) = R*g by A2;
hence thesis;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A3,A4);
hence thesis by A1;
end;
end;
theorem Th31:
iter(R,n).:X = {} & m >= n implies iter(R,m).:X = {}
proof assume
A1: iter(R,n).:X = {} & m >= n; then
consider k such that
A2: m = n+k by NAT_1:10;
thus iter(R,m).:X = (iter(R,n)*iter(R,k)).:X by A2,FUNCT_7:77
.= iter(R,k).:{} by A1,RELAT_1:126
.= {};
end;
theorem Th32:
(for n holds iter(R,n).:X <> {}) & X is finite implies ex x st x in X &
for n holds Im(iter(R,n),x) <> {}
proof
assume that
Z0: for n holds iter(R,n).:X <> {} and
Z3: X is finite and
Z1: for x st x in X ex n st Im(iter(R,n),x) = {};
defpred P[element,element] means
ex n st $2 = n & Im(iter(R,n),$1) = {};
A1: for x be element st x in X ex y be element st y in NAT & P[x,y]
proof let x be element; assume x in X; then
consider n such that
B1: Im(iter(R,n),x) = {} by Z1;
take y = n; thus thesis by B1,ORDINAL1:def 12;
end;
consider f being Function such that
A2: dom f = X & rng f c= NAT &
for x be element st x in X holds P[x,f.x] from FUNCT_1:sch 6(A1);
reconsider f as Function of X,NAT by A2,FUNCT_2:2;
consider n such that
A3: rng f c= Segm n by Z3,AFINSQ_2:2;
{{x} where x is Element of X: x in X} c= bool X
proof let z be element;
assume z in {{x} where x is Element of X: x in X}; then
consider x being Element of X such that
B2: z = {x} & x in X;
z is Subset of X by B2,ZFMISC_1:31;
hence thesis;
end; then
reconsider Y = {{x} where x is Element of X: x in X} as Subset-Family of X;
X = union Y
proof
thus X c= union Y
proof
let x be element; assume x in X; then
x in {x} & {x} in Y by TARSKI:def 1;
hence thesis by TARSKI:def 4;
end;
let x be element; assume x in union Y; then
consider z such that
B3: x in z & z in Y by TARSKI:def 4;
thus thesis by B3;
end; then
A6: iter(R,n).:X = union {iter(R,n).:y where y is Subset of X: y in Y}
by RELSET_2:14;
{iter(R,n).:y where y is Subset of X: y in Y} c= {{}}
proof
let z be element;
assume z in {iter(R,n).:y where y is Subset of X: y in Y}; then
consider y being Subset of X such that
A7: z = iter(R,n).:y & y in Y;
consider x being Element of X such that
A8: y = {x} & x in X by A7;
consider m such that
A9: f.x = m & Im(iter(R,m),x) = {} by A2,A8;
m in rng f by A2,A8,A9,FUNCT_1:def 3; then
m < n by A3,NAT_1:44; then
z = {} by A7,A8,A9,Th31;
hence thesis by TARSKI:def 1;
end; then
iter(R,n).:X c= union {{}} by A6,ZFMISC_1:77; then
iter(R,n).:X c= {} by ZFMISC_1:25; then
iter(R,n).:X = {};
hence contradiction by Z0;
end;
theorem Th33:
R is co-well_founded irreflexive & X is finite & R is finite
implies ex n st iter(R,n).:X = {}
proof
assume that
A1: R is co-well_founded irreflexive & X is finite and
A3: R is finite and
A2: iter(R,n).:X <> {};
defpred Q[element] means for n holds Im(iter(R,n),$1) <> {};
consider x0 being set such that
A4: x0 in X & Q[x0] by A1,A2,Th32;
defpred P[element,element,element] means
(Q[$2] implies $3 in Im(R,$2) & Q[$3]);
F0: for n being Nat, x be set ex y be set st P[n,x,y]
proof
let n be Nat, x be set;
per cases;
suppose
B1: not Q[x];
take 0; thus thesis by B1;
end;
suppose
B2: Q[x];
B5: Im(R,x) c= rng R by RELAT_1:111;
now let n;
iter(R,n).:Im(R,x) = (R*iter(R,n)).:{x} by RELAT_1:126
.= Im(iter(R,n+1),x) by FUNCT_7:69;
hence iter(R,n).:Im(R,x) <> {} by B2;
end; then
consider y such that
B4: y in Im(R,x) & Q[y] by A3,B5,Th32;
take y; thus thesis by B4;
end;
end;
consider f being Function such that
F1: dom f = NAT & f.0 = x0 & for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 1(F0);
defpred R[Nat] means Q[f.$1];
F3: R[0] by A4,F1;
F4: R[k] implies R[k+1] by F1;
F5: R[k] from NAT_1:sch 2(F3,F4);
F9: rng f c= field R
proof
let z be element; assume z in rng f; then
consider y be element such that
F7: y in NAT & z = f.y by F1,FUNCT_1:def 3;
reconsider y as Element of NAT by F7;
P[y,z,f.(y+1)] & R[y] by F1,F5,F7; then
[z,f.(y+1)] in R by F7,RELAT_1:169;
hence thesis by RELAT_1:15;
end; then
consider z be element such that
F6: z in rng f & for x be element st x in rng f & z <> x holds [z,x] nin R
by A1,F1,RELAT_1:42;
consider y be element such that
F7: y in NAT & z = f.y by F1,F6,FUNCT_1:def 3;
reconsider y as Element of NAT by F7;
P[y,z,f.(y+1)] & R[y] & y+1 in NAT by F1,F5,F7,ORDINAL1:def 12; then
F8: [z,f.(y+1)] in R & f.(y+1) in rng f
by F1,F7,RELAT_1:169,FUNCT_1:def 3; then
z = f.(y+1) & R is_irreflexive_in field R by A1,F6;
hence contradiction by F9,F8;
end;
definition
let X;
let O be Operation of X such that
AA: O is co-well_founded irreflexive finite;
func iteration_of O -> Relation of X means :ITER:
ex f being Function of X,NAT st it = value_of f &
for x being Element of X st x in X
ex n st f.x = n & (x.iter(O,n) <> {} or n = 0 & x.iter(O,n) = {}) &
x.iter(O,n+1) = {};
existence
proof
defpred P[element,element] means
ex n st $2 = n & (Im(iter(O,n),$1) <> {} or n = 0 & Im(iter(O,n),$1) = {})
& Im(iter(O,n+1),$1) = {};
A1: for x be element st x in X ex y be element st y in NAT & P[x,y]
proof
let x be element; assume x in X;
per cases;
suppose x nin field O; then
{x} /\ field O = {} by XBOOLE_0:def 7,ZFMISC_1:50; then
Im(id field O,x) = {} by Lm3; then
B2: Im(iter(O,0),x) = {} by FUNCT_7:68;
take y = 0; thus y in NAT;
take n = 0;
thus y = n & (Im(iter(O,n),x) <> {} or n = 0 & Im(iter(O,n),x) = {});
thus Im(iter(O,n+1),x) = Im(iter(O,n)*O,x) by FUNCT_7:71
.= O.:{} by B2,RELAT_1:126 .= {};
end;
suppose
x in field O; then
{x} /\ field O = {x} by XBOOLE_1:28,ZFMISC_1:31; then
(id field O).:{x} = {x} by Lm3; then
B2: Im(iter(O,0),x) = {x} by FUNCT_7:68;
defpred P[Nat] means iter(O,$1).:{x} = {};
B3: ex n st P[n] by AA,Th33;
consider n such that
B4: P[n] & for k st P[k] holds n <= k from NAT_1:sch 5(B3);
consider m such that
B5: n = m+1 by B2,B4,NAT_1:6;
take y = m; thus y in NAT by ORDINAL1:def 12;
take m;
m < n by B5,NAT_1:13;
hence thesis by B4,B5;
end;
end;
consider f being Function such that
A2: dom f = X & rng f c= NAT & for x be element st x in X holds P[x,f.x]
from FUNCT_1:sch 6(A1);
reconsider f as Function of X,NAT by A2,FUNCT_2:2;
take R = value_of f, f; thus R = value_of f;
let x be Element of X; assume x in X; then
consider n such that
A3: f.x = n & (Im(iter(O,n),x) <> {} or n = 0 & Im(iter(O,n),x) = {}) &
Im(iter(O,n+1),x) = {} by A2;
take n;
thus thesis by A3;
end;
uniqueness
proof
let R1,R2 be Relation of X;
given f1 being Function of X,NAT such that
A1: R1 = value_of f1 and
B1: for x being Element of X st x in X
ex n st f1.x = n & (x.iter(O,n) <> {} or n = 0 & x.iter(O,n) = {}) &
x.iter(O,n+1) = {};
given f2 being Function of X,NAT such that
A2: R2 = value_of f2 and
B2: for x being Element of X st x in X
ex n st f2.x = n & (x.iter(O,n) <> {} or n = 0 & x.iter(O,n) = {}) &
x.iter(O,n+1) = {};
A5: dom f1 = X & dom f2 = X by FUNCT_2:def 1;
now
let y be element; assume
C1: y in X; then reconsider x = y as Element of X;
consider n1 being Nat such that
C2: f1.x = n1 & (x.iter(O,n1) <> {} or n1 = 0 & x.iter(O,n1) = {}) &
x.iter(O,n1+1) = {} by C1,B1;
consider n2 being Nat such that
C3: f2.x = n2 & (x.iter(O,n2) <> {} or n2 = 0 & x.iter(O,n2) = {}) &
x.iter(O,n2+1) = {} by C1,B2;
A3: now assume
C4: n1 < n2; then n1+1 <= n2 by NAT_1:13;
hence contradiction by C4,C2,C3,Th31,NAT_1:2;
end;
now assume
C4: n2 < n1; then n2+1 <= n1 by NAT_1:13;
hence contradiction by C4,C2,C3,Th31,NAT_1:2;
end;
hence f1.y = f2.y by C2,C3,A3,XXREAL_0:1;
end;
hence thesis by A1,A2,A5,FUNCT_1:2;
end;
end;
registration
cluster empty -> irreflexive co-well_founded for Relation;
coherence
proof
let R; assume
A0: R is empty; then
A1: dom R = {} & rng R = {};
thus R is irreflexive
proof let x be element;
thus thesis by A0;
end;
let X; assume X c= field R & X <> {};
hence thesis by A1;
end;
end;
registration
let X;
cluster empty for Operation of X;
existence
proof
take {}[:X,X:]; thus thesis;
end;
end;
registration
let X;
let O be co-well_founded irreflexive finite Operation of X;
cluster iteration_of O -> antisymmetric transitive beta-transitive;
coherence
proof
consider f being Function of X,NAT such that
A1: iteration_of O = value_of f and
for x being Element of X st x in X
ex n st f.x = n & (x.iter(O,n) <> {} or n = 0 & x.iter(O,n) = {}) &
x.iter(O,n+1) = {} by ITER;
thus thesis by A1;
end;
end;
begin :: "value of" ordering
registration
let X be finite set;
cluster -> well_founded for Order of X;
coherence
proof let R be Order of X;
let Y be set; assume
A1: Y c= field R & Y <> {};
defpred P[set] means $1 <> {} implies
ex a being set st a in $1 & R-Seg a misses $1;
A2: Y is finite by A1;
A3: P[{}];
A4: for x, B being set st x in Y & B c= Y & P[B] holds P[B \/ {x}]
proof
let x, B be set; assume that
B1: x in Y & B c= Y & P[B] and
B \/ {x} <> {};
per cases;
suppose
B2: B = {};
take a = x; thus a in B\/{x} by B2,TARSKI:def 1;
x nin R-Seg a by WELLORD1:1;
hence R-Seg a misses B \/ {x} by B2,ZFMISC_1:50;
end;
suppose
B <> {}; then
consider a being set such that
B4: a in B & R-Seg a misses B by B1;
per cases;
suppose x nin R-Seg a; then
B5: R-Seg a misses {x} by ZFMISC_1:50;
take a; thus a in B\/{x} by B4,XBOOLE_0:def 3;
thus R-Seg a misses B \/ {x} by B4,B5,XBOOLE_1:70;
end;
suppose x in R-Seg a; then
B6: x <> a & [x,a] in R by WELLORD1:1;
take b = x;
b in {x} by TARSKI:def 1;
hence b in B\/{x} by XBOOLE_0:def 3;
assume R-Seg b meets B \/ {x}; then
consider c being element such that
B7: c in R-Seg b & c in B \/ {x} by XBOOLE_0:3;
reconsider cc = c, xx = x, aa = a as set by TARSKI:1;
B8: c <> b & [c,b] in R by B7,WELLORD1:1; then
cc,xx in R & x,a in R by B6; then
B9: cc,aa in R & c <> a by B8,ANTIS,TRANS; then
[c,a] in R & (c in B or c in {x})
by B7,XBOOLE_0:def 3; then
c in R-Seg a & c in B by B8,B9,TARSKI:def 1,WELLORD1:1;
hence thesis by B4,XBOOLE_0:3;
end;
end;
end;
P[Y] from FINSET_1:sch 2(A2,A3,A4);
hence ex a being element st a in Y & R-Seg a misses Y by A1;
end;
end;
registration
let X be finite set;
cluster -> well-ordering for connected Order of X;
coherence by WELLORD1:def 4;
end;
definition
let X;
let R be connected Order of X;
let S be finite Subset of X;
func order(S,R) -> XFinSequence of X means :ORD:
rng it = S & it is one-to-one &
for i,j being Nat st i in dom it & j in dom it holds
i <= j iff it.i,it.j in R;
existence
proof
set Q = R|_2 S;
A1: Q is total Relation of S &Q is reflexive transitive antisymmetric connected
by Lm5,WELLORD1:16,17,18; then
Q, RelIncl order_type_of Q are_isomorphic by WELLORD2:def 2; then
consider f being Function such that
A2: f is_isomorphism_of RelIncl order_type_of Q, Q by WELLORD1:def 8,40;
field RelIncl order_type_of Q = order_type_of Q by WELLORD2:def 1; then
A4: dom f = order_type_of Q by A2;
A5: rng f = field Q & f is one-to-one by A2; then
order_type_of Q, field Q are_equipotent by A4,WELLORD2:def 4; then
order_type_of Q is finite by CARD_1:38; then
reconsider f as XFinSequence by A4,AFINSQ_1:5;
field Q c= S by WELLORD1:13; then
reconsider f as XFinSequence of X by RELAT_1:def 19,A5,XBOOLE_1:1;
take f;
thus
B1: rng f = S & f is one-to-one by A5,A1,ORDERS_1:12;
let i,j be Nat; assume
A6: i in dom f & j in dom f; then
A7: f.i in S & f.j in S by B1,FUNCT_1:def 3;
[i,j] in RelIncl order_type_of Q iff i c= j by A4,A6,WELLORD2:def 1; then
i <= j iff [f.i,f.j] in Q by A2,A6,NAT_1:39; then
i <= j iff [f.i,f.j] in R by A7,Lm4;
hence i <= j iff f.i,f.j in R;
end;
uniqueness
proof let f1,f2 be XFinSequence of X such that
A1: rng f1 = S & f1 is one-to-one &
for i,j being Nat st i in dom f1 & j in dom f1 holds
i <= j iff f1.i,f1.j in R and
A2: rng f2 = S & f2 is one-to-one &
for i,j being Nat st i in dom f2 & j in dom f2 holds
i <= j iff f2.i,f2.j in R;
dom f1, S are_equipotent & dom f2, S are_equipotent
by A1,A2,WELLORD2:def 4; then
dom f1, dom f2 are_equipotent by WELLORD2:15; then
card dom f1 = dom f2 by CARD_1:def 2; then
A3: dom f1 = dom f2 by CARD_1:def 2;
assume f1 <> f2; then
consider x be element such that
A4: x in dom f1 & f1.x <> f2.x by A3;
defpred P[Nat] means $1 in dom f1 & f1.$1 <> f2.$1;
A5: ex n st P[n] by A4;
consider n such that
A6: P[n] & for m st P[m] holds n <= m from NAT_1:sch 5(A5);
f1.n in S by A1,A6,FUNCT_1:def 3; then
consider a being element such that
A7: a in dom f2 & f1.n = f2.a by A2,FUNCT_1:def 3;
f2.n in S by A2,A3,A6,FUNCT_1:def 3; then
consider b being element such that
A8: b in dom f1 & f2.n = f1.b by A1,FUNCT_1:def 3;
reconsider a,b as Element of NAT by A7,A8;
B9: now
assume a < n; then
f1.a = f2.a by A3,A6,A7;
hence contradiction by A1,A3,A6,A7;
end;
now
assume b < n; then
f1.b = f2.b by A6,A8;
hence contradiction by A2,A3,A6,A8;
end; then
f1.n,f1.b in R & f2.n,f2.a in R by A1,A2,A3,A6,A7,A8,B9;
hence contradiction by A6,A7,A8,ANTIS;
end;
end;
theorem
for S1,S2 being finite Subset of X
for R being connected Order of X holds
order(S1 \/ S2,R) = order(S1,R)^order(S2,R) iff
for x,y st x in S1 & y in S2 holds x <> y & x,y in R
proof
let S1,S2 be finite Subset of X;
let R be connected Order of X;
A1: rng order(S1\/S2,R) = S1\/S2 & rng order(S1,R) = S1 & rng order(S2,R) = S2
by ORD;
B1: dom (order(S1,R)^order(S2,R)) = dom order(S1,R)+^dom order(S2,R)
by ORDINAL4:def 1;
B2: order(S1\/S2,R) is one-to-one & order(S1,R) is one-to-one &
order(S2,R) is one-to-one by ORD;
hereby
assume
A5: order(S1 \/ S2,R) = order(S1,R)^order(S2,R);
let x,y; assume
A3: x in S1 & y in S2; then
consider z be element such that
A2: z in dom order(S1,R) & x = order(S1,R).z by A1,FUNCT_1:def 3;
consider s being element such that
A4: s in dom order(S2,R) & y = order(S2,R).s by A1,A3,FUNCT_1:def 3;
reconsider z,s as Element of NAT by A2,A4;
A7: order(S1\/S2,R).z = x & order(S1\/S2,R).(dom order(S1,R)+^s) = y
by A5,A2,A4,ORDINAL4:def 1;
A8: z in dom order(S1\/S2,R) & dom order(S1,R)+^s in dom order(S1\/S2,R)
by B1,A2,A4,A5,ORDINAL3:17,25;
A9: dom order(S1,R)+^s = Segm (dom order(S1,R)+s) by CARD_2:36;
z in dom order(S1,R)+^s by A2,ORDINAL3:25; then
z < dom order(S1,R)+s by A9,NAT_1:44;
hence x <> y & x,y in R by B2,A7,A8,A9,ORD;
end;
assume
C1: for x,y st x in S1 & y in S2 holds x <> y & x,y in R;
C2: rng(order(S1,R)^order(S2,R)) = S1 \/ S2 by A1,Lm8;
set o1 = order(S1,R), o2 = order(S2,R);
C3: order(S1,R)^order(S2,R) is one-to-one
proof
let x,y be element; assume
D1: x in dom (o1^o2) & y in dom (o1^o2) & (o1^o2).x = (o1^o2).y;
per cases by D1,B1,ORDINAL3:38;
suppose
D2: x in dom o1 & y in dom o1; then
(o1^o2).x = o1.x & (o1^o2).y = o1.y by ORDINAL4:def 1;
hence x = y by B2,D1,D2;
end;
suppose
D3: x in dom o1 & ex a being Ordinal st a in dom o2 & y = dom o1+^a; then
consider a being Ordinal such that
D4: a in dom o2 & y = dom o1+^a;
(o1^o2).x = o1.x & (o1^o2).y = o2.a by D3,D4,ORDINAL4:def 1; then
(o1^o2).x in S1 & (o1^o2).y in S2 by A1,D3,D4,FUNCT_1:def 3;
hence thesis by C1,D1;
end;
suppose
D3: y in dom o1 & ex a being Ordinal st a in dom o2 & x = dom o1+^a; then
consider a being Ordinal such that
D4: a in dom o2 & x = dom o1+^a;
(o1^o2).y = o1.y & (o1^o2).x = o2.a by D3,D4,ORDINAL4:def 1; then
(o1^o2).x in S2 & (o1^o2).y in S1 by A1,D3,D4,FUNCT_1:def 3;
hence thesis by C1,D1;
end;
suppose
D5: (ex a being Ordinal st a in dom o2 & x = dom o1+^a) &
ex a being Ordinal st a in dom o2 & y = dom o1+^a; then
consider a being Ordinal such that
D6: a in dom o2 & x = dom o1+^a;
consider b being Ordinal such that
D7: b in dom o2 & y = dom o1+^b by D5;
(o1^o2).x = o2.a & (o1^o2).y = o2.b by D6,D7,ORDINAL4:def 1;
hence thesis by D6,D7,B2,D1;
end;
end;
now let x,y be Nat;
assume
D1: x in dom(o1^o2) & y in dom(o1^o2);
per cases by D1,B1,ORDINAL3:38;
suppose
D2: x in dom o1 & y in dom o1; then
(o1^o2).x = o1.x & (o1^o2).y = o1.y by ORDINAL4:def 1;
hence x <= y iff (o1^o2).x, (o1^o2).y in R by D2,ORD;
end;
suppose
D3: x in dom o1 & ex a being Ordinal st a in dom o2 & y = dom o1+^a; then
consider a being Ordinal such that
D4: a in dom o2 & y = dom o1+^a;
(o1^o2).x = o1.x & (o1^o2).y = o2.a & x in Segm y
by D3,D4,ORDINAL3:25,ORDINAL4:def 1; then
(o1^o2).x in S1 & (o1^o2).y in S2 & x < y
by A1,D3,D4,FUNCT_1:def 3,NAT_1:44;
hence x <= y iff (o1^o2).x, (o1^o2).y in R by C1;
end;
suppose
D3: y in dom o1 & ex a being Ordinal st a in dom o2 & x = dom o1+^a; then
consider a being Ordinal such that
D4: a in dom o2 & x = dom o1+^a;
D7: (o1^o2).y = o1.y & (o1^o2).x = o2.a & y in Segm x
by D3,D4,ORDINAL3:25,ORDINAL4:def 1; then
D5: (o1^o2).x in S2 & (o1^o2).y in S1 & y < x
by A1,D3,D4,FUNCT_1:def 3,NAT_1:44;
thus x <= y implies (o1^o2).x, (o1^o2).y in R by D7,NAT_1:44;
assume
D6: (o1^o2).x, (o1^o2).y in R;
(o1^o2).y, (o1^o2).x in R by D5,C1;
hence x <= y by D1,C3,D6,ANTIS;
end;
suppose
D5: (ex a being Ordinal st a in dom o2 & x = dom o1+^a) &
ex a being Ordinal st a in dom o2 & y = dom o1+^a; then
consider a being Ordinal such that
D6: a in dom o2 & x = dom o1+^a;
consider b being Ordinal such that
D7: b in dom o2 & y = dom o1+^b by D5;
reconsider a,b as Element of NAT by D6,D7;
x <= y iff x c= y by NAT_1:39; then
x <= y iff a c= b by D6,D7,ORDINAL3:23,18; then
(x <= y iff a <= b) & (o1^o2).x = o2.a & (o1^o2).y = o2.b
by D6,D7,ORDINAL4:def 1,NAT_1:39;
hence x <= y iff (o1^o2).x, (o1^o2).y in R by D6,D7,ORD;
end;
end;
hence thesis by C2,C3,ORD;
end;
definition
let X be finite set;
let O be Operation of X;
let R be connected Order of X;
func value_of(O,R) -> Relation of X means :VAL2:
for x,y being Element of X holds
x,y in it iff x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
existence
proof
defpred P[element,element] means
ex x,y being Element of X st $1 = x & $2 = y &
x.O <> {} & (y.O = {} or y.O <> {} & order(x.O,R)/.0,order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
consider R1 such that
A1: for x,y be element holds [x,y] in R1 iff x in X & y in X & P[x,y]
from RELAT_1:sch 1;
R1 c= [:X,X:]
proof
let x,y be element; assume [x,y] in R1; then
x in X & y in X by A1;
hence thesis by ZFMISC_1:87;
end; then
reconsider R1 as Relation of X;
take R1;
let x,y be Element of X;
A2: x.O <> {} implies x in dom O by RELAT_1:170;
hereby
assume x,y in R1; then P[x,y] by A1;
hence x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
end;
assume x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
hence thesis by A1,A2;
end;
uniqueness
proof
let R1,R2 be Relation of X such that
A1: for x,y being Element of X holds
x,y in R1 iff x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0) and
A2: for x,y being Element of X holds
x,y in R2 iff x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
let x,y be element;
thus [x,y] in R1 implies [x,y] in R2
proof assume
A3: [x,y] in R1; then
reconsider x,y as Element of X by ZFMISC_1:87;
x,y in R1 by A3; then
x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0) by A1; then
x,y in R2 by A2;
hence thesis;
end;
assume
A3: [x,y] in R2; then
reconsider x,y as Element of X by ZFMISC_1:87;
x,y in R2 by A3; then
x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0) by A2; then
x,y in R1 by A1;
hence thesis;
end;
end;
registration
let X be finite set;
let O be Operation of X;
let R1 be connected Order of X;
cluster value_of(O,R1) -> antisymmetric transitive beta-transitive;
coherence
proof set R = value_of(O,R1);
thus R is antisymmetric
proof
let x,y; assume
A1: x,y in R & y,x in R; then
reconsider x,y as Element of X by Lm2;
y = y & x = x; then
x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R1)/.0, order(y.O,R1)/.0 in R1 &
order(x.O,R1)/.0 <> order(y.O,R1)/.0) &
y.O <> {} & (x.O = {} or
x.O <> {} & order(y.O,R1)/.0, order(x.O,R1)/.0 in R1 &
order(y.O,R1)/.0 <> order(x.O,R1)/.0) by A1,VAL2;
hence thesis by ANTIS;
end;
thus R is transitive
proof
let x,y,z; assume
A1: x,y in R & y,z in R; then
reconsider x,y,z as Element of X by Lm2;
y = y & z = z; then
x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R1)/.0, order(y.O,R1)/.0 in R1 &
order(x.O,R1)/.0 <> order(y.O,R1)/.0) &
y.O <> {} & (z.O = {} or
z.O <> {} & order(y.O,R1)/.0, order(z.O,R1)/.0 in R1 &
order(y.O,R1)/.0 <> order(z.O,R1)/.0) by A1,VAL2; then
x.O <> {} & (z.O = {} or
z.O <> {} & order(x.O,R1)/.0, order(z.O,R1)/.0 in R1 &
order(x.O,R1)/.0 <> order(z.O,R1)/.0) by TRANS,ANTIS;
hence thesis by VAL2;
end;
let x,y be Element of X such that
A2: x,y nin R;
let z be Element of X; assume x,z in R; then
x in X & z in X & x.O <> {} & (z.O = {} or
z.O <> {} & order(x.O,R1)/.0, order(z.O,R1)/.0 in R1 &
order(x.O,R1)/.0 <> order(z.O,R1)/.0) &
(x.O = {} or y.O <> {} &
(y.O = {} or order(x.O,R1)/.0,order(y.O,R1)/.0 nin R1 or
order(x.O,R1)/.0 = order(y.O,R1)/.0))
by A2,Lm2,VAL2; then
y.O <> {} & (z.O = {} or
z.O <> {} & order(y.O,R1)/.0, order(z.O,R1)/.0 in R1 &
order(y.O,R1)/.0 <> order(z.O,R1)/.0) by SEGM;
hence y,z in R by VAL2;
end;
end;