:: Sorting by Exchanging
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-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 ORDINAL6, EXCHSORT, ZFMISC_1, XBOOLE_0, RELAT_1, FUNCT_1,
ORDINAL1, ORDINAL2, ORDINAL4, FINSET_1, RELAT_2, FUNCT_4, FINSEQ_1,
AOFA_000, FUNCT_3, VALUED_0, WELLFND1, CARD_1, TARSKI, FUNCT_2, PARTFUN1,
FUNCT_7, REARRAN1, ORDINAL3, NAT_1, SUBSET_1, XXREAL_0, ARYTM_3,
AFINSQ_1, REWRITE1, NUMBERS, MSUALG_1, MEMBERED, STRUCT_0, ORDERS_2,
REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, BINOP_1,
FUNCT_4, FUNCT_7, ORDINAL1, NUMBERS, MEMBERED, VALUED_0, CARD_1,
XCMPLX_0, ORDINAL2, ORDINAL3, ORDINAL4, AFINSQ_1, STRUCT_0, ORDERS_2,
WAYBEL_0, XXREAL_0, XREAL_0, NAT_1, AOFA_000, ORDINAL5, FUNCT_3,
ORDINAL6;
constructors MEMBERED, VALUED_0, CATALAN2, ORDINAL3, INT_1, FUNCT_7, ORDINAL5,
WELLORD2, RELAT_2, FACIRC_1, BINOP_1, WAYBEL_0, RELSET_1, ORDINAL6,
XTUPLE_0;
registrations MEMBERED, SUBSET_1, RELSET_1, XXREAL_0, XBOOLE_0, FINSET_1,
RELAT_1, FUNCT_1, ORDINAL1, VALUED_0, ORDINAL5, AFINSQ_1, CARD_1,
FUNCT_2, FUNCT_7, FUNCTOR1, STRUCT_0, WAYBEL_0, ORDINAL6, XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, PARTFUN1, FUNCT_2, ORDINAL1,
WELLORD2, FUNCT_1, VALUED_0, ORDINAL5, ORDINAL6;
equalities ORDINAL1, ORDINAL2, BINOP_1;
expansions TARSKI, XBOOLE_0, ORDINAL1, WELLORD2, FUNCT_1, VALUED_0;
theorems TARSKI, CARD_1, ZFMISC_1, ORDINAL1, ORDINAL2, RELAT_1, RELSET_1,
MEMBERED, FINSET_1, CARD_2, TREES_1, GRFUNC_1, FUNCT_2, XBOOLE_1,
FINSEQ_3, NAT_1, XBOOLE_0, ORDINAL3, XXREAL_0, SETFAM_1, ORDINAL4,
FUNCT_1, FUNCT_7, SUBSET_1, FUNCT_3, FUNCT_4, FUNCT_5, AFINSQ_1,
PARTFUN1, ORDERS_2, YELLOW_0, WAYBEL_0, ORDINAL6, XTUPLE_0;
schemes NAT_1, ORDINAL2, RECDEF_1;
begin :: Preliminaries
reserve a,a1,a2,b,c,d for Ordinal,
n,m,k for Nat,
x,y,z,t,X,Y,Z for set;
theorem Th1:
x in (a+^b)\a iff ex c st x = a+^c & c in b
proof
A1: x in (a+^b)\a iff a c= x & x in a+^b by ORDINAL6:5;
hereby assume
A2: x in (a+^b)\a; then
reconsider c = x as Ordinal;
take d = c-^a;
thus x = a+^d by A1,A2,ORDINAL3:def 5;
hence d in b by A2,ORDINAL3:22;
end;
given c such that
A3: x = a+^c & c in b;
a c= x & x in a+^b by A3,ORDINAL2:32,ORDINAL3:24;
hence thesis by ORDINAL6:5;
end;
defpred Case1[set,set,set,set] means
$3 <> $1 & $3 <> $2 & $4 <> $1 & $4 <> $2;
defpred Case2[set,set,set,set] means
$3 in $1 & $4 = $1;
defpred Case3[set,set,set,set] means
$3 in $1 & $4 = $2;
defpred Case4[set,set,set,set] means
$3 = $1 & $4 in $2;
defpred Case5[set,set,set,set] means
$3 = $1 & $4 = $2;
defpred Case6[set,set,set,set] means
$3 = $1 & $2 in $4;
defpred Case7[set,set,set,set] means
$1 in $3 & $4 = $2;
defpred Case8[set,set,set,set] means
$3 = $2 & $2 in $4;
theorem Th2:
a in b & c in d implies
c <> a & c <> b & d <> a & d <> b or
c in a & d = a or c in a & d = b or
c = a & d in b or c = a & d = b or c = a & b in d or
a in c & d = b or c = b & b in d
proof assume
A1: a in b & c in d;
per cases by ORDINAL1:14;
suppose
c in a;
hence thesis by A1;
end;
suppose
c = a;
hence thesis by ORDINAL1:14;
end;
suppose
A2: a in c & c in b;
per cases by ORDINAL1:14;
suppose d in b;
hence thesis by A1;
end;
suppose d = b;
hence thesis by A2;
end;
suppose b in d;
hence thesis by A1;
end;
end;
suppose
c = b;
hence thesis by A1;
end;
suppose
b in c;
hence thesis by A1;
end;
end;
theorem
x nin y implies (y\/{x})\y = {x} by XBOOLE_1:88,ZFMISC_1:50;
theorem Th4:
(succ x)\x = {x}
proof
not x in x; then
succ x = x\/{x} & x nin x;
hence thesis by XBOOLE_1:88,ZFMISC_1:50;
end;
theorem Th5:
for f being Function, r being Relation
for x being object holds x in f.:r iff
ex y,z being object st [y,z] in r & [y,z] in dom f & f.(y,z) = x
proof
let f be Function;
let r be Relation;
let x be object;
hereby assume x in f.:r; then
consider t being object such that
A1: t in dom f & t in r & x = f.t by FUNCT_1:def 6;
consider y,z being object such that
A2: t = [y,z] by A1,RELAT_1:def 1;
f.(y,z) = f.[y,z];
hence ex y,z being object st [y,z] in r & [y,z] in dom f & f.(y,z) = x
by A1,A2;
end;
thus thesis by FUNCT_1:def 6;
end;
theorem Th6:
a\b <> {} implies inf(a\b) = b & sup(a\b) = a & union(a\b) = union a
proof assume
A1: a\b <> {};
set x = the Element of a\b;
A2: x in a\b by A1;
A3: x in a & x nin b by A1,XBOOLE_0:def 5; then
A: b c= x by ORDINAL6:4;
not b in b; then
b in a & b nin b by A,A3,ORDINAL1:12; then
A4: b in a\b by XBOOLE_0:def 5;
hence inf(a\b) c= b by ORDINAL2:14;
inf(a\b) in a\b by A2,ORDINAL2:17; then
inf(a\b) nin b by XBOOLE_0:def 5;
hence b c= inf(a\b) by ORDINAL6:4;
A5: On(a\b) = a\b by ORDINAL6:2;
thus sup(a\b) c= a by A5,ORDINAL2:def 3;
thus a c= sup(a\b)
proof
let c; assume
A6: c in a;
A7: b in sup(a\b) by A4,ORDINAL2:19;
per cases;
suppose c in b;
hence thesis by A7,ORDINAL1:10;
end;
suppose c nin b; then
c in a\b by A6,XBOOLE_0:def 5;
hence thesis by ORDINAL2:19;
end;
end;
thus union(a\b) c= union a by ZFMISC_1:77;
for y be object st y in union a holds y in union(a\b)
proof
let y be object; assume y in union a; then
consider x such that
A8: y in x & x in a by TARSKI:def 4;
reconsider x as Ordinal by A8;
per cases by ORDINAL6:4;
suppose x in b; then
y in b by A8,ORDINAL1:10;
hence thesis by A4,TARSKI:def 4;
end;
suppose b c= x; then
x in a\b by A8,ORDINAL6:5;
hence thesis by A8,TARSKI:def 4;
end;
end;
hence union a c= union(a\b);
end;
theorem Th7:
a\b is non empty finite implies
ex n being Nat st a = b+^n
proof assume
A1: a\b is non empty finite;
set x = the Element of a\b;
A2: x in a & x nin b by A1,XBOOLE_0:def 5; then
b c= x by ORDINAL6:4; then
consider c such that
A3: a = b+^c & c <> {} by A2,ORDINAL1:12,ORDINAL3:28;
deffunc F(Ordinal) = b+^$1;
consider f being Sequence such that
A4: dom f = omega & for d st d in omega holds f.d = F(d) from ORDINAL2:sch 2;
f is one-to-one
proof
let x,y be object; assume
A5: x in dom f & y in dom f & f.x = f.y & x <> y; then
reconsider x,y as Element of omega by A4;
A6: f.x = F(x) & f.y = F(y) by A4;
x in y or y in x by A5,ORDINAL1:14; then
b+^x in b+^y or b+^y in b+^x by ORDINAL2:32;
hence contradiction by A5,A6;
end; then
A7: omega, rng f are_equipotent by A4;
now assume
omega c= c; then
A8: F(omega) c= a by A3,ORDINAL2:33;
rng f c= a\b
proof
let y be object; assume y in rng f; then
consider x being object such that
A9: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as Element of omega by A4,A9;
A10: y = F(x) by A4,A9;
b c= F(x) & F(x) in F(omega) by ORDINAL2:32,ORDINAL3:24; then
y nin b & y in a by A8,A10,ORDINAL6:4;
hence thesis by XBOOLE_0:def 5;
end;
hence contradiction by A1,A7,CARD_1:38;
end; then
c in omega by ORDINAL6:4;
hence thesis by A3;
end;
begin :: Arrays
definition let f be set;
attr f is segmental means :Def1:
ex a,b st proj1 f = a\b;
end;
reserve f,g for Function;
theorem
dom f = dom g & f is segmental implies g is segmental;
theorem Th9:
f is segmental implies
for a,b,c st a c= b & b c= c & a in dom f & c in dom f holds b in dom f
proof given x,y being Ordinal such that
A1: dom f = x\y;
let a,b,c; assume
A2: a c= b & b c= c & a in dom f & c in dom f; then
y c= a & c in x by A1,ORDINAL6:5; then
y c= b & b in x by A2,ORDINAL1:12;
hence thesis by A1,ORDINAL6:5;
end;
registration
cluster Sequence-like -> segmental for Function;
coherence
proof
let f;
assume f is Sequence-like; then
reconsider f as Sequence;
take dom f, 0; thus thesis;
end;
cluster FinSequence-like -> segmental for Function;
coherence
proof
let f;
assume f is FinSequence-like; then
reconsider g = f as FinSequence;
take a = succ len g, b = 1;
reconsider c = len g as Nat;
thus dom f c= a\b
proof
let x be object; assume
A1: x in dom f; then x in dom g; then reconsider x as Nat;
x <= c by A1,FINSEQ_3:25; then
A2: 1 <= x & x <= c by A1,FINSEQ_3:25; then
Segm succ 0 c= Segm x & Segm x c= Segm c by NAT_1:39; then
A3: 0 in x & x in a by ORDINAL1:22;
not x in b by A2,CARD_1:49,TARSKI:def 1;
hence thesis by A3,XBOOLE_0:def 5;
end;
reconsider d = a as Element of NAT by ORDINAL1:def 12;
let x be object; assume
x in a\b; then
A4: x in d & not x in b by XBOOLE_0:def 5;
then x in Segm d;
then reconsider x as Nat;
Segm x c= Segm c & Segm b c= Segm x by A4,ORDINAL1:16,22; then
1 <= x & x <= c by NAT_1:39;
hence thesis by FINSEQ_3:25;
end;
end;
definition
let a;
let s be set;
attr s is a-based means b in proj1 s implies a in proj1 s & a c= b;
attr s is a-limited means a = sup proj1 s;
end;
theorem
f is a-based segmental iff ex b st dom f = b\a & a c= b
proof
thus f is a-based segmental implies ex b st dom f = b\a & a c= b
proof
assume
A1: b in dom f implies a in dom f & a c= b;
given c,d such that
A2: dom f = c\d;
set x = the Element of c\d;
per cases;
suppose dom f = {}; then
a\a = dom f by XBOOLE_1:37;
hence thesis;
end;
suppose
dom f <> {}; then
x in dom f by A2; then
a in dom f by A1; then
A3: d c= a & a in c by A2,ORDINAL6:5; then
d in c by ORDINAL1:12; then
d in dom f by A2,ORDINAL6:5; then
a c= d by A1; then
a = d & a c= c by A3,ORDINAL1:def 2;
hence thesis by A2;
end;
end;
given b such that
A4: dom f = b\a & a c= b;
thus f is a-based
proof
let c; assume
A5: c in dom f; then
a c= c & c in b by A4,ORDINAL6:5; then
a in b by ORDINAL1:12;
hence thesis by A4,A5,ORDINAL6:5;
end;
take b,a; thus thesis by A4;
end;
theorem
f is b-limited non empty segmental iff ex a st dom f = b\a & a in b
proof
thus f is b-limited non empty segmental implies
ex a st dom f = b\a & a in b
proof assume
A1: b = sup dom f;
assume
A2: f is non empty;
given c,d such that
A3: dom f = c\d;
set x = the Element of c\d;
take a = d;
A4: b = c by A2,A1,A3,Th6;
thus dom f = b\a by A2,A1,A3,Th6;
a c= x & x in b by A2,A3,A4,ORDINAL6:5;
hence a in b by ORDINAL1:12;
end;
given a such that
A5: dom f = b\a & a in b;
a in dom f by A5,ORDINAL6:5;
hence b = sup dom f by A5,Th6;
thus f is non empty by A5,ORDINAL6:5;
take b,a;
thus thesis by A5;
end;
registration
cluster Sequence-like -> 0-based for Function;
coherence
by ORDINAL3:8;
cluster FinSequence-like -> 1-based for Function;
coherence
proof
let f; assume
f is FinSequence-like; then
reconsider g = f as FinSequence;
let b; assume b in dom f; then
A1: b in dom g; then
reconsider bb=b as Nat;
A2: 1 <= bb & bb <= len g by A1,FINSEQ_3:25; then
A3: 1 <= len g by XXREAL_0:2;
thus 1 in proj1 f by FINSEQ_3:25,A3;
Segm 1 c= Segm bb by A2,NAT_1:39;
hence 1 c= b;
end;
end;
theorem Th12:
f is (inf dom f)-based
by ORDINAL2:14,ORDINAL2:17;
theorem
f is (sup dom f)-limited;
theorem
f is b-limited & a in dom f implies a in b
by ORDINAL2:19;
definition let f;
func base-f -> Ordinal means:
Def4:
f is it-based if ex a st a in dom f
otherwise it = 0;
existence
proof set b = inf dom f;
hereby
given a such that a in dom f;
take b; thus f is b-based by Th12;
end;
assume not ex a st a in dom f;
take 0; thus thesis;
end;
uniqueness
proof let b,c;
hereby
given a such that
A1: a in dom f;
assume
A2: f is b-based & f is c-based;
thus b = c
proof
c in dom f by A1,A2;
hence b c= c by A2;
b in dom f by A1,A2;
hence c c= b by A2;
end;
end;
thus thesis;
end;
consistency;
func limit-f -> Ordinal means:
Def5:
f is it-limited if ex a st a in dom f
otherwise it = 0;
existence
proof set b = sup dom f;
hereby
given a such that a in dom f;
take b; thus f is b-limited;
end;
assume not ex a st a in dom f;
take 0; thus thesis;
end;
uniqueness;
consistency;
end;
definition
let f;
func len-f -> Ordinal equals (limit-f)-^(base-f);
coherence;
end;
theorem Th15:
base-{} = 0 & limit-{} = 0 & len-{} = 0
proof
not ex a st a in dom {};
hence base-{} = 0 & limit-{} = 0 by Def4,Def5;
hence thesis by ORDINAL3:56;
end;
theorem Th16:
limit-f = sup dom f
proof
per cases;
suppose
A1: a nin dom f;
On dom f c= 0
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in On dom f; then
x in dom f & xx is ordinal by ORDINAL1:def 9;
hence thesis by A1;
end; then
sup dom f c= 0 by ORDINAL2:def 3; then
sup dom f = 0;
hence thesis by A1,Def5;
end;
suppose
A2: ex a st a in dom f;
f is (sup dom f)-limited;
hence thesis by A2,Def5;
end;
end;
theorem
f is (limit-f)-limited
by Th16;
theorem
for A being empty set holds A is a-based;
registration let a,X,Y;
cluster Y-defined X-valued a-based segmental finite empty for Sequence;
existence
proof
take A = {}[:Y,X:];
thus thesis;
end;
end;
definition
mode array is segmental Function;
end;
registration
let A be array;
cluster dom A -> ordinal-membered;
coherence
proof
consider a,b such that
A1: dom A = a\b by Def1;
take a; thus thesis by A1;
end;
end;
theorem
for f being array holds f is 0-limited iff f is empty
proof let f be array;
thus f is 0-limited implies f is empty
proof assume sup dom f = 0; then
dom f c= 0 by ORDINAL6:3;
hence f is empty;
end;
assume f is empty;
hence sup dom f = 0 by ORDINAL2:18;
end;
registration
cluster 0-based -> Sequence-like for array;
coherence
proof
let s be array;
assume
A1: b in proj1 s implies 0 in proj1 s & 0 c= b;
consider c,a such that
A2: dom s = c\a by Def1;
set x = the Element of c\a;
now assume
A3: c\a <> {}; then
x in c by XBOOLE_0:def 5; then
0 in dom s by A1,A2,A3; then
0 nin a by A2,XBOOLE_0:def 5; then
a c= 0 by ORDINAL6:4; then
a = 0;
hence dom s = c by A2;
end;
hence dom s is epsilon-transitive epsilon-connected by A2;
end;
end;
definition
let X;
mode array of X is X-valued array;
end;
definition
let X be 1-sorted;
mode array of X is array of the carrier of X;
end;
definition
let a,X;
mode array of a,X is a-defined array of X;
end;
reserve A,B,C for array;
theorem Th20:
base-f = inf dom f
proof set A = f;
set b = inf dom A;
A1: A is b-based by Th12;
per cases;
suppose ex a st a in dom A;
hence thesis by A1,Def4;
end;
suppose
A2: not ex a st a in dom A;
set x = the Element of On dom A;
now
assume On dom A <> {}; then
x in dom A by ORDINAL1:def 9;
hence contradiction by A2;
end; then
b = 0 by SETFAM_1:def 1;
hence thesis by A2,Def4;
end;
end;
theorem
f is (base-f)-based
proof
base-f = inf dom f by Th20;
hence thesis by Th12;
end;
theorem
dom A = (limit-A) \ (base-A)
proof
consider a,b such that
A1: dom A = a\b by Def1;
A2: limit-A = sup dom A by Th16;
A3: base-A = inf dom A by Th20;
thus dom A c= (limit-A) \ (base-A)
proof let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in dom A; then
A4: base-A c= xx & x in limit-A by A2,A3,ORDINAL2:14,19; then
A: x in base-A implies x in xx;
not xx in xx;
hence thesis by A,A4,XBOOLE_0:def 5;
end;
let x be object; assume
A5: x in (limit-A) \ (base-A); then
reconsider x as Ordinal;
ex c st c in dom A & x c= c by A2,A5,ORDINAL2:21; then
a = limit-A & b = base-A by A1,A2,A3,Th6;
hence thesis by A1,A5;
end;
theorem Th23:
dom A = a\b & A is non empty implies base-A = b & limit-A = a
proof assume
A1: dom A = a\b & A is non empty;
set x = the Element of dom A;
dom A <> {} by A1; then
A2: x in a\b by A1;
A: b c= x & x in a by A1,ORDINAL6:5;
not b in b; then
A3: b in a & b nin b by A,ORDINAL1:12; then
b in a\b by XBOOLE_0:def 5; then
A4: b in sup dom A by A1,ORDINAL2:19;
A is b-based
by A1,A3,ORDINAL6:5;
hence base-A = b by Def4,A1,A2;
A5: a c= sup dom A
proof
let x be Ordinal; assume
A6: x in a;
per cases;
suppose
x in b;
hence thesis by A4,ORDINAL1:10;
end;
suppose
x nin b; then
x in a\b by A6,XBOOLE_0:def 5;
hence thesis by A1,ORDINAL2:19;
end;
end;
sup dom A c= sup a by A1,ORDINAL2:22; then
sup dom A c= a by ORDINAL2:18; then
a = sup dom A by A5;
hence thesis by Th16;
end;
theorem Th24:
for f be Sequence holds
base-f = 0 & limit-f = dom f & len-f = dom f
proof
let f be Sequence;
per cases;
suppose f = {};
hence thesis by Th15;
end;
suppose
A1: f <> {};
(dom f)\0 = dom f;
hence base-f = 0 & limit-f = dom f by A1,Th23;
hence len-f = dom f by ORDINAL3:56;
end;
end;
registration
let a,b,X;
cluster b-based natural-valued INT-valued real-valued complex-valued
finite for array of a,X;
existence
proof
set A = the empty array of a,X;
take A; thus thesis;
end;
end;
registration
let a,x;
cluster {[a,x]} -> segmental;
coherence
proof
take succ a, a;
thus dom {[a,x]} = {a} by FUNCT_5:12
.= (succ a)\a by Th4;
end;
end;
registration
let a; let x be Nat;
cluster {[a,x]} -> natural-valued for array;
coherence
proof let A; assume A = {[a,x]}; then
rng A = {x} by FUNCT_5:12; then
rng A c= NAT by MEMBERED:6;
hence A is natural-valued;
end;
end;
registration
let a; let x be Real;
cluster {[a,x]} -> real-valued for array;
coherence
proof let A; assume A = {[a,x]}; then
rng A = {x} by FUNCT_5:12; then
rng A c= REAL by MEMBERED:3;
hence A is real-valued;
end;
end;
registration
let a; let X be non empty set;
let x be Element of X;
cluster {[a,x]} -> X-valued for array;
coherence
proof let A; assume A = {[a,x]}; then
rng A = {x} by FUNCT_5:12;
hence rng A c= X by ZFMISC_1:31;
end;
end;
registration
let a,x;
cluster {[a,x]} -> a-based succ a-limited for array;
coherence
proof
let s be array such that
A1: s = {[a,x]};
A2: dom s = {a} by A1,FUNCT_5:12;
thus s is a-based
by A2,TARSKI:def 1;
sup dom s = succ a by A2,ORDINAL2:23;
hence thesis;
end;
end;
registration
let b;
cluster non empty b-based natural-valued INT-valued real-valued
complex-valued finite for array;
existence
proof
set x = the Nat;
reconsider A = {[b,x]} as natural-valued array;
take A; thus thesis;
end;
let X be non empty set;
cluster non empty b-based finite X-valued for array;
existence
proof
set x = the Element of X;
reconsider A = {[b,x]} as array of X;
take A; thus thesis;
end;
end;
notation
let s be Sequence;
synonym s last for last s;
end;
definition
let A be array;
func last A -> set equals A.union dom A;
coherence;
end;
registration
let A be Sequence;
identify A last with last A;
compatibility;
end;
begin :: Descending sequence
definition
let f be Function;
attr f is descending means
for a,b st a in dom f & b in dom f & a in b holds f.b c< f.a;
end;
theorem
for f being finite array
st for a st a in dom f & succ a in dom f holds f.succ a c< f.a
holds f is descending
proof
let f be finite array; assume
A1: for a st a in dom f & succ a in dom f holds f.succ a c< f.a;
let a,b; assume
A2: a in dom f & b in dom f & a in b;
consider c,d such that
A3: dom f = c\d by Def1;
consider n being Nat such that
A4: c = d+^n by A2,A3,Th7;
consider e1 being Ordinal such that
A5: a = d+^e1 & e1 in Segm n by A2,A3,A4,Th1;
consider e2 being Ordinal such that
A6: b = d+^e2 & e2 in n by A2,A3,A4,Th1;
reconsider e1,e2 as Nat by A5,A6;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
A7: succ a = d+^succ e1 by A5,ORDINAL2:28;
e1 in e2 by A2,A5,A6,ORDINAL3:22; then
Segm succ e1 c= Segm e2 by ORDINAL1:21; then
succ e1 <= e2 by NAT_1:39; then
consider k being Nat such that
A8: e2 = se1+k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
deffunc Y(Ordinal) = (succ a)+^$1;
defpred P[Nat] means Y($1) in dom f implies f.Y($1) c< f.a;
Y(0) = succ a by ORDINAL2:27; then
A9: P[ 0 ] by A1,A2;
A10: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
Segm(k+1) = succ Segm k by NAT_1:38; then
A11: Y(k+1) = succ Y(k) by ORDINAL2:28; then
A12: Y(k) in Y(k+1) & a in succ a by ORDINAL1:6; then
A13: Y(k) c= Y(k+1) & a c= succ a by ORDINAL1:def 2;
succ a c= Y(k) by ORDINAL3:24; then
A14: a c= Y(k) by A12,ORDINAL1:def 2;
assume
A15: P[k] & Y(k+1) in dom f; then
Y(k) in dom f by A2,A13,A14,Th9; then
f.Y(k) c< f.a & f.Y(k+1) c< f.Y(k) by A1,A11,A15;
hence f.Y(k+1) c< f.a by XBOOLE_1:56;
end;
A16: for k being Nat holds P[k] from NAT_1:sch 2(A9,A10);
b = d+^(se1+^k) by A6,A8,CARD_2:36
.= (succ a)+^k by A7,ORDINAL3:30;
hence f.b c< f.a by A2,A16;
end;
theorem Th26:
for f being array st len-f = omega &
for a st a in dom f & succ a in dom f holds f.succ a c< f.a
holds f is descending
proof
let f be array; assume
A1: len-f = omega; assume
A2: for a st a in dom f & succ a in dom f holds f.succ a c< f.a;
let a,b; assume
A3: a in dom f & b in dom f & a in b;
consider c,d such that
A4: dom f = c\d by Def1;
f is non empty by A3; then
A5: base-f = d & limit-f = c by A4,Th23;
d c= a & a in c by A3,A4,ORDINAL6:5; then
d in c by ORDINAL1:12; then
d c= c by ORDINAL1:def 2; then
A6: c = d+^omega by A5,A1,ORDINAL3:def 5;
consider e1 being Ordinal such that
A7: a = d+^e1 & e1 in omega by A3,A4,A6,Th1;
consider e2 being Ordinal such that
A8: b = d+^e2 & e2 in omega by A3,A4,A6,Th1;
reconsider e1,e2 as Nat by A7,A8;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
A9: succ a = d+^succ e1 by A7,ORDINAL2:28;
e1 in e2 by A3,A7,A8,ORDINAL3:22; then
Segm succ e1 c= Segm e2 by ORDINAL1:21; then
succ e1 <= e2 by NAT_1:39; then
consider k being Nat such that
A10: e2 = se1+k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
deffunc Y(Ordinal) = (succ a)+^$1;
defpred P[Nat] means Y($1) in dom f implies f.Y($1) c< f.a;
Y(0) = succ a by ORDINAL2:27; then
A11: P[ 0 ] by A2,A3;
A12: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
Segm(k+1) = succ Segm k by NAT_1:38; then
A13: Y(k+1) = succ Y(k) by ORDINAL2:28; then
A14: Y(k) in Y(k+1) & a in succ a by ORDINAL1:6; then
A15: Y(k) c= Y(k+1) & a c= succ a by ORDINAL1:def 2;
succ a c= Y(k) by ORDINAL3:24; then
A16: a c= Y(k) by A14,ORDINAL1:def 2;
assume
A17: P[k] & Y(k+1) in dom f; then
Y(k) in dom f by A3,A15,A16,Th9; then
f.Y(k) c< f.a & f.Y(k+1) c< f.Y(k) by A2,A13,A17;
hence f.Y(k+1) c< f.a by XBOOLE_1:56;
end;
A18: for k being Nat holds P[k] from NAT_1:sch 2(A11,A12);
b = d+^(se1+^k) by A8,A10,CARD_2:36
.= (succ a)+^k by A9,ORDINAL3:30;
hence f.b c< f.a by A3,A18;
end;
theorem Th27:
for f being Sequence st f is descending & f.0 is finite
holds f is finite
proof let f be Sequence;
assume
A1: f is descending;
assume
A2: f.0 is finite;
deffunc G(set) = card (f.$1);
consider g being Sequence such that
A3: dom g = dom f & for a st a in dom f holds g.a = G(a)
from ORDINAL2:sch 2;
defpred P[set] means f.$1 is finite;
A4: P[0] by A2;
A5: P[a] implies P[succ a]
proof
per cases;
suppose succ a nin dom f;
hence thesis by FUNCT_1:def 2;
end;
suppose
A6: succ a in dom f;
A7: a in succ a by ORDINAL1:6; then
a in dom f by A6,ORDINAL1:10; then
f.succ a c< f.a by A1,A6,A7; then
f.succ a c= f.a;
hence thesis;
end;
end;
A8: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b]
holds P[a]
proof let a;
assume a <> 0; then
A9: 0 in a by ORDINAL3:8;
per cases;
suppose a in dom f; then
0 in dom f & a in dom f by ORDINAL3:8; then
f.a c< f.0 by A1,A9; then
f.a c= f.0;
hence thesis by A2;
end;
suppose a nin dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
A10: P[a] from ORDINAL2:sch 1(A4,A5,A8);
g is decreasing
proof
let a,b; assume
A11: a in b & b in dom g; then
a in dom f by A3,ORDINAL1:10; then
A12: g.a = G(a) & f.a is finite & f.b c< f.a & g.b = G(b) & f.b is finite
by A1,A3,A11,A10;
reconsider ga = g.a as Nat by A12;
g.b in Segm ga by CARD_2:48,A12;
hence g.b in g.a;
end;
hence f is finite by A3,FINSET_1:10;
end;
theorem
for f being Sequence st f is descending & f.0 is finite &
for a st f.a <> {} holds succ a in dom f
holds last f = {}
proof
let f be Sequence such that
A1: f is descending & f.0 is finite and
A2: for a st f.a <> {} holds succ a in dom f;
f is finite by A1,Th27; then
reconsider d = dom f as finite Ordinal;
set u = union d;
per cases;
suppose d = 0;
hence last f = {} by FUNCT_1:def 2;
end;
suppose d <> 0; then
consider n being Nat such that
A3: d = n+1 by NAT_1:6;
d = Segm(n+1) by A3;
then
A4: d = succ Segm n by NAT_1:38; then
A5: u = n by ORDINAL2:2;
f.u <> 0 implies d in d by A2,A4,A5;
hence last f = {};
end;
end;
scheme A{A() -> Sequence, F(set)->set}:
A() is finite
provided
A1: F(A().0) is finite and
A2: for a st succ a in dom A() & F(A().a) is finite
holds F(A().succ a) c< F(A().a)
proof
deffunc G(set) = F(A().$1);
consider F being Sequence such that
A3: dom F = dom A() & for a st a in dom A() holds F.a = G(a)
from ORDINAL2:sch 2;
per cases by ORDINAL6:4;
suppose dom F in omega;
hence thesis by A3,FINSET_1:10;
end;
suppose
A4: omega c= dom F;
set f = F|omega;
A5: dom f = omega by A4,RELAT_1:62;
A6: len-f = dom f by Th24;
A7: f.0 = F.0 by A5,FUNCT_1:47 .= G(0) by A3,A4;
defpred P[Nat] means f.$1 is finite;
A8: P[ 0] by A1,A7;
A9: P[n] implies P[n+1]
proof set a = n;
assume
A10: P[n];
A11: n in omega & succ n in omega by ORDINAL1:def 12; then
A12: a in dom F & succ a in dom F & f.a = F.a & f.succ a = F.succ a
by A4,A5,FUNCT_1:47;
A13: Segm(n+1) = succ Segm n by NAT_1:38;
F.a = G(a) & F.succ a = G(succ a) by A3,A4,A11; then
f.succ a c< f.a by A2,A3,A10,A12; then
f.succ a c= f.a;
hence thesis by A10,A13;
end;
A14: P[n] from NAT_1:sch 2(A8,A9);
for a st a in dom f & succ a in dom f holds f.succ a c< f.a
proof
let a; assume
A15: a in dom f & succ a in dom f; then
reconsider n = a as Nat by A5;
A16: P[n] & f.a = F.a & f.succ a = F.succ a by A15,A14,FUNCT_1:47;
F.a = G(a) & F.succ a = G(succ a) by A3,A15,A4,A5;
hence f.succ a c< f.a by A2,A3,A16,A15,A4,A5;
end; then
f is descending by A6,Th26,A4,RELAT_1:62; then
f is finite by A1,A7,Th27;
hence thesis by A5;
end;
end;
begin :: Swap
registration
let X;
let f be X-defined Function;
let a,b be object;
cluster Swap(f,a,b) -> X-defined;
coherence
proof
dom Swap(f,a,b) = dom f by FUNCT_7:99;
hence dom Swap(f,a,b) c= X;
end;
end;
registration
let X be set;
let f be X-valued Function;
let x,y be object;
cluster Swap(f,x,y) -> X-valued;
coherence
proof
rng Swap(f,x,y) = rng f by FUNCT_7:103;
hence rng Swap(f,x,y) c= X by RELAT_1:def 19;
end;
end;
theorem Th29:
x in dom f & y in dom f implies Swap(f,x,y).x = f.y
proof assume
A1: x in dom f & y in dom f; then
A2: Swap(f,x,y) = f+*(x,f.y)+*(y,f.x) by FUNCT_7:def 12;
A3: dom f = dom(f+*(x,f.y)) by FUNCT_7:30;
now assume x <> y; then
Swap(f,x,y).x = (f+*(x,f.y)).x by A2,FUNCT_7:32;
hence thesis by A1,FUNCT_7:31;
end;
hence Swap(f,x,y).x = f.y by A3,A1,A2,FUNCT_7:31;
end;
theorem Th30:
for f being array of X st x in dom f & y in dom f
holds Swap(f,x,y)/.x = f/.y
proof
let f be array of X;
assume
A1: x in dom f & y in dom f;
dom Swap(f,x,y) = dom f by FUNCT_7:99;
hence Swap(f,x,y)/.x = Swap(f,x,y).x by A1,PARTFUN1:def 6
.= f.y by A1,Th29 .= f/.y by A1,PARTFUN1:def 6;
end;
theorem Th31:
x in dom f & y in dom f implies Swap(f,x,y).y = f.x
proof assume
A1: x in dom f & y in dom f; then
A2: Swap(f,x,y) = f+*(x,f.y)+*(y,f.x) by FUNCT_7:def 12;
dom f = dom(f+*(x,f.y)) by FUNCT_7:30;
hence thesis by A1,A2,FUNCT_7:31;
end;
theorem Th32:
for f being array of X st x in dom f & y in dom f
holds Swap(f,x,y)/.y = f/.x
proof
let f be array of X;
assume
A1: x in dom f & y in dom f;
dom Swap(f,x,y) = dom f by FUNCT_7:99;
hence Swap(f,x,y)/.y = Swap(f,x,y).y by A1,PARTFUN1:def 6
.= f.x by A1,Th31 .= f/.x by A1,PARTFUN1:def 6;
end;
theorem Th33:
for x,y,z being object holds
z <> x & z <> y implies Swap(f,x,y).z = f.z
proof let x,y,z be object;
assume
A1: z <> x & z <> y;
per cases;
suppose
x in dom f & y in dom f; then
Swap(f,x,y) = f+*(x,f.y)+*(y,f.x) by FUNCT_7:def 12;
hence Swap(f,x,y).z = (f+*(x,f.y)).z by A1,FUNCT_7:32
.= f.z by A1,FUNCT_7:32;
end;
suppose
not (x in dom f & y in dom f);
hence Swap(f,x,y).z = f.z by FUNCT_7:def 12;
end;
end;
theorem Th34:
for f being array of X st z in dom f & z <> x & z <> y
holds Swap(f,x,y)/.z = f/.z
proof
let f be array of X;
assume
A1: z in dom f & z <> x & z <> y;
dom Swap(f,x,y) = dom f by FUNCT_7:99;
hence Swap(f,x,y)/.z = Swap(f,x,y).z by A1,PARTFUN1:def 6
.= f.z by A1,Th33 .= f/.z by A1,PARTFUN1:def 6;
end;
theorem
x in dom f & y in dom f implies Swap(f,x,y) = Swap(f,y,x)
proof assume
A1: x in dom f & y in dom f;
A2: dom Swap(f,x,y) = dom f & dom Swap(f,y,x) = dom f by FUNCT_7:99;
now let z be object such that
z in dom f;
per cases;
suppose z = x & z = y;
hence Swap(f,x,y).z = Swap(f,y,x).z;
end;
suppose z = x & z <> y; then
Swap(f,x,y).z = f.y & Swap(f,y,x).z = f.y by A1,Th29,Th31;
hence Swap(f,x,y).z = Swap(f,y,x).z;
end;
suppose z <> x & z = y; then
Swap(f,x,y).z = f.x & Swap(f,y,x).z = f.x by A1,Th29,Th31;
hence Swap(f,x,y).z = Swap(f,y,x).z;
end;
suppose z <> x & z <> y; then
Swap(f,x,y).z = f.z & Swap(f,y,x).z = f.z by Th33;
hence Swap(f,x,y).z = Swap(f,y,x).z;
end;
end;
hence Swap(f,x,y) = Swap(f,y,x) by A2;
end;
registration
let X be non empty set;
cluster onto for X-valued non empty Function;
existence
proof
take id X; thus thesis;
end;
end;
registration
let X be non empty set;
let f be onto X-valued non empty Function;
let x,y be Element of dom f;
cluster Swap(f,x,y) -> onto;
coherence
proof
rng Swap(f,x,y) = rng f by FUNCT_7:103;
hence rng Swap(f,x,y) = X by FUNCT_2:def 3;
end;
end;
registration
let A;
let x,y;
cluster Swap(A,x,y) -> segmental;
coherence
proof
consider a1,a2 such that
A1: dom A = a1\a2 by Def1;
take a1,a2; thus thesis by A1,FUNCT_7:99;
end;
end;
theorem
x in dom A & y in dom A implies Swap(Swap(A,x,y),x,y) = A
proof assume
A1: x in dom A & y in dom A;
set B = Swap(A,x,y);
set C = Swap(B,x,y);
A2: dom C = dom B & dom B = dom A by FUNCT_7:99;
now let z be object;
assume
z in dom B;
per cases;
suppose
A3: z <> x & z <> y;
hence C.z = B.z by Th33 .= A.z by A3,Th33;
end;
suppose
A4: z = x;
hence C.z = B.y by A1,A2,Th29 .= A.z by A1,A4,Th31;
end;
suppose
A5: z = y;
hence C.z = B.x by A1,A2,Th31 .= A.z by A1,A5,Th29;
end;
end;
hence C = A by A2;
end;
registration
let A be real-valued array;
let x,y;
cluster Swap(A,x,y) -> real-valued for array;
coherence;
end;
begin :: Permutations
definition
let A be array;
mode permutation of A -> array means:
Def9:
ex f being Permutation of dom A st it = A*f;
existence
proof
take A;
take id dom A; thus thesis by RELAT_1:51;
end;
end;
theorem Th37:
for B being permutation of A holds dom B = dom A & rng B = rng A
proof
let B be permutation of A;
consider f being Permutation of dom A such that
A1: B = A*f by Def9;
dom A <> {} implies dom A <> {}; then
rng f = dom A & dom f = dom A by FUNCT_2:def 1,def 3;
hence thesis by A1,RELAT_1:27,28;
end;
theorem Th38:
A is permutation of A
proof
take id dom A; thus thesis by RELAT_1:51;
end;
theorem Th39:
A is permutation of B implies B is permutation of A
proof assume
A1: A is permutation of B; then
A2: dom A = dom B by Th37;
consider f being Permutation of dom B such that
A3: A = B*f by A1,Def9;
reconsider g = f" as Permutation of dom A by A2;
take g;
thus B = B*id dom B by RELAT_1:52
.= B*(f*g) by FUNCT_2:61
.= A*g by A3,RELAT_1:36;
end;
theorem Th40:
A is permutation of B & B is permutation of C implies A is permutation of C
proof assume
A1: A is permutation of B & B is permutation of C; then
A2: dom C = dom B by Th37;
consider f being Permutation of dom B such that
A3: A = B*f by A1,Def9;
consider g being Permutation of dom C such that
A4: B = C*g by A1,Def9;
reconsider h = g*f as Permutation of dom C by A2;
take h;
thus A = C*h by A3,A4,RELAT_1:36;
end;
theorem Th41:
Swap(id X,x,y) is one-to-one
proof
A1: dom id X = X;
per cases;
suppose
A2: x in X & y in X;
set g = id X;
set f = Swap(g,x,y);
let z,t be object; assume
A3: z in dom f & t in dom f & f.z = f.t;
A4: g.z = z & g.t = t & g.x = x & g.y = y by A2,A3,FUNCT_1:17; then
A5: (z = x implies f.z = y) & (z = y implies f.z = x) &
(z <> x & z <> y implies f.z = z)
by A2,A1,Th29,Th31,Th33;
(t = x implies f.t = y) & (t = y implies f.t = x) &
(t <> x & t <> y implies f.t = t)
by A2,A1,A4,Th29,Th31,Th33;
hence z = t by A3,A5;
end;
suppose
not (x in X & y in X);
hence thesis by A1,FUNCT_7:def 12;
end;
end;
registration
let X be non empty set;
let x,y be Element of X;
cluster Swap(id X,x,y) -> one-to-one X-valued X-defined;
coherence by Th41;
end;
registration
let X be non empty set;
let x,y be Element of X;
cluster Swap(id X,x,y) -> onto total;
coherence
proof
A1: dom id X = X;
reconsider a=x, b=y as Element of dom id X;
Swap(id X,a,b) is onto;
hence Swap(id X,x,y) is onto;
thus dom Swap(id X,x,y) = X by A1,FUNCT_7:99;
end;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
let x,y be Element of X;
redefine func Swap(f,x,y) -> Function of X,Y; :: redefines Swap (FUNCT_7, definition)
coherence
proof
set g = Swap(f,x,y);
A1: dom f = X by FUNCT_2:def 1;
A2: dom g = dom f & rng g = rng f by FUNCT_7:99,103;
rng f c= Y by RELAT_1:def 19;
hence thesis by A1,A2,FUNCT_2:2;
end;
end;
theorem Th42:
x in X & y in X & f = Swap(id X,x,y) & X = dom A implies
Swap(A,x,y) = A*f
proof assume that
A1: x in X & y in X and
A2: f = Swap(id X,x,y) & X = dom A;
set g = id X;
set s = Swap(A,x,y);
A3: dom g = X & rng g = X; then
A4: dom f = X & rng f = X by A2,FUNCT_7:99,103;
A5: dom s = dom A by FUNCT_7:99;
A6: dom (A*f) = dom f by A2,A4,RELAT_1:27;
now
let z be object; assume
A7: z in X;
A8: g.x = x & g.y = y & g.z = z by A1,A7,FUNCT_1:17;
z = x or z = y or z <> x & z <> y; then
s.z = A.y & f.z = g.y or
s.z = A.x & f.z = g.x or
s.z = A.z & f.z = g.z by A1,A2,A3,Th29,Th31,Th33;
hence s.z = (A*f).z by A7,A8,A4,FUNCT_1:13;
end;
hence Swap(A,x,y) = A*f by A2,A4,A5,A6;
end;
theorem Th43:
x in dom A & y in dom A implies
Swap(A,x,y) is permutation of A & A is permutation of Swap(A,x,y)
proof set X = dom A;
assume
A1: x in X & y in X;
thus Swap(A,x,y) is permutation of A
proof
reconsider X as non empty set by A1;
reconsider x,y as Element of X by A1;
reconsider f = Swap(id X,x,y) as Permutation of dom A;
take f;
thus thesis by Th42;
end;
hence A is permutation of Swap(A,x,y) by Th39;
end;
theorem
x in dom A & y in dom A & A is permutation of B implies
Swap(A,x,y) is permutation of B & A is permutation of Swap(B,x,y)
proof set X = dom A;
assume
A1: x in X & y in X & A is permutation of B; then
X = dom B by Th37; then
Swap(A,x,y) is permutation of A &
B is permutation of Swap(B,x,y) by A1,Th43;
hence thesis by A1,Th40;
end;
begin :: Exchanging
definition
let O be RelStr;
let A be array of O;
attr A is ascending means
for a,b st a in dom A & b in dom A & a in b holds A/.a <= A/.b;
func inversions A -> set equals
{[a,b] where a,b is Element of dom A: a in b & not A/.a <= A/.b};
coherence;
end;
registration
let O be RelStr;
cluster -> ascending for empty array of O;
coherence;
let A be empty array of O;
cluster inversions A -> empty;
coherence
proof
set w = the Element of inversions A;
assume inversions A is non empty; then
w in inversions A; then
consider a,b being Element of dom A such that
A1: w = [a,b] & a in b & not A/.a <= A/.b;
thus thesis by A1,SUBSET_1:def 1;
end;
end;
reserve O for connected non empty Poset;
reserve R,Q for array of O;
theorem Th45:
for O for x,y being Element of O holds x > y iff not x <= y
proof
let O; let x,y be Element of O;
A1: x <= y & y <= x implies x = y by YELLOW_0:def 3;
(x <= y or x >= y) & x <= x by WAYBEL_0:def 29;
hence x > y iff not x <= y by A1,ORDERS_2:def 6;
end;
definition
let O,R;
redefine func inversions R equals :: redefines inversions (EXCHSORT, definition)
{[a,b] where a,b is Element of dom R: a in b & R/.a > R/.b};
compatibility
proof
set N = {[a,b] where a,b is Element of dom R: a in b & R/.a > R/.b};
inversions R = N
proof
thus inversions R c= N
proof
let x be object; assume x in inversions R; then
consider a,b being Element of dom R such that
A1: x = [a,b] & a in b & not R/.a <= R/.b;
R/.a > R/.b by A1,Th45;
hence thesis by A1;
end;
let x be object; assume x in N; then
consider a,b being Element of dom R such that
A2: x = [a,b] & a in b & R/.a > R/.b;
not R/.a <= R/.b by A2,Th45;
hence thesis by A2;
end;
hence thesis;
end;
end;
theorem Th46:
for x being object, y being set holds
[x,y] in inversions R iff x in dom R & y in dom R & x in y & R/.x > R/.y
proof let x be object, y be set;
hereby
assume
A1: [x,y] in inversions R; then
reconsider R1 = R as non empty Function;
consider a,b being Element of dom R1 such that
A2: [x,y] = [a,b] & a in b & not R/.a <= R/.b by A1;
x = a & y = b by A2,XTUPLE_0:1;
hence x in dom R & y in dom R & x in y & R/.x > R/.y by A2,Th45;
end;
thus thesis;
end;
theorem Th47:
inversions R c= [:dom R, dom R:]
proof
let x be object; assume
A1: x in inversions R; then
consider a,b being Element of dom R such that
A2: x = [a,b] & a in b & R/.a > R/.b;
a in dom R & b in dom R by A2,A1,Th46;
hence thesis by A2,ZFMISC_1:def 2;
end;
registration
let O;
let R be finite array of O;
cluster inversions R -> finite;
coherence
proof
inversions R c= [:dom R, dom R:] by Th47;
hence thesis;
end;
end;
theorem Th48:
R is ascending iff inversions R = {}
proof
thus R is ascending implies inversions R = {}
proof assume
A1: for a,b st a in dom R & b in dom R & a in b holds R/.a <= R/.b;
set x = the Element of inversions R;
assume
A2: inversions R <> {}; then x in inversions R; then
consider a,b being Element of dom R such that
A3: x = [a,b] & a in b & R/.a > R/.b;
R <> {} by A2; then
R/.a <= R/.b by A1,A3;
hence thesis by A3,Th45;
end;
assume
A4: inversions R = {};
let a,b; assume
a in dom R & b in dom R & a in b; then
R/.a > R/.b implies [a,b] in inversions R;
hence thesis by A4,Th45;
end;
theorem Th49:
[x,y] in inversions R implies [y,x] nin inversions R
proof assume [x,y] in inversions R; then
not y in x by Th46; then
y nin x;
hence [y,x] nin inversions R by Th46;
end;
theorem Th50:
[x,y] in inversions R & [y,z] in inversions R implies [x,z] in inversions R
proof assume
A1: [x,y] in inversions R & [y,z] in inversions R; then
reconsider x,y,z as Element of dom R by Th46;
x in y & R/.x > R/.y & y in z & R/.y > R/.z by A1,Th46; then
x in z & R/.x > R/.z by ORDERS_2:5,ORDINAL1:10;
hence thesis;
end;
registration
let O,R;
cluster inversions R -> Relation-like;
coherence
proof
inversions R c= [:dom R, dom R:] by Th47;
hence thesis;
end;
end;
registration
let O,R;
cluster inversions R -> asymmetric transitive for Relation;
coherence
proof
let r be Relation; assume
A1: r = inversions R;
thus r is asymmetric
proof
let x,y be object;
thus thesis by A1,Th49;
end;
let x,y be object;
thus thesis by A1,Th50;
end;
end;
definition
let O;
let a,b be Element of O;
redefine pred a < b; :: redefines < (ORDERS_2, definition)
asymmetry by ORDERS_2:5;
end;
theorem Th51:
[x,y] in inversions R implies [x,y] nin inversions Swap(R,x,y)
proof assume
A1: [x,y] in inversions R; then
A2: x in dom R & y in dom R & R/.x > R/.y by Th46;
A3: not R/.x < R/.y by A1,Th46;
Swap(R,x,y)/.x = R/.y & Swap(R,x,y)/.y = R/.x by A2,Th30,Th32;
hence [x,y] nin inversions Swap(R,x,y) by A3,Th46;
end;
theorem Th52:
x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y
implies
([z,t] in inversions R iff [z,t] in inversions Swap(R,x,y))
proof set s = Swap(R,x,y);
assume
x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y; then
A1: (z in dom R implies s/.z = R/.z) & (t in dom R implies s/.t = R/.t) &
dom s = dom R by Th34,FUNCT_7:99;
hereby
assume [z,t] in inversions R; then
z in dom R & t in dom R & z in t & R/.z > R/.t by Th46;
hence [z,t] in inversions Swap(R,x,y) by A1;
end;
assume [z,t] in inversions Swap(R,x,y); then
z in dom R & t in dom R & z in t & s/.z > s/.t by A1,Th46;
hence thesis by A1;
end;
theorem Th53:
[x,y] in inversions R implies
([z,y] in inversions R & z in x iff [z,x] in inversions Swap(R,x,y))
proof set s = Swap(R,x,y);
assume [x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46; then
A2: s/.x = R/.y & s/.y = R/.x & dom s = dom R by Th30,Th32,FUNCT_7:99;
hereby assume
A3: [z,y] in inversions R & z in x; then
A4: z in dom R & z in y & R/.z > R/.y by Th46; then
x <> z & y <> z by A3; then
s/.z = R/.z by A4,Th34;
hence [z,x] in inversions Swap(R,x,y) by A3,A1,A2,A4;
end;
assume [z,x] in inversions Swap(R,x,y); then
A5: z in dom R & z in x & s/.z > s/.x by A2,Th46; then
A6: z in y by A1,ORDINAL1:10;
s/.z = R/.z by A1,A5,Th34;
hence thesis by A1,A2,A5,A6;
end;
theorem Th54:
[x,y] in inversions R implies
([z,x] in inversions R iff z in x & [z,y] in inversions Swap(R,x,y))
proof assume
[x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
A2: dom Swap(R,x,y) = dom R by FUNCT_7:99;
hereby assume
[z,x] in inversions R; then
A3: z in dom R & z in x & R/.z > R/.x by Th46; then
A4: z in y by A1,ORDINAL1:10;
Swap(R,x,y)/.y = R/.x & Swap(R,x,y)/.z = R/.z
by A1,A3,Th32,Th34;
hence z in x & [z,y] in inversions Swap(R,x,y) by A1,A2,A3,A4;
end;
assume
A5: z in x & [z,y] in inversions Swap(R,x,y); then
A6: z in dom R & z in y & Swap(R,x,y)/.z > Swap(R,x,y)/.y by A2,Th46; then
z <> x & z <> y by A5; then
Swap(R,x,y)/.y = R/.x & Swap(R,x,y)/.z = R/.z by A1,A6,Th32,Th34;
hence [z,x] in inversions R by A1,A6,A5;
end;
theorem Th55:
[x,y] in inversions R & z in y & [x,z] in inversions Swap(R,x,y) implies
[x,z] in inversions R
proof assume
[x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
A2: dom Swap(R,x,y) = dom R by FUNCT_7:99;
assume
A3: z in y;
assume
[x,z] in inversions Swap(R,x,y); then
A4: z in dom R & x in z & Swap(R,x,y)/.x > Swap(R,x,y)/.z by A2,Th46; then
z <> x & z <> y by A3; then
Swap(R,x,y)/.x = R/.y & Swap(R,x,y)/.z = R/.z by A1,A4,Th30,Th34; then
R/.x > R/.z by A1,A4,ORDERS_2:5;
hence [x,z] in inversions R by A1,A4;
end;
theorem Th56:
[x,y] in inversions R & x in z & [z,y] in inversions Swap(R,x,y) implies
[z,y] in inversions R
proof assume
[x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
A2: dom Swap(R,x,y) = dom R by FUNCT_7:99;
assume
A3: x in z;
assume
[z,y] in inversions Swap(R,x,y); then
A4: z in dom R & z in y & Swap(R,x,y)/.z > Swap(R,x,y)/.y by A2,Th46; then
z <> x & z <> y by A3; then
Swap(R,x,y)/.y = R/.x & Swap(R,x,y)/.z = R/.z by A1,A4,Th32,Th34; then
R/.z > R/.y by A1,A4,ORDERS_2:5;
hence [z,y] in inversions R by A1,A4;
end;
theorem Th57:
[x,y] in inversions R & y in z & [x,z] in inversions Swap(R,x,y) implies
[y,z] in inversions R
proof assume
[x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
A2: dom Swap(R,x,y) = dom R by FUNCT_7:99;
assume
A3: y in z;
assume
[x,z] in inversions Swap(R,x,y); then
A4: z in dom R & x in z & Swap(R,x,y)/.x > Swap(R,x,y)/.z by A2,Th46; then
z <> x & z <> y by A3; then
Swap(R,x,y)/.x = R/.y & Swap(R,x,y)/.z = R/.z by A1,A4,Th30,Th34;
hence [y,z] in inversions R by A1,A4,A3;
end;
theorem Th58:
[x,y] in inversions R implies
(y in z & [x,z] in inversions R iff [y,z] in inversions Swap(R,x,y))
proof assume
[x,y] in inversions R; then
A1: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
A2: dom Swap(R,x,y) = dom R by FUNCT_7:99;
hereby assume
A3: y in z & [x,z] in inversions R; then
A4: z in dom R & x in z & R/.z < R/.x by Th46; then
z <> x & z <> y by A3; then
Swap(R,x,y)/.y = R/.x & Swap(R,x,y)/.z = R/.z by A1,A4,Th32,Th34;
hence [y,z] in inversions Swap(R,x,y) by A1,A2,A4,A3;
end;
assume
[y,z] in inversions Swap(R,x,y); then
A5: z in dom R & y in z & Swap(R,x,y)/.y > Swap(R,x,y)/.z by A2,Th46; then
A6: x in z by A1,ORDINAL1:10;
Swap(R,x,y)/.y = R/.x & Swap(R,x,y)/.z = R/.z by A1,Th32,Th34,A5;
hence thesis by A1,A5,A6;
end;
definition
let O,R,x,y;
func (R,x,y)incl -> Function equals
[:Swap(id dom R,x,y), Swap(id dom R,x,y):] +*
id([:{x},(succ y)\x:]\/[:(succ y)\x,{y}:]);
coherence;
end;
theorem Th59:
c in (succ b)\a iff a c= c & c c= b
proof
a c= c iff c nin a by ORDINAL6:4; then
c in (succ b)\a iff c in succ b & a c= c by XBOOLE_0:def 5;
hence thesis by ORDINAL1:22;
end;
reserve T for non empty array of O;
reserve p,q,r,s for Element of dom T;
theorem Th60:
(succ q)\p c= dom T
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A1: x in (succ q)\p;
A2: p c= xx & xx c= q by A1,Th59;
consider a,b such that
A3: dom T = a\b by Def1;
q in a & p nin b by A3,XBOOLE_0:def 5; then
x in a & x nin b by A1,A2,ORDINAL1:12;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem Th61:
dom (T,p,q)incl = [:dom T, dom T:] & rng (T,p,q)incl c= [:dom T, dom T:]
proof
set X = dom T;
set i = id X;
set s = Swap(i,p,q);
set f = [:s,s:];
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
dom i = X; then
A1: dom s = X by FUNCT_7:99;
A2: {p} c= X & {q} c= X & Y c= X by Th60,ZFMISC_1:31;
A3: [:X, X:] \/ (Z1\/Z2) = [:X, X:] \/ Z1 \/Z2 by XBOOLE_1:4
.= [:X, X:] \/Z2 by A2,XBOOLE_1:12,ZFMISC_1:96
.= [:X,X:] by A2,XBOOLE_1:12,ZFMISC_1:96;
thus dom (T,p,q)incl = dom f \/ dom g by FUNCT_4:def 1
.= dom f \/ (Z1\/Z2)
.= [:X, X:] by A1,A3,FUNCT_3:def 8;
A4: rng g = Z1\/Z2 & rng i = X;
rng s = X by A4,FUNCT_7:103; then
rng f = [:X,X:] by FUNCT_3:67;
hence rng (T,p,q)incl c= [:X,X:] by A3,A4,FUNCT_4:17;
end;
theorem Th62:
p c= r & r c= q implies
(T,p,q)incl.(p,r) = [p, r] & (T,p,q)incl.(r,q) = [r,q]
proof assume
A1: p c= r & r c= q;
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
p in {p} & q in {q} & r in Y by A1,Th59,TARSKI:def 1; then
[p,r] in Z1 & [r,q] in Z2 by ZFMISC_1:def 2; then
A2: [p,r] in Z1\/Z2 & [r,q] in Z1\/Z2 by XBOOLE_0:def 3;
A3: dom g = Z1\/Z2;
hence (T,p,q)incl.(p,r) = g.(p,r) by A2,FUNCT_4:13
.= [p, r] by A2,FUNCT_1:17;
thus (T,p,q)incl.(r,q) = g.(r,q) by A2,A3,FUNCT_4:13
.= [r, q] by A2,FUNCT_1:17;
end;
theorem Th63:
r <> p & s <> q & f = Swap(id dom T,p,q)
implies (T,p,q)incl.(r,s) = [f.r,f.s]
proof assume that
A1: r <> p & s <> q and
A2: f = Swap(id dom T,p,q);
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
A3: dom f = dom id dom T by A2,FUNCT_7:99 .= dom T;
r nin {p} & s nin {q} by A1,TARSKI:def 1; then
[r,s] nin Z1 & [r,s] nin Z2 by ZFMISC_1:87; then
[r,s] nin dom g by XBOOLE_0:def 3;
hence (T,p,q)incl.(r,s) = [:f,f:].(r,s) by A2,FUNCT_4:11
.= [f.r,f.s] by A3,FUNCT_3:def 8;
end;
theorem Th64:
r in p & f = Swap(id dom T,p,q) implies
(T,p,q)incl.(r,q) = [f.r,f.q] & (T,p,q)incl.(r,p) = [f.r,f.p]
proof assume that
A1: r in p and
A2: f = Swap(id dom T,p,q);
set X = dom T;
set i = id X;
set s = Swap(i,p,q);
set h = [:s,s:];
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
dom i = X; then
A3: dom s = X by FUNCT_7:99;
not p c= r by A1,ORDINAL6:4; then
r nin {p} & r nin Y by Th59,TARSKI:def 1; then
[r,p] nin Z1 & [r,p] nin Z2 & [r,q] nin Z1 & [r,q] nin Z2
by ZFMISC_1:87; then
A4: [r,q] nin dom g & [r,p] nin dom g by XBOOLE_0:def 3;
hence (T,p,q)incl.(r,q) = h.(r,q) by FUNCT_4:11
.= [f.r,f.q] by A2,A3,FUNCT_3:def 8;
thus (T,p,q)incl.(r,p) = h.(r,p) by A4,FUNCT_4:11
.= [f.r,f.p] by A2,A3,FUNCT_3:def 8;
end;
theorem Th65:
q in r & f = Swap(id dom T,p,q) implies
(T,p,q)incl.(p,r) = [f.p,f.r] & (T,p,q)incl.(q,r) = [f.q,f.r]
proof assume that
A1: q in r and
A2: f = Swap(id dom T,p,q);
set X = dom T;
set i = id X;
set s = Swap(i,p,q);
set h = [:s,s:];
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
dom i = X; then
A3: dom s = X by FUNCT_7:99;
not r c= q by A1,ORDINAL6:4; then
r nin {q} & r nin Y by Th59,TARSKI:def 1; then
[p,r] nin Z1 & [p,r] nin Z2 & [q,r] nin Z1 & [q,r] nin Z2
by ZFMISC_1:87; then
A4: [p,r] nin dom g & [q,r] nin dom g by XBOOLE_0:def 3;
hence (T,p,q)incl.(p,r) = h.(p,r) by FUNCT_4:11
.= [f.p,f.r] by A2,A3,FUNCT_3:def 8;
thus (T,p,q)incl.(q,r) = h.(q,r) by A4,FUNCT_4:11
.= [f.q,f.r] by A2,A3,FUNCT_3:def 8;
end;
theorem Th66:
p in q implies (T,p,q)incl.(p,q) = [p,q]
proof assume
p in q; then
p c= q by ORDINAL1:def 2;
hence thesis by Th62;
end;
theorem Th67:
p in q & r <> p & r <> q & s <> p & s <> q implies (T,p,q)incl.(r,s) = [r,s]
proof assume
A1: p in q & r <> p & r <> q & s <> p & s <> q;
set X = dom T;
set i = id X;
set f = Swap(i,p,q);
set h = [:f,f:];
set Y = (succ q)\p;
thus (T,p,q)incl.(r,s) = [f.r,f.s] by A1,Th63
.= [i.r,f.s] by A1,Th33 .= [i.r,i.s] by A1,Th33
.= [r,i.s]
.= [r,s];
end;
theorem Th68:
r in p & p in q implies (T,p,q)incl.(r,p) = [r,q] & (T,p,q)incl.(r,q) = [r,p]
proof assume
A1: r in p & p in q;
set X = dom T;
set i = id X;
set f = Swap(i,p,q);
set h = [:f,f:];
set Y = (succ q)\p;
A2: dom i = X;
A3: r <> p & r <> q by A1;
thus (T,p,q)incl.(r,p) = [f.r,f.p] by A1,Th64
.= [i.r,f.p] by A3,Th33
.= [r,f.p]
.= [r,i.q] by A2,Th29
.= [r,q];
thus (T,p,q)incl.(r,q) = [f.r,f.q] by A1,Th64
.= [i.r,f.q] by A3,Th33
.= [r,f.q]
.= [r,i.p] by A2,Th31
.= [r,p];
end;
theorem Th69:
p in s & s in q implies (T,p,q)incl.(p,s) = [p,s] & (T,p,q)incl.(s,q) = [s,q]
proof assume
p in s & s in q; then
p c= s & s c= q by ORDINAL1:def 2;
hence thesis by Th62;
end;
theorem Th70:
p in q & q in s implies (T,p,q)incl.(p,s) = [q,s] & (T,p,q)incl.(q,s) = [p,s]
proof assume
A1: p in q & q in s;
set X = dom T;
set i = id X;
set f = Swap(i,p,q);
set h = [:f,f:];
set Y = (succ q)\p;
A2: dom i = X;
A3: s <> p & s <> q by A1;
thus (T,p,q)incl.(p,s) = [f.p,f.s] by A1,Th65
.= [f.p,i.s] by A3,Th33
.= [f.p,s]
.= [i.q,s] by A2,Th29
.= [q,s];
thus (T,p,q)incl.(q,s) = [f.q,f.s] by A1,Th65
.= [f.q,i.s] by A3,Th33
.= [f.q,s]
.= [i.p,s] by A2,Th31
.= [p,s];
end;
Lm1: p in q & f = (T,p,q)incl implies
for x1,x2,y1,y2 being Element of dom T st x1 in y1 & x2 in y2
holds f.(x1,y1) = f.(x2,y2) implies x1 = x2 & y1 = y2
proof assume
A1: p in q & f = (T,p,q)incl; then
A2: p <> q;
let x1,x2,y1,y2 be Element of dom T such that
A3: x1 in y1 & x2 in y2 and
A4: f.(x1,y1) = f.(x2,y2);
set X = dom T;
set i = id X;
set s = Swap(i,p,q);
set h = [:s,s:];
set Y = (succ q)\p;
set Z1 = [:{p},Y:], Z2 = [:Y,{q}:];
set g = id(Z1\/Z2);
per cases by A1,A3,Th2;
suppose
A5: x1 <> p & x1 <> q & y1 <> p & y1 <> q; then
A6: f.(x1,y1) = [x1,y1] by A1,Th67;
per cases by A1,A3,Th2;
suppose Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A4,A6,XTUPLE_0:1;
end;
suppose Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] by A1,Th68;
hence x1 = x2 & y1 = y2 by A5,A4,A6,XTUPLE_0:1;
end;
suppose Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A5,A4,A6,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A6,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A6,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A5,A4,A6,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A6,XTUPLE_0:1;
end;
suppose Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A5,A4,A6,XTUPLE_0:1;
end;
end;
suppose
A7: x1 = p & y1 in q; then
A8: f.(x1,y1) = [x1,y1] by A1,A3,Th69;
per cases by A1,A3,Th2;
suppose Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A4,A8,XTUPLE_0:1;
end;
suppose Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] & x2 <> p by A1,Th68;
hence x1 = x2 & y1 = y2 by A7,A4,A8,XTUPLE_0:1;
end;
suppose Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] & x2 <> p by A1,Th68;
hence x1 = x2 & y1 = y2 by A7,A4,A8,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A8,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A8,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A2,A7,A4,A8,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A8,XTUPLE_0:1;
end;
suppose
A9: Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A7,A9,A4,A8,XTUPLE_0:1;
end;
end;
suppose
A10: x1 = p & y1 = q; then
A11: f.(x1,y1) = [x1,y1] by A1,Th66;
per cases by A1,A3,Th2;
suppose Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A4,A11,XTUPLE_0:1;
end;
suppose Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] & x2 <> p by A1,Th68;
hence x1 = x2 & y1 = y2 by A10,A4,A11,XTUPLE_0:1;
end;
suppose Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A2,A10,A4,A11,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A11,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A11,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A2,A10,A4,A11,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A11,XTUPLE_0:1;
end;
suppose
Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] & y2 <> q by A1,Th70;
hence x1 = x2 & y1 = y2 by A10,A4,A11,XTUPLE_0:1;
end;
end;
suppose
A12: p in x1 & y1 = q; then
A13: f.(x1,y1) = [x1,y1] by A1,A3,Th69;
per cases by A1,A3,Th2;
suppose Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A4,A13,XTUPLE_0:1;
end;
suppose
A14: Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] by A1,Th68;
hence x1 = x2 & y1 = y2 by A14,A12,A4,A13,XTUPLE_0:1;
end;
suppose
A15: Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A15,A12,A4,A13,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A13,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A13,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] & y2 <> q by A1,Th70;
hence x1 = x2 & y1 = y2 by A12,A4,A13,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A13,XTUPLE_0:1;
end;
suppose Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] & y2 <> q by A1,Th70;
hence x1 = x2 & y1 = y2 by A12,A4,A13,XTUPLE_0:1;
end;
end;
suppose
A16: x1 in p & y1 = p; then
A17: f.(x1,y1) = [x1,q] by A1,Th68;
per cases by A1,A3,Th2;
suppose
A18: Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A18,A4,A17,XTUPLE_0:1;
end;
suppose
A19: Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] by A1,Th68;
hence x1 = x2 & y1 = y2 by A19,A16,A4,A17,XTUPLE_0:1;
end;
suppose Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A2,A4,A17,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & x2 <> x1 by A16,A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A17,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & x2 <> x1 by A16,A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A17,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] & y2 <> q by A1,Th70;
hence x1 = x2 & y1 = y2 by A4,A17,XTUPLE_0:1;
end;
suppose
A20: Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A16,A20,A4,A17,XTUPLE_0:1;
end;
suppose Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] & x1 <> p by A16,A1,Th70;
hence x1 = x2 & y1 = y2 by A4,A17,XTUPLE_0:1;
end;
end;
suppose
A21: x1 in p & y1 = q; then
A22: f.(x1,y1) = [x1,p] by A1,Th68;
per cases by A1,A3,Th2;
suppose
A23: Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A23,A4,A22,XTUPLE_0:1;
end;
suppose Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] by A1,Th68;
hence x1 = x2 & y1 = y2 by A2,A4,A22,XTUPLE_0:1;
end;
suppose
A24: Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A24,A21,A4,A22,XTUPLE_0:1;
end;
suppose
A25: Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & x1 <> p by A21,A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A25,A4,A22,XTUPLE_0:1;
end;
suppose
A26: Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A26,A2,A4,A22,XTUPLE_0:1;
end;
suppose
Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A1,A21,A4,A22,XTUPLE_0:1;
end;
suppose
A27: Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A2,A27,A4,A22,XTUPLE_0:1;
end;
suppose Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] & x1 <> p by A21,A1,Th70;
hence x1 = x2 & y1 = y2 by A4,A22,XTUPLE_0:1;
end;
end;
suppose
A28: x1 = p & q in y1; then
A29: f.(x1,y1) = [q,y1] by A1,Th70;
per cases by A1,A3,Th2;
suppose
A30: Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A30,A4,A29,XTUPLE_0:1;
end;
suppose
A31: Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] by A1,Th68;
hence x1 = x2 & y1 = y2 by A1,A31,A4,A29,XTUPLE_0:1;
end;
suppose
Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] by A1,Th68;
hence x1 = x2 & y1 = y2 by A1,A28,A4,A29,XTUPLE_0:1;
end;
suppose Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & x2 <> q by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A29,XTUPLE_0:1;
end;
suppose
A32: Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th66;
hence x1 = x2 & y1 = y2 by A2,A32,A4,A29,XTUPLE_0:1;
end;
suppose
A33: Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A33,A28,A4,A29,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & x2 <> q by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A29,XTUPLE_0:1;
end;
suppose Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A2,A4,A29,XTUPLE_0:1;
end;
end;
suppose
A34: x1 = q & q in y1; then
A35: f.(x1,y1) = [p,y1] by A1,Th70;
per cases by A1,A3,Th2;
suppose
A36: Case1[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,Th67;
hence x1 = x2 & y1 = y2 by A36,A4,A35,XTUPLE_0:1;
end;
suppose Case2[p,q,x2,y2]; then
f.(x2,y2) = [x2,q] & p <> x2 by A1,Th68;
hence x1 = x2 & y1 = y2 by A4,A35,XTUPLE_0:1;
end;
suppose Case3[p,q,x2,y2]; then
f.(x2,y2) = [x2,p] & p <> x2 by A1,Th68;
hence x1 = x2 & y1 = y2 by A4,A35,XTUPLE_0:1;
end;
suppose
A37: Case4[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] by A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A34,A37,A4,A35,XTUPLE_0:1;
end;
suppose Case5[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & y1 <> y2 by A34,A1,Th66;
hence x1 = x2 & y1 = y2 by A4,A35,XTUPLE_0:1;
end;
suppose Case6[p,q,x2,y2]; then
f.(x2,y2) = [q,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A2,A4,A35,XTUPLE_0:1;
end;
suppose Case7[p,q,x2,y2]; then
f.(x2,y2) = [x2,y2] & y2 <> y1 by A34,A1,A3,Th69;
hence x1 = x2 & y1 = y2 by A4,A35,XTUPLE_0:1;
end;
suppose
A38: Case8[p,q,x2,y2]; then
f.(x2,y2) = [p,y2] by A1,Th70;
hence x1 = x2 & y1 = y2 by A38,A34,A4,A35,XTUPLE_0:1;
end;
end;
end;
theorem Th71:
p in q implies (T,p,q)incl|(inversions Swap(T,p,q) qua set) is one-to-one
proof assume
A1: p in q;
set f = (T,p,q)incl;
set s = Swap(T,p,q);
set w = inversions s;
set fw = f|(w qua set);
A2: dom s = dom T by FUNCT_7:99;
let x,y be object; assume x in dom fw & y in dom fw; then
A3: x in w & y in w by RELAT_1:57; then
consider x1,y1 being Element of dom T such that
A4: x = [x1,y1] & x1 in y1 & s/.x1 > s/.y1 by A2;
consider x2,y2 being Element of dom T such that
A5: y = [x2,y2] & x2 in y2 & s/.x2 > s/.y2 by A2,A3;
assume fw.x = fw.y; then
f.(x1,y1) = fw.y by A4,A3,FUNCT_1:49 .= f.(x2,y2) by A5,A3,FUNCT_1:49; then
x1 = x2 & y1 = y2 by A1,A4,A5,Lm1;
hence thesis by A4,A5;
end;
registration
let O,R,x,y,z;
cluster (R,x,y)incl.:z -> Relation-like;
coherence
proof
set X = dom R;
set i = id X;
set s = Swap(i,x,y);
set h = [:s,s:];
set Y = (succ y)\x;
set Z1 = [:{x},Y:], Z2 = [:Y,{y}:];
set g = id(Z1\/Z2);
A1: (R,x,y)incl.:z c= rng (R,x,y)incl by RELAT_1:111;
A2: rng h = [:rng s, rng s:] by FUNCT_3:67;
rng (R,x,y)incl c= rng h \/ rng g by FUNCT_4:17;
hence thesis by A1,A2;
end;
end;
begin :: Correctness of sorting by exchanging
theorem Th72:
[x,y] in inversions R implies
(R,x,y)incl.:inversions Swap(R,x,y) c< inversions R
proof assume
A1: [x,y] in inversions R; then
A2: x in dom R & y in dom R & x in y & R/.x > R/.y by Th46;
reconsider T=R as non empty array of O by A1;
reconsider p=x, q=y as Element of dom T by A1,Th46;
set j = (R,x,y)incl, k = (T,p,q)incl;
set s = Swap(R,x,y), t = Swap(T,p,q);
set ws = inversions s, w = inversions R;
A3: dom t = dom T by FUNCT_7:99;
thus j.:ws c= w
proof
let z,t be object; assume
[z,t] in j.:ws; then
consider a,b being object such that
A4: [a,b] in ws & [a,b] in dom j & [z,t] = j.(a,b) by Th5;
reconsider a,b as set by TARSKI:1;
[a,b] in inversions s implies
a in dom s & b in dom s & a in b by Th46;
then
A5: a in b & a in dom T & b in dom T by A4,A3;
then reconsider a,b as Element of dom T;
per cases by A2,A5,Th2;
suppose
A6: a <> p & a <> q & b <> p & b <> q; then
[z,t] = [a,b] by A4,A2,Th67;
hence thesis by A4,A6,Th52;
end;
suppose
A7: a in p & b = p; then
[z,t] = [a,q] by A4,A2,Th68;
hence thesis by A1,A4,A7,Th53;
end;
suppose
A8: a in p & b = q; then
[z,t] = [a,p] by A4,A2,Th68;
hence thesis by A1,A4,A8,Th54;
end;
suppose
A9: a = p & b in q; then
[z,t] = [a,b] by A5,A4,Th69;
hence thesis by A1,A4,A9,Th55;
end;
suppose
a = p & b = q;
hence thesis by A1,A4,A2,Th66;
end;
suppose
A10: a = p & q in b; then
[z,t] = [q,b] by A4,A2,Th70;
hence thesis by A1,A4,A10,Th57;
end;
suppose
A11: a = q & q in b; then
[z,t] = [p,b] by A4,A2,Th70;
hence thesis by A1,A4,A11,Th58;
end;
suppose
A12: p in a & q = b; then
[z,t] = [a,b] by A4,A5,Th69;
hence thesis by A1,A4,A12,Th56;
end;
end;
now assume
[x,y] in j.:ws; then
consider a,b being object such that
A13: [a,b] in ws & [a,b] in dom j & [x,y] = j.(a,b) by Th5;
A14: j.(p,q) = [p,q] by A2,Th66;
reconsider a,b as set by TARSKI:1;
[a,b] in inversions s implies
a in dom s & b in dom s & a in b by Th46;
then
A15: a in b & a in dom T & b in dom T by A13,A3;
then reconsider a,b as Element of dom T;
a = p & b = q by A2,A13,A14,A15,Lm1;
hence [x,y] in ws by A13;
end;
hence thesis by A1,Th51;
end;
registration
let R be finite Function;
let x,y;
cluster Swap(R,x,y) -> finite;
coherence
proof
dom Swap(R,x,y) = dom R by FUNCT_7:99;
hence thesis by FINSET_1:10;
end;
end;
theorem Th73:
for R being array of O
st [x,y] in inversions R & inversions R is finite
holds card inversions Swap(R,x,y) in card inversions R
proof
let R be array of O;
set s = Swap(R,x,y);
set h = (R,x,y)incl, ws = inversions s;
assume
A1: [x,y] in inversions R & inversions R is finite; then
reconsider w = inversions R as finite set;
h.:ws c< inversions R by A1,Th72; then
h.:ws c= w; then
reconsider hws = h.:ws as finite set;
card (hws) < card w by A1,Th72,TREES_1:6; then
A2: card (hws) in Segm card w by NAT_1:44;
A3: x in dom R & y in dom R & x in y by A1,Th46;
A4: R is non empty by A1;
ws,h.:ws are_equipotent
proof
take hw = h|(ws qua set);
thus hw is one-to-one by A3,A4,Th71;
dom s = dom R by FUNCT_7:99; then
ws c= [:dom R, dom R:] by Th47; then
ws c= dom h by A3,A4,Th61;
hence dom hw = ws by RELAT_1:62;
thus thesis by RELAT_1:115;
end;
hence card inversions Swap(R,x,y) in card inversions R by A2,CARD_1:5;
end;
theorem
for R being finite array of O st [x,y] in inversions R
holds card inversions Swap(R,x,y) < card inversions R
proof let R being finite array of O such that
A1: [x,y] in inversions R;
card inversions Swap(R,x,y) in Segm card inversions R by A1,Th73;
hence card inversions Swap(R,x,y) < card inversions R by NAT_1:44;
end;
definition
let O,R;
mode arr_computation of R -> non empty array means:
Def14:
it.(base-it) = R & (for a st a in dom it holds it.a is array of O) &
for a st a in dom it & succ a in dom it
ex R,x,y st [x,y] in inversions R & it.a = R & it.succ a = Swap(R,x,y);
existence
proof
reconsider C = <%R%> as 0-based non empty array;
take C;
A1: dom C = 1 & 0 in Segm 1 by AFINSQ_1:def 4,NAT_1:44; then
base-C = 0 by Def4;
hence C.(base-C) = R;
hereby let a; assume
a in dom C; then
a = 0 by A1,ORDINAL3:15,TARSKI:def 1;
hence C.a is array of O;
end;
let a; assume
a in dom C & succ a in dom C;
hence thesis by A1,ORDINAL3:15,TARSKI:def 1;
end;
end;
theorem Th75:
{[a,R]} is arr_computation of R
proof
reconsider C = {[a,R]} as a-based non empty array;
C is arr_computation of R
proof
A1: dom C = {a} & a in {a} by FUNCT_5:12,TARSKI:def 1; then
base-C = a by Def4;
hence C.(base-C) = R by GRFUNC_1:6;
hereby let b; assume
b in dom C; then
a = b by A1,TARSKI:def 1;
hence C.b is array of O by GRFUNC_1:6;
end;
let b; assume
b in dom C & succ b in dom C; then
a = b & a = succ b by A1,TARSKI:def 1; then
a in a by ORDINAL1:6;
hence thesis;
end;
hence thesis;
end;
registration
let O,R,a;
cluster a-based finite for arr_computation of R;
existence
proof
reconsider C = {[a,R]} as a-based non empty finite array;
C is arr_computation of R by Th75;
hence thesis;
end;
end;
registration
let O,R;
let C be arr_computation of R;
let x;
cluster C.x -> segmental Function-like Relation-like;
coherence
proof
per cases;
suppose x nin dom C;
hence thesis by FUNCT_1:def 2;
end;
suppose x in dom C;
hence thesis by Def14;
end;
end;
end;
registration
let O,R;
let C be arr_computation of R;
let x;
cluster C.x -> the carrier of O-valued;
coherence
proof
per cases;
suppose x nin dom C;
then C.x = {} by FUNCT_1:def 2;
then rng (C.x) = {};
hence rng (C.x) c= the carrier of O;
end;
suppose x in dom C;
hence thesis by Def14;
end;
end;
end;
registration
let O,R;
let C be arr_computation of R;
cluster last C -> segmental Relation-like Function-like;
coherence;
end;
registration
let O,R;
let C be arr_computation of R;
cluster last C -> the carrier of O-valued;
coherence;
end;
definition
let O,R;
let C be arr_computation of R;
attr C is complete means last C is ascending;
end;
theorem Th76:
for C being 0-based arr_computation of R st R is finite array of O
holds C is finite
proof
let C be 0-based arr_computation of R;
assume R is finite array of O; then
reconsider R as finite array of O;
A1: C.(base-C) = R by Def14;
deffunc F(array of O) = card inversions $1;
base-C = 0 by Th24; then
A2: F(C.0) is finite by A1;
A3: for a st succ a in dom C & F(C.a) is finite holds F(C.succ a) c< F(C.a)
proof let a; assume
A4: succ a in dom C & F(C.a) is finite;
a in succ a by ORDINAL1:6; then
a in dom C by A4,ORDINAL1:10; then
consider R,x,y such that
A5: [x,y] in inversions R & C.a = R & C.succ a = Swap(R,x,y) by A4,Def14;
inversions R is finite by A4,A5; then
F(C.succ a) in F(C.a) by A5,Th73; then
F(C.succ a) c= F(C.a) & F(C.succ a) <> F(C.a) by ORDINAL1:def 2;
hence F(C.succ a) c< F(C.a);
end;
thus C is finite from A(A2,A3);
end;
theorem
for C being 0-based arr_computation of R st R is finite array of O &
for a st inversions (C.a) <> {} holds succ a in dom C
holds C is complete
proof
let C be 0-based arr_computation of R;
assume R is finite array of O; then
C is finite by Th76; then
reconsider d = dom C as non empty finite Ordinal;
assume
A1: for a st inversions (C.a) <> {} holds succ a in dom C;
set u = union d;
consider n being Nat such that
A2: d = n+1 by NAT_1:6;
d = Segm(n+1) by A2;
then
A3: d = succ Segm n by NAT_1:38; then
A4: u = n by ORDINAL2:2;
inversions (C.u) <> 0 implies d in d by A1,A3,A4;
hence last C is ascending by Th48;
end;
theorem Th78:
for C being finite arr_computation of R
holds last C is permutation of R &
for a st a in dom C holds C.a is permutation of R
proof
let C be finite arr_computation of R;
consider a,b such that
A1: dom C = a\b by Def1;
consider n such that
A2: a = b+^n by A1,Th7;
defpred P[Nat] means
b+^$1 in dom C implies C.(b+^$1) is permutation of R;
A3: b+^(0 qua Ordinal) = b by ORDINAL2:27; then
n <> 0 by A1,A2,XBOOLE_1:37; then
consider m being Nat such that
A4: n = m+1 by NAT_1:6;
n = Segm(m+1) by A4;
then
A5: a = b+^succ Segm m by A2,NAT_1:38 .= succ(b+^m) by ORDINAL2:28; then
A6: b+^m = union a by ORDINAL2:2 .= union (a\b) by A1,Th6;
C.(base-C) = R by Def14; then
C.b = R by A1,Th23; then
A7: P[ 0] by A3,Th38;
A8: P[k] implies P[k+1]
proof assume
A9: P[k] & b+^(k+1) in dom C;
Segm(k+1) = succ Segm k by NAT_1:38; then
A10: b+^(k+1) = succ(b+^k) by ORDINAL2:28; then
b+^k in b+^(k+1) & b+^(k+1) in a by A1,A9,ORDINAL1:6; then
A11: b c= b+^k & b+^k in a by ORDINAL1:10,ORDINAL3:24; then
b+^k in dom C by A1,ORDINAL6:5; then
consider Q,x,y such that
A12: [x,y] in inversions Q & C.(b+^k) = Q & C.(b+^(k+1)) = Swap(Q,x,y)
by A9,A10,Def14;
x in dom Q & y in dom Q by A12,Th46; then
Swap(Q,x,y) is permutation of Q by Th43;
hence thesis by A9,A1,A11,A12,Th40,ORDINAL6:5;
end;
A13: P[k] from NAT_1:sch 2(A7,A8);
b c= b+^m & b+^m in a by A5,ORDINAL1:6,ORDINAL3:24; then
P[m] & b+^m in dom C by A1,A13,ORDINAL6:5;
hence last C is permutation of R by A1,A6;
let c; assume
A14: c in dom C; then
A15: b c= c & c in a by A1,ORDINAL6:5; then
c = b+^(c-^b) by ORDINAL3:def 5; then
c-^b in n by A2,A14,A1,ORDINAL3:22;
then c-^b in Segm n;
then reconsider k = c-^b as Nat;
P[k] by A13;
hence thesis by A14,A15,ORDINAL3:def 5;
end;
begin :: Existence of Complete Computations
theorem Th79:
for A being 0-based finite array of X st A <> {} holds last A in X
proof
let A be 0-based finite array of X;
assume A <> {}; then
consider n such that
A1: dom A = n+1 by NAT_1:6;
Segm(n+1) = succ Segm n by NAT_1:38; then
n in dom A & union dom A = n by A1,ORDINAL1:6,ORDINAL2:2;
hence last A in X by FUNCT_1:102;
end;
theorem Th80:
last <%x%> = x
proof
dom <%x%> = succ 0 by AFINSQ_1:def 4; then
union dom <%x%> = 0 by ORDINAL2:2;
hence thesis;
end;
theorem Th81:
for A being 0-based finite array holds last (A^<%x%>) = x
proof
let A be 0-based finite array;
dom <%x%> = 1 by AFINSQ_1:def 4; then
dom(A^<%x%>) = (dom A)+^1 by ORDINAL4:def 1
.= succ dom A by ORDINAL2:31; then
union dom (A^<%x%>) = len A by ORDINAL2:2;
hence thesis by AFINSQ_1:36;
end;
registration
let X be set;
cluster -> X-valued for Element of X^omega;
coherence by AFINSQ_1:42;
end;
scheme A{F(set)->set, X()->non empty set, P[set,set], s()->set}:
ex f being finite 0-based non empty array, k being Element of X() st
k = last f & F(k) = {} & f.0 = s() &
for a st succ a in dom f
ex x,y being Element of X() st x = f.a & y = f.succ a & P[x,y]
provided
A1: s() in X() and
A2: F(s()) is finite and
A3: for x being Element of X() st F(x) <> {}
ex y being Element of X() st P[x,y] & F(y) c< F(x)
proof
set D = X()^omega;
reconsider s0 = s() as Element of X() by A1;
reconsider f0 = <%s0%> as Element of D by AFINSQ_1:42;
defpred P[set,Element of D,Element of D] means
($2 = {} or F(last $2) = {} implies $2 = $3) &
($2 <> {} & F(last $2) <> {} implies
ex y being Element of X() st
P[last $2,y] & F(y) c< F(last $2) & $2^<%y%> = $3);
A4: for a being Nat
for x being Element of D
ex y being Element of D st P[a,x,y]
proof
let a be Nat;
let x be Element of D;
per cases;
suppose
A5: x = {} or F(last x) = {};
take y = x;
thus P[a,x,y] by A5;
end;
suppose
A6: x <> {} & F(last x) <> {}; then
last x in X() by Th79; then
consider y being Element of X() such that
A7: P[last x,y] & F(y) c< F(last x) by A3,A6;
reconsider z = x^<%y%> as Element of D by AFINSQ_1:42;
take z;
thus P[a,x,z] by A6,A7;
end;
end;
consider F being sequence of D such that
A8: F.0 = f0 & for a being Nat holds
P[a,F.a qua Element of D,F.(a+1) qua Element of D]
from RECDEF_1:sch 2(A4);
defpred S[Nat] means F.$1 <> {};
A9: S[0] by A8;
A10: S[m] implies S[m+1]
proof assume
S[m]; then
reconsider f = F.m as non empty Sequence;
P[m,F.m qua Element of D,F.(m+1) qua Element of D] by A8; then
F.(m+1) = f or ex x st F.(m+1) = f^<%x%>;
hence thesis;
end;
A11: S[m] from NAT_1:sch 2(A9,A10);
defpred X[Function] means $1.0 = s() &
for a st succ a in dom $1
ex x,y being Element of X() st x = $1.a & y = $1.succ a & P[x,y];
defpred T[Nat] means X[F.$1];
A12: T[0]
proof
thus F.0.0 = s() by A8;
let a; assume succ a in dom(F.0); then
succ a in 1 by A8,AFINSQ_1:def 4;
hence thesis by CARD_1:49,TARSKI:def 1;
end;
A13: T[m] implies T[m+1]
proof assume
A14: T[m];
A15: P[m,F.m qua Element of D,F.(m+1) qua Element of D] by A8;
per cases;
suppose F.m = {} or F(last(F.m qua Element of D)) = {};
hence thesis by A14,A15;
end;
suppose
A16: F.m <> {} & F(last(F.m qua Element of D)) <> {};
reconsider fm = F.m as non empty finite Sequence of X() by A16;
reconsider fm1 = F.(m+1) as finite Sequence of X();
consider y being Element of X() such that
A17: P[last fm,y] & F(y) c< F(last fm) & fm^<%y%> = F.(m+1) by A8,A16;
0 in dom fm by ORDINAL3:8;
hence F.(m+1).0 = s() by A14,A17,ORDINAL4:def 1;
let a; assume
A18: succ a in dom(F.(m+1));
A19: a in succ a by ORDINAL1:6; then
A20: a in dom fm1 by A18,ORDINAL1:10;
then reconsider n = a as Nat;
reconsider x = fm1.a, z = fm1.succ a as Element of X()
by A18,A20,FUNCT_1:102;
A21: dom <%y%> = 1 by AFINSQ_1:def 4; then
dom fm1 = (dom fm)+^1 by A17,ORDINAL4:def 1
.= succ dom fm by ORDINAL2:31; then
A22: a in dom fm by A18,ORDINAL3:3;
take x,z;
thus x = (F.(m+1)).a & z = (F.(m+1)).succ a;
per cases by ORDINAL6:4;
suppose
A23: succ a in dom fm; then
a in dom fm by A19,ORDINAL1:10; then
A24: x = fm.a & z = fm.succ a by A17,A23,ORDINAL4:def 1;
ex x,y being Element of X() st x = fm.a & y = fm.succ a & P[x,y]
by A14,A23;
hence P[x,z] by A24;
end;
suppose
A25: dom fm c= succ a;
succ a c= dom fm by A22,ORDINAL1:21; then
A26: dom fm = succ a by A25; then
union dom fm = a by ORDINAL2:2; then
A27: last fm = fm1.a by A17,A22,ORDINAL4:def 1;
0 in Segm 1 & (succ a)+^(0 qua Ordinal) = succ a
by NAT_1:44,ORDINAL2:27; then
z = <%y%>.0 by A21,A17,A26,ORDINAL4:def 1;
hence P[x,z] by A17,A27;
end;
end;
end;
A28: T[m] from NAT_1:sch 2(A12,A13);
defpred Q[Nat] means ex n st card F(last(F.n qua Element of D)) = $1;
A29: ex n st Q[n]
proof
last f0 = s0 by Th80; then
reconsider n = card F(last(F.0 qua Element of D)) as Nat by A2,A8;
take n;
thus thesis;
end;
A30: for n st n <> 0 & Q[n] ex m st m < n & Q[m]
proof
let n; assume
A31: n <> 0;
given k being Nat such that
A32: card F(last(F.k qua Element of D)) = n;
reconsider fk = F.k, fk1 = F.(k+1) as Element of D;
P[k,fk,fk1] & fk <> {} by A11,A8; then
consider y being Element of X() such that
A33: P[last fk,y] & F(y) c< F(last fk) & fk^<%y%> = fk1 by A31,A32;
A34: F(last fk) is finite & F(y) c= F(last fk) by A32,A33;
A35: last fk1 = y by A33,Th81; then
reconsider m = card F(last fk1) as Nat by A34;
take m;
thus m < n by A32,A33,A34,A35,TREES_1:6;
thus Q[m];
end;
Q[0] from NAT_1:sch 7(A29,A30); then
consider n such that
A36: card F(last(F.n qua Element of D)) = 0;
reconsider f = F.n as non empty XFinSequence of X() by A11;
take f;
reconsider k = last f as Element of X() by Th79;
take k;
thus k = last f & F(k) = {} by A36;
thus X[f] by A28;
end;
reserve A for array, B for permutation of A;
theorem Th82:
B in Funcs(dom A, rng A)
proof
dom B = dom A & rng B = rng A by Th37;
hence thesis by FUNCT_2:def 2;
end;
registration
let A be real-valued array;
cluster -> real-valued for permutation of A;
coherence
proof
let B be permutation of A;
ex f being Permutation of dom A st B = A*f by Def9;
hence thesis;
end;
end;
registration
let a;
let X be non empty set;
cluster -> Sequence-like for Element of Funcs(a,X);
coherence
by FUNCT_2:92;
end;
registration
let X;
let Y be real-membered non empty set;
cluster -> real-valued for Element of Funcs(X,Y);
coherence;
end;
registration
let X;
let A be array of X;
cluster -> X-valued for permutation of A;
coherence
proof
let B be permutation of A;
ex f being Permutation of dom A st B = A*f by Def9;
hence thesis;
end;
end;
registration
let X be set;
let Z be set;
let Y be Subset of Z;
cluster -> Z-valued for Element of Funcs(X,Y);
coherence
proof
let f be Element of Funcs(X,Y);
per cases by SUBSET_1:def 1;
suppose f = {};
then rng f = {};
hence rng f c= Z;
end;
suppose Funcs(X,Y) <> {};
then rng f c= Y by FUNCT_2:92;
hence rng f c= Z by XBOOLE_1:1;
end;
end;
end;
theorem
for r being X-defined Y-valued Relation holds r is Relation of X,Y
proof
let r be X-defined Y-valued Relation;
[:dom r, rng r:] c= [:X,Y:] & r c= [:dom r, rng r:]
by RELAT_1:7,ZFMISC_1:96;
hence r is Relation of X,Y by XBOOLE_1:1;
end;
theorem
Th84: for a being finite Ordinal, x st x in a
holds x = 0 or ex b st x = succ b
proof
let a be finite Ordinal;
let x;
assume
A1: x in a & x <> 0; then
A2: {} in x by ORDINAL3:8;
now assume x is limit_ordinal; then
omega c= x & x c= a by A1,A2,ORDINAL1:def 2,def 11;
hence contradiction;
end;
hence thesis by A1,ORDINAL1:29;
end;
theorem Th85:
for A being 0-based finite non empty array of O
ex C being 0-based arr_computation of A st C is complete
proof
let A be 0-based finite non empty array of O;
reconsider rA = rng A as non empty Subset of O by RELAT_1:def 19;
reconsider a = dom A as Ordinal;
set X = Funcs(a, rA);
deffunc F(array of O) = card inversions $1;
defpred P[Element of X, Element of X] means
ex p,q being Element of dom A
st [p,q] in inversions
(($1 qua Element of Funcs(a, rA qua Subset of O)) qua array of O) &
$2 = Swap($1,p,q);
A is permutation of A by Th38; then
A1: A in X by Th82;
A2: F(A) is finite;
A3: for x being Element of X st
F((x qua Element of Funcs(a, rA qua Subset of O)) qua array of O) <> {}
ex y being Element of X st P[x,y] &
F((y qua Element of Funcs(a, rA qua Subset of O)) qua array of O) c<
F((x qua Element of Funcs(a, rA qua Subset of O)) qua array of O)
proof
let x be Element of X;
reconsider c = x as array of O;
set z = the Element of inversions c;
set Fx = F((x qua Element of Funcs(a, rA qua Subset of O))
qua array of O);
assume Fx <> {}; then
A4: inversions c <> {}; then
z in inversions c &
inversions c is Relation of dom x,dom x by Th47; then
consider p,q being object such that
A5: z = [p,q] & p in dom x & q in dom x by RELSET_1:2;
set y = Swap(x,p,q);
A6: dom y = dom x & rng y = rng x by FUNCT_7:99,103;
dom x = dom A & rng x c= rng A by FUNCT_2:92; then
reconsider y as Element of X by A6,FUNCT_2:def 2;
reconsider b = y as array of O;
set Fy = F((y qua Element of Funcs(a, rA qua Subset of O))
qua array of O);
take y;
thus P[x,y] by A4,A5;
F(b) in F(c) by A4,A5,Th73;
hence Fy c= Fx & Fy <> Fx by ORDINAL1:def 2;
end;
consider f being finite 0-based non empty array, k being Element of X
such that
A7: k = last f &
F((k qua Element of Funcs(a, rA qua Subset of O)) qua array of O) = {} &
f.0 = A and
A8: for a st succ a in dom f
ex x,y being Element of X st x = f.a & y = f.succ a & P[x,y]
from A(A1,A2,A3);
f is arr_computation of A
proof
thus f.(base-f) = A by A7,Th24;
thus for a st a in dom f holds f.a is array of O
proof
let a; assume
A9: a in dom f;
per cases by A9,Th84;
suppose a = 0;
hence f.a is array of O by A7;
end;
suppose ex b st a = succ b; then
consider b such that
A10: a = succ b;
ex x,y being Element of X st x = f.b & y = f.a & P[x,y] by A8,A9,A10;
hence f.a is array of O;
end;
end;
let a; assume
a in dom f & succ a in dom f; then
ex x,y being Element of X st x = f.a & y = f.succ a & P[x,y] by A8;
hence thesis;
end; then
reconsider f as 0-based arr_computation of A;
take f;
inversions last f = {} by A7;
hence last f is ascending by Th48;
end;
theorem Th86:
for A being 0-based finite non empty array of O
ex B being permutation of A st B is ascending
proof
let A be 0-based finite non empty array of O;
consider C being 0-based arr_computation of A such that
A1: C is complete by Th85;
C is finite by Th76; then
reconsider B = last C as permutation of A by Th78;
take B;
thus B is ascending by A1;
end;
registration
let O;
let A be 0-based finite array of O;
cluster ascending for permutation of A;
existence
proof
A1: A is permutation of A by Th38;
A is empty implies A is ascending;
hence thesis by A1,Th86;
end;
end;