:: On Multiset Ordering
:: by Grzegorz Bancerek
::
:: Received December 31, 2015
:: Copyright (c) 2015-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 TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FINSET_1, ARYTM_1,
ARYTM_3, FUNCT_1, PARTFUN1, BINOP_1, XXREAL_0, VALUED_0, NUMBERS, CARD_1,
MESFUNC1, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2, PRE_POLY, BAGORD_2,
ZFMISC_1, NAT_1, FUNCOP_1, ORDERS_1, REWRITE1, FINSEQ_1, ORDINAL4,
GROEB_1, CARD_3, INTERVA1, MIDSP_1, GRAPH_2, MCART_1, BAGORDER;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2,
ORDINAL1,
RELSET_1, NECKLACE, FUNCT_1, PARTFUN1, BINOP_1, CARD_1, FINSEQ_1,
FINSEQ_2, FINSET_1, VALUED_0, NUMBERS, FUNCT_2, XXREAL_0, XCMPLX_0,
NAT_1, NAT_D, REWRITE1, GRAPH_2, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2,
WAYBEL_4, PRE_POLY, FINSEQ_6;
constructors DOMAIN_1, RELSET_1, NECKLACE, BINOP_2, WAYBEL_4, REWRITE1,
GRAPH_2, NAT_D, MONOID_1, FINSEQ_6, PRE_POLY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, ORDINAL1, XREAL_0, VALUED_0,
STRUCT_0, ORDERS_2, MONOID_0, CARD_1, PRE_POLY, FINSEQ_1, FINSET_1,
REWRITE1, NAT_1, RELAT_1, XTUPLE_0, FUNCT_2;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, OPOSET_1,
ORDERS_2, PBOOLE, PRE_POLY;
equalities FINSEQ_1, STRUCT_0, PBOOLE;
theorems TARSKI, XBOOLE_0, ZFMISC_1, NAT_1, NAT_2, NAT_D, GRAPH_2, FUNCT_1,
PARTFUN1, FUNCT_2, ORDINAL1, XREAL_0, XREAL_1, XXREAL_0, VALUED_0,
ORDERS_2, MONOID_0, MONOID_1, PRE_POLY, PBOOLE, FUNCOP_1, TREES_2,
WAYBEL_4, NECKLACE, PREFER_1, YELLOW_0, FINSEQ_1, RELAT_2, RELSET_1,
REWRITE1, FINSEQ_2, FINSEQ_3, FINSEQ_5, RELAT_1, XBOOLE_1, RFUNCT_1,
BAGORDER, CARD_2, XTUPLE_0, FOMODEL0, TREES_1, FINSEQ_6;
schemes RELSET_1, PARTFUN1, FINSEQ_1, FUNCT_2, NAT_1;
begin
theorem Th6:
for m,n being Nat holds n = (m-'(m-'n))+(n-'m)
proof
let m,n be Nat;
per cases;
suppose m <= n;
then
A1: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233;
then m-'(m-'n) = m by NAT_D:40;
hence thesis by A1;
end;
suppose m > n;
then n-'m = 0 & m-'(m-'n) = n & n+0 = n by NAT_D:58,NAT_2:8;
hence thesis;
end;
end;
theorem
for n,m being Nat holds m-'n >= m-n by XREAL_0:def 2;
theorem Th5:
for m,n,x,y being Nat st n = (m-'x)+y holds m-'n <= x & n-'m <= y
proof
let m,n,x,y be Nat such that
A0: n = (m-'x)+y;
per cases;
suppose m <= n;
then
A1: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233;
n <= m+y by A0,XREAL_1:6,NAT_D:35;
hence thesis by A1,XREAL_1:20;
end;
suppose
m > n;
then
A2: n-'m = 0 & m-'(m-'n) = n >= m-'x by A0,NAT_D:58,NAT_1:11,NAT_2:8;
m-'(m-'n) = m-(m-'n) & m-'x >= m-x
by XREAL_0:def 2,XREAL_1:233,NAT_D:35;
then m-(m-'n) >= m-x by A2,XXREAL_0:2;
hence thesis by XREAL_1:10,A2;
end;
end;
theorem Th5A:
for m,n,x,y being Nat st x <= m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m)
proof
let m,n,x,y be Nat;
assume Z0: x <= m;
assume Z1: n = (m-'x)+y;
then m-'n <= x & n-'m <= y by Th5;
then
A2: x-'(m-'n) = x-(m-'n) & y-'(n-'m) = y-(n-'m) by XREAL_1:233;
A3: n-y = m-x by Z0,Z1,XREAL_1:233;
per cases;
suppose m <= n;
then
A4: m-'n = 0 & n-'m = n-m by NAT_2:8,XREAL_1:233;
hence x-'(m-'n) = x by A2 .= y-n+m by A3
.= y-'(n-'m) by A2,A4;
end;
suppose m > n;
then
A5: n-'m = 0 & m-'n = m-n by NAT_2:8,XREAL_1:233;
hence x-'(m-'n) = x-m+n by A2 .= y by A3
.= y-'(n-'m) by A2,A5;
end;
end;
theorem Th14:
for k,x1,x2,y1,y2 being Nat st x2 <= k & x1 <= (k-'x2)+y2
holds x2+(x1-'y2) <= k &
(((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1)
proof
let k,x1,x2,y1,y2 be Nat;
assume Z0: x2 <= k;
then A1: k-'x2 = k-x2 by XREAL_1:233;
assume Z1: x1 <= (k-'x2)+y2;
thus x2+(x1-'y2) <= k
proof
per cases;
suppose x1 < y2;
then x1-'y2 = 0 by NAT_2:8;
hence thesis by Z0;
end;
suppose x1 >= y2;
then x1-'y2 = x1-y2 by XREAL_1:233;
then x1-'y2 <= (k-x2)+y2-y2 = k-x2 by A1,Z1,XREAL_1:9;
then x2+(x1-'y2) <= k-x2+x2 by XREAL_1:6;
hence thesis;
end;
end;
then
A2: k-'(x2+(x1-'y2)) = k-(x2+(x1-'y2)) & ((k-'x2)+y2)-'x1 = ((k-x2)+y2)-x1
by Z1,A1,XREAL_1:233;
per cases;
suppose x1 <= y2;
then x1-'y2 = 0 & y2-'x1 = y2-x1 by XREAL_1:233,NAT_2:8;
hence (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) by A2;
end;
suppose x1 > y2;
then y2-'x1 = 0 & x1-'y2 = x1-y2 by XREAL_1:233,NAT_2:8;
hence (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1) by A2;
end;
end;
::$CT
reserve a,b for object, I,J for set;
registration
cluster asymmetric transitive non empty for RelStr;
existence
proof
set X = {0};
set r = {}[:X,X:];
take R = RelStr(#X,r#);
thus R is asymmetric
proof let a,b;
assume a in the carrier of R & b in the carrier of R;
thus thesis;
end;
thus R is transitive
proof let a;
thus thesis;
end;
thus thesis;
end;
end;
registration
let I;
cluster asymmetric transitive for Relation of I;
existence
proof
set X = I;
take r = {}[:X,X:];
thus r is asymmetric
proof let a,b;
thus thesis;
end;
thus r is transitive
proof let a;
thus thesis;
end;
end;
end;
registration
let R be asymmetric RelStr;
cluster the InternalRel of R -> asymmetric;
coherence by NECKLACE:def 4;
end;
registration
let I;
let p,q be I-valued FinSequence;
cluster p^q -> I-valued;
coherence;
end;
theorem Lem8:
for p,q being FinSequence st p^q is I-valued
holds p is I-valued & q is I-valued
proof
let p,q be FinSequence;
assume Z1: rng (p^q) c= I;
A1: rng (p^q) = rng p \/ rng q by FINSEQ_1:31;
rng p c= rng p \/ rng q by XBOOLE_1:7;
hence rng p c= I by Z1,A1,XBOOLE_1:1;
rng q c= rng p \/ rng q by XBOOLE_1:7;
hence rng q c= I by Z1,A1,XBOOLE_1:1;
end;
registration
let I;
let f be I-valued FinSequence;
let n be Nat;
cluster f|n -> I-valued;
coherence;
end;
theorem Lem9:
for p being FinSequence st a in rng p
ex q,r being FinSequence st p = q^<*a*>^r
proof
let p be FinSequence;
assume a in rng p;
then consider i being object such that
A1: i in dom p & a = p.i by FUNCT_1:def 3;
reconsider i as Nat by A1;
A3: 1 <= i <= len p by A1,FINSEQ_3:25;
consider k being Nat such that
A2: i = 1+k by NAT_1:10,A1,FINSEQ_3:25;
set q = (1,k)-cut p;
set r = (i+1,len p)-cut p;
take q,r;
k <= i & (i,i)-cut p = <*a*> by A1,A3,A2,NAT_1:11,
FINSEQ_6:132;
hence p = q^<*a*>^r by A3,A2,FINSEQ_6:136;
end;
theorem Lem12:
for p,q being FinSequence holds p c< q iff len p < len q &
for i being Nat st i in dom p holds p.i = q.i
proof
let p,q be FinSequence;
hereby
assume Z0: p c< q;
hence len p < len q by TREES_1:6;
p c= q by Z0,XBOOLE_0:def 8;
hence for i being Nat st i in dom p holds p.i = q.i by FOMODEL0:51;
end;
assume Z2: len p < len q;
then dom p c< dom q by FINSEQ_3:118;
then
A1: dom p c= dom q by XBOOLE_0:def 8;
assume for i being Nat st i in dom p holds p.i = q.i;
then for i being set st i in dom p holds i in dom q & p.i = q.i by A1;
hence p c< q by Z2,XBOOLE_0:def 8,FOMODEL0:51;
end;
theorem Lem13:
for p,q,r being FinSequence holds r^p c< r^q iff p c< q
proof let p,q,r be FinSequence;
thus r^p c< r^q implies p c< q
proof
assume
A0: r^p c< r^q;
len(r^p) = len r+len p & len(r^q) = len r+len q by FINSEQ_1:22;
then
A2: len p < len q by A0,Lem12,XREAL_1:6;
then
A3: dom p c= dom q by FINSEQ_3:30;
for i being Nat st i in dom p holds p.i = q.i
proof let i be Nat;
assume i in dom p;
then p.i = (r^p).(len r+i) & q.i = (r^q).(len r+i) &
len r+i in dom(r^p) by A3,FINSEQ_1:def 7,28;
hence thesis by A0,Lem12;
end;
hence thesis by A2,Lem12;
end;
assume p c< q;
then r^p c= r^q & r^p <> r^q by FINSEQ_6:13,FINSEQ_1:33,XBOOLE_0:def 8;
hence thesis by XBOOLE_0:def 8;
end;
definition
let R be asymmetric non empty RelStr;
let x,y be Element of R;
redefine pred x <= y; :: redefines <= (ORDERS_2, definition)
asymmetry
proof
let a,b be Element of R;
assume [a,b] in the InternalRel of R;
hence not [b,a] in the InternalRel of R by PREFER_1:22;
end;
end;
theorem Lem2:
for R being asymmetric non empty RelStr
for x,y being Element of R holds x <= y iff x < y
proof
let R be asymmetric non empty RelStr;
let x,y be Element of R;
hereby
assume Z0: x <= y;
then x <> y;
hence x < y by Z0,ORDERS_2:def 6;
end;
assume x < y;
hence x <= y by ORDERS_2:def 6;
end;
begin
definition
let I;
mode multiset of I is Element of finite-MultiSet_over I;
end;
registration
let I;
cluster -> I-defined natural-valued for multiset of I;
coherence
proof
let m be multiset of I;
m in the carrier of finite-MultiSet_over I c=
the carrier of MultiSet_over I by MONOID_0:23;
hence thesis by MONOID_1:27;
end;
end;
registration
let I;
cluster -> total for multiset of I;
coherence
proof
let m be multiset of I;
m in the carrier of finite-MultiSet_over I c=
the carrier of MultiSet_over I by MONOID_0:23;
then m is Function of I,NAT by MONOID_1:27;
hence thesis;
end;
end;
definition
let m be natural-valued Function;
redefine func support m equals :: redefines support (PRE_POLY, definition)
m"(NAT\{0});
compatibility
proof
let I;
support m = m"(NAT\{0})
proof
thus support m c= m"(NAT\{0})
proof
let a; assume a in support m;
then
A1: m.a <> 0 by PRE_POLY:def 7;
then
A2: a in dom m by FUNCT_1:def 2;
m.a in NAT & not m.a in {0} by A1,TARSKI:def 1,ORDINAL1:def 12;
then m.a in NAT\{0} by XBOOLE_0:def 5;
hence thesis by A2,FUNCT_1:def 7;
end;
let a; assume a in m"(NAT\{0});
then m.a in NAT\{0} by FUNCT_1:def 7;
then not m.a in {0} by XBOOLE_0:def 5;
then m.a <> 0 by TARSKI:def 1;
hence thesis by PRE_POLY:def 7;
end;
hence I = support m iff I = m"(NAT\{0});
end;
end;
registration
let I;
cluster -> finite-support for multiset of I;
coherence
proof
let m be multiset of I;
m in the carrier of finite-MultiSet_over I c=
the carrier of MultiSet_over I by MONOID_0:23;
then support m is finite by MONOID_1:def 6;
hence thesis by PRE_POLY:def 8;
end;
end;
theorem Th1:
a is multiset of I iff a is bag of I
proof
thus a is multiset of I implies a is bag of I;
assume a is bag of I;
then reconsider b = a as bag of I;
dom b = I & rng b c= NAT by PARTFUN1:def 2,VALUED_0:def 6;
then b is Function of I,NAT by FUNCT_2:2;
then b is Multiset of I & support b is finite by MONOID_1:27;
hence thesis by MONOID_1:def 6;
end;
theorem Th11:
1.finite-MultiSet_over I = EmptyBag I
proof
1.MultiSet_over I = I --> 0 = EmptyBag I by MONOID_1:26;
hence thesis by MONOID_0:def 24;
end;
definition
let R be RelStr;
let x,y be Element of R;
pred x ## y means not x <= y & not y <= x;
symmetry;
end;
definition
struct(multMagma,RelStr) RelMultMagma (#
carrier -> set,
multF -> BinOp of the carrier,
InternalRel -> Relation of the carrier
#);
end;
definition
struct(multLoopStr,RelStr) RelMonoid (#
carrier -> set,
multF -> BinOp of the carrier,
OneF -> Element of the carrier,
InternalRel -> Relation of the carrier
#);
end;
definition
let M be multLoopStr;
mode RelExtension of M -> RelMonoid means :RE:
the multLoopStr of it = the multLoopStr of M;
existence
proof
set r = the Relation of the carrier of M;
take R = RelMonoid(#the carrier of M, the multF of M, the OneF of M,r#);
thus thesis;
end;
end;
registration
let M be non empty multLoopStr;
cluster -> non empty for RelExtension of M;
coherence
proof
let R be RelExtension of M;
the multLoopStr of R = the multLoopStr of M by RE;
hence thesis;
end;
end;
registration
let M be multLoopStr;
cluster strict for RelExtension of M;
existence
proof
set r = the Relation of the carrier of M;
set R = RelMonoid(#the carrier of M, the multF of M, the OneF of M,r#);
the multLoopStr of R = the multLoopStr of M;
then R is RelExtension of M by RE;
hence thesis;
end;
end;
theorem Th2:
for N being multLoopStr, M being RelExtension of N holds
a is Element of M iff a is Element of N
proof
let N be multLoopStr;
let M be RelExtension of N;
the multLoopStr of N = the multLoopStr of M by RE;
hence thesis;
end;
theorem Th3:
for N being multLoopStr, M being RelExtension of N holds 1.N = 1.M
proof
let N be multLoopStr;
let M be RelExtension of N;
the multLoopStr of N = the multLoopStr of M by RE;
hence thesis;
end;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> Function-like Relation-like for Element of M;
coherence
proof
let m be Element of M;
m is multiset of I by Th2;
hence thesis;
end;
end;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> I-defined natural-valued finite-support for Element of M;
coherence
proof
let m be Element of M;
m is multiset of I by Th2;
hence thesis;
end;
end;
registration
let I;
let M be RelExtension of finite-MultiSet_over I;
cluster -> total for Element of M;
coherence
proof
let m be Element of M;
m is multiset of I by Th2;
hence thesis;
end;
end;
theorem
for M being RelExtension of finite-MultiSet_over I holds
the carrier of M = Bags I
proof set N = finite-MultiSet_over I;
let M be RelExtension of finite-MultiSet_over I;
thus the carrier of M c= Bags I
proof let a;
assume a in the carrier of M;
hence a in Bags I by PRE_POLY:def 12;
end;
let a; assume a in Bags I;
then a is bag of I by PRE_POLY:def 12;
then a is Element of N by Th1;
then a is Element of M by Th2;
hence thesis;
end;
scheme RelEx{M() -> non empty multLoopStr, R[object,object]}:
ex N being strict RelExtension of M() st
for x,y being Element of N holds x <= y iff R[x,y];
consider R being Relation of the carrier of M() such that
A1: for x,y being Element of M() holds [x,y] in R iff R[x,y]
from RELSET_1:sch 2;
set N = RelMonoid(#the carrier of M(),the multF of M(),the OneF of M(),R#);
the multLoopStr of N = the multLoopStr of M();
then reconsider N as strict RelExtension of M() by RE;
take N;
let x,y be Element of N;
[x,y] in R iff R[x,y] by A1;
hence thesis by ORDERS_2:def 5;
end;
theorem Th4:
for N being multLoopStr, M1,M2 being strict RelExtension of N
st for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y
holds m <= n iff x <= y
holds M1 = M2
proof
let N be multLoopStr;
let M1,M2 be strict RelExtension of N;
assume
Z4: for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y
holds m <= n iff x <= y;
A2: the multLoopStr of M1 = the multLoopStr of N &
the multLoopStr of M2 = the multLoopStr of N by RE;
the InternalRel of M1 = the InternalRel of M2
proof let a,b;
hereby
assume
A3: [a,b] in the InternalRel of M1;
then reconsider m = a, n = b as Element of M1 by ZFMISC_1:87;
reconsider x = m, y = n as Element of M2 by A2;
m <= n by A3,ORDERS_2:def 5;
then x <= y by Z4;
hence [a,b] in the InternalRel of M2 by ORDERS_2:def 5;
end;
assume
A3: [a,b] in the InternalRel of M2;
then reconsider m = a, n = b as Element of M2 by ZFMISC_1:87;
reconsider x = m, y = n as Element of M1 by A2;
m <= n by A3,ORDERS_2:def 5;
then x <= y by Z4;
hence [a,b] in the InternalRel of M1 by ORDERS_2:def 5;
end;
hence M1 = M2 by A2;
end;
begin
definition
let R be non empty RelStr;
func DershowitzMannaOrder R -> strict RelExtension of
finite-MultiSet_over the carrier of R means :DM:
for m,n being Element of it holds m <= n iff ex x,y being Element of it st
1.it <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
existence
proof set M = finite-MultiSet_over the carrier of R;
defpred R[bag of the carrier of R,bag of the carrier of R] means
ex x,y being Element of M st
1.M <> x divides $2 & $1 = ($2 -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
consider N being strict RelExtension of M such that
A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx;
take N; let m,n be Element of N;
hereby assume m <= n;
then consider x,y being Element of M such that
A2: 1.M <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A1;
reconsider x,y as Element of N by Th2;
take x,y;
thus 1.N <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A2,Th3;
end;
given x,y being Element of N such that
A3: 1.N <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
reconsider x,y as Element of M by Th2;
1.M <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A3,Th3;
hence thesis by A1;
end;
uniqueness
proof set M = finite-MultiSet_over the carrier of R;
let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R;
assume that
A1: for m,n being Element of N1 holds m <= n iff ex x,y being Element of N1 st
1.N1 <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a and
A2: for m,n being Element of N2 holds m <= n iff ex x,y being Element of N2 st
1.N2 <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y
holds m <= n iff x <= y
proof
let m,n be Element of N1;
let k,l be Element of N2;
assume Z0: m = k;
assume Z1: n = l;
A5: 1.N1 = 1.M = 1.N2 by Th3;
hereby
assume m <= n;
then consider x,y being Element of N1 such that
A3: 1.N1 <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A1;
reconsider x,y as Element of M by Th2;
reconsider x,y as Element of N2 by Th2;
1.N2 <> x divides l & k = (l -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by Z0,Z1,A3,A5;
hence k <= l by A2;
end;
assume k <= l;
then consider x,y being Element of N2 such that
A4: 1.N2 <> x divides l & k = (l -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A2;
reconsider x,y as Element of M by Th2;
reconsider x,y as Element of N1 by Th2;
1.N1 <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by Z0,Z1,A4,A5;
hence m <= n by A1;
end;
hence thesis by Th4;
end;
end;
theorem Th7:
for m,n being bag of I holds n = (m-'(m-'n))+(n-'m)
proof
let m,n be bag of I;
let a; assume a in I;
thus n.a = (m.a-'(m.a-'n.a))+(n.a-'m.a) by Th6
.= (m.a-'(m-'n).a)+(n.a-'m.a) by PRE_POLY:def 6
.= (m-'(m-'n)).a+(n.a-'m.a) by PRE_POLY:def 6
.= (m-'(m-'n)).a+(n-'m).a by PRE_POLY:def 6
.= ((m-'(m-'n))+(n-'m)).a by PRE_POLY:def 5;
end;
theorem Th8:
for m,n,x,y being bag of I st n = (m-'x)+y holds m-'n divides x &
n-'m divides y
proof
let m,n,x,y be bag of I;
assume Z0: n = (m-'x)+y;
thus m-'n divides x
proof let a;
n.a = (m-'x).a+y.a by Z0,PRE_POLY:def 5
.= (m.a-'x.a)+y.a by PRE_POLY:def 6;
then m.a-'n.a <= x.a by Th5;
hence (m-'n).a <= x.a by PRE_POLY:def 6;
end;
let a;
n.a = (m-'x).a+y.a by Z0,PRE_POLY:def 5
.= (m.a-'x.a)+y.a by PRE_POLY:def 6;
then n.a-'m.a <= y.a by Th5;
hence thesis by PRE_POLY:def 6;
end;
theorem Th8A:
for m,n,x,y being bag of I st x divides m & n = (m-'x)+y holds
x-'(m-'n) = y-'(n-'m)
proof
let m,n,x,y be bag of I;
assume Z0: x divides m;
assume Z1: n = (m-'x)+y;
let a; assume a in I;
A1: n.a = (m-'x).a+y.a = (m.a-'x.a)+y.a & x.a <= m.a
by Z0,Z1,PRE_POLY:def 5,def 6,def 11;
thus (x-'(m-'n)).a = x.a-'(m-'n).a by PRE_POLY:def 6
.= x.a-'(m.a-'n.a) by PRE_POLY:def 6
.= y.a-'(n.a-'m.a) by A1,Th5A
.= y.a-'(n-'m).a by PRE_POLY:def 6
.= (y-'(n-'m)).a by PRE_POLY:def 6;
end;
theorem Th9:
for m,x,y being bag of I st x divides m & x <> y holds m <> (m-'x)+y
proof
let m,x,y be bag of I;
assume Z0: for a holds x.a <= m.a;
given a such that
Z1: a in I & x.a <> y.a;
take a; thus a in I by Z1;
A1: ((m-'x)+y).a = (m-'x).a+y.a = (m.a-'x.a)+y.a by PRE_POLY:def 5,def 6;
m.a-'x.a = m.a-x.a by Z0,XREAL_1:233;
hence thesis by A1,Z1;
end;
theorem Lem5:
for I being non empty set, R being Relation of I
for r being RedSequence of R
st len r > 1 holds r.len r in I
proof
let I be non empty set;
let R be Relation of I;
let r be RedSequence of R;
assume Z0: len r > 1;
then consider i being Nat such that
A1: len r = 1+i by NAT_1:10;
len r >= i >= 1 by Z0,A1,NAT_1:13;
then i in dom r & i+1 in dom r by A1,FINSEQ_3:25,FINSEQ_5:6;
then [r.i,r.len r] in R by A1,REWRITE1:def 2;
hence r.len r in I by ZFMISC_1:87;
end;
theorem Th13:
for R being asymmetric transitive Relation of I
for r being RedSequence of R holds r is one-to-one
proof
let R be asymmetric transitive Relation of I;
let r be RedSequence of R;
let a,b; assume Z0: a in dom r & b in dom r;
then reconsider i = a, j = b as Nat;
assume Z1: r.a = r.b & a <> b;
A1: for i,j being Nat st i > j & i in dom r & j in dom r holds r.i <> r.j
proof
let i,j be Nat;
assume i > j; then
A1: i >= j+1 by NAT_1:13;
assume Z3: i in dom r;
assume Z4: j in dom r;
defpred P[Nat] means $1 in dom r implies [r.j,r.$1] in R & r.$1 <> r.j;
A2: P[j+1]
proof
assume j+1 in dom r;
hence [r.j,r.(j+1)] in R by Z4,REWRITE1:def 2;
hence thesis by PREFER_1:22;
end;
A3: for i being Nat st i >= j+1 & P[i] holds P[i+1]
proof
let i be Nat; assume
Z5: i >= j+1 & P[i] & i+1 in dom r;
then 1 <= j+1 & i < i+1 <= len r by NAT_1:11,13,FINSEQ_3:25;
then 1 <= i <= len r by Z5,XXREAL_0:2;
then i in dom r by FINSEQ_3:25;
then
ZZ: [r.j,r.i] in R & [r.i,r.(i+1)] in R by Z5,REWRITE1:def 2;
hence [r.j,r.(i+1)] in R by RELAT_2:31;
thus thesis by PREFER_1:22,ZZ;
end;
for i being Nat st i >= j+1 holds P[i] from NAT_1:sch 8(A2,A3);
hence r.i <> r.j by A1,Z3;
end;
i < j or j < i by Z1,XXREAL_0:1;
hence thesis by Z0,Z1,A1;
end;
theorem Th12:
for R being asymmetric transitive non empty RelStr
for X being set st X is finite & ex x being Element of R st x in X
ex x being Element of R st x is_maximal_in X
proof
let R be asymmetric transitive non empty RelStr;
let X be set;
assume X is finite;
then reconsider X1 = X as finite set;
given x being Element of R such that
Z1: x in X;
set Y = {r where r is Element of X1*:
r is RedSequence of the InternalRel of R};
defpred P[Nat] means ex r being RedSequence of the InternalRel of R st
r in Y & len r = $1;
A1: for k being Nat st P[k] holds k <= card X1
proof
let k be Nat;
given r being RedSequence of the InternalRel of R such that
A2: r in Y & len r = k;
consider q being Element of X1* such that
A3: r = q & q is RedSequence of the InternalRel of R by A2;
rng r c= X1 & r is one-to-one by A3,Th13,FINSEQ_1:def 4;
then len r = card rng r <= card X1 by PRE_POLY:19,NAT_1:43;
hence thesis by A2;
end;
B1: P[1]
proof
set k = 1;
reconsider r = <*x*> as RedSequence of the InternalRel of R
by REWRITE1:6;
take r;
<*x*> is FinSequence of X1 by Z1,FINSEQ_1:74;
then <*x*> in X1* by FINSEQ_1:def 11;
hence r in Y;
thus len r = k by FINSEQ_1:39;
end;
then
A4: ex k being Nat st P[k];
consider k being Nat such that
A5: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1,A4);
consider r being RedSequence of the InternalRel of R such that
A6: r in Y & len r = k by A5;
consider q being Element of X1* such that
A7: r = q & q is RedSequence of the InternalRel of R by A6;
1 <= k by B1,A5;
then per cases by XXREAL_0:1;
suppose
C1: k = 1;
take x;
not ex y being Element of R st y in X & x < y
proof
given y being Element of R such that
A8: y in X & x < y;
[x,y] in the InternalRel of R by A8,ORDERS_2:def 5,def 6;
then reconsider r = <*x,y*> as RedSequence of the InternalRel of R
by REWRITE1:7;
<*x,y*> is FinSequence of X1 by Z1,A8,FINSEQ_2:13;
then r in X1* by FINSEQ_1:def 11;
then r in Y & len r = 2 by FINSEQ_1:44;
hence contradiction by A5,C1;
end;
hence x is_maximal_in X by Z1,WAYBEL_4:55;
end;
suppose
A8: k > 1;
then reconsider x = r.k as Element of R by A6,Lem5;
take x;
A9: k in dom r & r is FinSequence of X1 by A6,A7,FINSEQ_5:6;
not ex y being Element of R st y in X & x < y
proof
given y being Element of R such that
B1: y in X & x < y;
[x,y] in the InternalRel of R by B1,ORDERS_2:def 5,def 6;
then reconsider p = <*x,y*> as RedSequence of the InternalRel of R
by REWRITE1:7;
p.1 = x;
then reconsider rp = r$^p as RedSequence of the InternalRel of R
by A6,REWRITE1:8;
ex i being Nat st k = 1+i by A8,NAT_1:10;
then consider t being FinSequence, a such that
B2: r = t^<*a*> by A6,FINSEQ_2:18;
k = len t + 1 by A6,B2,FINSEQ_2:16;
then x = a by B2,FINSEQ_1:42;
then
B3: rp = r^<*y*> by B2,REWRITE1:3;
reconsider yy = <*y*>, r1 = r as FinSequence of X1
by A7,B1,FINSEQ_1:74;
r1^yy is FinSequence of X1;
then rp in X1* by B3,FINSEQ_1:def 11;
then rp in Y & len rp = k+1 by A6,B3,FINSEQ_2:16;
then k+1 <= k by A5;
hence contradiction by NAT_1:13;
end;
hence x is_maximal_in X by A9,FUNCT_1:102,WAYBEL_4:55;
end;
end;
theorem Lem3:
for m,n being bag of I holds m-'n divides m
proof
let m,n be bag of I;
let a;
m.a-'n.a <= m.a by NAT_D:35;
hence (m-'n).a <= m.a by PRE_POLY:def 6;
end;
registration
let I;
cluster -> Function-like Relation-like for Element of Bags I;
coherence by PRE_POLY:def 12;
end;
theorem Lem4:
for m,n being bag of I holds
m-'n <> EmptyBag I or m = n or n-'m <> EmptyBag I
proof
let m,n be bag of I;
assume Z0: m-'n = EmptyBag I;
assume m <> n;
then consider a such that
A1: a in I & m.a <> n.a by PBOOLE:def 10;
per cases by A1,XXREAL_0:1;
suppose m.a > n.a;
then m.a-n.a > 0 by XREAL_1:50;
then m.a-'n.a > 0 by XREAL_0:def 2;
then 0 < (m-'n).a = 0 by A1,Z0,FUNCOP_1:7,PRE_POLY:def 6;
hence thesis;
end;
suppose
A3: n.a > m.a;
take a; thus a in I by A1;
n.a-m.a > 0 by A3,XREAL_1:50;
then n.a-'m.a > 0 by XREAL_0:def 2;
then (n-'m).a > 0 by PRE_POLY:def 6;
hence (n-'m).a <> (EmptyBag I).a by A1,FUNCOP_1:7;
end;
end;
definition
let R being asymmetric transitive non empty RelStr;
redefine func DershowitzMannaOrder R means :HO: :: redefines DershowitzMannaOrder (BAGORD_2, definition)
for m,n being Element of it holds m <= n iff m <> n &
for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b;
compatibility
proof
let M be strict RelExtension of finite-MultiSet_over the carrier of R;
hereby
assume
A1: M = DershowitzMannaOrder R;
let m,n be Element of M;
hereby assume m <= n;
then consider x,y being Element of M such that
A2: 1.M <> x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a by A1,DM;
set X = {a where a is Element of R: x.a > 0 &
ex b being Element of R st y.b > 0 & b <= a};
B1: X c= support x
proof
let a; assume a in X;
then consider c being Element of R such that
A3: a = c & x.c > 0 & ex b being Element of R st y.b > 0 & b <= c;
thus thesis by A3,PRE_POLY:def 7;
end;
x <> y
proof
per cases by Th3;
suppose y = 1.M;
hence thesis by A2;
end;
suppose y <> 1.finite-MultiSet_over the carrier of R;
then y <> EmptyBag the carrier of R by Th11;
then consider b such that
A5: b in the carrier of R & y.b <> ((the carrier of R)-->0).b
by PBOOLE:def 10;
reconsider b as Element of R by A5;
A6: 0 <= y.b <> 0 by A5,FUNCOP_1:7;
then consider a being Element of R such that
A7: x.a > 0 & b <= a by A2;
a in X by A6,A7;
then consider c being Element of R such that
A8: c is_maximal_in X by B1,Th12;
A9: c in X & not ex a being Element of R st a in X & c < a
by A8,WAYBEL_4:55;
not c in support y
proof assume c in support y;
then
A11: 0 <= y.c <> 0 by PRE_POLY:def 7;
then consider a being Element of R such that
A12: x.a > 0 & c <= a by A2;
a in X & c < a by A11,A12,Lem2;
hence contradiction by A8,WAYBEL_4:55;
end;
hence thesis by B1,A9;
end;
end;
hence m <> n by A2,Th9;
let a be Element of R; assume m.a > n.a; then m.a-n.a>0 by XREAL_1:50;
then m.a-'n.a>0 by XREAL_0:def 2;
then
A3: (m-'n).a>0 by PRE_POLY:def 6;
m-'n divides y by A2,Th8;
then y.a > 0 by A3,PRE_POLY:def 11;
then consider b being Element of R such that
A4: x.b > 0 & a <= b by A2;
set X = {c where c is Element of R: x.c > 0 & a <= c};
X c= support x
proof
let b; assume b in X;
then consider c being Element of R such that
B2: b = c & x.c > 0 & a <= c;
thus thesis by B2,PRE_POLY:def 7;
end;
then X is finite & b in X by A4;
then consider c being Element of R such that
B3: c is_maximal_in X by Th12;
c in X & not ex a being Element of R st a in X & c < a
by B3,WAYBEL_4:55;
then consider d being Element of R such that
B5: c = d & x.d > 0 & a <= d;
take c;
thus a <= c by B5;
assume m.c >= n.c;
then per cases by XXREAL_0:1;
suppose m.c > n.c;
then m.c-n.c > 0 by XREAL_1:50;
then m.c-'n.c > 0 & m-'n divides y by A2,Th8,XREAL_0:def 2;
then y.c >= (m-'n).c > 0 by PRE_POLY:def 6,def 11;
then consider e being Element of R such that
B6: x.e > 0 & c <= e by A2;
a <= e by B5,B6,YELLOW_0:def 2;
then e in X & c < e by B6,Lem2;
hence contradiction by B3,WAYBEL_4:55;
end;
suppose
m.c = n.c;
then x.c = x.c-'0 = x.c-'(n.c-'m.c) = x.c-'(n-'m).c =
(x-'(n-'m)).c = (y-'(m-'n)).c = y.c-'(m-'n).c = y.c-'(m.c-'n.c) =
y.c-'0 = y.c
by A2,Th8A,XREAL_1:232,NAT_D:40,PRE_POLY:def 6;
then consider e being Element of R such that
B6: x.e > 0 & c <= e by A2,B5;
a <= e by B5,B6,YELLOW_0:def 2;
then e in X & c < e by B6,Lem2;
hence contradiction by B3,WAYBEL_4:55;
end;
end;
assume
A5: m <> n &
for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b;
reconsider x = n-'m, y = m-'n as multiset of the carrier of R by Th1;
reconsider x,y as Element of M by Th2;
A6: m = (n-'x)+y by Th7;
A8: x divides n by Lem3;
A9: now let b be Element of R;
assume y.b > 0;
then m.b-'n.b>0 by PRE_POLY:def 6;
then m.b-n.b > 0 by XREAL_0:def 2;
then consider a being Element of R such that
A7: b <= a & m.a < n.a by A5,XREAL_1:47;
take a; n.a-m.a > 0 by A7,XREAL_1:50;
then n.a-'m.a > 0 by XREAL_0:def 2;
hence x.a > 0 & b <= a by A7,PRE_POLY:def 6;
end;
1.M <> x
proof
per cases by A5,Lem4;
suppose EmptyBag the carrier of R <> x;
then 1.finite-MultiSet_over the carrier of R <> x by Th11;
hence thesis by Th3;
end;
suppose EmptyBag the carrier of R <> y;
then consider b such that
A10: b in the carrier of R & (EmptyBag the carrier of R).b <> y.b
by PBOOLE:def 10;
reconsider b as Element of R by A10;
0 <> y.b >= 0 by A10,FUNCOP_1:7;
then consider a being Element of R such that
A11: x.a > 0 & b <= a by A9;
take a;
EmptyBag the carrier of R = 1.finite-MultiSet_over the carrier of R
= 1.M by Th11,Th3;
hence thesis by A11,FUNCOP_1:7;
end;
end;
hence m <= n by A1,A6,A8,A9,DM;
end;
assume
B1: for m,n being Element of M holds m <= n iff m <> n &
for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b;
for m,n being Element of M holds m <= n iff ex x,y being Element of M st
1.M <> x & x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a
proof
let m,n be Element of M;
hereby
assume Z0: m <= n;
reconsider x = n-'m, y = m-'n as multiset of the carrier of R by Th1;
reconsider x,y as Element of M by Th2;
take x,y;
A9: now let b be Element of R;
assume y.b > 0;
then m.b-'n.b>0 by PRE_POLY:def 6;
then m.b-n.b > 0 by XREAL_0:def 2;
then consider a being Element of R such that
A7: b <= a & m.a < n.a by Z0,B1,XREAL_1:47;
take a; n.a-m.a > 0 by A7,XREAL_1:50;
then n.a-'m.a > 0 by XREAL_0:def 2;
hence x.a > 0 & b <= a by A7,PRE_POLY:def 6;
end;
thus 1.M <> x
proof
per cases by Z0,B1,Lem4;
suppose EmptyBag the carrier of R <> x;
then 1.finite-MultiSet_over the carrier of R <> x by Th11;
hence thesis by Th3;
end;
suppose EmptyBag the carrier of R <> y;
then consider b such that
A10: b in the carrier of R & (EmptyBag the carrier of R).b <> y.b
by PBOOLE:def 10;
reconsider b as Element of R by A10;
0 <> y.b >= 0 by A10,FUNCOP_1:7;
then consider a being Element of R such that
A11: x.a > 0 & b <= a by A9;
take a;
EmptyBag the carrier of R = 1.finite-MultiSet_over the carrier of R
= 1.M by Th11,Th3;
hence thesis by A11,FUNCOP_1:7;
end;
end;
thus x divides n by Lem3;
thus m = (n -' x) + y by Th7;
let b be Element of R;
assume y.b > 0;
hence ex a being Element of R st x.a > 0 & b <= a by A9;
end;
given x,y being Element of M such that
A2: 1.M <> x & x divides n & m = (n -' x) + y &
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a;
now
set X = {a where a is Element of R: x.a > 0 &
ex b being Element of R st y.b > 0 & b <= a};
B1: X c= support x
proof
let a; assume a in X;
then consider c being Element of R such that
A3: a = c & x.c > 0 & ex b being Element of R st y.b > 0 & b <= c;
thus thesis by A3,PRE_POLY:def 7;
end;
x <> y
proof
per cases by Th3;
suppose y = 1.M;
hence thesis by A2;
end;
suppose y <> 1.finite-MultiSet_over the carrier of R;
then y <> EmptyBag the carrier of R by Th11;
then consider b such that
A5: b in the carrier of R & y.b <> ((the carrier of R)-->0).b
by PBOOLE:def 10;
reconsider b as Element of R by A5;
A6: 0 <= y.b <> 0 by A5,FUNCOP_1:7;
then consider a being Element of R such that
A7: x.a > 0 & b <= a by A2;
a in X by A6,A7;
then consider c being Element of R such that
A8: c is_maximal_in X by B1,Th12;
A9: c in X & not ex a being Element of R st a in X & c < a
by A8,WAYBEL_4:55;
not c in support y
proof assume c in support y;
then
A11: 0 <= y.c <> 0 by PRE_POLY:def 7;
then consider a being Element of R such that
A12: x.a > 0 & c <= a by A2;
a in X & c < a by A11,A12,Lem2;
hence contradiction by A8,WAYBEL_4:55;
end;
hence thesis by B1,A9;
end;
end;
hence m <> n by A2,Th9;
let a be Element of R; assume m.a > n.a; then m.a-n.a>0 by XREAL_1:50;
then m.a-'n.a>0 by XREAL_0:def 2;
then
A3: (m-'n).a>0 by PRE_POLY:def 6;
m-'n divides y by A2,Th8;
then (m-'n).a <= y.a by PRE_POLY:def 11;
then consider b being Element of R such that
A4: x.b > 0 & a <= b by A2,A3;
set X = {c where c is Element of R: x.c > 0 & a <= c};
X c= support x
proof
let b; assume b in X;
then consider c being Element of R such that
B2: b = c & x.c > 0 & a <= c;
thus thesis by B2,PRE_POLY:def 7;
end;
then X is finite & b in X by A4;
then consider c being Element of R such that
B3: c is_maximal_in X by Th12;
c in X & not ex a being Element of R st a in X & c < a
by B3,WAYBEL_4:55;
then consider d being Element of R such that
B5: c = d & x.d > 0 & a <= d;
take c;
thus a <= c by B5;
assume m.c >= n.c;
then per cases by XXREAL_0:1;
suppose m.c > n.c;
then m.c-n.c > 0 by XREAL_1:50;
then m.c-'n.c > 0 & m-'n divides y by A2,Th8,XREAL_0:def 2;
then y.c >= (m-'n).c > 0 by PRE_POLY:def 6,def 11;
then consider e being Element of R such that
B6: x.e > 0 & c <= e by A2;
a <= e by B5,B6,YELLOW_0:def 2;
then e in X & c < e by B6,Lem2;
hence contradiction by B3,WAYBEL_4:55;
end;
suppose
m.c = n.c;
then x.c = x.c-'0 = x.c-'(n.c-'m.c) = x.c-'(n-'m).c =
(x-'(n-'m)).c = (y-'(m-'n)).c = y.c-'(m-'n).c = y.c-'(m.c-'n.c) =
y.c-'0 = y.c
by A2,Th8A,XREAL_1:232,NAT_D:40,PRE_POLY:def 6;
then consider e being Element of R such that
B6: x.e > 0 & c <= e by A2,B5;
a <= e by B5,B6,YELLOW_0:def 2;
then e in X & c < e by B6,Lem2;
hence contradiction by B3,WAYBEL_4:55;
end;
end;
hence m <= n by B1;
end;
hence M = DershowitzMannaOrder R by DM;
end;
end;
theorem Th15:
for k,x1,x2,y1,y2 being bag of I st x2 divides k & x1 divides (k-'x2)+y2
holds x2+(x1-'y2) divides k &
(((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1)
proof let k,x1,x2,y1,y2 be bag of I;
assume
A1: for a holds x2.a <= k.a;
assume
A2: for a holds x1.a <= ((k-'x2)+y2).a;
hereby
let a;
x2.a <= k.a & x1.a <= ((k-'x2)+y2).a = (k-'x2).a+y2.a = (k.a-'x2.a)+y2.a
by A1,A2,PRE_POLY:def 5,def 6;
then x2.a+(x1.a-'y2.a) <= k.a by Th14;
then x2.a+(x1-'y2).a <= k.a by PRE_POLY:def 6;
hence (x2+(x1-'y2)).a <= k.a by PRE_POLY:def 5;
end;
let a such that a in I;
x2.a <= k.a & x1.a <= ((k-'x2)+y2).a = (k-'x2).a+y2.a = (k.a-'x2.a)+y2.a
by A1,A2,PRE_POLY:def 5,def 6;
then
A3: (((k.a-'x2.a)+y2.a)-'x1.a)+y1.a =
(k.a-'(x2.a+(x1.a-'y2.a)))+((y2.a-'x1.a)+y1.a) by Th14;
A4: (((k.a-'x2.a)+y2.a)-'x1.a)+y1.a
= (((k-'x2).a+y2.a)-'x1.a)+y1.a by PRE_POLY:def 6
.= (((k-'x2)+y2).a-'x1.a)+y1.a by PRE_POLY:def 5
.= (((k-'x2)+y2)-'x1).a+y1.a by PRE_POLY:def 6
.= ((((k-'x2)+y2)-'x1)+y1).a by PRE_POLY:def 5;
(k.a-'(x2.a+(x1.a-'y2.a)))+((y2.a-'x1.a)+y1.a)
= (k.a-'(x2.a+(x1.a-'y2.a)))+((y2-'x1).a+y1.a) by PRE_POLY:def 6
.= (k.a-'(x2.a+(x1-'y2).a))+((y2-'x1).a+y1.a) by PRE_POLY:def 6
.= (k.a-'(x2+(x1-'y2)).a)+((y2-'x1).a+y1.a) by PRE_POLY:def 5
.= (k.a-'(x2+(x1-'y2)).a)+((y2-'x1)+y1).a by PRE_POLY:def 5
.= (k-'(x2+(x1-'y2))).a+((y2-'x1)+y1).a by PRE_POLY:def 6;
hence thesis by A3,A4,PRE_POLY:def 5;
end;
registration
let R be asymmetric transitive non empty RelStr;
cluster DershowitzMannaOrder R -> asymmetric transitive;
coherence
proof set DM = DershowitzMannaOrder R;
thus DM is asymmetric
proof
let a,b; assume a in the carrier of DM & b in the carrier of DM;
then reconsider m = a, n = b as Element of DM;
assume [a,b] in the InternalRel of DM & [b,a] in the InternalRel of DM;
then
A0: m <= n & n <= m by ORDERS_2:def 5;
then m <> n & (for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b) &
for a being Element of R st n.a > m.a
ex b being Element of R st a <= b & n.b < m.b by HO;
then consider c being object such that
A2: c in the carrier of R & m.c <> n.c by PBOOLE:def 10;
reconsider c as Element of R by A2;
set X = {d where d is Element of R: c <= d & m.d > n.d};
BC: X c= support m
proof
let a; assume a in X;
then consider d being Element of R such that
A3: a = d & c <= d & m.d > n.d;
thus thesis by A3,PRE_POLY:def 7;
end;
ex b being Element of R st b in X
proof
per cases by A2,XXREAL_0:1;
suppose m.c < n.c;
then consider d being Element of R such that
A5: c <= d & n.d < m.d by A0,HO;
take d; thus d in X by A5;
end;
suppose m.c > n.c;
then consider d being Element of R such that
A5: c <= d & n.d > m.d by A0,HO;
consider e being Element of R such that
A6: d <= e & n.e < m.e by A0,HO,A5;
take e; c <= e by A5,A6,ORDERS_2:3;
hence e in X by A6;
end;
end;
then consider d being Element of R such that
A7: d is_maximal_in X by BC,Th12;
d in X & not ex a being Element of R st a in X & d < a
by A7,WAYBEL_4:55;
then consider e being Element of R such that
A8: d = e & c <= e & n.e < m.e;
consider f being Element of R such that
A9: e <= f & n.f > m.f by A0,HO,A8;
consider g being Element of R such that
A10: f <= g & n.g < m.g by A0,HO,A9;
c <= f by A8,A9,ORDERS_2:3;
then c <= g & d <= g by A8,A9,A10,ORDERS_2:3;
then g in X & d < g by A10,Lem2;
hence contradiction by A7,WAYBEL_4:55;
end;
thus DM is transitive
proof
let a,b,c be object;
assume a in the carrier of DM & b in the carrier of DM &
c in the carrier of DM;
then reconsider m=a, n=b, k=c as Element of DM;
assume [a,b] in the InternalRel of DM & [b,c] in the InternalRel of DM;
then
A0: m <= n & n <= k by ORDERS_2:def 5;
consider x1,y1 being Element of DM such that
A2: 1.DM <> x1 divides n & m = (n -' x1) + y1 &
for b being Element of R st y1.b > 0
ex a being Element of R st x1.a > 0 & b <= a by A0,DM;
consider x2,y2 being Element of DM such that
A3: 1.DM <> x2 divides k & n = (k -' x2) + y2 &
for b being Element of R st y2.b > 0
ex a being Element of R st x2.a > 0 & b <= a by A0,DM;
reconsider x = x2+(x1-'y2), y = (y2-'x1)+y1 as
multiset of the carrier of R by Th1;
reconsider x, y as Element of DM by Th2;
A4: m = (((k-'x2)+y2)-'x1)+y1 = (k -' x) + y by A2,A3,Th15;
A5: 1.DM <> x
proof
consider a such that
A7: a in the carrier of R & (1.DM).a <> x2.a by A3,PBOOLE:def 10;
reconsider a as Element of R by A7;
1.DM = 1.finite-MultiSet_over the carrier of R =
EmptyBag the carrier of R by Th3,Th11;
then
A8: (1.DM).a = 0 by FUNCOP_1:7;
take a;
0 < x2.a <= x2.a+(x1-'y2).a by A7,A8,NAT_1:11;
hence thesis by A8,PRE_POLY:def 5;
end;
A6: x divides k by A2,A3,Th15;
for b being Element of R st y.b > 0
ex a being Element of R st x.a > 0 & b <= a
proof
let b be Element of R;
assume y.b > 0;
then (y2-'x1).b+y1.b > 0 by PRE_POLY:def 5;
then per cases;
suppose (y2-'x1).b > 0;
then y2.b-'x1.b > 0 by PRE_POLY:def 6;
then y2.b-x1.b > 0 by XREAL_0:def 2;
then y2.b > x1.b >= 0 by XREAL_1:47;
then consider a being Element of R such that
B4: x2.a > 0 & b <= a by A3;
take a;
x.a = x2.a+(x1-'y2).a >= x2.a by NAT_1:11,PRE_POLY:def 5;
hence thesis by B4;
end;
suppose y1.b > 0;
then consider a being Element of R such that
B1: x1.a > 0 & b <= a by A2;
per cases;
suppose B2: (x1-'y2).a > 0;
take a;
(x2+(x1-'y2)).a = x2.a+(x1-'y2).a by PRE_POLY:def 5;
hence x.a > 0 by B2;
thus b <= a by B1;
end;
suppose (x1-'y2).a = 0;
then x1.a-'y2.a = 0 by PRE_POLY:def 6;
then x1.a <= y2.a by NAT_D:36;
then consider c being Element of R such that
B3: x2.c > 0 & a <= c by A3,B1;
take c;
x.c = x2.c+(x1-'y2).c by PRE_POLY:def 5;
hence thesis by B1,B3,ORDERS_2:3;
end;
end;
end;
then m <= k by A4,A5,A6,DM;
hence thesis by ORDERS_2:def 5;
end;
end;
end;
definition
let I;
func DivOrder I -> Relation of Bags I means :DO:
for b1,b2 being bag of I holds [b1,b2] in it iff b1 <> b2 & b1 divides b2;
existence
proof
defpred R[bag of I, bag of I] means $1 <> $2 & $1 divides $2;
consider R being Relation of Bags I such that
A1: for b1,b2 being Element of Bags I holds [b1,b2] in R iff R[b1,b2]
from RELSET_1:sch 2;
take R;
let b1,b2 be bag of I;
b1 in Bags I & b2 in Bags I by PRE_POLY:def 12;
hence thesis by A1;
end;
uniqueness
proof
let R1,R2 be Relation of Bags I such that
A1: for b1,b2 being bag of I holds [b1,b2] in R1 iff b1 <> b2 & b1 divides b2
and
A2: for b1,b2 being bag of I holds [b1,b2] in R2 iff b1 <> b2 & b1 divides b2;
let b1,b2 be Element of Bags I;
[b1,b2] in R1 iff b1 <> b2 & b1 divides b2 by A1;
hence thesis by A2;
end;
end;
theorem Lem7:
for a,b,c being bag of I st a divides b divides c holds a divides c
proof
let a,b,c be bag of I; assume that
A1: for x being object holds a.x <= b.x and
A2: for x being object holds b.x <= c.x;
let x be object;
a.x <= b.x <= c.x by A1,A2;
hence thesis by XXREAL_0:2;
end;
registration
let I;
cluster DivOrder I -> asymmetric transitive;
coherence
proof set R = DivOrder I;
now let x, y be object; assume
A1: [x,y] in R;
then reconsider a = x, b = y as Element of Bags I by ZFMISC_1:87;
A2: a <> b & a divides b by DO,A1;
then consider o being object such that
A3: o in I & a.o <> b.o by PBOOLE:def 10;
a.o <= b.o by A2,PRE_POLY:def 11;
then a.o < b.o by A3,XXREAL_0:1;
then not b divides a by PRE_POLY:def 11;
hence not [y,x] in R by DO;
end;
hence R is asymmetric by PREFER_1:22;
let a,b,c be object;
assume a in field R & b in field R & c in field R;
assume
A4: [a,b] in R & [b,c] in R;
then reconsider a,b,c as Element of Bags I by ZFMISC_1:87;
A5: a <> b & a divides b & b divides c by A4,DO;
then consider x being object such that
A6: x in I & a.x <> b.x by PBOOLE:def 10;
a.x <= b.x by A5,PRE_POLY:def 11;
then a.x < b.x <= c.x by A5,A6,XXREAL_0:1,PRE_POLY:def 11;
then a <> c & a divides c by A5,Lem7;
hence thesis by DO;
end;
end;
theorem Th16:
for R being asymmetric transitive non empty RelStr holds
DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R
proof
let R be asymmetric transitive non empty RelStr;
set DM = DershowitzMannaOrder R;
let a,b be Element of Bags the carrier of R;
assume
A1: [a,b] in DivOrder the carrier of R;
reconsider a,b as multiset of the carrier of R by Th1;
reconsider a,b as Element of DM by Th2;
A2: a <> b & a divides b by A1,DO;
then for x being Element of R st a.x > b.x
ex y being Element of R st x <= y & a.y < b.y by PRE_POLY:def 11;
then a <= b by A2,HO;
hence thesis by ORDERS_2:def 5;
end;
theorem
for R being asymmetric transitive non empty RelStr
st the InternalRel of R is empty
holds the InternalRel of DershowitzMannaOrder R = DivOrder the carrier of R
proof
let R be asymmetric transitive non empty RelStr;
assume Z0: the InternalRel of R is empty;
let a,b;
hereby
assume
A1: [a,b] in the InternalRel of DershowitzMannaOrder R;
then reconsider m = a, n = b as Element of DershowitzMannaOrder R
by ZFMISC_1:87;
A5: m <= n by A1,ORDERS_2:def 5;
then
A3: m <> n & for a being Element of R st m.a > n.a
ex b being Element of R st a <= b & m.b < n.b by HO;
m divides n
proof
let a;
assume
A4: m.a > n.a;
a in dom m by A4,FUNCT_1:def 2;
then reconsider a as Element of R;
consider b being Element of R such that
A2: a <= b & m.b < n.b by A5,HO,A4;
thus thesis by Z0,A2,ORDERS_2:def 5;
end;
hence [a,b] in DivOrder the carrier of R by A3,DO;
end;
DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R
by Th16;
hence thesis;
end;
theorem
for R1,R2 being asymmetric transitive non empty RelStr
st the carrier of R1 = the carrier of R2 &
the InternalRel of R1 c= the InternalRel of R2
holds the InternalRel of DershowitzMannaOrder R1
c= the InternalRel of DershowitzMannaOrder R2
proof
let R1,R2 be asymmetric transitive non empty RelStr;
assume Z0: the carrier of R1 = the carrier of R2 &
the InternalRel of R1 c= the InternalRel of R2;
let a,b be Element of DershowitzMannaOrder R1;
assume [a,b] in the InternalRel of DershowitzMannaOrder R1;
then
A3: a <= b by ORDERS_2:def 5;
then
A1: a <> b & for x being Element of R1 st a.x > b.x
ex y being Element of R1 st x <= y & a.y < b.y by HO;
reconsider b1 = b, a1 = a as multiset of the carrier of R1 by Th1;
reconsider b1, a1 as Element of DershowitzMannaOrder R2 by Z0,Th2;
now
let x be Element of R2;
reconsider x1 = x as Element of R1 by Z0;
assume a1.x > b1.x;
then consider y being Element of R1 such that
A2: x1 <= y & a.y < b.y by A3,HO;
reconsider y1 = y as Element of R2 by Z0;
take y1;
[x1,y] in the InternalRel of R1 by A2,ORDERS_2:def 5;
hence x <= y1 & a1.y1 < b1.y1 by Z0,A2,ORDERS_2:def 5;
end;
then a1 <= b1 by A1,HO;
hence thesis by ORDERS_2:def 5;
end;
begin
definition
let I;
let f be (Bags I)-valued FinSequence;
func Sum f -> bag of I means :SUM:
ex F being Function of NAT, Bags I st
it = F.len f &
F.0 = EmptyBag I &
for i being Nat
for b being bag of I
st i < len f & b = f.(i + 1)
holds F.(i + 1) = F.i + b;
existence
proof
defpred P[set] means
for F being (Bags I)-valued FinSequence
st len F = $1 ex u being bag of I st
ex f being Function of NAT, Bags I st u = f.(len F) & f.0 = EmptyBag I &
for j being Nat, v being bag of I st j < len F & v = F.(j + 1)
holds f.(j + 1) = f.j + v;
set V = Bags I;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
let F be (Bags I)-valued FinSequence;
A3: rng F c= Bags I by RELAT_1:def 19;
then reconsider F1 = F as FinSequence of V by FINSEQ_1:def 4;
reconsider G = F1 | Seg(n) as FinSequence of V by FINSEQ_1:18;
assume
A4: len F = n + 1;
then dom F = Seg(n + 1) by FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:4;
then F.(n + 1) in rng F by FUNCT_1:def 3;
then reconsider u1 = F.(n + 1) as Element of V by A3;
A5: n < n + 1 by NAT_1:13;
then consider u being bag of I, f being Function of NAT,V such that
u = f.(len G) and
A6: f.0 = EmptyBag I and
A7: for j being Nat, v being bag of I st j < len G & v = G.(j + 1)
holds f.(j + 1) = f.j + v by A2,A4,FINSEQ_1:17;
defpred P[set,set] means
for j being Nat st $1 = j holds (j < n + 1 implies $2 = f.$1) &
(n + 1 <= j implies for u being bag of I st u = F.(n + 1)
holds $2 = f.(len G) + u);
A8: for k being Element of NAT ex v being Element of V st P[k,v]
proof
let k be Element of NAT;
reconsider i = k as Element of NAT;
A9: now
assume
A10: n + 1 <= i;
take v = f.(len G) + u1;
let j be Nat;
assume k = j;
hence j < n + 1 implies v = f.k by A10;
assume n + 1 <= j;
let u2 be bag of I;
assume u2 = F.(n + 1);
hence v = f.(len G) + u2;
end;
now
assume
A11: i < n + 1;
take v = f.k;
let j be Nat such that
A12: k = j;
thus j < n + 1 implies v = f.k;
thus n + 1 <= j implies for u being bag of I st u = F.(n + 1)
holds v = f.(len G) + u by A11,A12;
end;
then consider v being bag of I such that
B13: P[k,v] by A9;
v in V by PRE_POLY:def 12;
hence thesis by B13;
end;
consider f9 being sequence of Bags I such that
A13: for k being Element of NAT holds P[k,f9.k] from FUNCT_2:sch 3(A8);
A14: for k being Nat holds P[k,f9.k]
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A13;
end;
take z = f9.(n + 1);
take f99 = f9;
thus z = f99.(len F) by A4;
thus f99.0 = EmptyBag I by A6,A14;
let j be Nat, v be bag of I;
assume that
A15: j < len F and
A16: v = F.(j + 1);
A17: len G = n by A4,A5,FINSEQ_1:17;
A18: now
assume
A19: j = n;
then f99.(j + 1) = f.j + v by A17,A14,A16;
hence f99.(j + 1) = f99.j + v by A5,A14,A19;
end;
A20: now
assume
A21: j < n;
then
A22: j + 1 < n + 1 by XREAL_1:6;
1 <= 1 + j & j + 1 <= n by A21,NAT_1:11,13;
then j + 1 in Seg n;
then
A23: v = G.(j + 1) by A16,FUNCT_1:49;
j < len G by A4,A5,A21,FINSEQ_1:17;
then
A24: f.(j + 1) = f.j + v by A7,A23;
j < n + 1 by A21,NAT_1:13;
then f.(j + 1) = f9.j + v by A14,A24;
hence f99.(j + 1) = f99.j + v by A14,A22;
end;
j <= n by A4,A15,NAT_1:13;
hence f99.(j + 1) = f99.j + v by A20,A18,XXREAL_0:1;
end;
A25: P[0]
proof
reconsider f = NAT --> EmptyBag I as sequence of Bags I;
let F be (Bags I)-valued FinSequence;
assume
A26: len F = 0;
take u = f.(len F);
take f9 = f;
thus u = f9.(len F) & f9.0 = EmptyBag I by FUNCOP_1:7;
let j be Nat;
let v be bag of I;
thus j < len F & v = F.(j + 1)
implies f9.(j + 1) = f9.j + v by A26;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A25,A1);
hence thesis;
end;
uniqueness
proof
let v1,v2 be bag of I;
given F being Function of NAT, Bags I such that
A27: v1 = F.(len f) and
A28: F.0 = EmptyBag I and
A29: for j being Nat, v being bag of I st j < len f & v = f.(j + 1)
holds F.(j + 1) = F.j + v;
given f9 being Function of NAT, Bags I such that
A30: v2 = f9.(len f) and
A31: f9.0 = EmptyBag I and
A32: for j being Nat, v being bag of I st j < len f & v = f.(j + 1)
holds f9.(j + 1) = f9.j + v;
defpred P[Nat] means $1 <= len f implies F.$1 = f9.$1;
now
A33: rng f c= Bags I by RELAT_1:def 19;
let k be Nat;
assume
A34: P[k];
assume
A35: k + 1 <= len f;
1 <= k + 1 & dom f = Seg(len f) by FINSEQ_1:def 3,NAT_1:11;
then k + 1 in dom f by A35;
then f.(k + 1) in rng f by FUNCT_1:def 3;
then reconsider u1 = f.(k + 1) as Element of Bags I by A33;
F.(k + 1) = F.k + u1 by A29,A35,NAT_1:13;
hence F.(k + 1) = f9.(k + 1) by A32,A34,A35,NAT_1:13;
end;
then
A37: for k being Nat st P[k] holds P[k+1];
A38: P[0] by A28,A31;
for k being Nat holds P[k] from NAT_1:sch 2(A38,A37);
hence thesis by A27,A30;
end;
end;
theorem Th21:
Sum (<*>Bags I) = EmptyBag I
proof set f = <*>Bags I;
consider F being Function of NAT, Bags I such that
A1: Sum f = F.len f and
A2: F.0 = EmptyBag I and
for i being Nat
for b being bag of I
st i < len f & b = f.(i + 1)
holds F.(i + 1) = F.i + b by SUM;
thus thesis by A1,A2;
end;
registration
let I;
let b be bag of I;
cluster <*b*> -> Bags I-valued for FinSequence;
coherence
proof
rng <*b*> = {b} & b in Bags I by PRE_POLY:def 12,FINSEQ_1:39;
hence thesis by RELAT_1:def 19,ZFMISC_1:31;
end;
end;
theorem Th22:
for p being Bags I-valued FinSequence, b being bag of I holds
Sum (p^<*b*>) = Sum p + b
proof
let p be Bags I-valued FinSequence;
let b be bag of I;
set f = p^<*b*>;
consider F being Function of NAT, Bags I such that
A1: Sum f = F.len f and
A2: F.0 = EmptyBag I and
A3: for i being Nat
for b being bag of I
st i < len f & b = f.(i + 1)
holds F.(i + 1) = F.i + b by SUM;
consider F1 being Function of NAT, Bags I such that
A4: Sum p = F1.len p and
A5: F1.0 = EmptyBag I and
A6: for i being Nat
for b being bag of I
st i < len p & b = p.(i + 1)
holds F1.(i + 1) = F1.i + b by SUM;
defpred P[Nat] means $1 <= len p implies F.$1 = F1.$1;
A7: P[0] by A2,A5;
A8: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A9: P[i] & i+1 <= len p;
then
i < len p < len p+1 = len f by FINSEQ_2:16,NAT_1:13;
then
A11: i < len f by XXREAL_0:2;
A12: i+1 in dom p by A9,NAT_1:11,FINSEQ_3:25;
then reconsider b = p.(i+1) as Element of Bags I by FUNCT_1:102;
f.(i+1) = b by A12,FINSEQ_1:def 7;
hence F.(i+1) = F.i + b by A3,A11
.= F1.i + b by A9,NAT_1:13
.= F1.(i+1) by A6,A9,NAT_1:13;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A7,A8);
then Sum p = F.len p & len p < len p+1 = len f & f.(len p+1) = b
by A4,NAT_1:13,FINSEQ_2:16,FINSEQ_1:42;
hence Sum (p^<*b*>) = Sum p + b by A1,A3;
end;
reserve b for bag of I;
theorem Th23:
Sum <*b*> = b
proof
thus Sum <*b*> = Sum ((<*>Bags I)^<*b*>) by FINSEQ_1:34
.= Sum <*>Bags I + b by Th22
.= EmptyBag I + b by Th21
.= b by PRE_POLY:53;
end;
theorem Th24:
for p,q being Bags I-valued FinSequence holds
Sum (p^q) = Sum p + Sum q
proof
let p,q be Bags I-valued FinSequence;
set f = p^q;
consider F being Function of NAT, Bags I such that
A1: Sum f = F.len f and
A2: F.0 = EmptyBag I and
A3: for i being Nat
for b being bag of I
st i < len f & b = f.(i + 1)
holds F.(i + 1) = F.i + b by SUM;
consider F1 being Function of NAT, Bags I such that
A4: Sum p = F1.len p and
A5: F1.0 = EmptyBag I and
A6: for i being Nat
for b being bag of I
st i < len p & b = p.(i + 1)
holds F1.(i + 1) = F1.i + b by SUM;
consider F2 being Function of NAT, Bags I such that
B1: Sum q = F2.len q and
B2: F2.0 = EmptyBag I and
B3: for i being Nat
for b being bag of I
st i < len q & b = q.(i + 1)
holds F2.(i + 1) = F2.i + b by SUM;
defpred P[Nat] means $1 <= len p implies F.$1 = F1.$1;
A7: P[0] by A2,A5;
A8: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A9: P[i] & i+1 <= len p;
then
i < len p <= len p+len q = len f by FINSEQ_1:22,NAT_1:11,13;
then
A11: i < len f by XXREAL_0:2;
A12: i+1 in dom p by A9,NAT_1:11,FINSEQ_3:25;
then reconsider b = p.(i+1) as Element of Bags I by FUNCT_1:102;
f.(i+1) = b by A12,FINSEQ_1:def 7;
hence F.(i+1) = F.i + b by A3,A11
.= F1.i + b by A9,NAT_1:13
.= F1.(i+1) by A6,A9,NAT_1:13;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A7,A8);
then
A13:Sum p = F.len p by A4;
defpred Q[Nat] means $1 <= len q implies F.(len p+$1) = Sum p+F2.$1;
A14:Q[0] by A13,B2,PRE_POLY:53;
A15:for i being Nat st Q[i] holds Q[i+1]
proof
let i be Nat;
assume
A9: Q[i] & i+1 <= len q;
then
A10: i < len q & len p+len q = len f by FINSEQ_1:22,NAT_1:13;
A12: i+1 in dom q by A9,NAT_1:11,FINSEQ_3:25;
then reconsider b = q.(i+1) as Element of Bags I by FUNCT_1:102;
reconsider lp = len p as Nat;
reconsider lpi = (lp)+i as Nat;
f.(len p+(i+1)) = b & len p+(i+1) = len p+i+1 by A12,FINSEQ_1:def 7;
hence F.(len p+(i+1)) = F.(lpi) + b by A3,A10,XREAL_1:6
.= Sum p+F2.i + b by A9,NAT_1:13
.= Sum p+(F2.i + b) by RFUNCT_1:8
.= Sum p+F2.(i+1) by B3,A9,NAT_1:13;
end;
for i being Nat holds Q[i] from NAT_1:sch 2(A14,A15);
then F.(len p+len q) = Sum p+Sum q by B1;
hence Sum (p^q) = Sum p + Sum q by A1,FINSEQ_1:22;
end;
theorem Th25:
for p being Bags I-valued FinSequence holds Sum (<*b*>^p) = b + Sum p
proof
let p be Bags I-valued FinSequence;
thus Sum (<*b*>^p) = Sum <*b*> + Sum p by Th24
.= b + Sum p by Th23;
end;
theorem Th26:
for p being Bags I-valued FinSequence st b in rng p holds b divides Sum p
proof
let p be Bags I-valued FinSequence;
assume b in rng p;
then consider q,r being FinSequence such that
A1: p = q^<*b*>^r by Lem9;
reconsider qb = q^<*b*>, r as Bags I-valued FinSequence by A1,Lem8;
qb = qb;
then reconsider q as Bags I-valued FinSequence by Lem8;
Sum p = Sum(q^<*b*>)+Sum r = Sum q + b + Sum r = Sum r+Sum q+b
by A1,Th22,Th24,RFUNCT_1:8;
hence b divides Sum p by PRE_POLY:50;
end;
theorem Th27:
for p being Bags I-valued FinSequence, i being object st i in support Sum p
ex b st b in rng p & i in support b
proof
defpred P[Nat] means
for p being Bags I-valued FinSequence st len p = $1
for i being object st i in support Sum p
ex b st b in rng p & i in support b;
A1: P[0]
proof
let p be Bags I-valued FinSequence such that
A2: len p = 0;
let i be object;
assume Z0: i in support Sum p;
p = {} = <*>Bags I by A2;
then i in support EmptyBag I by Z0,Th21;
hence thesis;
end;
A3: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat; assume
A4: P[j];
let p be Bags I-valued FinSequence such that
A2: len p = j+1;
consider w being FinSequence, x being set such that
A5: p = w^<*x*> & len w = j by A2,TREES_2:3;
reconsider w, xx = <*x*> as Bags I-valued FinSequence by A5,Lem8;
len xx = 1 by FINSEQ_1:40;
then 1 in dom xx by FINSEQ_3:25;
then x = xx.1 in Bags I by FUNCT_1:102;
then reconsider x as Element of Bags I;
Sum p = Sum w+x by A5,Th22;
then
A6: support Sum p = (support Sum w)\/support x by PRE_POLY:38;
let i be object;
assume i in support Sum p;
then per cases by A6,XBOOLE_0:def 3;
suppose i in support Sum w;
then consider b such that
A7: b in rng w & i in support b by A4,A5;
take b;
rng p = rng w \/ rng xx by A5,FINSEQ_1:31;
hence thesis by A7,XBOOLE_0:def 3;
end;
suppose
A8: i in support x;
take b = x;
rng p = rng w \/ rng xx & x in {x} = rng xx
by A5,FINSEQ_1:31,39,TARSKI:def 1;
hence thesis by A8,XBOOLE_0:def 3;
end;
end;
let p be Bags I-valued FinSequence;
for j being Nat holds P[j] from NAT_1:sch 2(A1,A3);
then P[len p];
hence thesis;
end;
definition
let I,b;
mode partition of b -> Bags I-valued FinSequence means :PART:
b = Sum it;
existence
proof
take <*b*>;
thus thesis by Th23;
end;
end;
definition
let I,b;
redefine func <*b*> -> partition of b; :: redefines <* (FINSEQ_1, definition)
coherence
proof
thus b = Sum <*b*> by Th23;
end;
end;
definition
let R be RelStr;
let M be RelExtension of finite-MultiSet_over the carrier of R;
let b be Element of M;
let p be partition of b;
attr p is co-ordered means
for i being Nat st i in dom p & i+1 in dom p
for b1,b2 being Element of M st b1 = p.i & b2 = p.(i+1) holds b2 <= b1;
end;
definition
let R be non empty RelStr;
let b be bag of the carrier of R;
let p be partition of b;
attr p is ordered means
(for m being bag of the carrier of R st m in rng p
for x being Element of R st m.x > 0 holds m.x = b.x) &
(for m being bag of the carrier of R st m in rng p
for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y
holds x ## y) &
(for m being bag of the carrier of R st m in rng p
holds m <> EmptyBag the carrier of R) &
(for i being Nat st i in dom p & i+1 in dom p
for x being Element of R st (p/.(i+1)).x > 0
ex y being Element of R st (p/.i).y > 0 & x <= y);
end;
reserve R for asymmetric transitive non empty RelStr,
a,b,c for bag of the carrier of R,
x,y,z for Element of R;
theorem
<*a*> is ordered iff a <> EmptyBag the carrier of R &
for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y
proof
hereby
assume Z0: <*a*> is ordered;
a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39;
hence a <> EmptyBag the carrier of R &
for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y by Z0;
end;
assume Z3: a <> EmptyBag the carrier of R;
assume Z4: for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y;
set p = <*a*>;
hereby let m be bag of the carrier of R;
assume m in rng p;
then m in {a} by FINSEQ_1:39;
hence for x being Element of R st m.x > 0 holds m.x = a.x
by TARSKI:def 1;
end;
hereby let m be bag of the carrier of R;
assume m in rng p;
then m in {a} by FINSEQ_1:39;
then m = a by TARSKI:def 1;
hence for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y
holds x ## y by Z4;
end;
hereby let m be bag of the carrier of R;
assume m in rng p;
then m in {a} by FINSEQ_1:39;
hence m <> EmptyBag the carrier of R by Z3,TARSKI:def 1;
end;
let i be Nat;
assume i in dom p & i+1 in dom p;
then 1 <= i < i+1 <= len p = 1 by FINSEQ_1:40,FINSEQ_3:25,NAT_1:13;
hence thesis by XXREAL_0:2;
end;
theorem Th28:
for p being Bags I-valued FinSequence
for a,b being bag of I holds
<*a*>^p is partition of b iff a divides b & p is partition of b-'a
proof
let p be Bags I-valued FinSequence;
let a,b be bag of I;
thus <*a*>^p is partition of b implies a divides b & p is partition of b-'a
proof
assume b = Sum(<*a*>^p);
then A1: b = a+Sum p by Th25;
hence a divides b by PRE_POLY:50;
thus b-'a = Sum p by A1,PRE_POLY:48;
end;
assume Z1: a divides b;
assume b-'a = Sum p;
then Sum p+a = b-'a+a = b by Z1,PRE_POLY:47;
hence b = Sum(<*a*>^p) by Th25;
end;
reserve p for partition of b-'a, q for partition of b;
theorem Th30:
q = <*a*>^p & q is ordered implies p is ordered
proof
assume Z1: q = <*a*>^p;
assume Z2: q is ordered;
hereby let m be bag of the carrier of R;
assume
A0: m in rng p;
then
A1: m in rng<*a*>\/rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31;
let x be Element of R; assume
A2: m.x > 0;
m divides Sum p = b-'a divides b by A0,Th26,PART,Lem3;
then b.x = m.x <= (b-'a).x <= b.x by A1,A2,Z2,PRE_POLY:def 11;
hence m.x = (b-'a).x by XXREAL_0:1;
end;
hereby let m be bag of the carrier of R;
assume m in rng p;
then m in rng<*a*>\/rng p = rng q by Z1,FINSEQ_1:31,XBOOLE_0:def 3;
hence for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y
holds x ## y by Z2;
end;
hereby let m be bag of the carrier of R;
assume m in rng p;
then m in rng<*a*>\/rng p = rng q by Z1,FINSEQ_1:31,XBOOLE_0:def 3;
hence m <> EmptyBag the carrier of R by Z2;
end;
let i be Nat;
assume
A1: i in dom p & i+1 in dom p;
A2: len <*a*> = 1 by FINSEQ_1:40;
then
A3: q.(1+i) = p.i & q.(1+(i+1)) = p.(i+1) by Z1,A1,FINSEQ_1:def 7;
A4: 1+i in dom q & 1+i+1 = 1+(i+1) in dom q by Z1,A1,A2,FINSEQ_1:28;
then
q.(1+i) = q/.(1+i) & p/.i = p.i & q.(1+(i+1)) = q/.(1+i+1) &
p.(i+1) = p/.(i+1) by A1,PARTFUN1:def 6;
hence thesis by Z2,A3,A4;
end;
definition
let I;
let m be bag of I;
let J be set;
func m|J -> bag of I means :BAR:
for i being object st i in I holds (i in J implies it.i = m.i) &
(not i in J implies it.i = 0);
existence
proof
defpred C[object] means $1 in J;
deffunc F(object) = m.$1;
deffunc G(object) = 0;
consider f being Function such that
A1: dom f = I &
for x being object st x in I holds (C[x] implies f.x = F(x)) &
(not C[x] implies f.x = G(x)) from PARTFUN1:sch 1;
rng f c= NAT
proof
let x be object; assume x in rng f;
then consider i being object such that
A2: i in dom f & x = f.i by FUNCT_1:def 3;
x = F(i) or x = G(i) by A1,A2;
hence thesis by ORDINAL1:def 12;
end;
then reconsider f as Function of I,NAT by A1,FUNCT_2:2;
f is finite-support
proof
support f c= support m
proof let x be object;
assume x in support f;
then
A3: f.x <> 0 by PRE_POLY:def 7;
then
x in dom f by FUNCT_1:def 2;
then f.x = m.x by A1,A3;
hence thesis by A3,PRE_POLY:def 7;
end;
hence support f is finite;
end;
then reconsider f as bag of I;
take f; thus thesis by A1;
end;
uniqueness
proof
let b1,b2 be bag of I such that
A1: for i being object st i in I holds (i in J implies b1.i = m.i) &
(not i in J implies b1.i = 0) and
A2: for i being object st i in I holds (i in J implies b2.i = m.i) &
(not i in J implies b2.i = 0);
let i be object; assume
A3: i in I;
per cases;
suppose i in J;
then b1.i = m.i = b2.i by A1,A2,A3;
hence thesis;
end;
suppose not i in J;
then b1.i = 0 = b2.i by A1,A2,A3;
hence thesis;
end;
end;
end;
reserve J for set, m for bag of I;
theorem Th44:
support (m|J) = J /\ support m
proof set f = m|J;
thus support f c= J /\ support m
proof let x be object;
assume x in support f;
then
A3: f.x <> 0 by PRE_POLY:def 7;
then
A4: x in dom f = I by PARTFUN1:def 2,FUNCT_1:def 2;
then
A5: x in J by BAR,A3;
then f.x = m.x by BAR,A4;
then x in support m by A3,PRE_POLY:def 7;
hence thesis by A5,XBOOLE_0:def 4;
end;
let x be object;
assume x in J /\ support m;
then
A1: x in J & x in support m by XBOOLE_0:def 4;
then
A2: m.x <> 0 by PRE_POLY:def 7;
then x in dom m = I by PARTFUN1:def 2,FUNCT_1:def 2;
then f.x = m.x by A1,BAR;
hence thesis by A2,PRE_POLY:def 7;
end;
theorem
(m|J)+(m|(I\J)) = m
proof
let i be object;
assume
A1: i in I;
A3: ((m|J)+(m|(I\J))).i = (m|J).i+(m|(I\J)).i by PRE_POLY:def 5;
per cases;
suppose
A2: i in J;
then not i in I\J by XBOOLE_0:def 5;
then (m|J).i = m.i & (m|(I\J)).i = 0 by A1,A2,BAR;
hence thesis by A3;
end;
suppose
A2: not i in J;
then i in I\J by A1,XBOOLE_0:def 5;
then (m|J).i = 0 & (m|(I\J)).i = m.i by A2,BAR;
hence thesis by A3;
end;
end;
theorem Th43:
m|J divides m
proof
let i be object;
per cases;
suppose
A1: not i in I;
dom (m|J) = I & dom m = I by PARTFUN1:def 2;
hence thesis by A1,FUNCT_1:def 2;
end;
suppose
A2: i in I;
per cases;
suppose i in J;
hence thesis by A2,BAR;
end;
suppose not i in J;
hence thesis by A2,BAR;
end;
end;
end;
theorem
support m c= J implies m|J = m
proof
assume
A1: support m c= J;
let i be object;
assume
A2: i in I;
per cases;
suppose i in J;
hence thesis by A2,BAR;
end;
suppose not i in J;
then (m|J).i = 0 & not i in support m by A1,A2,BAR;
hence thesis by PRE_POLY:def 7;
end;
end;
theorem Th27A:
support(m-'(m|J)) = (support m)\J
proof
thus support(m-'(m|J)) c= (support m)\J
proof let x be object;
assume x in support(m-'(m|J));
then (m-'(m|J)).x <> 0 by PRE_POLY:def 7;
then m.x-'(m|J).x <> 0 by PRE_POLY:def 6;
then m.x-'(m|J).x > 0;
then m.x-(m|J).x > 0 by XREAL_0:def 2;
then m.x > (m|J).x by XREAL_1:47;
then m.x <> (m|J).x & x in dom m = I & m.x > 0
by PARTFUN1:def 2,FUNCT_1:def 2;
then not x in J & x in support m by BAR,PRE_POLY:def 7;
hence x in (support m)\J by XBOOLE_0:def 5;
end;
let x be object;
assume x in (support m)\J;
then
A1: x in (support m) & not x in J by XBOOLE_0:def 5; then
A2: m.x <> 0 by PRE_POLY:def 7;
then x in dom m = I by PARTFUN1:def 2,FUNCT_1:def 2;
then (m|J).x = 0 by A1,BAR;
then (m-'(m|J)).x = m.x-'(m|J).x <> 0 by A2,NAT_D:40,PRE_POLY:def 6;
hence thesis by PRE_POLY:def 7;
end;
theorem Th31:
q is ordered & q = <*a*>^p & a.x > 0 implies a.x = b.x
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
assume Z2: a.x > 0;
a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39;
then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31;
hence thesis by Z0,Z2;
end;
theorem Th32:
q is ordered & q = <*a*>^p & a.x > 0 & a.y > 0 & x <> y implies x ## y
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
assume Z2: a.x > 0 & a.y > 0;
a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39;
then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31;
hence thesis by Z0,Z2;
end;
theorem Th32A:
q is ordered & q = <*a*>^p implies a <> EmptyBag the carrier of R
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
a in {a} = rng <*a*> by TARSKI:def 1,FINSEQ_1:39;
then a in rng <*a*> \/ rng p = rng q by Z1,XBOOLE_0:def 3,FINSEQ_1:31;
hence thesis by Z0;
end;
theorem
for c being bag of the carrier of R,
r being Bags the carrier of R-valued FinSequence
st q is ordered & q = <*a,c*>^r & c.y > 0
ex x st a.x > 0 & y <= x
proof
let c be bag of the carrier of R;
let r be Bags the carrier of R-valued FinSequence;
assume Z0: q is ordered;
assume Z1: q = <*a,c*>^r;
assume Z2: c.y > 0;
len <*a,c*> = 2 by FINSEQ_1:44;
then
A1: 1 in dom <*a,c*> & 2 in dom <*a,c*> & dom <*a,c*> c= dom q
by Z1,FINSEQ_1:26,FINSEQ_3:25;
q/.1 = q.1 = <*a,c*>.1 = a & q/.(1+1) = q.2 = <*a,c*>.2 = c
by Z1,A1,PARTFUN1:def 6,FINSEQ_1:def 7;
hence thesis by Z0,Z2,A1;
end;
theorem
x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I
proof
assume Z0: x in I;
assume Z1: for y st y in I & y <> x holds x ## y;
not ex y st y in I & x < y
proof let y;
assume y in I & x <= y & x <> y;
then x ## y & x <= y by Z1;
hence contradiction;
end;
hence x is_maximal_in I by Z0,WAYBEL_4:55;
end;
theorem Th36:
q is ordered & q = <*a*>^p & c in rng p & c.x > 0 implies
ex y st a.y > 0 & x <= y
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
assume c in rng p;
then consider i being object such that
A1: i in dom p & c = p.i by FUNCT_1:def 3;
reconsider i as Nat by A1;
A2: 1 <= i & p.i = p/.i by A1,FINSEQ_3:25,PARTFUN1:def 6;
defpred P[Nat] means $1 in dom p implies for x st (p/.$1).x > 0
ex y st a.y > 0 & x <= y;
A5: len <*a*> = 1 & dom <*a*> c= dom q by Z1,FINSEQ_1:26,40;
A3: P[1]
proof assume
A4: 1 in dom p;
then
A6: 1+1 in dom q by Z1,A5,FINSEQ_1:28;
B0: 1 in dom <*a*> by A5,FINSEQ_3:25;
then 1 in dom q & q.1 = <*a*>.1 = a by Z1,A5,FINSEQ_1:def 7;
then q/.1 = a & q/.2 = q.2 = p.1 = p/.1
by Z1,A4,A5,A6,FINSEQ_1:def 7,PARTFUN1:def 6;
hence thesis by Z0,A6,A5,B0;
end;
A8: for i being Nat st i >= 1 & P[i] holds P[i+1]
proof let i be Nat; assume
B1: i >= 1 & P[i] & i+1 in dom p;
then i < i+1 <= len p by NAT_1:13,FINSEQ_3:25;
then
BB: i <= len p by XXREAL_0:2;
then
B3: i in dom p by B1,FINSEQ_3:25;
B4: 1+i in dom q & 1+i+1 in dom q by Z1,A5,B1,BB,FINSEQ_3:25,FINSEQ_1:28;
B5: q/.(1+i) = q.(1+i) = p.i = p/.i & q/.(1+i+1) = q.(1+i+1) = p.(i+1)
= p/.(i+1) by Z1,A5,B1,B3,FINSEQ_1:28,def 7,PARTFUN1:def 6;
let x; assume
(p/.(i+1)).x > 0;
then consider y such that
B6: (p/.i).y > 0 & x <= y by Z0,B4,B5;
consider z such that
B7: a.z > 0 & y <= z by BB,B1,FINSEQ_3:25,B6;
take z;
thus a.z > 0 & x <= z by B6,B7,ORDERS_2:3;
end;
for i being Nat st i >= 1 holds P[i] from NAT_1:sch 8(A3,A8);
hence thesis by A1,A2;
end;
theorem Th34:
q is ordered & q = <*a*>^p implies (x is_maximal_in support b iff a.x > 0)
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
rng p c= Bags the carrier of R by RELAT_1:def 19;
then reconsider p as FinSequence of Bags the carrier of R
by FINSEQ_1:def 4;
set I = the carrier of R;
hereby assume x is_maximal_in support b;
then
A7: x in support b & not ex y st y in support b & x < y by WAYBEL_4:55;
then x in support Sum q by PART;
then consider d being bag of the carrier of R such that
A8: d in rng q & x in support d by Th27;
consider i being object such that
A9: i in dom q & d = q.i by A8,FUNCT_1:def 3;
reconsider i as Nat by A9;
1 <= i by A9,FINSEQ_3:25;
then per cases by XXREAL_0:1;
suppose i = 1;
then d = a by Z1,A9,FINSEQ_1:41;
then a.x <> 0 by A8,PRE_POLY:def 7;
hence a.x > 0;
end;
suppose i > 1;
then i >= 1+1 by NAT_1:13;
then consider k being Nat such that
A10: i = 1+1+k by NAT_1:10;
1 <= 1+k <= 1+k+1 = i <= len q by A9,A10,NAT_1:11,FINSEQ_3:25;
then 1 <= 1+k <= len q by XXREAL_0:2;
then
A11: 1+k in dom q by FINSEQ_3:25; then
A12: q/.i = q.i & q/.(1+k) = q.(1+k) by A9,PARTFUN1:def 6;
d.x <> 0 by A8,PRE_POLY:def 7;
then d.x > 0 & i = 1+k+1 by A10;
then consider y such that
A13: (q/.(1+k)).y > 0 & x <= y by Z0,A9,A11,A12;
q.(1+k) in rng q by A11,FUNCT_1:def 3;
then y in support (q/.(1+k)) c= support Sum q = support b
by A13,A12,Th26,PART,BAGORDER:21,PRE_POLY:def 7;
hence a.x > 0 by A7,A13,Lem2;
end;
end;
assume
B0: a.x > 0;
then
B1: x in support a by PRE_POLY:def 7;
a in {a} = rng <*a*> c= rng q by Z1,TARSKI:def 1,FINSEQ_1:39,29;
then
B4: a divides Sum q = b by Th26,PART; then
AA: support a c= support b by BAGORDER:21;
not ex y st y in support b & x < y
proof let y;
assume
B3: y in support b & x <= y & x <> y;
per cases;
suppose a.y > 0;
then x ## y by Z0,Z1,B0,B3,Th32;
hence contradiction by B3;
end;
suppose
B5: a.y = 0;
consider d being bag of the carrier of R such that
B6: d in rng q & y in support d by B4,B3,Th27;
B7: d.y <> 0 by B6,PRE_POLY:def 7;
then not d in {a} & {a} = rng <*a*> & rng q = rng <*a*> \/ rng p
by Z1,B5,TARSKI:def 1,FINSEQ_1:31,39;
then d.y > 0 & d in rng p by B6,B7,XBOOLE_0:def 3;
then consider z such that
B8: a.z > 0 & y <= z by Z0,Z1,Th36;
x <= z & x ## z by Z0,Z1,B0,B3,B8,ORDERS_2:3,Th32;
hence contradiction;
end;
end;
hence x is_maximal_in support b by B1,AA,WAYBEL_4:55;
end;
theorem Th40:
q is ordered & q = <*a*>^p implies a = b|{x:x is_maximal_in support b}
proof
assume Z0: q is ordered;
assume Z1: q = <*a*>^p;
let y; set J = {x:x is_maximal_in support b};
per cases;
suppose
A0: y in J;
then consider x such that
A1: y = x & x is_maximal_in support b;
a.y > 0 by Z0,Z1,A1,Th34;
hence a.y = b.y by Z0,Z1,Th31 .= (b|J).y by A0,BAR;
end;
suppose
A2: not y in J;
then not y is_maximal_in support b;
then a.y <= 0 by Z0,Z1,Th34;
hence a.y = 0 .= (b|J).y by A2,BAR;
end;
end;
theorem Lem10:
for p being Bags I-valued FinSequence st Sum p = EmptyBag I &
for a being bag of I st a in rng p holds a <> EmptyBag I
holds p = {}
proof
let p be Bags I-valued FinSequence;
assume Z0: Sum p = EmptyBag I;
assume Z1: for a being bag of I st a in rng p holds a <> EmptyBag I;
assume p <> {};
then consider a being object such that
A1: a in rng p by XBOOLE_0:7;
rng p c= Bags I by RELAT_1:def 19;
then reconsider a as Element of Bags I by A1;
consider x being object such that
A2: x in I & a.x <> (EmptyBag I).x by A1,Z1,PBOOLE:def 10;
A4: (EmptyBag I).x = 0 by A2,FUNCOP_1:7;
then
A3: a.x > 0 by A2;
thus thesis by A4,A3,Z0,A1,Th26,PRE_POLY:def 11;
end;
theorem Lem11:
for a,b being bag of I st a <> EmptyBag I holds a+b <> EmptyBag I
proof let a,b be bag of I;
given i being object such that
A1: i in I & a.i <> (EmptyBag I).i;
take i; thus i in I by A1;
(EmptyBag I).i = 0 by A1,FUNCOP_1:7;
then a.i+b.i <> (EmptyBag I).i by A1;
hence thesis by PRE_POLY:def 5;
end;
theorem
for p,q being partition of b st p is ordered & q is ordered holds p = q
proof
let p,q be partition of b;
defpred P[Nat] means for b,q st len q = $1 & q is ordered
for p being partition of b st p is ordered holds q = p;
A1: P[0]
proof let b,q; assume
len q = 0 & q is ordered;
then
A3: b = Sum q & Sum <*>Bags the carrier of R = EmptyBag the carrier of R &
q = {} by PART,Th21;
let p be partition of b;
assume
A4: p is ordered;
Sum p = b by PART;
hence q = p by A3,A4,Lem10;
end;
A5: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat; assume
A6: P[i];
let b,q; assume
A7: len q = i+1 & q is ordered;
then q <> {} & q is FinSequence of Bags the carrier of R
by RELAT_1:def 19,FINSEQ_1:def 4;
then consider w being FinSequence of Bags the carrier of R,
n being Element of Bags the carrier of R such that
A8: q = <*n*>^w by FINSEQ_2:130;
reconsider w as partition of b-'n by A8,Th28;
A9: b = Sum q = n+Sum w <> EmptyBag the carrier of R
by A8,A7,Th32A,Th25,Lem11,PART;
let p be partition of b; assume
A10: p is ordered;
Sum p = b & rng p c= Bags the carrier of R by PART,RELAT_1:def 19;
then p <> <*>Bags the carrier of R &
p is FinSequence of Bags the carrier of R by A9,Th21,FINSEQ_1:def 4;
then consider u being FinSequence of Bags the carrier of R,
m being Element of Bags the carrier of R such that
A11: p = <*m*>^u by FINSEQ_2:130;
reconsider u as partition of b-'m by A11,Th28;
u = u & w = w;
then
A12: m = b|{x: x is_maximal_in support b} = n by A10,A11,A7,A8,Th40;
A13: w is ordered & u is ordered by A10,A11,A7,A8,Th30;
len q = len <*n*> + len w = 1+len w by A8,FINSEQ_1:22,40;
hence thesis by A6,A7,A8,A11,A12,A13;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A5);
then P[len p];
hence thesis;
end;
definition
let I;
let a,b be bag of I;
redefine func [a,b] -> Element of [:Bags I,Bags I:]; :: redefines [ (TARSKI, definition)
coherence
proof
a in Bags I & b in Bags I by PRE_POLY:def 12;
hence thesis by ZFMISC_1:87;
end;
end;
theorem Th42:
a <> EmptyBag the carrier of R implies {x:x is_maximal_in support a} <> {}
proof set I = the carrier of R;
given x such that
A1: a.x <> (EmptyBag I).x;
(EmptyBag I).x = 0 by FUNCOP_1:7;
then x in support a by A1,PRE_POLY:def 7;
then consider x such that
A2: x is_maximal_in support a by Th12;
x in {y:y is_maximal_in support a} by A2;
hence thesis;
end;
definition
let R,b;
func OrderedPartition b -> Bags the carrier of R-valued FinSequence means
:OP:
ex F,G being Function of NAT, Bags the carrier of R st F.0 = b &
G.0 = EmptyBag the carrier of R &
(for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
F.(i+1) = (F.i)-'(G.(i+1))) &
ex i being Nat st F.i = EmptyBag the carrier of R & it = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R;
existence
proof
set I = the carrier of R;
deffunc S(bag of I) = {x:x is_maximal_in support $1};
deffunc h(Nat,Element of [:Bags I,Bags I:]) =
[$2`1-'($2`1|S($2`1)),$2`1|S($2`1)];
consider f being Function of NAT,[:Bags I,Bags I:] such that
A1: f.0 = [b,EmptyBag I] & for i being Nat holds f.(i+1) = h(i,f.i)
from NAT_1:sch 12;
defpred P[Nat] means ex i being Nat st card support (f.i)`1 = $1;
defpred Q[Nat] means card support (f.$1)`1 = 0;
A2: ex k being Nat st P[k]
proof
take k = card support (f.0)`1;
take i = 0; thus thesis;
end;
A3: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof
let k be Nat;
assume Z0: k <> 0;
given i being Nat such that
Z1: card support (f.i)`1 = k;
(f.i)`1 <> EmptyBag I by Z0,Z1;
then
B1: S((f.i)`1) <> {} by Th42;
f.(i+1) = h(i,f.i) by A1;
then
B2: support (f.(i+1))`1 = (support (f.i)`1)\S((f.i)`1) by Th27A;
S((f.i)`1) c= support (f.i)`1
proof
let x be object;
assume x in S((f.i)`1);
then ex y st x = y & y is_maximal_in support (f.i)`1;
hence thesis by WAYBEL_4:55;
end;
then reconsider S = S((f.i)`1) as finite Subset of support (f.i)`1;
take n = card support (f.(i+1))`1;
card S <> 0 by B1;
then n = k - card S & card S > 0 by Z1,B2,CARD_2:44;
hence n < k by XREAL_1:44;
thus P[n];
end;
P[0] from NAT_1:sch 7(A2,A3);
then
A4: ex i being Nat st Q[i];
consider i being Nat such that
A5: Q[i] & for n being Nat st Q[n] holds i <= n from NAT_1:sch 5(A4);
Seg i c= NAT = dom pr2 f by FUNCT_2:def 1;
then dom ((pr2 f)|Seg i) = Seg i by RELAT_1:62;
then reconsider p = (pr2 f)|Seg i as
Bags the carrier of R-valued FinSequence by FINSEQ_1:def 2;
take p;
take F = pr1 f;
take G = pr2 f;
thus F.0 = (f.0)`1 by FUNCT_2:def 5 .= b by A1;
thus G.0 = (f.0)`2 by FUNCT_2:def 6 .= EmptyBag I by A1;
hereby let i be Nat;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
A6: G.(i+1) = (f.(i+1))`2 by FUNCT_2:def 6 .= (h(i,f.i))`2 by A1
.= (f.j)`1|S((f.j)`1);
(f.j)`1 = F.i by FUNCT_2:def 5;
hence G.(i+1) = (F.i)|S(F.i) by A6;
thus F.(i+1) = (f.(i+1))`1 by FUNCT_2:def 5 .= (h(i,f.i))`1 by A1
.= (f.j)`1-'(G.(i+1)) by A6 .= (F.i)-'(G.(i+1)) by FUNCT_2:def 5;
end;
take i;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
support (f.i)`1 = {} by A5;
then (f.j)`1 = EmptyBag I by PRE_POLY:81;
hence F.i = EmptyBag I by FUNCT_2:def 5;
thus p = G|Seg i;
let k be Nat;
reconsider j = k as Element of NAT by ORDINAL1:def 12;
assume k < i;
then not Q[k] by A5;
then (f.j)`1 <> EmptyBag I;
hence F.k <> EmptyBag I by FUNCT_2:def 5;
end;
uniqueness
proof
let p1,p2 be Bags the carrier of R-valued FinSequence;
given F1,G1 being Function of NAT, Bags the carrier of R such that
A1: F1.0 = b & G1.0 = EmptyBag the carrier of R &
(for i being Nat holds G1.(i+1) = (F1.i)|{x:x is_maximal_in support (F1.i)}
& F1.(i+1) = (F1.i)-'(G1.(i+1))) &
ex i being Nat st F1.i = EmptyBag the carrier of R & p1 = G1|Seg i &
for j being Nat st j < i holds F1.j <> EmptyBag the carrier of R;
given F2,G2 being Function of NAT, Bags the carrier of R such that
A2: F2.0 = b & G2.0 = EmptyBag the carrier of R &
(for i being Nat holds G2.(i+1) = (F2.i)|{x:x is_maximal_in support (F2.i)}
& F2.(i+1) = (F2.i)-'(G2.(i+1))) &
ex i being Nat st F2.i = EmptyBag the carrier of R & p2 = G2|Seg i &
for j being Nat st j < i holds F2.j <> EmptyBag the carrier of R;
defpred P[Nat] means G1.$1 = G2.$1 & F1.$1 = F2.$1;
A3: P[0] by A1,A2;
A4: for i being Nat st P[i] holds P[i+1]
proof let i be Nat; assume
A5: P[i];
hence G1.(i+1) = (F2.i)|{x:x is_maximal_in support (F2.i)} by A1
.= G2.(i+1) by A2;
hence F1.(i+1) = (F2.i)-'(G2.(i+1)) by A1,A5 .= F2.(i+1) by A2;
end;
A6: for i being Nat holds P[i] from NAT_1:sch 2(A3,A4);
A7: F1 = F2
proof
let i be Element of NAT;
thus F1.i = F2.i by A6;
end;
A8: G1 = G2
proof
let i be Element of NAT;
thus G1.i = G2.i by A6;
end;
consider i1 being Nat such that
A9: F1.i1 = EmptyBag the carrier of R & p1 = G1|Seg i1 &
for j being Nat st j < i1 holds F1.j <> EmptyBag the carrier of R by A1;
consider i2 being Nat such that
AA: F1.i2 = EmptyBag the carrier of R & p2 = G1|Seg i2 &
for j being Nat st j < i2 holds F1.j <> EmptyBag the carrier of R
by A2,A7,A8;
i1 <= i2 <= i1 by A9,AA;
hence p1 = p2 by A9,AA,XXREAL_0:1;
end;
end;
definition
let R,b;
redefine func OrderedPartition b -> partition of b; :: redefines OrderedPartition (BAGORD_2, definition)
coherence
proof set p = OrderedPartition b;
consider F,G being Function of NAT, Bags the carrier of R such that
A1: F.0 = b & G.0 = EmptyBag the carrier of R &
(for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
F.(i+1) = (F.i)-'(G.(i+1))) &
ex i being Nat st F.i = EmptyBag the carrier of R & p = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by OP;
consider i being Nat such that
A2: F.i = EmptyBag the carrier of R & p = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by A1;
defpred P[Nat] means $1 <= i implies b = F.$1 + Sum (p|$1);
set I = the carrier of R;
A3: P[0]
proof
p|0 = <*>Bags I;
then Sum (p|0) = EmptyBag I by Th21;
hence 0 <= i implies b = F.0 + Sum(p|0) by A1,PRE_POLY:53;
end;
dom G = NAT by FUNCT_2:def 1;
then dom p = Seg i & i in NAT by A2,RELAT_1:62,ORDINAL1:def 12;
then
A5: len p = i by FINSEQ_1:def 3;
A4: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat; assume
B1: P[j] & j+1 <= i;
rng p c= Bags I by RELAT_1:def 19;
then reconsider q = p as FinSequence of Bags I by FINSEQ_1:def 4;
B2: q|(j+1) = q|j^<*q/.(j+1)*> by B1,A5,FINSEQ_5:82;
j+1 in dom p by A5,B1,NAT_1:11,FINSEQ_3:25;
then
B4: q/.(j+1) = p.(j+1) = G.(j+1) by A2,PARTFUN1:def 6,FUNCT_1:47;
G.(j+1) = (F.j)|{x:x is_maximal_in support (F.j)} by A1;
then F.(j+1) = F.j-'(G.(j+1)) & G.(j+1) divides F.j by A1,Th43;
then F.(j+1)+G.(j+1) = F.j by PRE_POLY:47;
hence b = F.(j+1)+(G.(j+1)+Sum(p|j)) by B1,NAT_1:13,RFUNCT_1:8
.= F.(j+1)+Sum(p|(j+1)) by B2,B4,Th22;
end;
for j being Nat holds P[j] from NAT_1:sch 2(A3,A4);
then P[len p] & p|len p = p by FINSEQ_1:58;
hence b = Sum p by A2,A5,PRE_POLY:53;
end;
end;
registration
let R,b;
cluster OrderedPartition b -> ordered for partition of b;
coherence
proof
let p be partition of b such that
A0: p = OrderedPartition b;
consider F,G being Function of NAT, Bags the carrier of R such that
A1: F.0 = b & G.0 = EmptyBag the carrier of R &
(for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
F.(i+1) = (F.i)-'(G.(i+1))) &
ex i being Nat st F.i = EmptyBag the carrier of R & p = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by OP,A0;
consider i being Nat such that
A2: F.i = EmptyBag the carrier of R & p = G|Seg i &
for j being Nat st j < i holds F.j <> EmptyBag the carrier of R by A1;
set I = the carrier of R;
dom G = NAT by FUNCT_2:def 1;
then dom p = Seg i & i in NAT by A2,RELAT_1:62,ORDINAL1:def 12;
then
A3: len p = i by FINSEQ_1:def 3;
defpred P[Nat] means for x st F.$1.x > 0 holds F.$1.x = b.x;
A4: P[0] by A1;
A5: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat; assume
A6: P[j];
let x; assume
A7: F.(j+1).x > 0;
set S = {y:y is_maximal_in support (F.j)};
F.(j+1) = F.j-'G.(j+1) & G.(j+1) = F.j|S by A1;
then
A8: F.(j+1).x = F.j.x-'(F.j|S).x by PRE_POLY:def 6;
per cases;
suppose x in S;
then (F.j|S).x = F.j.x by BAR;
hence thesis by A7,A8,XREAL_1:232;
end;
suppose not x in S;
then (F.j|S).x = 0 by BAR;
then F.(j+1).x = F.j.x by A8,NAT_D:40;
hence thesis by A6,A7;
end;
end;
A9: for j being Nat holds P[j] from NAT_1:sch 2(A4,A5);
hereby
let a; assume a in rng p;
then consider j being object such that
B1: j in dom p & a = p.j by FUNCT_1:def 3;
reconsider j as Nat by B1;
consider k being Nat such that
B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10;
set S = {x:x is_maximal_in support (F.k)};
B3: a = G.j = (F.k)|S by A1,B2,B1,FUNCT_1:47;
let x; assume
B4: a.x > 0;
then x in S by B3,BAR;
then a.x = F.k.x by B3,BAR;
hence a.x = b.x by A9,B4;
end;
hereby
let a; assume a in rng p;
then consider j being object such that
B1: j in dom p & a = p.j by FUNCT_1:def 3;
reconsider j as Nat by B1;
consider k being Nat such that
B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10;
B3: a = G.j = (F.k)|{x:x is_maximal_in support (F.k)} by A1,B2,B1,FUNCT_1:47;
{x:x is_maximal_in support (F.k)} c= support (F.k)
proof let z be object;
assume z in {x:x is_maximal_in support (F.k)};
then ex x st z = x & x is_maximal_in support (F.k);
hence thesis by WAYBEL_4:55;
end;
then (support (F.k))/\{x:x is_maximal_in support (F.k)} =
{y:y is_maximal_in support (F.k)} by XBOOLE_1:28;
then
B4: support a = {x:x is_maximal_in support (F.k)} by B3,Th44;
let x,y; assume
B5: a.x > 0 & a.y > 0 & x <> y;
then x in support a by PRE_POLY:def 7;
then consider z such that
B6: x = z & z is_maximal_in support (F.k) by B4;
y in support a by B5,PRE_POLY:def 7;
then consider u being Element of R such that
B7: y = u & u is_maximal_in support (F.k) by B4;
x in support (F.k) & y in support (F.k) by B6,B7,WAYBEL_4:55;
then not x < y & not y < x by B6,B7,WAYBEL_4:55;
hence x ## y by Lem2;
end;
hereby
let a; assume a in rng p;
then consider j being object such that
B1: j in dom p & a = p.j by FUNCT_1:def 3;
reconsider j as Nat by B1;
consider k being Nat such that
B2: j = 1+k by B1,FINSEQ_3:25,NAT_1:10;
B3: a = G.j = (F.k)|{x:x is_maximal_in support (F.k)} by A1,B2,B1,FUNCT_1:47;
k < j <= i by A3,B2,B1,NAT_1:13,FINSEQ_3:25;
then k < i by XXREAL_0:2;
then
B4: {x:x is_maximal_in support (F.k)} <> {} by A2,Th42;
{x:x is_maximal_in support (F.k)} c= support (F.k)
proof let z be object;
assume z in {x:x is_maximal_in support (F.k)};
then ex x st z = x & x is_maximal_in support (F.k);
hence thesis by WAYBEL_4:55;
end;
then (support (F.k))/\{x:x is_maximal_in support (F.k)} =
{y:y is_maximal_in support (F.k)} by XBOOLE_1:28;
then support a = {x:x is_maximal_in support (F.k)} by B3,Th44;
hence a <> EmptyBag the carrier of R by B4;
end;
let j be Nat;
assume
C1: j in dom p & j+1 in dom p;
then consider k being Nat such that
B2: j = 1+k by NAT_1:10,FINSEQ_3:25;
let x; assume
C2: (p/.(j+1)).x > 0;
set S = {y:y is_maximal_in support (F.j)};
set T = {y:y is_maximal_in support (F.k)};
C4: p/.(j+1) = p.(j+1) = G.(j+1) = F.j|S & p/.j = p.j = G.j = F.k|T &
F.j = F.k-'G.j by C1,B2,A1,FUNCT_1:47,PARTFUN1:def 6;
then x in S by C2,BAR;
then consider y such that
C5: x = y & y is_maximal_in support F.j;
C6: x in support F.j c= support F.k by C4,C5,WAYBEL_4:55,PRE_POLY:39;
T c= support F.k
proof
let u being object;
assume u in T;
then ex z st u = z & z is_maximal_in support F.k;
hence thesis by WAYBEL_4:55;
end;
then (support F.k)/\T = T by XBOOLE_1:28;
then
D2: support(p/.j) = T by C4,Th44;
support F.j = (support F.k) \ T by C4,Th27A;
then not x in T by C6,XBOOLE_0:def 5;
then not x is_maximal_in support F.k;
then consider z such that
C7: z in support F.k & x < z by C6,WAYBEL_4:55;
take z;
not z in support F.j & support F.j = (support F.k) \ T
by C4,C5,C7,Th27A,WAYBEL_4:55;
then z in T by C7,XBOOLE_0:def 5;
then (p/.j).z <> 0 by D2,PRE_POLY:def 7;
hence (p/.j).z > 0;
thus x <= z by C7,Lem2;
end;
end;
theorem
b = EmptyBag the carrier of R iff OrderedPartition b = {}
proof
set I = the carrier of R;
set E = EmptyBag I;
set p = OrderedPartition b;
consider F,G being Function of NAT, Bags the carrier of R such that
A1: F.0 = b & G.0 = E &
(for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
F.(i+1) = (F.i)-'(G.(i+1))) &
ex i being Nat st F.i = E & p = G|Seg i &
for j being Nat st j < i holds F.j <> E by OP;
consider i being Nat such that
A2: F.i = E & p = G|Seg i & for j being Nat st j < i holds F.j <> E by A1;
hereby assume b = E;
then i <= 0 by A1,A2;
then i = 0;
hence p = {} by A2;
end;
assume p = {};
then p = <*>Bags I;
then Sum p = E by Th21;
hence thesis by PART;
end;
definition
let R;
func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R
means :PM:
for m,n being Element of it holds m <= n iff m <> n &
for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y;
existence
proof
set I = the carrier of R;
set M = finite-MultiSet_over I;
defpred R[bag of I,bag of I] means $1 <> $2 &
for x st $1.x > 0 holds $1.x < $2.x or ex y st $2.y > 0 & x <= y;
consider N being strict RelExtension of M such that
A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx;
take N; thus thesis by A1;
end;
uniqueness
proof
let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R
such that
A1: for m,n being Element of N1 holds m <= n iff m <> n &
for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y and
A2: for m,n being Element of N2 holds m <= n iff m <> n &
for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y;
for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y
holds m <= n iff x <= y
proof
let m,n be Element of N1;
let k,l be Element of N2;
assume Z0: m = k;
assume Z1: n = l;
m <= n iff m <> n &
for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y by A1;
hence thesis by A2,Z0,Z1;
end;
hence thesis by Th4;
end;
end;
registration
let R;
cluster PrecM R -> asymmetric transitive;
coherence
proof set RR = the InternalRel of PrecM R;
thus
A0: PrecM R is asymmetric
proof
let a,b be object; assume
a in the carrier of PrecM R & b in the carrier of PrecM R;
then reconsider m = a, n = b as Element of PrecM R;
assume [a,b] in RR & [b,a] in RR;
then
A0: m <= n & n <= m by ORDERS_2:def 5;
then m <> n &
(for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y) &
(for x st n.x > 0 holds n.x < m.x or ex y st m.y > 0 & x <= y) by PM;
then consider x such that
A2: m.x <> n.x by PBOOLE:def 21;
set X = {y: m.y > 0 & x <= y};
ex y st m.y > 0 & x <= y
proof per cases by A2,XXREAL_0:1;
suppose
m.x < n.x;
hence ex y st m.y > 0 & x <= y by A0,PM;
end;
suppose
n.x < m.x;
then consider y such that
A5: n.y > 0 & x <= y by A0,PM;
per cases by A0,PM;
suppose n.y <= m.y;
hence ex y st m.y > 0 & x <= y by A5;
end;
suppose ex z st m.z > 0 & y <= z;
hence ex y st m.y > 0 & x <= y by A5,ORDERS_2:3;
end;
end;
end;
then consider y such that
A6: m.y > 0 & x <= y;
A7: y in X by A6;
X c= support m
proof
let z be object;
assume z in X;
then ex y st z = y & m.y > 0 & x <= y;
hence thesis by PRE_POLY:def 7;
end;
then consider y such that
A8: y is_maximal_in X by A7,Th12;
y in X by A8,WAYBEL_4:55;
then consider z such that
A9: y = z & m.z > 0 & x <= z;
per cases by A0,PM,A9;
suppose m.z < n.z;
then consider u being Element of R such that
A10: m.u > 0 & z <= u by A0,PM;
x <= u by A9,A10,ORDERS_2:3;
then u in X & y < u by A9,A10,Lem2;
hence contradiction by A8,WAYBEL_4:55;
end;
suppose ex u being Element of R st n.u > 0 & z <= u;
then consider u being Element of R such that
A11: n.u > 0 & z <= u;
per cases by A0,PM;
suppose n.u <= m.u;
then m.u > 0 & x <= u by A9,A11,ORDERS_2:3;
then u in X & y < u by A9,A11,Lem2;
hence contradiction by A8,WAYBEL_4:55;
end;
suppose ex v being Element of R st m.v > 0 & u <= v;
then consider v being Element of R such that
A12: m.v > 0 & u <= v;
A13: z <= v by A11,A12,ORDERS_2:3;
then x <= v by A9,ORDERS_2:3;
then v in X & y < v by A9,A12,A13,Lem2;
hence contradiction by A8,WAYBEL_4:55;
end;
end;
end;
thus PrecM R is transitive
proof
let a,b,c be object;
assume
a in the carrier of PrecM R & b in the carrier of PrecM R &
c in the carrier of PrecM R;
assume
A4: [a,b] in RR & [b,c] in RR;
then reconsider a,b,c as Element of PrecM R by ZFMISC_1:87;
A6: a <= b <= c by A4,ORDERS_2:def 5;
A5: now let x; assume
a.x > 0;
then per cases by A6,PM;
suppose
A4: a.x < b.x;
then b.x < c.x or ex y st c.y > 0 & x <= y by A6,PM;
hence a.x < c.x or ex y st c.y > 0 & x <= y by A4,XXREAL_0:2;
end;
suppose ex y st b.y > 0 & x <= y;
then consider y such that
B1: b.y > 0 & x <= y;
per cases by A6,PM;
suppose b.y <= c.y;
hence a.x < c.x or ex y st c.y > 0 & x <= y by B1;
end;
suppose ex z st c.z > 0 & y <= z;
then consider z such that
B2: c.z > 0 & y <= z;
thus a.x < c.x or ex y st c.y > 0 & x <= y by B2,B1,ORDERS_2:3;
end;
end;
end;
a <> c by A4,A0,PREFER_1:22;
then a <= c by A5,PM;
hence thesis by ORDERS_2:def 5;
end;
end;
end;
definition
let I;
let R be Relation of I,I;
func LexOrder(I,R) -> Relation of I* means :LO:
for p,q being I-valued FinSequence holds [p,q] in it iff p c< q or
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n;
existence
proof
defpred R[Element of I*, Element of I*] means $1 c< $2 or
ex k being Nat st k in dom $1 & k in dom $2 & [$1.k,$2.k] in R &
for n being Nat st 1 <= n < k holds $1.n = $2.n;
consider R being Relation of I* such that
A1: for b1,b2 being Element of I* holds [b1,b2] in R iff R[b1,b2]
from RELSET_1:sch 2;
take R;
let b1,b2 be I-valued FinSequence;
rng b1 c= I & rng b2 c= I by RELAT_1:def 19;
then b1 is FinSequence of I & b2 is FinSequence of I by FINSEQ_1:def 4;
then b1 in I* & b2 in I* by FINSEQ_1:def 11;
hence thesis by A1;
end;
uniqueness
proof
let R1,R2 be Relation of I* such that
A1: for p,q being I-valued FinSequence holds [p,q] in R1 iff p c< q or
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n and
A2: for p,q being I-valued FinSequence holds [p,q] in R2 iff p c< q or
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n;
let p,q be Element of I*;
[p,q] in R1 iff p c< q or
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n by A1;
hence thesis by A2;
end;
end;
registration
let I;
let R be transitive Relation of I;
cluster LexOrder(I,R) -> transitive;
coherence
proof set Q = LexOrder(I,R);
let a,b,c be object;
assume a in field Q & b in field Q & c in field Q;
assume
A1: [a,b] in Q & [b,c] in Q;
then reconsider a,b,c as Element of I* by ZFMISC_1:87;
per cases by A1,LO;
suppose a c< b & b c< c;
then a c< c by XBOOLE_1:56;
hence thesis by LO;
end;
suppose
A2: a c< b &
ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
then consider k being Nat such that
A3: k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
per cases;
suppose
A4: len a < k;
k <= len c by A3,FINSEQ_3:25;
then
A5: len a < len c by A4,XXREAL_0:2;
for n being Nat st n in dom a holds a.n = c.n
proof
let n be Nat;
assume
A6: n in dom a;
then n <= len a by FINSEQ_3:25;
then 1 <= n < k by A4,A6,XXREAL_0:2,FINSEQ_3:25;
then b.n = c.n by A3;
hence thesis by A2,A6,Lem12;
end;
then a c< c by A5,Lem12;
hence thesis by LO;
end;
suppose
A7: len a >= k;
1 <= k by A3,FINSEQ_3:25;
then
A8: k in dom a by A7,FINSEQ_3:25;
then
A9: [a.k,c.k] in R by A2,A3,Lem12;
for n being Nat st 1 <= n < k holds a.n = c.n
proof
let n be Nat; assume
A10: 1 <= n < k;
then n < len a by A7,XXREAL_0:2;
then n in dom a by A10,FINSEQ_3:25;
then a.n = b.n by A2,Lem12;
hence thesis by A10,A3;
end;
hence thesis by A3,A8,A9,LO;
end;
end;
suppose
A12: b c< c &
ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n;
then consider k being Nat such that
A11: k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n;
dom b c= dom c by A12,XBOOLE_0:def 8,XTUPLE_0:8;
then
A13: k in dom c & [a.k,c.k] in R by A12,A11,Lem12;
for n being Nat st 1 <= n < k holds a.n = c.n
proof
let n be Nat; assume
A14: 1 <= n < k;
k <= len b by A11,FINSEQ_3:25;
then n < len b by A14,XXREAL_0:2;
then b.n = c.n by A12,Lem12,A14,FINSEQ_3:25;
hence thesis by A11,A14;
end;
hence thesis by A11,A13,LO;
end;
suppose
A15: (ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n) &
ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
then consider k1 being Nat such that
A16: k1 in dom a & k1 in dom b & [a.k1,b.k1] in R &
for n being Nat st 1 <= n < k1 holds a.n = b.n;
consider k2 being Nat such that
A17: k2 in dom b & k2 in dom c & [b.k2,c.k2] in R &
for n being Nat st 1 <= n < k2 holds b.n = c.n by A15;
per cases by XXREAL_0:1;
suppose
A18: k1 < k2;
k2 <= len c by A17,FINSEQ_3:25;
then 1 <= k1 < len c by A16,A18,FINSEQ_3:25,XXREAL_0:2;
then
A19: k1 in dom c & [a.k1,c.k1] in R by A16,A17,A18,FINSEQ_3:25;
for n being Nat st 1 <= n < k1 holds a.n = c.n
proof
let n be Nat;
assume 1 <= n < k1;
then a.n = b.n & 1 <= n < k2 by A16,A18,XXREAL_0:2;
hence thesis by A17;
end;
hence thesis by A16,A19,LO;
end;
suppose
A20: k1 = k2;
then
A21: [a.k1,c.k1] in R by A16,A17,RELAT_2:31;
for n being Nat st 1 <= n < k1 holds a.n = c.n
proof
let n be Nat;
assume 1 <= n < k1;
then a.n = b.n & b.n = c.n by A16,A17,A20;
hence thesis;
end;
hence thesis by A20,A16,A17,A21,LO;
end;
suppose
A22: k1 > k2;
k1 <= len a by A16,FINSEQ_3:25;
then 1 <= k2 < len a by A17,A22,FINSEQ_3:25,XXREAL_0:2;
then
A19: k2 in dom a & [a.k2,c.k2] in R by A16,A17,A22,FINSEQ_3:25;
for n being Nat st 1 <= n < k2 holds a.n = c.n
proof
let n be Nat;
assume 1 <= n < k2;
then c.n = b.n & 1 <= n < k1 by A17,A22,XXREAL_0:2;
hence thesis by A16;
end;
hence thesis by A17,A19,LO;
end;
end;
end;
end;
registration
let I;
let R be asymmetric Relation of I;
cluster LexOrder(I,R) -> asymmetric;
coherence
proof set Q = LexOrder(I,R);
let a,b be object;
assume a in field Q & b in field Q;
assume
A1: [a,b] in Q & [b,a] in Q;
then reconsider a,b as Element of I* by ZFMISC_1:87;
set c = a;
per cases by A1,LO;
suppose a c< b & b c< c;
hence thesis;
end;
suppose
A2: a c< b &
ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
then consider k being Nat such that
A3: k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
[a.k,c.k] in R by A2,A3,Lem12;
hence thesis by PREFER_1:22;
end;
suppose
A12: b c< c &
ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n;
then consider k being Nat such that
A11: k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n;
k in dom c & [a.k,c.k] in R by A12,A11,Lem12;
hence thesis by PREFER_1:22;
end;
suppose
A15: (ex k being Nat st k in dom a & k in dom b & [a.k,b.k] in R &
for n being Nat st 1 <= n < k holds a.n = b.n) &
ex k being Nat st k in dom b & k in dom c & [b.k,c.k] in R &
for n being Nat st 1 <= n < k holds b.n = c.n;
then consider k1 being Nat such that
A16: k1 in dom a & k1 in dom b & [a.k1,b.k1] in R &
for n being Nat st 1 <= n < k1 holds a.n = b.n;
consider k2 being Nat such that
A17: k2 in dom b & k2 in dom c & [b.k2,c.k2] in R &
for n being Nat st 1 <= n < k2 holds b.n = c.n by A15;
per cases by XXREAL_0:1;
suppose
A18: k1 < k2;
k2 <= len c by A17,FINSEQ_3:25;
then 1 <= k1 < len c by A16,A18,FINSEQ_3:25,XXREAL_0:2;
then k1 in dom c & [a.k1,c.k1] in R by A16,A17,A18;
hence thesis by PREFER_1:22;
end;
suppose
k1 = k2;
hence thesis by A16,A17,PREFER_1:22;
end;
suppose
A22: k1 > k2;
k1 <= len a by A16,FINSEQ_3:25;
then 1 <= k2 < len a by A17,A22,FINSEQ_3:25,XXREAL_0:2;
then k2 in dom a & [a.k2,c.k2] in R by A16,A17,A22;
hence thesis by PREFER_1:22;
end;
end;
end;
end;
theorem
for R being asymmetric Relation of I
for p,q,r being I-valued FinSequence holds
[p,q] in LexOrder(I,R) iff [r^p,r^q] in LexOrder(I,R)
proof
let R be asymmetric Relation of I;
let p,q,r be I-valued FinSequence;
hereby
assume [p,q] in LexOrder(I,R);
then per cases by LO;
suppose p c< q;
then r^p c= r^q & r^p <> r^q by FINSEQ_6:13,FINSEQ_1:33,XBOOLE_0:def 8;
then r^p c< r^q by XBOOLE_0:def 8;
hence [r^p,r^q] in LexOrder(I,R) by LO;
end;
suppose
ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n;
then consider k being Nat such that
A1: k in dom p & k in dom q & [p.k,q.k] in R &
for n being Nat st 1 <= n < k holds p.n = q.n;
set i = len r; set j = i+k;
A2: j in dom(r^p) & j in dom(r^q) by A1,FINSEQ_1:28;
A3: (r^p).j = p.k & (r^q).j = q.k by A1,FINSEQ_1:def 7;
for n being Nat st 1 <= n < j holds (r^p).n = (r^q).n
proof let n be Nat;
assume
A4: 1 <= n < j;
per cases by NAT_1:13;
suppose n <= i;
then n in dom r by A4,FINSEQ_3:25;
then (r^p).n = r.n = (r^q).n by FINSEQ_1:def 7;
hence thesis;
end;
suppose i+1 <= n;
then consider m being Nat such that
A5: n = i+1+m by NAT_1:10;
A5A: n = i+(1+m) by A5;
then
A6: 1 <= 1+m < k by A4,NAT_1:11,XREAL_1:6;
k <= len p & k <= len q by A1,FINSEQ_3:25;
then 1 <= 1+m <= len p & 1+m <= len q by A6,XXREAL_0:2;
then 1+m in dom p & 1+m in dom q by FINSEQ_3:25;
then (r^p).n = p.(1+m) & (r^q).n = q.(1+m) by A5A,FINSEQ_1:def 7;
hence thesis by A1,A6;
end;
end;
hence [r^p,r^q] in LexOrder(I,R) by LO,A1,A2,A3;
end;
end;
assume [r^p,r^q] in LexOrder(I,R);
then per cases by LO;
suppose r^p c< r^q;
then p c< q by Lem13;
hence [p,q] in LexOrder(I,R) by LO;
end;
suppose
ex k being Nat st k in dom(r^p) & k in dom(r^q) &
[(r^p).k,(r^q).k] in R &
for n being Nat st 1 <= n < k holds (r^p).n = (r^q).n;
then consider k being Nat such that
A1: k in dom(r^p) & k in dom(r^q) & [(r^p).k,(r^q).k] in R &
for n being Nat st 1 <= n < k holds (r^p).n = (r^q).n;
set i = len r;
A3: 1 <= k by A1,FINSEQ_3:25;
now assume k <= i;
then k in dom r by A3,FINSEQ_3:25;
then (r^p).k = r.k = (r^q).k by FINSEQ_1:def 7;
hence contradiction by A1,PREFER_1:22;
end;
then k >= i+1 by NAT_1:13;
then consider j being Nat such that
A4: k = i+1+j by NAT_1:10;
A5: k = i+(1+j) by A4;
k <= len(r^p) = i+len p & k <= len(r^q) = i+len q
by A1,FINSEQ_3:25,FINSEQ_1:22;
then
A9: 1 <= 1+j <= len p & 1+j <= len q by A5,NAT_1:11,XREAL_1:6;
then
A6: 1+j in dom p & 1+j in dom q by FINSEQ_3:25;
then
A7: (r^p).k = p.(1+j) & (r^q).k = q.(1+j) by A5,FINSEQ_1:def 7;
for n being Nat st 1 <= n < 1+j holds p.n = q.n
proof let n be Nat; assume
A8: 1 <= n < 1+j;
then n < len p & n < len q by A9,XXREAL_0:2;
then n in dom p & n in dom q by A8,FINSEQ_3:25;
then p.n = (r^p).(i+n) & q.n = (r^q).(i+n) & 1 <= i+n < k
by FINSEQ_1:def 7,NAT_1:12,XREAL_1:6,A5,A8;
hence thesis by A1;
end;
hence thesis by LO,A1,A6,A7;
end;
end;
definition
let R;
func PrecPrecM R -> strict RelExtension of
finite-MultiSet_over the carrier of R means :PPM:
for m,n being Element of it holds m <= n iff
[OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R);
existence
proof
set I = the carrier of R;
set M = finite-MultiSet_over I;
defpred R[bag of I,bag of I] means
[OrderedPartition $1, OrderedPartition $2] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R);
consider N being strict RelExtension of M such that
A1: for m,n being Element of N holds m <= n iff R[m,n] from RelEx;
take N; thus thesis by A1;
end;
uniqueness
proof
let N1,N2 be strict RelExtension of finite-MultiSet_over the carrier of R
such that
A1: for m,n being Element of N1 holds m <= n iff
[OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) and
A2: for m,n being Element of N2 holds m <= n iff
[OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R);
for m,n being Element of N1 for x,y being Element of N2 st m = x & n = y
holds m <= n iff x <= y
proof
let m,n be Element of N1;
let k,l be Element of N2;
assume Z0: m = k;
assume Z1: n = l;
m <= n iff [OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by A1;
hence thesis by A2,Z0,Z1;
end;
hence thesis by Th4;
end;
end;
registration
let R;
cluster PrecPrecM R -> asymmetric transitive;
coherence
proof set Q = the InternalRel of PrecPrecM R;
thus PrecPrecM R is asymmetric
proof
let a,b be object;
assume a in the carrier of PrecPrecM R & b in the carrier of PrecPrecM R;
then reconsider m = a, n = b as Element of PrecPrecM R;
assume [a,b] in Q & [b,a] in Q;
then m <= n <= m by ORDERS_2:def 5;
then [OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) &
[OrderedPartition n, OrderedPartition m] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by PPM;
hence thesis by PREFER_1:22;
end;
let a,b,c be object;
assume a in the carrier of PrecPrecM R & b in the carrier of PrecPrecM R &
c in the carrier of PrecPrecM R;
then reconsider m = a, n = b, o = c as Element of PrecPrecM R;
assume [a,b] in Q & [b,c] in Q;
then m <= n <= o by ORDERS_2:def 5;
then [OrderedPartition m, OrderedPartition n] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) &
[OrderedPartition n, OrderedPartition o] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by PPM;
then [OrderedPartition m, OrderedPartition o] in
LexOrder(the carrier of PrecM R, the InternalRel of PrecM R) by RELAT_2:31;
then m <= o by PPM;
hence thesis by ORDERS_2:def 5;
end;
end;
theorem
for a,b being Element of DershowitzMannaOrder R st a <= b
holds b <> EmptyBag the carrier of R
proof set DM = DershowitzMannaOrder R;
set I = the carrier of R;
set E = EmptyBag I;
let a,b be Element of DM;
assume Z0: a <= b;
per cases;
suppose a = E;
hence b <> E by Z0;
end;
suppose
A1: a <> E;
E divides a by PRE_POLY:59;
then [E,a] in DivOrder I c= the InternalRel of DM by A1,DO,Th16;
hence thesis by Z0,ORDERS_2:def 5;
end;
end;
theorem
for a,b,c,d being Element of DershowitzMannaOrder R
for e being bag of the carrier of R st a <= b & e divides a & e divides b
holds c = a-'e & d = b-'e implies c <= d
proof
let a,b,c,d be Element of DershowitzMannaOrder R;
let e be bag of the carrier of R;
assume Z1: a <= b;
assume Z2: e divides a;
assume Z3: e divides b;
assume Z4: c = a-'e;
assume d = b-'e; then
A0: a = c+e & b = d+e & a <> b by Z1,Z2,Z3,Z4,PRE_POLY:47;
for x st c.x > d.x ex y st x <= y & c.y < d.y
proof let x;
assume c.x > d.x;
then a.x = c.x+e.x > d.x+e.x = b.x by A0,PRE_POLY:def 5,XREAL_1:6;
then consider y such that
A2: x <= y & a.y < b.y by Z1,HO;
take y;
a.y = c.y+e.y & b.y = d.y+e.y by A0,PRE_POLY:def 5;
hence thesis by A2,XREAL_1:6;
end;
hence c <= d by A0,HO;
end;
theorem Lem14:
for p being Bags I-valued FinSequence, x being object
st x in I & (Sum p).x > 0
ex i being Nat st i in dom p & (p/.i).x > 0
proof
let p be Bags I-valued FinSequence;
let x be object;
assume Z0: x in I;
assume Z1: (Sum p).x > 0;
defpred P[object] means for p being Bags I-valued FinSequence
st p = $1 & (Sum p).x > 0 ex i being Nat st i in dom p & (p/.i).x > 0;
A1: P[ {} ]
proof
let p be Bags I-valued FinSequence;
assume p = {};
then p = <*>Bags I;
then Sum p = EmptyBag I by Th21;
hence thesis by Z0,FUNCOP_1:7;
end;
A2: for p being FinSequence, a being object st P[p] holds P[p^<*a*>]
proof
let p be FinSequence;
let a be object;
assume Z0: P[p];
let q be Bags I-valued FinSequence;
assume
A3: q = p^<*a*>;
then reconsider p, aa = <*a*> as Bags I-valued FinSequence by Lem8;
len aa = 1 by FINSEQ_1:40;
then 1 in dom aa by FINSEQ_3:25;
then aa.1 in Bags I by FUNCT_1:102;
then reconsider a as Element of Bags I;
assume (Sum q).x > 0;
then (Sum p).x+a.x = ((Sum p)+a).x > 0 by Th22,A3,PRE_POLY:def 5;
then per cases;
suppose
A4: a.x > 0;
take i = len p+1;
len q = len p+1 >= 1 by A3,NAT_1:11,FINSEQ_2:16;
hence i in dom q by FINSEQ_3:25;
then q/.i = q.i by PARTFUN1:def 6;
hence thesis by A4,A3,FINSEQ_1:42;
end;
suppose
(Sum p).x > 0;
then consider i being Nat such that
A5: i in dom p & (p/.i).x > 0 by Z0;
take i;
A6: dom p c= dom q by A3,FINSEQ_1:26;
hence i in dom q by A5;
q/.i = q.i = p.i by A3,A5,A6,FINSEQ_1:def 7,PARTFUN1:def 6;
hence (q/.i).x > 0 by PARTFUN1:def 6,A5;
end;
end;
for p being FinSequence holds P[p] from FINSEQ_1:sch 3(A1,A2);
hence thesis by Z1;
end;
theorem
q is ordered & (q/.1).x = 0 & b.x > 0 implies
ex y st (q/.1).y > 0 & x <= y
proof
assume Z0: q is ordered;
assume Z2: (q/.1).x = 0;
assume Z3: b.x > 0;
defpred P[Nat] means $1 in dom q implies for x st (q/.$1).x > 0
ex y st (q/.1).y > 0 & x <= y;
A1: P[2]
proof
assume
A2: 2 in dom q;
then 2 <= len q by FINSEQ_3:25;
then 1 <= len q by XXREAL_0:2;
then 1 in dom q & 2 = 1+1 by FINSEQ_3:25;
hence thesis by A2,Z0;
end;
A3: for i being Nat st 2 <= i & P[i] holds P[i+1]
proof let i be Nat;
assume
A4: 2 <= i & P[i] & i+1 in dom q;
then i <= i+1 <= len q by NAT_1:11,FINSEQ_3:25;
then
A0: 1 <= i <= len q by A4,XXREAL_0:2;
then
A5: i in dom q by FINSEQ_3:25;
let x; assume (q/.(i+1)).x > 0;
then consider y such that
A6: (q/.i).y > 0 & x <= y by Z0,A4,A5;
consider z such that
A7: (q/.1).z > 0 & y <= z by A4,A0,A6,FINSEQ_3:25;
take z;
thus (q/.1).z > 0 by A7;
thus x <= z by A6,A7,ORDERS_2:3;
end;
A8: for i being Nat st i >= 2 holds P[i] from NAT_1:sch 8(A1,A3);
b = Sum q by PART;
then consider i being Nat such that
A9: i in dom q & (q/.i).x > 0 by Z3,Lem14;
1 <= i & i <> 1 by A9,Z2,FINSEQ_3:25;
then 1 < i by XXREAL_0:1;
then 1+1 <= i by NAT_1:13;
hence thesis by A8,A9;
end;