exchsort.miz
begin
reserve a,a1,a2,b,c,d for
Ordinal,
n,m,k for
Nat,
x,y,z,t,X,Y,Z for
set;
theorem ::
EXCHSORT:1
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 ::
EXCHSORT:2
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 ::
EXCHSORT:3
x
nin y implies ((y
\/
{x})
\ y)
=
{x} by
XBOOLE_1: 88,
ZFMISC_1: 50;
theorem ::
EXCHSORT:4
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 ::
EXCHSORT:5
Th5: for f be
Function, r be
Relation holds for x be
object holds x
in (f
.: r) iff ex y,z be
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 be
object such that
A1: t
in (
dom f) & t
in r & x
= (f
. t) by
FUNCT_1:def 6;
consider y,z be
object such that
A2: t
=
[y, z] by
A1,
RELAT_1:def 1;
(f
. (y,z))
= (f
.
[y, z]);
hence ex y,z be
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 ::
EXCHSORT:6
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 ::
EXCHSORT:7
Th7: (a
\ b) is non
empty
finite implies ex n be
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 be
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 be
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
definition
let f be
set;
::
EXCHSORT:def1
attr f is
segmental means
:
Def1: ex a, b st (
proj1 f)
= (a
\ b);
end
reserve f,g for
Function;
theorem ::
EXCHSORT:8
(
dom f)
= (
dom g) & f is
segmental implies g is
segmental;
theorem ::
EXCHSORT:9
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 be
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,
ORDINAL1: 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;
::
EXCHSORT:def2
attr s is a
-based means b
in (
proj1 s) implies a
in (
proj1 s) & a
c= b;
::
EXCHSORT:def3
attr s is a
-limited means a
= (
sup (
proj1 s));
end
theorem ::
EXCHSORT:10
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 ::
EXCHSORT:11
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 ::
EXCHSORT:12
Th12: f is (
inf (
dom f))
-based by
ORDINAL2: 14,
ORDINAL2: 17;
theorem ::
EXCHSORT:13
f is (
sup (
dom f))
-limited;
theorem ::
EXCHSORT:14
f is b
-limited & a
in (
dom f) implies a
in b by
ORDINAL2: 19;
definition
let f;
::
EXCHSORT:def4
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 ;
::
EXCHSORT:def5
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;
::
EXCHSORT:def6
func
len- f ->
Ordinal equals ((
limit- f)
-^ (
base- f));
coherence ;
end
theorem ::
EXCHSORT:15
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 ::
EXCHSORT:16
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 ::
EXCHSORT:17
f is (
limit- f)
-limited by
Th16;
theorem ::
EXCHSORT:18
for A be
empty
set holds A is a
-based;
registration
let a, X, Y;
cluster Y
-definedX
-valueda
-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 ::
EXCHSORT:19
for f be
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 ::
EXCHSORT:20
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 ::
EXCHSORT:21
f is (
base- f)
-based
proof
(
base- f)
= (
inf (
dom f)) by
Th20;
hence thesis by
Th12;
end;
theorem ::
EXCHSORT:22
(
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,
ORDINAL2: 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 ::
EXCHSORT:23
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 ::
EXCHSORT:24
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;
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;
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;
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;
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
emptyb
-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
emptyb
-based
finiteX
-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;
::
EXCHSORT:def7
func
last A ->
set equals (A
. (
union (
dom A)));
coherence ;
end
registration
let A be
Sequence;
identify
last A with A
last ;
compatibility ;
end
begin
definition
let f be
Function;
::
EXCHSORT:def8
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 ::
EXCHSORT:25
for f be
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 be
Nat such that
A4: c
= (d
+^ n) by
A2,
A3,
Th7;
consider e1 be
Ordinal such that
A5: a
= (d
+^ e1) & e1
in (
Segm n) by
A2,
A3,
A4,
Th1;
consider e2 be
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 be
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 be
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(+)
= (
succ
Y(k)) by
ORDINAL2: 28;
then
A12:
Y(k)
in
Y(+) & a
in (
succ a) by
ORDINAL1: 6;
then
A13:
Y(k)
c=
Y(+) & 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(+)
in (
dom f);
then
Y(k)
in (
dom f) by
A2,
A13,
A14,
Th9;
then (f
.
Y(k))
c< (f
. a) & (f
.
Y(+))
c< (f
.
Y(k)) by
A1,
A11,
A15;
hence (f
.
Y(+))
c< (f
. a) by
XBOOLE_1: 56;
end;
A16: for k be
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 ::
EXCHSORT:26
Th26: for f be
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 be
Ordinal such that
A7: a
= (d
+^ e1) & e1
in
omega by
A3,
A4,
A6,
Th1;
consider e2 be
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 be
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 be
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(+)
= (
succ
Y(k)) by
ORDINAL2: 28;
then
A14:
Y(k)
in
Y(+) & a
in (
succ a) by
ORDINAL1: 6;
then
A15:
Y(k)
c=
Y(+) & 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(+)
in (
dom f);
then
Y(k)
in (
dom f) by
A3,
A15,
A16,
Th9;
then (f
.
Y(k))
c< (f
. a) & (f
.
Y(+))
c< (f
.
Y(k)) by
A2,
A13,
A17;
hence (f
.
Y(+))
c< (f
. a) by
XBOOLE_1: 56;
end;
A18: for k be
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 ::
EXCHSORT:27
Th27: for f be
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 be
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 ::
EXCHSORT:28
for f be
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 be
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 ::
EXCHSORT:sch1
A { A() ->
Sequence , F(
set) ->
set } :
A() is
finite
provided
A1: F(.) is
finite
and
A2: for a st (
succ a)
in (
dom A()) & F(.) is
finite holds F(.)
c< F(.);
deffunc
G(
set) = F(.);
consider F be
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) 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) 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
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 ::
EXCHSORT:29
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 ::
EXCHSORT:30
Th30: for f be
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 ::
EXCHSORT:31
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 ::
EXCHSORT:32
Th32: for f be
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 ::
EXCHSORT:33
Th33: for x,y,z be
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 ::
EXCHSORT:34
Th34: for f be
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 ::
EXCHSORT:35
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
ontoX
-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 ::
EXCHSORT:36
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;
coherence
proof
let B be
array;
assume
A1: B
= (
Swap (A,x,y));
let z be
object;
assume z
in (
dom B);
then
A2: z
in (
dom A) & (x
= z or x
<> z) & (y
= z or y
<> z) by
A1,
FUNCT_7: 99;
not x
in (
dom A) or not y
in (
dom A) implies B
= A by
A1,
FUNCT_7:def 12;
then (B
. z)
= (A
. y) or (B
. z)
= (A
. x) or (B
. z)
= (A
. z) by
A1,
A2,
Th29,
Th31,
Th33;
hence thesis;
end;
end
begin
definition
let A be
array;
::
EXCHSORT:def9
mode
permutation of A ->
array means
:
Def9: ex f be
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 ::
EXCHSORT:37
Th37: for B be
permutation of A holds (
dom B)
= (
dom A) & (
rng B)
= (
rng A)
proof
let B be
permutation of A;
consider f be
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,
FUNCT_2:def 3;
hence thesis by
A1,
RELAT_1: 27,
RELAT_1: 28;
end;
theorem ::
EXCHSORT:38
Th38: A is
permutation of A
proof
take (
id (
dom A));
thus thesis by
RELAT_1: 51;
end;
theorem ::
EXCHSORT:39
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 be
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 ::
EXCHSORT:40
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 be
Permutation of (
dom B) such that
A3: A
= (B
* f) by
A1,
Def9;
consider g be
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 ::
EXCHSORT:41
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-oneX
-valuedX
-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;
:: original:
Swap
redefine
func
Swap (f,x,y) ->
Function of X, Y ;
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,
FUNCT_7: 103;
(
rng f)
c= Y by
RELAT_1:def 19;
hence thesis by
A1,
A2,
FUNCT_2: 2;
end;
end
theorem ::
EXCHSORT:42
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,
FUNCT_7: 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 ::
EXCHSORT:43
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 ::
EXCHSORT:44
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
definition
let O be
RelStr;
let A be
array of O;
::
EXCHSORT:def10
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);
::
EXCHSORT:def11
func
inversions A ->
set equals {
[a, b] where a,b be
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 be
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 ::
EXCHSORT:45
Th45: for O holds for x,y be
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;
:: original:
inversions
redefine
::
EXCHSORT:def12
func
inversions R equals {
[a, b] where a,b be
Element of (
dom R) : a
in b & (R
/. a)
> (R
/. b) };
compatibility
proof
set N = {
[a, b] where a,b be
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 be
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 be
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 ::
EXCHSORT:46
Th46: for x be
object, y be
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 be
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 ::
EXCHSORT:47
Th47: (
inversions R)
c=
[:(
dom R), (
dom R):]
proof
let x be
object;
assume
A1: x
in (
inversions R);
then
consider a,b be
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 ::
EXCHSORT:48
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 be
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 ::
EXCHSORT:49
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 ::
EXCHSORT:50
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;
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;
:: original:
<
redefine
pred a
< b;
asymmetry by
ORDERS_2: 5;
end
theorem ::
EXCHSORT:51
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 ::
EXCHSORT:52
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 ::
EXCHSORT:53
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 ::
EXCHSORT:54
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 ::
EXCHSORT:55
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 ::
EXCHSORT:56
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 ::
EXCHSORT:57
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 ::
EXCHSORT:58
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;
::
EXCHSORT:def13
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 ::
EXCHSORT:59
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 ::
EXCHSORT:60
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 ::
EXCHSORT:61
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 ::
EXCHSORT:62
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 ::
EXCHSORT:63
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 ::
EXCHSORT:64
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 ::
EXCHSORT:65
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 ::
EXCHSORT:66
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 ::
EXCHSORT:67
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 ::
EXCHSORT:68
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 ::
EXCHSORT:69
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 ::
EXCHSORT:70
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 be
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 ::
EXCHSORT:71
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 be
Element of (
dom T) such that
A4: x
=
[x1, y1] & x1
in y1 & (s
/. x1)
> (s
/. y1) by
A2;
consider x2,y2 be
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
theorem ::
EXCHSORT:72
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 be
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 be
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 ::
EXCHSORT:73
Th73: for R be
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 ::
EXCHSORT:74
for R be
finite
array of O st
[x, y]
in (
inversions R) holds (
card (
inversions (
Swap (R,x,y))))
< (
card (
inversions R))
proof
let R be
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;
::
EXCHSORT:def14
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 ) holds 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 ::
EXCHSORT:75
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;
::
EXCHSORT:def15
attr C is
complete means (
last C) is
ascending;
end
theorem ::
EXCHSORT:76
Th76: for C be
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(.) is
finite by
A1;
A3: for a st (
succ a)
in (
dom C) &
F(.) is
finite holds
F(.)
c<
F(.)
proof
let a;
assume
A4: (
succ a)
in (
dom C) &
F(.) 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(.)
in
F(.) by
A5,
Th73;
then
F(.)
c=
F(.) &
F(.)
<>
F(.) by
ORDINAL1:def 2;
hence
F(.)
c<
F(.);
end;
thus C is
finite from
A(
A2,
A3);
end;
theorem ::
EXCHSORT:77
for C be
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 be
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 ::
EXCHSORT:78
Th78: for C be
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 be
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
theorem ::
EXCHSORT:79
Th79: for A be
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 ::
EXCHSORT:80
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 ::
EXCHSORT:81
Th81: for A be
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 ::
EXCHSORT:sch2
A { F(
set) ->
set , X() -> non
empty
set , P[
set,
set], s() ->
set } :
ex f be
finite
0
-based non
empty
array, k be
Element of X() st k
= (
last f) & F(k)
=
{} & (f
.
0 )
= s() & for a st (
succ a)
in (
dom f) holds ex x,y be
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 be
Element of X() st F(x)
<>
{} holds ex y be
Element of X() st P[x, y] & F(y)
c< F(x);
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)
=
{} implies $2
= $3) & ($2
<>
{} & F(last)
<>
{} implies ex y be
Element of X() st P[(
last $2), y] & F(y)
c< F(last) & ($2
^
<%y%>)
= $3);
A4: for a be
Nat holds for x be
Element of D holds ex y be
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)
=
{} ;
take y = x;
thus
P[a, x, y] by
A5;
end;
suppose
A6: x
<>
{} & F(last)
<>
{} ;
then (
last x)
in X() by
Th79;
then
consider y be
Element of X() such that
A7: P[(
last x), y] & F(y)
c< F(last) 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 be
sequence of D such that
A8: (F
.
0 )
= f0 & for a be
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) holds ex x,y be
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)
=
{} ;
hence thesis by
A14,
A15;
end;
suppose
A16: (F
. m)
<>
{} & F(last)
<>
{} ;
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 be
Element of X() such that
A17: P[(
last fm), y] & F(y)
c< F(last) & (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 be
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))
= $1;
A29: ex n st
Q[n]
proof
(
last f0)
= s0 by
Th80;
then
reconsider n = (
card F(last)) as
Nat by
A2,
A8;
take n;
thus thesis;
end;
A30: for n st n
<>
0 &
Q[n] holds ex m st m
< n &
Q[m]
proof
let n;
assume
A31: n
<>
0 ;
given k be
Nat such that
A32: (
card F(last))
= n;
reconsider fk = (F
. k), fk1 = (F
. (k
+ 1)) as
Element of D;
P[k, fk, fk1] & fk
<>
{} by
A11,
A8;
then
consider y be
Element of X() such that
A33: P[(
last fk), y] & F(y)
c< F(last) & (fk
^
<%y%>)
= fk1 by
A31,
A32;
A34: F(last) is
finite & F(y)
c= F(last) by
A32,
A33;
A35: (
last fk1)
= y by
A33,
Th81;
then
reconsider m = (
card F(last)) 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))
=
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 ::
EXCHSORT:82
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 be
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 be
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 ::
EXCHSORT:83
for r be X
-definedY
-valued
Relation holds r is
Relation of X, Y
proof
let r be X
-definedY
-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 ::
EXCHSORT:84
Th84: for a be
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,
ORDINAL1:def 11;
hence contradiction;
end;
hence thesis by
A1,
ORDINAL1: 29;
end;
theorem ::
EXCHSORT:85
Th85: for A be
0
-based
finite non
empty
array of O holds ex C be
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 be
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 be
Element of X st
F()
<>
{} holds ex y be
Element of X st
P[x, y] &
F()
c<
F()
proof
let x be
Element of X;
reconsider c = x as
array of O;
set z = the
Element of (
inversions c);
set Fx =
F();
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 be
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,
FUNCT_7: 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();
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 be
finite
0
-based non
empty
array, k be
Element of X such that
A7: k
= (
last f) &
F()
=
{} & (f
.
0 )
= A and
A8: for a st (
succ a)
in (
dom f) holds ex x,y be
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 be
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 be
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 ::
EXCHSORT:86
Th86: for A be
0
-based
finite non
empty
array of O holds ex B be
permutation of A st B is
ascending
proof
let A be
0
-based
finite non
empty
array of O;
consider C be
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