:: The Class of Series-Parallel Graphs, {II}
:: by Krzysztof Retel
::
:: Received May 29, 2003
:: Copyright (c) 2003-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 NUMBERS, CLASSES2, RELAT_1, ZFMISC_1, ORDERS_2, NECKLACE, CARD_1,
ARYTM_3, SUBSET_1, XBOOLE_0, TARSKI, XXREAL_0, ORDINAL1, FINSET_1,
CLASSES1, STRUCT_0, FUNCT_1, SETFAM_1, NAT_1, CARD_3, NECKLA_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELSET_1, PARTIT_2,
FINSET_1, CARD_1, ORDINAL1, NUMBERS, CLASSES2, SETFAM_1, CLASSES1,
CARD_3, XCMPLX_0, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0,
ORDERS_2, NECKLACE;
constructors NAT_1, CLASSES2, REALSET2, COH_SP, NECKLACE, RELSET_1, PARTIT_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XREAL_0,
CLASSES2, STRUCT_0, ORDERS_2, CARD_1, CLASSES1, NAT_1;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
definitions TARSKI;
equalities TARSKI;
expansions TARSKI;
theorems FUNCT_1, FUNCT_2, ENUMSET1, RELSET_1, ZFMISC_1, XBOOLE_1, TARSKI,
ORDINAL1, PARTFUN1, NECKLACE, CLASSES2, CLASSES1, XBOOLE_0, SETFAM_1,
CARD_5, NAT_1, STRUCT_0, RELAT_1, CARD_2, XREAL_1, XXREAL_0, XTUPLE_0;
schemes TARSKI, XBOOLE_0, NAT_1, XFAMILY;
begin
reserve U for Universe;
theorem Th1:
for X,Y being set st X in U & Y in U for R being Relation of X,Y holds R in U
proof
let X,Y being set;
assume that
A1: X in U and
A2: Y in U;
[:X,Y:] in U by A1,A2,CLASSES2:61;
hence thesis by CLASSES1:def 1;
end;
theorem Th2:
the InternalRel of Necklace 4 = {[0,1],[1,0],[1,2],[2,1],[2,3],[3 ,2]}
proof
set A = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}, B = the InternalRel of
Necklace 4;
A1: [0+1,0] in {[i+1,i] where i is Element of NAT:i+1 < 4};
A2: B = {[i,i+1] where i is Element of NAT:i+1 < 4} \/ {[i+1,i] where i is
Element of NAT:i+1 < 4} by NECKLACE:18;
A3: B c= A
proof
let x be object;
assume
A4: x in B;
then consider y,z being object such that
A5: x = [y,z] by RELAT_1:def 1;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
x in {[i,i+1] where i is Element of NAT: i+1<4};
then consider i be Element of NAT such that
A6: [y,z] = [i,i+1] and
A7: i+1 < 4 by A5;
A8: y = i by A6,XTUPLE_0:1;
i + 1 < 1 + 3 by A7;
then i < 2+1 by XREAL_1:7;
then i <= 2 by NAT_1:13;
then y = 0 or ... or y = 2 by A8;
hence thesis by A5,A6,A8,ENUMSET1:def 4;
end;
suppose
x in {[i+1,i] where i is Element of NAT: i+1<4};
then consider i be Element of NAT such that
A9: [y,z] = [i+1,i] and
A10: i+1 < 4 by A5;
A11: z = i by A9,XTUPLE_0:1;
i + 1 < 1 + 3 by A10;
then i < 2+1 by XREAL_1:7;
then i <= 2 by NAT_1:13;
then z = 0 or ... or z = 2 by A11;
hence thesis by A5,A9,A11,ENUMSET1:def 4;
end;
end;
A12: [2+1,1+1] in {[i+1,i] where i is Element of NAT:i+1 < 4};
A13: [1+1,2+1] in {[i,i+1] where i is Element of NAT:i+1 < 4};
A14: [1+1,0+1] in {[i+1,i] where i is Element of NAT:i+1 < 4};
A15: [0+1,1+1] in {[i,i+1] where i is Element of NAT:i+1 < 4};
A16: [0,0+1] in {[i,i+1] where i is Element of NAT:i+1 < 4};
A c= B
proof
let x be object;
assume
A17: x in A;
per cases by A17,ENUMSET1:def 4;
suppose
x = [0,1];
hence thesis by A2,A16,XBOOLE_0:def 3;
end;
suppose
x=[1,0];
hence thesis by A2,A1,XBOOLE_0:def 3;
end;
suppose
x=[1,2];
hence thesis by A2,A15,XBOOLE_0:def 3;
end;
suppose
x=[2,1];
hence thesis by A2,A14,XBOOLE_0:def 3;
end;
suppose
x=[2,3];
hence thesis by A2,A13,XBOOLE_0:def 3;
end;
suppose
x=[3,2];
hence thesis by A2,A12,XBOOLE_0:def 3;
end;
end;
hence thesis by A3,XBOOLE_0:def 10;
end;
registration
let n be Nat;
cluster -> finite for Element of Rank n;
coherence
proof
reconsider m = n as Element of NAT by ORDINAL1:def 12;
let x be Element of Rank n;
per cases;
suppose
Rank n = {};
hence thesis;
end;
suppose
A1: Rank n <> {};
A2: Rank m is finite by CARD_2:67;
x c= Rank n by A1,ORDINAL1:def 2;
hence thesis by A2;
end;
end;
end;
theorem Th3:
for x be set st x in FinSETS holds x is finite
proof
A1: omega is limit_ordinal by ORDINAL1:def 11;
let x be set;
assume x in FinSETS;
then consider n being Ordinal such that
A2: n in omega and
A3: x in Rank n by A1,CLASSES1:31,CLASSES2:64;
reconsider n as Nat by A2;
x is Element of Rank n by A3;
hence thesis;
end;
registration
cluster -> finite for Element of FinSETS;
coherence by Th3;
end;
definition
let G be non empty RelStr;
attr G is N-free means
not G embeds Necklace 4;
end;
registration
cluster strict finite N-free for non empty RelStr;
existence
proof
set X = {0,1}, Y = Necklace 4;
reconsider r = id X as Relation of X by RELSET_1:14;
take R = RelStr(#X,r#);
now
let f being Function of Y,R;
A1: dom f = the carrier of Y by FUNCT_2:def 1
.= {0,1,2,3} by NECKLACE:1,20;
then
A2: 3 in dom f by ENUMSET1:def 2;
then
A3: f.3 in X by PARTFUN1:4;
A4: 2 in dom f by A1,ENUMSET1:def 2;
then f.2 in X by PARTFUN1:4;
then
A5: f.2 = 0 or f.2 = 1 by TARSKI:def 2;
A6: 1 in dom f by A1,ENUMSET1:def 2;
then f.1 in X by PARTFUN1:4;
then
A7: f.1 = 0 or f.1 = 1 by TARSKI:def 2;
assume
A8: f is one-to-one;
then
A9: f.2 <> f.3 by A4,A2,FUNCT_1:def 4;
f.1 <> f.3 by A8,A6,A2,FUNCT_1:def 4;
hence
ex x,y being Element of Y st not ([x,y] in the InternalRel of Y iff
[f.x,f.y] in the InternalRel of R) by A8,A6,A4,A9,A3,A7,A5,FUNCT_1:def 4
,TARSKI:def 2;
end;
then not R embeds Y by NECKLACE:def 1;
hence thesis;
end;
end;
definition
let R,S be RelStr;
func union_of(R,S) -> strict RelStr means
:Def2:
the carrier of it = (the
carrier of R) \/ (the carrier of S) & the InternalRel of it = (the InternalRel
of R) \/ (the InternalRel of S);
existence
proof
set X = (the carrier of R) \/ (the carrier of S);
A1: the carrier of S c= X by XBOOLE_1:7;
the carrier of R c= X by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as
Relation of X by A1,RELSET_1:7;
set D = IR \/ IS;
reconsider D as Relation of X;
take RelStr (# X, D #);
thus thesis;
end;
uniqueness;
end;
definition
let R, S be RelStr;
func sum_of(R,S) -> strict RelStr means
:Def3:
the carrier of it = (the
carrier of R) \/ (the carrier of S) & the InternalRel of it = (the InternalRel
of R) \/ (the InternalRel of S) \/ [:the carrier of R, the carrier of S:] \/ [:
the carrier of S, the carrier of R:];
existence
proof
set X = (the carrier of R) \/ (the carrier of S);
A1: the carrier of S c= X by XBOOLE_1:7;
A2: the carrier of R c= X by XBOOLE_1:7;
then reconsider
IQ = [:the carrier of R, the carrier of S:] as Relation of X by A1,
ZFMISC_1:96;
reconsider IP = [:the carrier of S, the carrier of R:] as Relation of X by
A2,A1,ZFMISC_1:96;
A3: the carrier of S c= X by XBOOLE_1:7;
the carrier of R c= X by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as
Relation of X by A3,RELSET_1:7;
set D = IR \/ IS \/ IQ \/ IP;
take RelStr (# X, D #);
thus thesis;
end;
uniqueness;
end;
definition
func fin_RelStr -> set means
:Def4:
for X being object holds X in it iff ex R being
strict RelStr st X = R & the carrier of R in FinSETS;
existence
proof
defpred P[object,object] means
ex R being strict RelStr st $1 = [the carrier of
R,the InternalRel of R] & $2 = R;
A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z being object;
given R1 being strict RelStr such that
A2: x = [the carrier of R1,the InternalRel of R1] and
A3: y = R1;
given R2 being strict RelStr such that
A4: x = [the carrier of R2,the InternalRel of R2] and
A5: z = R2;
the carrier of R1 = the carrier of R2 by A2,A4,XTUPLE_0:1;
hence thesis by A2,A3,A4,A5,XTUPLE_0:1;
end;
consider X being set such that
A6: for x being object holds x in X
iff ex y being object st y in FinSETS & P[y,x] from TARSKI:sch 1(A1);
take X;
for x being object holds x in X iff ex R being strict RelStr st x = R &
the carrier of R in FinSETS
proof
let x be object;
thus x in X implies ex R being strict RelStr st x = R & the carrier of R
in FinSETS
proof
assume x in X;
then consider y being object such that
A7: y in FinSETS and
A8: ex R being strict RelStr st y = [the carrier of R,the
InternalRel of R] & x = R by A6;
consider R being strict RelStr such that
A9: y = [the carrier of R,the InternalRel of R] and
A10: x = R by A8;
A11: {the carrier of R} in {{the carrier of R, the InternalRel of R},
{the carrier of R}} by TARSKI:def 2;
{{the carrier of R, the InternalRel of R}, {the carrier of R}} c=
FinSETS by A7,A9,ORDINAL1:def 2;
then
A12: {the carrier of R} c= FinSETS by A11,ORDINAL1:def 2;
the carrier of R in {the carrier of R} by TARSKI:def 1;
hence thesis by A10,A12;
end;
given R being strict RelStr such that
A13: x = R and
A14: the carrier of R in FinSETS;
consider R being strict RelStr such that
A15: x = R and
A16: the carrier of R in FinSETS by A13,A14;
the InternalRel of R in FinSETS by A16,Th1;
then [the carrier of R,the InternalRel of R] in FinSETS by A16,
CLASSES2:58;
hence thesis by A6,A15;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means
ex R being strict RelStr st $1 = R & the carrier of R
in FinSETS;
thus for X1,X2 being set
st (for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
registration
cluster fin_RelStr -> non empty;
correctness
proof
RelStr(#{},{}({},{})#) in fin_RelStr
proof
set X = RelStr(#{},{}({},{})#);
the carrier of X in FinSETS by CLASSES1:2,CLASSES2:def 2;
hence thesis by Def4;
end;
hence thesis;
end;
end;
definition
func fin_RelStr_sp -> Subset of fin_RelStr means
:Def5:
(for R be strict
RelStr st the carrier of R is 1-element & the carrier of R in FinSETS
holds R in it) & (for H1,H2 be strict RelStr st (the carrier of H1) misses (the
carrier of H2) & H1 in it & H2 in it holds union_of(H1,H2) in it & sum_of(H1,H2
) in it) & for M be Subset of fin_RelStr st ( (for R be strict RelStr st the
carrier of R is 1-element & the carrier of R in FinSETS holds R in M) &
for H1,H2 be strict RelStr st (the carrier of H1) misses (the carrier of H2) &
H1 in M & H2 in M holds union_of(H1,H2) in M & sum_of(H1,H2) in M ) holds it c=
M;
existence
proof
defpred P[set] means
(for R being strict RelStr st the carrier of R is 1-element
& the carrier of R in FinSETS holds R in $1 ) & (for H1,H2 be
strict RelStr st (the carrier of H1) misses (the carrier of H2) & H1 in $1 & H2
in $1 holds union_of(H1,H2) in $1 & sum_of(H1,H2) in $1);
consider X being set such that
A1: for x being set holds x in X iff x in bool fin_RelStr & P[x] from
XFAMILY:sch 1;
for x being object holds x in X implies x in bool fin_RelStr by A1;
then reconsider X as Subset-Family of fin_RelStr by TARSKI:def 3;
take IT = Intersect X;
A2: P[fin_RelStr]
proof
set A = fin_RelStr;
for H1,H2 be strict RelStr st (the carrier of H1) misses (the
carrier of H2) & H1 in A & H2 in A holds union_of(H1,H2) in A & sum_of(H1,H2)
in A
proof
let H1,H2 be strict RelStr such that
(the carrier of H1) misses (the carrier of H2) and
A3: H1 in A and
A4: H2 in A;
consider S2 being strict RelStr such that
A5: S2 = H2 and
A6: the carrier of S2 in FinSETS by A4,Def4;
reconsider RS9 = sum_of(H1,H2) as strict RelStr;
consider S1 being strict RelStr such that
A7: S1 = H1 and
A8: the carrier of S1 in FinSETS by A3,Def4;
reconsider RS = union_of(S1,S2) as strict RelStr;
A9: (the carrier of H1) \/ (the carrier of H2) in FinSETS by A7,A8,A5,A6,
CLASSES2:60;
then the carrier of RS in FinSETS by A7,A5,Def2;
hence union_of(H1,H2) in A by A7,A5,Def4;
the carrier of RS9 in FinSETS by A9,Def3;
hence thesis by Def4;
end;
hence thesis by Def4;
end;
fin_RelStr in bool fin_RelStr by ZFMISC_1:def 1;
then
A10: X <> {} by A1,A2;
then
A11: IT = meet X by SETFAM_1:def 9;
P[IT] & for X be Subset of fin_RelStr st P[X] holds IT c= X
proof
A12: for H1,H2 be strict RelStr st (the carrier of H1) misses (the
carrier of H2) & H1 in IT & H2 in IT holds union_of(H1,H2) in IT & sum_of(H1,H2
) in IT
proof
let H1,H2 be strict RelStr such that
A13: (the carrier of H1) misses (the carrier of H2) and
A14: H1 in IT and
A15: H2 in IT;
A16: for Y being set holds Y in X implies sum_of(H1,H2) in Y
proof
let Y be set;
assume
A17: Y in X;
then
A18: H2 in Y by A11,A15,SETFAM_1:def 1;
H1 in Y by A11,A14,A17,SETFAM_1:def 1;
hence thesis by A1,A13,A17,A18;
end;
for Y being set holds Y in X implies union_of(H1,H2) in Y
proof
let Y being set;
assume
A19: Y in X;
then
A20: H2 in Y by A11,A15,SETFAM_1:def 1;
H1 in Y by A11,A14,A19,SETFAM_1:def 1;
hence thesis by A1,A13,A19,A20;
end;
hence thesis by A10,A11,A16,SETFAM_1:def 1;
end;
for R being strict RelStr st the carrier of R is 1-element
& the carrier of R in FinSETS holds R in IT
proof
let R being strict RelStr such that
A21: the carrier of R is 1-element and
A22: the carrier of R in FinSETS;
for Y being set holds Y in X implies R in Y by A1,A21,A22;
hence thesis by A10,A11,SETFAM_1:def 1;
end;
hence P[IT] by A12;
let Y be Subset of fin_RelStr such that
A23: P[Y];
IT c= Y
proof
A24: Y in X by A1,A23;
let x be object;
assume x in IT;
hence thesis by A11,A24,SETFAM_1:def 1;
end;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Subset of fin_RelStr;
assume that
A25: for R be strict RelStr st the carrier of R is 1-element &
the carrier of R in FinSETS holds R in X1 and
A26: for H1,H2 be strict RelStr st (the carrier of H1) misses (the
carrier of H2) & H1 in X1 & H2 in X1 holds union_of(H1,H2) in X1 & sum_of(H1,H2
) in X1 and
A27: for M be Subset of fin_RelStr st ( (for R be strict RelStr st the
carrier of R is 1-element & the carrier of R in FinSETS holds R in M) &
for H1,H2 be strict RelStr st (the carrier of H1) misses (the carrier of H2) &
H1 in M & H2 in M holds union_of(H1,H2) in M & sum_of(H1,H2) in M ) holds X1 c=
M and
A28: for R be strict RelStr st the carrier of R is 1-element &
the carrier of R in FinSETS holds R in X2 and
A29: for H1,H2 be strict RelStr st (the carrier of H1) misses (the
carrier of H2) & H1 in X2 & H2 in X2 holds union_of(H1,H2) in X2 & sum_of(H1,H2
) in X2 and
A30: for M be Subset of fin_RelStr st ( (for R be strict RelStr st the
carrier of R is 1-element & the carrier of R in FinSETS holds R in M) &
for H1,H2 be strict RelStr st (the carrier of H1) misses (the carrier of H2) &
H1 in M & H2 in M holds union_of(H1,H2) in M & sum_of(H1,H2) in M ) holds X2 c=
M;
A31: X2 c= X1 by A25,A26,A30;
X1 c= X2 by A27,A28,A29;
hence thesis by A31,XBOOLE_0:def 10;
end;
end;
registration
cluster fin_RelStr_sp -> non empty;
correctness
proof
[:{0},{0}:] c= [:{0},{0}:];
then reconsider R = [:{0},{0}:] as Relation of {0};
RelStr(#{0},R#) in fin_RelStr_sp
proof
set X = RelStr(#{0},R#);
A1: the carrier of X in FinSETS by CLASSES2:56,57;
thus thesis by A1,Def5;
end;
hence thesis;
end;
end;
theorem Th4:
for X being set st X in fin_RelStr_sp holds X is finite strict
non empty RelStr
proof
let X be set;
assume
A1: X in fin_RelStr_sp;
then
A2: ex R being strict RelStr st X = R & the carrier of R in FinSETS by Def4;
then reconsider R=X as strict RelStr;
now
set M = fin_RelStr_sp \ {R}, F = fin_RelStr_sp;
reconsider M as Subset of fin_RelStr;
A3: R in {R} by TARSKI:def 1;
assume
A4: R is empty;
A5: now
let H1,H2 be strict RelStr;
assume that
A6: (the carrier of H1) misses (the carrier of H2) and
A7: H1 in M and
A8: H2 in M;
A9: H2 in F by A8,XBOOLE_0:def 5;
A10: not H1 in {R} by A7,XBOOLE_0:def 5;
the carrier of H1 <> {}
proof
per cases by A10,TARSKI:def 1;
suppose
(the carrier of H1) <> (the carrier of R);
hence thesis by A4;
end;
suppose
A11: (the InternalRel of H1) <> (the InternalRel of R);
set InterH1 = the InternalRel of H1;
InterH1 <> {} by A4,A11;
hence thesis;
end;
end;
then reconsider A = the carrier of H1 as non empty set;
A \/ (the carrier of H2) <> {};
then union_of(H1,H2) <> R by A4,Def2;
then
A12: not union_of(H1,H2) in {R} by TARSKI:def 1;
the carrier of sum_of(H1,H2) = A \/ (the carrier of H2) by Def3;
then
A13: not sum_of(H1,H2) in {R} by A4,TARSKI:def 1;
A14: H1 in F by A7,XBOOLE_0:def 5;
then union_of(H1,H2) in F by A6,A9,Def5;
hence union_of(H1,H2) in M by A12,XBOOLE_0:def 5;
sum_of(H1,H2) in F by A6,A14,A9,Def5;
hence sum_of(H1,H2) in M by A13,XBOOLE_0:def 5;
end;
now
let S be strict RelStr;
assume that
A15: the carrier of S is 1-element and
A16: the carrier of S in FinSETS;
A17: not S in {R} by A4,A15,TARSKI:def 1;
S in F by A15,A16,Def5;
hence S in M by A17,XBOOLE_0:def 5;
end;
then F c= M by A5,Def5;
hence contradiction by A1,A3,XBOOLE_0:def 5;
end;
hence thesis by A2;
end;
theorem
for R being RelStr st R in fin_RelStr_sp holds (the carrier of R) in FinSETS
proof
let R be RelStr;
assume R in fin_RelStr_sp;
then
ex S being strict RelStr st R = S & the carrier of S in FinSETS by Def4;
hence thesis;
end;
theorem Th6:
for X being set st X in fin_RelStr_sp
holds X is strict 1-element RelStr or
ex H1,H2 being strict RelStr st the carrier of H1 misses
the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & (X = union_of(
H1,H2) or X = sum_of(H1,H2) )
proof
deffunc F(set,set) = $2 \/ {x where x is Element of fin_RelStr_sp: ex R1,R2
being strict RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in
$2 & R2 in $2 & (x = union_of(R1,R2) or x = sum_of(R1,R2) )};
set Y = fin_RelStr_sp;
let X be set such that
A1: X in fin_RelStr_sp;
consider f being Function such that
A2: dom f = NAT and
A3: f.0 = {x where x is Element of fin_RelStr_sp: x is trivial RelStr} and
A4: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
A5: Union f c= fin_RelStr_sp
proof
defpred P[Nat] means f.$1 c= fin_RelStr_sp;
let y be object;
assume y in Union f;
then consider x being object such that
A6: x in dom f and
A7: y in f.x by CARD_5:2;
reconsider x as Element of NAT by A2,A6;
A8: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A9: P[k];
A10: {a where a is Element of fin_RelStr_sp: ex R1,R2 being strict
RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f.k & R2 in f.
k & (a = union_of(R1,R2) or a = sum_of(R1,R2))} c= fin_RelStr_sp
proof
let x be object;
set S = {a where a is Element of fin_RelStr_sp: ex R1,R2 being strict
RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f.k & R2 in f.
k & (a = union_of(R1,R2) or a = sum_of(R1,R2))};
assume x in S;
then ex a being Element of fin_RelStr_sp st x = a & ex R1,R2 being
strict RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f .k &
R2 in f.k & (a = union_of(R1,R2) or a = sum_of(R1, R2));
hence thesis;
end;
f.(k+1) = f.k \/ {a where a is Element of fin_RelStr_sp: ex R1,R2
being strict RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f
.k & R2 in f.k & (a = union_of(R1,R2) or a = sum_of(R1,R2))} by A4;
hence thesis by A9,A10,XBOOLE_1:8;
end;
A11: P[0]
proof
let y be object;
assume y in f.0;
then ex a being Element of fin_RelStr_sp st y = a & a is trivial RelStr
by A3;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A11,A8);
then f.x c= fin_RelStr_sp;
hence thesis by A7;
end;
then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A12: for i being Nat holds f.i c= f.(i+1)
proof
let i being Nat;
A13: f.(i+1) = f.i \/ {b where b is Element of fin_RelStr_sp: ex R1,R2
being strict RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f
.i & R2 in f.i & (b = union_of(R1,R2) or b = sum_of(R1,R2))} by A4;
let x be object;
assume x in f.i;
hence thesis by A13,XBOOLE_0:def 3;
end;
A14: for i,j being Element of NAT st i <= j holds f.i c= f.j
proof
let i,j being Element of NAT;
defpred P[Nat] means f.i c= f.(i+$1);
assume i <= j;
then
A15: ex k being Nat st j=i+k by NAT_1:10;
A16: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A17: P[k];
f.(i+k) c= f.(i+k+1) by A12;
hence thesis by A17,XBOOLE_1:1;
end;
A18: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A18,A16);
hence thesis by A15;
end;
A19: for H1,H2 be strict RelStr st (the carrier of H1) misses (the carrier
of H2) & H1 in M & H2 in M holds union_of(H1,H2) in M & sum_of(H1,H2) in M
proof
let H1,H2 be strict RelStr such that
A20: (the carrier of H1) misses (the carrier of H2) and
A21: H1 in M and
A22: H2 in M;
consider x2 being object such that
A23: x2 in dom f and
A24: H2 in f.x2 by A22,CARD_5:2;
consider x1 being object such that
A25: x1 in dom f and
A26: H1 in f.x1 by A21,CARD_5:2;
reconsider x1, x2 as Element of NAT by A2,A25,A23;
set W = {a where a is Element of fin_RelStr_sp: ex R1,R2 being strict
RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f.max(x1,x2) &
R2 in f.max(x1,x2) & (a = union_of(R1,R2) or a = sum_of(R1,R2))};
A27: f.(max(x1,x2)+1) = f.max(x1,x2) \/ W by A4;
A28: f.x1 c= f.max(x1,x2) by A14,XXREAL_0:25;
A29: f.x2 c= f.max(x1,x2) by A14,XXREAL_0:25;
sum_of(H1,H2) in fin_RelStr_sp by A5,A20,A21,A22,Def5;
then sum_of(H1,H2) in W by A20,A26,A24,A28,A29;
then
A30: sum_of(H1,H2) in f.(max(x1,x2)+1) by A27,XBOOLE_0:def 3;
union_of(H1,H2) in fin_RelStr_sp by A5,A20,A21,A22,Def5;
then union_of(H1,H2) in W by A20,A26,A24,A28,A29;
then union_of(H1,H2) in f.(max(x1,x2) + 1) by A27,XBOOLE_0:def 3;
hence thesis by A2,A30,CARD_5:2;
end;
for R be strict RelStr st the carrier of R is 1-element & the
carrier of R in FinSETS holds R in M
proof
A31: f.0 c= M
by A2,CARD_5:2;
let R be strict RelStr such that
A32: the carrier of R is 1-element and
A33: the carrier of R in FinSETS;
A34: R is trivial RelStr by A32;
R is Element of fin_RelStr_sp by A32,A33,Def5;
then R in f.0 by A3,A34;
hence thesis by A31;
end;
then
A35: fin_RelStr_sp c= M by A19,Def5;
then
A36: Union f = fin_RelStr_sp by A5,XBOOLE_0:def 10;
assume
A37: not X is strict 1-element RelStr;
ex H1,H2 being strict RelStr st (the carrier of H1) misses (the carrier
of H2) & H1 in Y & H2 in Y & ( X = union_of(H1,H2) or X = sum_of(H1,H2) )
proof
defpred P[Nat] means X in f.$1 implies ex H1,H2 being strict RelStr st (
the carrier of H1) misses (the carrier of H2) & H1 in Y & H2 in Y & ( X =
union_of(H1,H2) or X = sum_of(H1,H2) );
A38: for k being Nat st P[k] holds P[k+1]
proof
let n be Nat such that
A39: P[n];
set W = {a where a is Element of fin_RelStr_sp: ex R1,R2 being strict
RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f.n & R2 in f.
n & (a = union_of(R1,R2) or a = sum_of(R1,R2))};
assume
A40: X in f.(n+1);
reconsider n as Element of NAT by ORDINAL1:def 12;
A41: f.(n+1) = f.n \/ W by A4;
per cases by A40,A41,XBOOLE_0:def 3;
suppose
X in f.n;
hence thesis by A39;
end;
suppose
X in W;
then ex a being Element of fin_RelStr_sp st a = X & ex R1,R2 being
strict RelStr st (the carrier of R1) misses (the carrier of R2) & R1 in f .n &
R2 in f.n & (a = union_of(R1,R2) or a = sum_of(R1,R2));
then consider R1,R2 being strict RelStr such that
A42: (the carrier of R1) misses (the carrier of R2) and
A43: R1 in f.n and
A44: R2 in f.n and
A45: X = union_of(R1,R2) or X = sum_of(R1,R2);
A46: R2 in Y by A2,A36,A44,CARD_5:2;
R1 in Y by A2,A36,A43,CARD_5:2;
hence thesis by A42,A45,A46;
end;
end;
A47: P[0]
proof
assume X in f.0;
then consider a being Element of fin_RelStr_sp such that
A48: X = a & a is trivial RelStr by A3;
a is strict non empty RelStr by Th4;
then a is non empty trivial strict RelStr by A48;
then reconsider a as non empty trivial strict RelStr;
a is 1-element strict RelStr;
hence thesis by A37,A48;
end;
A49: for n being Nat holds P[n] from NAT_1:sch 2(A47,A38);
ex y being object st y in dom f & X in f.y by A1,A35,CARD_5:2;
hence thesis by A2,A49;
end;
hence thesis;
end;
Lm1: the carrier of Necklace 4 = {0,1,2,3} by NECKLACE:1,20;
theorem
for R being strict non empty RelStr st R in fin_RelStr_sp holds R is N-free
proof
let R be strict non empty RelStr;
set N4 = Necklace 4;
defpred P[Nat] means ex S being strict non empty RelStr st S in
fin_RelStr_sp & card (the carrier of S) = $1 & S embeds N4;
assume
A1: R in fin_RelStr_sp;
then
ex S being strict RelStr st R = S & the carrier of S in FinSETS by Def4;
then reconsider C = the carrier of R as Element of FinSETS;
set k = card C;
A2: for m being Nat st m <> 0 & P[m] ex n being Nat st n < m & P[n]
proof
let m be Nat such that
m <> 0 and
A3: P[m];
consider S being non empty strict RelStr such that
A4: S in fin_RelStr_sp and
A5: card (the carrier of S) = m and
A6: S embeds N4 by A3;
per cases by A4,Th6;
suppose
A7: S is strict 1-element RelStr;
A8: dom the InternalRel of S c= (the carrier of S) by RELAT_1:def 18;
A9: rng the InternalRel of S c= (the carrier of S) by RELAT_1:def 19;
consider f being Function of N4,S such that
f is one-to-one and
A10: for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of S by A6,NECKLACE:def 1;
A11: the carrier of N4 = {0,1,2,3} by NECKLACE:1,20;
then
A12: 0 in the carrier of N4 by ENUMSET1:def 2;
A13: 1 in the carrier of N4 by A11,ENUMSET1:def 2;
0 = 0+1 or 1 = 0+1;
then [0,1] in the InternalRel of N4 by A12,A13,NECKLACE:25;
then
A14: [f.0,f.1] in the InternalRel of S by A10,A12,A13;
then
A15: f.1 in rng (the InternalRel of S) by XTUPLE_0:def 13;
f.0 in dom (the InternalRel of S) by A14,XTUPLE_0:def 12;
then f.0 = f.1 by A7,A15,A8,A9,STRUCT_0:def 10;
then [0,0] in (the InternalRel of N4) by A10,A12,A14;
then
[0,0] = [0,1] or [0,0]=[1,0] or [0,0]=[1,2] or [0,0]=[2,1] or [0,0]
=[2,3] or [0,0]=[3,2] by Th2,ENUMSET1:def 4;
hence thesis by XTUPLE_0:1;
end;
suppose
ex H1,H2 being strict RelStr st the carrier of H1 misses the
carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & (S = union_of(H1,H2
) or S = sum_of(H1,H2));
then consider H1,H2 being strict RelStr such that
A16: the carrier of H1 misses the carrier of H2 and
A17: H1 in fin_RelStr_sp and
A18: H2 in fin_RelStr_sp and
A19: S = union_of(H1,H2) or S = sum_of(H1,H2);
A20: now
A21: not [1,3] in the InternalRel of N4
proof
assume
A22: [1,3] in the InternalRel of N4;
per cases by A22,Th2,ENUMSET1:def 4;
suppose
[1,3] = [0,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[1,3] = [1,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[1,3] = [2,3];
hence contradiction by XTUPLE_0:1;
end;
suppose
[1,3] = [3,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[1,3] = [2,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[1,3] = [1,0];
hence contradiction by XTUPLE_0:1;
end;
end;
A23: not [0,2] in the InternalRel of N4
proof
assume
A24: [0,2] in the InternalRel of N4;
per cases by A24,Th2,ENUMSET1:def 4;
suppose
[0,2] = [0,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,2] = [1,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,2] = [2,3];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,2] = [3,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,2] = [2,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,2] = [1,0];
hence contradiction by XTUPLE_0:1;
end;
end;
A25: the carrier of N4 = {0,1,2,3} by NECKLACE:1,20;
then
A26: 0 in the carrier of N4 by ENUMSET1:def 2;
A27: not [0,3] in the InternalRel of N4
proof
assume
A28: [0,3] in the InternalRel of N4;
per cases by A28,Th2,ENUMSET1:def 4;
suppose
[0,3] = [0,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,3] = [1,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,3] = [2,3];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,3] = [3,2];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,3] = [2,1];
hence contradiction by XTUPLE_0:1;
end;
suppose
[0,3] = [1,0];
hence contradiction by XTUPLE_0:1;
end;
end;
set A = the InternalRel of H1, B = the InternalRel of H2, C = [:the
carrier of H1,the carrier of H2:], D = [:the carrier of H2, the carrier of H1:]
, cH1 = the carrier of H1, cH2 = the carrier of H2, cS = the carrier of S;
A29: dom (the InternalRel of S) c= cS by RELAT_1:def 18;
assume
A30: S = sum_of(H1,H2);
A31: C c= (the InternalRel of S)
proof
let x be object;
assume x in C;
then
A32: x in (A \/ B) \/ C by XBOOLE_0:def 3;
((A \/ B) \/ C) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:7;
then ((A \/ B) \/ C) c= the InternalRel of S by A30,Def3;
hence thesis by A32;
end;
A33: rng (the InternalRel of S) c= cS by RELAT_1:def 19;
A34: 3 in the carrier of N4 by A25,ENUMSET1:def 2;
A35: D c= (the InternalRel of S)
proof
let x be object;
((B \/ C) \/ D) c= A \/ ((B \/ C) \/ D) by XBOOLE_1:7;
then ((B \/ C) \/ D) c= A \/ (B \/ (C \/ D)) by XBOOLE_1:4;
then ((B \/ C) \/ D) c= (A \/ B) \/ (C \/ D) by XBOOLE_1:4;
then ((B \/ C) \/ D) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:4;
then
A36: ((B \/ C) \/ D) c= the InternalRel of S by A30,Def3;
assume x in D;
then x in (B \/ C) \/ D by XBOOLE_0:def 3;
hence thesis by A36;
end;
A37: rng A c= cH1 by RELAT_1:def 19;
A38: 1 in the carrier of N4 by A25,ENUMSET1:def 2;
consider f being Function of N4,S such that
A39: f is one-to-one and
A40: for x,y being Element of N4 holds [x,y] in the InternalRel
of N4 iff [f.x,f.y] in the InternalRel of S by A6,NECKLACE:def 1;
[1,0] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A41: [f.1,f.0] in the InternalRel of S by A40,A26,A38;
A42: 2 in the carrier of N4 by A25,ENUMSET1:def 2;
[3,2] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A43: [f.3,f.2] in the InternalRel of S by A40,A42,A34;
[2,1] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A44: [f.2,f.1] in the InternalRel of S by A40,A38,A42;
A45: rng B c= cH2 by RELAT_1:def 19;
[2,3] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A46: [f.2,f.3] in the InternalRel of S by A40,A42,A34;
then f.3 in rng (the InternalRel of S) by XTUPLE_0:def 13;
then f.3 in cS by A33;
then
A47: f.3 in cH1 \/ cH2 by A30,Def3;
[0,1] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A48: [f.0,f.1] in the InternalRel of S by A40,A26,A38;
then f.0 in dom (the InternalRel of S) by XTUPLE_0:def 12;
then f.0 in cS by A29;
then
A49: f.0 in cH1 \/ cH2 by A30,Def3;
f.1 in rng (the InternalRel of S) by A48,XTUPLE_0:def 13;
then f.1 in cS by A33;
then
A50: f.1 in cH1 \/ cH2 by A30,Def3;
A51: dom A c= cH1 by RELAT_1:def 18;
[1,2] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A52: [f.1,f.2] in the InternalRel of S by A40,A38,A42;
then f.2 in rng (the InternalRel of S) by XTUPLE_0:def 13;
then f.2 in cS by A33;
then
A53: f.2 in cH1 \/ cH2 by A30,Def3;
A54: dom B c= cH2 by RELAT_1:def 18;
per cases by A49,XBOOLE_0:def 3;
suppose
A55: f.0 in cH1;
set x1=[f.0,f.1], x2=[f.1,f.2], x3=[f.2,f.3], x4=[f.1,f.0], x5=[f.2,
f.1], x6=[f.3,f.2];
A56: now
assume x1 in D;
then f.0 in cH2 by ZFMISC_1:87;
hence contradiction by A16,A55,XBOOLE_0:3;
end;
A57: now
assume f.2 in cH2;
then [f.0,f.2] in C by A55,ZFMISC_1:87;
hence contradiction by A40,A26,A42,A23,A31;
end;
A58: now
assume x4 in B;
then f.0 in rng B by XTUPLE_0:def 13;
hence contradiction by A16,A45,A55,XBOOLE_0:3;
end;
A59: now
assume x4 in C;
then f.0 in cH2 by ZFMISC_1:87;
hence contradiction by A16,A55,XBOOLE_0:3;
end;
A60: now
assume x1 in B;
then f.0 in dom B by XTUPLE_0:def 12;
hence contradiction by A16,A54,A55,XBOOLE_0:3;
end;
A61: now
assume f.3 in cH2;
then [f.0,f.3] in C by A55,ZFMISC_1:87;
hence contradiction by A40,A26,A34,A27,A31;
end;
then
A62: f.3 in cH1 by A47,XBOOLE_0:def 3;
A63: now
assume f.1 in cH2;
then [f.1,f.3] in D by A62,ZFMISC_1:87;
hence contradiction by A40,A38,A34,A21,A35;
end;
A64: dom f = the carrier of N4 by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be object;
assume y in rng f;
then consider x being object such that
A65: x in dom f and
A66: y = f.x by FUNCT_1:def 3;
per cases by A64,A65,Lm1,ENUMSET1:def 2;
suppose
x = 0;
hence thesis by A55,A66;
end;
suppose
x = 1;
hence thesis by A50,A63,A66,XBOOLE_0:def 3;
end;
suppose
x = 2;
hence thesis by A53,A57,A66,XBOOLE_0:def 3;
end;
suppose
x = 3;
hence thesis by A47,A61,A66,XBOOLE_0:def 3;
end;
end;
then
A67: f is Function of the carrier of N4,cH1 by FUNCT_2:6;
H1 is finite by A17,Th4;
then reconsider cH1 as finite set;
A68: H1 is strict non empty RelStr by A17,Th4;
A69: now
assume x6 in B;
then f.2 in rng B by XTUPLE_0:def 13;
hence contradiction by A45,A57;
end;
A70: now
assume x3 in B;
then f.2 in dom B by XTUPLE_0:def 12;
hence contradiction by A54,A57;
end;
x4 in (A \/ B \/ C \/ D) by A30,A41,Def3;
then x4 in ((A\/ B) \/ C) or x4 in D by XBOOLE_0:def 3;
then x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 3;
then
A71: [f.1,f.0] in A by A58,A59,A63,XBOOLE_0:def 3,ZFMISC_1:87;
A72: now
assume x2 in B;
then f.1 in dom B by XTUPLE_0:def 12;
hence contradiction by A54,A63;
end;
x2 in (A \/ B \/ C \/ D) by A30,A52,Def3;
then x2 in ((A\/ B) \/ C) or x2 in D by XBOOLE_0:def 3;
then x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 3;
then
A73: [f.1,f.2] in A by A72,A57,A63,XBOOLE_0:def 3,ZFMISC_1:87;
x6 in (A \/ B \/ C \/ D) by A30,A43,Def3;
then x6 in ((A\/ B) \/ C) or x6 in D by XBOOLE_0:def 3;
then x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 3;
then
A74: [f.3,f.2] in A by A69,A57,A61,XBOOLE_0:def 3,ZFMISC_1:87;
x3 in (A \/ B \/ C \/ D) by A30,A46,Def3;
then x3 in ((A\/ B) \/ C) or x3 in D by XBOOLE_0:def 3;
then x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 3;
then
A75: [f.2,f.3] in A by A70,A61,A57,XBOOLE_0:def 3,ZFMISC_1:87;
A76: now
assume x5 in B;
then f.1 in rng B by XTUPLE_0:def 13;
hence contradiction by A45,A63;
end;
H2 is finite by A18,Th4;
then reconsider cH2 as finite set;
cS = cH1 \/ cH2 by A30,Def3;
then reconsider cS as finite set;
A77: H2 is non empty by A18,Th4;
A78: cH1 <> cS
proof
A79: cS = cH1 \/ cH2 by A30,Def3;
assume
A80: cH1 = cS;
consider x being object such that
A81: x in cH2 by A77,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16,XBOOLE_0:def 7;
then not x in cH1 by A81,XBOOLE_0:def 4;
hence contradiction by A80,A79,A81,XBOOLE_0:def 3;
end;
cS = cH1 \/ cH2 by A30,Def3;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A78,XBOOLE_0:def 8;
then
A82: card cH1 < card cS by CARD_2:48;
x5 in (A \/ B \/ C \/ D) by A30,A44,Def3;
then x5 in ((A\/ B) \/ C) or x5 in D by XBOOLE_0:def 3;
then x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 3;
then
A83: [f.2,f.1] in A by A76,A63,A57,XBOOLE_0:def 3,ZFMISC_1:87;
x1 in (A \/ B \/ C \/ D) by A30,A48,Def3;
then x1 in ((A \/ B) \/ C ) or x1 in D by XBOOLE_0:def 3;
then x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 3;
then
A84: [f.0,f.1] in A by A60,A63,A56,XBOOLE_0:def 3,ZFMISC_1:87;
for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of H1
proof
let x,y being Element of N4;
thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the
InternalRel of H1
proof
assume
A85: [x,y] in the InternalRel of N4;
per cases by A85,Th2,ENUMSET1:def 4;
suppose
A86: [x,y] = [0,1];
then x = 0 by XTUPLE_0:1;
hence thesis by A84,A86,XTUPLE_0:1;
end;
suppose
A87: [x,y] = [1,0];
then x = 1 by XTUPLE_0:1;
hence thesis by A71,A87,XTUPLE_0:1;
end;
suppose
A88: [x,y] = [1,2];
then x = 1 by XTUPLE_0:1;
hence thesis by A73,A88,XTUPLE_0:1;
end;
suppose
A89: [x,y] = [2,1];
then x = 2 by XTUPLE_0:1;
hence thesis by A83,A89,XTUPLE_0:1;
end;
suppose
A90: [x,y] = [2,3];
then x = 2 by XTUPLE_0:1;
hence thesis by A75,A90,XTUPLE_0:1;
end;
suppose
A91: [x,y] = [3,2];
then x = 3 by XTUPLE_0:1;
hence thesis by A74,A91,XTUPLE_0:1;
end;
end;
thus [f.x,f.y] in the InternalRel of H1 implies [x,y] in the
InternalRel of N4
proof
[f.x,f.y] in the InternalRel of S implies [x,y] in the
InternalRel of N4 by A40;
then [f.x,f.y] in (((A \/ B) \/ C) \/ D) implies [x,y] in the
InternalRel of N4 by A30,Def3;
then [f.x,f.y] in ((A \/ B) \/ (C\/ D)) implies [x,y] in the
InternalRel of N4 by XBOOLE_1:4;
then
A92: [f.x,f.y] in (A \/ (B\/(C\/D))) implies [x,y] in the
InternalRel of N4 by XBOOLE_1:4;
assume [f.x,f.y] in the InternalRel of H1;
hence thesis by A92,XBOOLE_0:def 3;
end;
end;
then H1 embeds N4 by A39,A67,NECKLACE:def 1;
hence thesis by A5,A17,A68,A82;
end;
suppose
A93: f.0 in the carrier of H2;
set x1=[f.0,f.1], x2=[f.1,f.2], x3=[f.2,f.3], x4=[f.1,f.0], x5=[f.2,
f.1], x6=[f.3,f.2];
A94: now
assume x1 in C;
then f.0 in cH1 by ZFMISC_1:87;
hence contradiction by A16,A93,XBOOLE_0:3;
end;
A95: now
assume x4 in D;
then f.0 in cH1 by ZFMISC_1:87;
hence contradiction by A16,A93,XBOOLE_0:3;
end;
A96: now
assume f.3 in cH1;
then [f.0,f.3] in D by A93,ZFMISC_1:87;
hence contradiction by A40,A26,A34,A27,A35;
end;
then
A97: f.3 in cH2 by A47,XBOOLE_0:def 3;
A98: now
assume f.1 in cH1;
then [f.1,f.3] in C by A97,ZFMISC_1:87;
hence contradiction by A40,A38,A34,A21,A31;
end;
A99: now
assume x4 in A;
then f.1 in dom A by XTUPLE_0:def 12;
hence contradiction by A51,A98;
end;
x4 in (A \/ B \/ C \/ D) by A30,A41,Def3;
then x4 in ((A\/ B) \/ C) or x4 in D by XBOOLE_0:def 3;
then x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 3;
then
A100: [f.1,f.0] in B by A99,A98,A95,XBOOLE_0:def 3,ZFMISC_1:87;
A101: now
assume x5 in A;
then f.1 in rng A by XTUPLE_0:def 13;
hence contradiction by A37,A98;
end;
A102: now
assume f.2 in cH1;
then [f.0,f.2] in D by A93,ZFMISC_1:87;
hence contradiction by A40,A26,A42,A23,A35;
end;
A103: dom f = the carrier of N4 by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be object;
assume y in rng f;
then consider x being object such that
A104: x in dom f and
A105: y = f.x by FUNCT_1:def 3;
per cases by A103,A104,Lm1,ENUMSET1:def 2;
suppose
x = 0;
hence thesis by A93,A105;
end;
suppose
x = 1;
hence thesis by A50,A98,A105,XBOOLE_0:def 3;
end;
suppose
x = 2;
hence thesis by A53,A102,A105,XBOOLE_0:def 3;
end;
suppose
x = 3;
hence thesis by A47,A96,A105,XBOOLE_0:def 3;
end;
end;
then
A106: f is Function of the carrier of N4,cH2 by FUNCT_2:6;
H1 is finite by A17,Th4;
then reconsider cH1 as finite set;
A107: H2 is strict non empty RelStr by A18,Th4;
A108: now
assume x1 in A;
then f.0 in dom A by XTUPLE_0:def 12;
hence contradiction by A16,A51,A93,XBOOLE_0:3;
end;
A109: now
assume x6 in A;
then f.2 in rng A by XTUPLE_0:def 13;
hence contradiction by A37,A102;
end;
A110: now
assume x3 in A;
then f.2 in dom A by XTUPLE_0:def 12;
hence contradiction by A51,A102;
end;
x6 in (A \/ B \/ C \/ D) by A30,A43,Def3;
then x6 in ((A\/ B) \/ C) or x6 in D by XBOOLE_0:def 3;
then x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 3;
then
A111: [f.3,f.2] in B by A109,A96,A102,XBOOLE_0:def 3,ZFMISC_1:87;
A112: now
assume x2 in A;
then f.2 in rng A by XTUPLE_0:def 13;
hence contradiction by A37,A102;
end;
x2 in (A \/ B \/ C \/ D) by A30,A52,Def3;
then x2 in ((A\/ B) \/ C) or x2 in D by XBOOLE_0:def 3;
then x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 3;
then
A113: [f.1,f.2] in B by A112,A98,A102,XBOOLE_0:def 3,ZFMISC_1:87;
x3 in (A \/ B \/ C \/ D) by A30,A46,Def3;
then x3 in ((A\/ B) \/ C) or x3 in D by XBOOLE_0:def 3;
then x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 3;
then
A114: [f.2,f.3] in B by A110,A102,A96,XBOOLE_0:def 3,ZFMISC_1:87;
x5 in (A \/ B \/ C \/ D) by A30,A44,Def3;
then x5 in ((A\/ B) \/ C) or x5 in D by XBOOLE_0:def 3;
then x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 3;
then
A115: [f.2,f.1] in B by A101,A102,A98,XBOOLE_0:def 3,ZFMISC_1:87;
H2 is finite by A18,Th4;
then reconsider cH2 as finite set;
cS = cH1 \/ cH2 by A30,Def3;
then reconsider cS as finite set;
A116: H1 is non empty by A17,Th4;
A117: cH2 <> cS
proof
A118: cS = cH1 \/ cH2 by A30,Def3;
assume
A119: cH2 = cS;
consider x being object such that
A120: x in cH1 by A116,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16,XBOOLE_0:def 7;
then not x in cH2 by A120,XBOOLE_0:def 4;
hence contradiction by A119,A118,A120,XBOOLE_0:def 3;
end;
cS = cH1 \/ cH2 by A30,Def3;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A117,XBOOLE_0:def 8;
then
A121: card cH2 < card cS by CARD_2:48;
x1 in (A \/ B \/ C \/ D) by A30,A48,Def3;
then x1 in ((A \/ B) \/ C ) or x1 in D by XBOOLE_0:def 3;
then x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 3;
then
A122: [f.0,f.1] in B by A108,A94,A98,XBOOLE_0:def 3,ZFMISC_1:87;
for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of H2
proof
let x,y being Element of N4;
thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the
InternalRel of H2
proof
assume
A123: [x,y] in the InternalRel of N4;
per cases by A123,Th2,ENUMSET1:def 4;
suppose
A124: [x,y] = [0,1];
then x = 0 by XTUPLE_0:1;
hence thesis by A122,A124,XTUPLE_0:1;
end;
suppose
A125: [x,y] = [1,0];
then x = 1 by XTUPLE_0:1;
hence thesis by A100,A125,XTUPLE_0:1;
end;
suppose
A126: [x,y] = [1,2];
then x = 1 by XTUPLE_0:1;
hence thesis by A113,A126,XTUPLE_0:1;
end;
suppose
A127: [x,y] = [2,1];
then x = 2 by XTUPLE_0:1;
hence thesis by A115,A127,XTUPLE_0:1;
end;
suppose
A128: [x,y] = [2,3];
then x = 2 by XTUPLE_0:1;
hence thesis by A114,A128,XTUPLE_0:1;
end;
suppose
A129: [x,y] = [3,2];
then x = 3 by XTUPLE_0:1;
hence thesis by A111,A129,XTUPLE_0:1;
end;
end;
thus [f.x,f.y] in the InternalRel of H2 implies [x,y] in the
InternalRel of N4
proof
[f.x,f.y] in the InternalRel of S implies [x,y] in the
InternalRel of N4 by A40;
then [f.x,f.y] in (((A \/ B) \/ C) \/ D) implies [x,y] in the
InternalRel of N4 by A30,Def3;
then [f.x,f.y] in ((A \/ B) \/ (C\/ D)) implies [x,y] in the
InternalRel of N4 by XBOOLE_1:4;
then
A130: [f.x,f.y] in (B \/ (A\/(C\/D))) implies [x,y] in the
InternalRel of N4 by XBOOLE_1:4;
assume [f.x,f.y] in the InternalRel of H2;
hence thesis by A130,XBOOLE_0:def 3;
end;
end;
then H2 embeds N4 by A39,A106,NECKLACE:def 1;
hence thesis by A5,A18,A107,A121;
end;
end;
now
A131: the carrier of N4 = {0,1,2,3} by NECKLACE:1,20;
then
A132: 0 in the carrier of N4 by ENUMSET1:def 2;
A133: 3 in the carrier of N4 by A131,ENUMSET1:def 2;
A134: 1 in the carrier of N4 by A131,ENUMSET1:def 2;
A135: dom (the InternalRel of S) c= (the carrier of S) by RELAT_1:def 18;
consider f being Function of N4,S such that
A136: f is one-to-one and
A137: for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of S by A6,NECKLACE:def 1;
assume
A138: S = union_of(H1,H2);
[0,1] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A139: [f.0,f.1] in the InternalRel of S by A137,A132,A134;
then f.0 in dom (the InternalRel of S) by XTUPLE_0:def 12;
then f.0 in (the carrier of S) by A135;
then
A140: f.0 in (the carrier of H1) \/ (the carrier of H2) by A138,Def2;
A141: 2 in the carrier of N4 by A131,ENUMSET1:def 2;
[3,2] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A142: [f.3,f.2] in the InternalRel of S by A137,A141,A133;
[2,3] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A143: [f.2,f.3] in the InternalRel of S by A137,A141,A133;
[2,1] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A144: [f.2,f.1] in the InternalRel of S by A137,A134,A141;
[1,2] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A145: [f.1,f.2] in the InternalRel of S by A137,A134,A141;
[1,0] in the InternalRel of N4 by Th2,ENUMSET1:def 4;
then
A146: [f.1,f.0] in the InternalRel of S by A137,A132,A134;
per cases by A140,XBOOLE_0:def 3;
suppose
A147: f.0 in the carrier of H1;
set cS = the carrier of S, cH1 = the carrier of H1, cH2 = the
carrier of H2;
A148: dom f = the carrier of N4 by FUNCT_2:def 1;
H2 is finite by A18,Th4;
then reconsider cH2 as finite set;
H1 is finite by A17,Th4;
then reconsider cH1 as finite set;
A149: cS = cH1 \/ cH2 by A138,Def2;
A150: dom (the InternalRel of H2) c= (the carrier of H2) by RELAT_1:def 18;
A151: now
assume [f.0,f.1] in the InternalRel of H2;
then f.0 in dom (the InternalRel of H2) by XTUPLE_0:def 12;
hence contradiction by A16,A147,A150,XBOOLE_0:3;
end;
A152: rng (the InternalRel of H2) c= (the carrier of H2) by RELAT_1:def 19;
A153: now
assume [f.1,f.0] in the InternalRel of H2;
then f.0 in rng (the InternalRel of H2) by XTUPLE_0:def 13;
hence contradiction by A16,A147,A152,XBOOLE_0:3;
end;
[f.1,f.0] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A146,Def2;
then
A154: [f.1,f.0] in the InternalRel of H1 by A153,XBOOLE_0:def 3;
A155: H1 is strict non empty RelStr by A17,Th4;
reconsider cS as finite set by A149;
A156: rng (the InternalRel of H1) c= (the carrier of H1) by RELAT_1:def 19;
[f.0,f.1] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A139,Def2;
then
A157: [f.0,f.1] in the InternalRel of H1 by A151,XBOOLE_0:def 3;
then
A158: f.1 in rng (the InternalRel of H1) by XTUPLE_0:def 13;
A159: now
assume [f.2,f.1] in the InternalRel of H2;
then f.1 in rng (the InternalRel of H2) by XTUPLE_0:def 13;
hence contradiction by A16,A156,A152,A158,XBOOLE_0:3;
end;
A160: H2 is non empty by A18,Th4;
A161: cH1 <> cS
proof
A162: cS = cH1 \/ cH2 by A138,Def2;
assume
A163: cH1 = cS;
consider x being object such that
A164: x in cH2 by A160,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16,XBOOLE_0:def 7;
then not x in cH1 by A164,XBOOLE_0:def 4;
hence contradiction by A163,A162,A164,XBOOLE_0:def 3;
end;
cS = cH1 \/ cH2 by A138,Def2;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A161,XBOOLE_0:def 8;
then
A165: card cH1 < card cS by CARD_2:48;
A166: [f.2,f.3] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A143,Def2;
A167: [f.1,f.2] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A145,Def2;
now
assume [f.1,f.2] in the InternalRel of H2;
then f.1 in dom (the InternalRel of H2) by XTUPLE_0:def 12;
hence contradiction by A16,A156,A150,A158,XBOOLE_0:3;
end;
then
A168: [f.1,f.2] in the InternalRel of H1 by A167,XBOOLE_0:def 3;
then
A169: f.2 in rng (the InternalRel of H1) by XTUPLE_0:def 13;
now
assume [f.2,f.3] in the InternalRel of H2;
then f.2 in dom (the InternalRel of H2) by XTUPLE_0:def 12;
hence contradiction by A16,A156,A150,A169,XBOOLE_0:3;
end;
then
A170: [f.2,f.3] in the InternalRel of H1 by A166,XBOOLE_0:def 3;
[f.2,f.1] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A144,Def2;
then
A171: [f.2,f.1] in the InternalRel of H1 by A159,XBOOLE_0:def 3;
A172: now
assume [f.3,f.2] in the InternalRel of H2;
then f.2 in rng (the InternalRel of H2) by XTUPLE_0:def 13;
hence contradiction by A16,A156,A152,A169,XBOOLE_0:3;
end;
[f.3,f.2] in (the InternalRel of H1) \/ (the InternalRel of H2)
by A138,A142,Def2;
then
A173: [f.3,f.2] in the InternalRel of H1 by A172,XBOOLE_0:def 3;
A174: for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of H1
proof
let x,y being Element of N4;
thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the
InternalRel of H1
proof
assume
A175: [x,y] in the InternalRel of N4;
per cases by A175,Th2,ENUMSET1:def 4;
suppose
A176: [x,y] = [0,1];
then x = 0 by XTUPLE_0:1;
hence thesis by A157,A176,XTUPLE_0:1;
end;
suppose
A177: [x,y] = [1,0];
then x = 1 by XTUPLE_0:1;
hence thesis by A154,A177,XTUPLE_0:1;
end;
suppose
A178: [x,y] = [1,2];
then x = 1 by XTUPLE_0:1;
hence thesis by A168,A178,XTUPLE_0:1;
end;
suppose
A179: [x,y] = [2,1];
then x = 2 by XTUPLE_0:1;
hence thesis by A171,A179,XTUPLE_0:1;
end;
suppose
A180: [x,y] = [2,3];
then x = 2 by XTUPLE_0:1;
hence thesis by A170,A180,XTUPLE_0:1;
end;
suppose
A181: [x,y] = [3,2];
then x = 3 by XTUPLE_0:1;
hence thesis by A173,A181,XTUPLE_0:1;
end;
end;
thus [f.x,f.y] in the InternalRel of H1 implies [x,y] in the
InternalRel of N4
proof
[f.x,f.y] in the InternalRel of S implies [x,y] in the
InternalRel of N4 by A137;
then
A182: [f.x,f.y] in (the InternalRel of H1) \/ (the InternalRel
of H2) implies [x,y] in the InternalRel of N4 by A138,Def2;
assume [f.x,f.y] in the InternalRel of H1;
hence thesis by A182,XBOOLE_0:def 3;
end;
end;
A183: f.3 in rng (the InternalRel of H1) by A170,XTUPLE_0:def 13;
rng f c= the carrier of H1
proof
let y be object;
assume y in rng f;
then consider x being object such that
A184: x in dom f and
A185: y = f.x by FUNCT_1:def 3;
per cases by A148,A184,Lm1,ENUMSET1:def 2;
suppose
x = 0;
hence thesis by A147,A185;
end;
suppose
x = 1;
hence thesis by A156,A158,A185;
end;
suppose
x = 2;
hence thesis by A156,A169,A185;
end;
suppose
x = 3;
hence thesis by A156,A183,A185;
end;
end;
then f is Function of the carrier of N4,the carrier of H1 by
FUNCT_2:6;
then H1 embeds N4 by A136,A174,NECKLACE:def 1;
hence thesis by A5,A17,A155,A165;
end;
suppose
A186: f.0 in the carrier of H2;
set cS = the carrier of S, cH1 = the carrier of H1, cH2 = the
carrier of H2;
A187: dom f = the carrier of N4 by FUNCT_2:def 1;
H2 is finite by A18,Th4;
then reconsider cH2 as finite set;
H1 is finite by A17,Th4;
then reconsider cH1 as finite set;
A188: cS = cH1 \/ cH2 by A138,Def2;
A189: dom (the InternalRel of H1) c= (the carrier of H1) by RELAT_1:def 18;
A190: now
assume [f.0,f.1] in the InternalRel of H1;
then f.0 in dom (the InternalRel of H1) by XTUPLE_0:def 12;
hence contradiction by A16,A186,A189,XBOOLE_0:3;
end;
A191: rng (the InternalRel of H1) c= (the carrier of H1) by RELAT_1:def 19;
A192: now
assume [f.1,f.0] in the InternalRel of H1;
then f.0 in rng (the InternalRel of H1) by XTUPLE_0:def 13;
hence contradiction by A16,A186,A191,XBOOLE_0:3;
end;
[f.1,f.0] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A146,Def2;
then
A193: [f.1,f.0] in the InternalRel of H2 by A192,XBOOLE_0:def 3;
A194: H2 is strict non empty RelStr by A18,Th4;
reconsider cS as finite set by A188;
A195: rng (the InternalRel of H2) c= (the carrier of H2) by RELAT_1:def 19;
[f.0,f.1] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A139,Def2;
then
A196: [f.0,f.1] in the InternalRel of H2 by A190,XBOOLE_0:def 3;
then
A197: f.1 in rng (the InternalRel of H2) by XTUPLE_0:def 13;
A198: now
assume [f.2,f.1] in the InternalRel of H1;
then f.1 in rng (the InternalRel of H1) by XTUPLE_0:def 13;
hence contradiction by A16,A195,A191,A197,XBOOLE_0:3;
end;
A199: H1 is non empty by A17,Th4;
A200: cH2 <> cS
proof
A201: cS = cH1 \/ cH2 by A138,Def2;
assume
A202: cH2 = cS;
consider x being object such that
A203: x in cH1 by A199,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16,XBOOLE_0:def 7;
then not x in cH2 by A203,XBOOLE_0:def 4;
hence contradiction by A202,A201,A203,XBOOLE_0:def 3;
end;
cS = cH1 \/ cH2 by A138,Def2;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A200,XBOOLE_0:def 8;
then
A204: card cH2 < card cS by CARD_2:48;
A205: [f.2,f.3] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A143,Def2;
A206: [f.1,f.2] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A145,Def2;
now
assume [f.1,f.2] in the InternalRel of H1;
then f.1 in dom (the InternalRel of H1) by XTUPLE_0:def 12;
hence contradiction by A16,A195,A189,A197,XBOOLE_0:3;
end;
then
A207: [f.1,f.2] in the InternalRel of H2 by A206,XBOOLE_0:def 3;
then
A208: f.2 in rng (the InternalRel of H2) by XTUPLE_0:def 13;
now
assume [f.2,f.3] in the InternalRel of H1;
then f.2 in dom (the InternalRel of H1) by XTUPLE_0:def 12;
hence contradiction by A16,A195,A189,A208,XBOOLE_0:3;
end;
then
A209: [f.2,f.3] in the InternalRel of H2 by A205,XBOOLE_0:def 3;
[f.2,f.1] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A144,Def2;
then
A210: [f.2,f.1] in the InternalRel of H2 by A198,XBOOLE_0:def 3;
A211: now
assume [f.3,f.2] in the InternalRel of H1;
then f.2 in rng (the InternalRel of H1) by XTUPLE_0:def 13;
hence contradiction by A16,A195,A191,A208,XBOOLE_0:3;
end;
[f.3,f.2] in (the InternalRel of H1) \/ (the InternalRel of H2
) by A138,A142,Def2;
then
A212: [f.3,f.2] in the InternalRel of H2 by A211,XBOOLE_0:def 3;
A213: for x,y being Element of N4 holds [x,y] in the InternalRel of
N4 iff [f.x,f.y] in the InternalRel of H2
proof
let x,y being Element of N4;
thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the
InternalRel of H2
proof
assume
A214: [x,y] in the InternalRel of N4;
per cases by A214,Th2,ENUMSET1:def 4;
suppose
A215: [x,y] = [0,1];
then x = 0 by XTUPLE_0:1;
hence thesis by A196,A215,XTUPLE_0:1;
end;
suppose
A216: [x,y] = [1,0];
then x = 1 by XTUPLE_0:1;
hence thesis by A193,A216,XTUPLE_0:1;
end;
suppose
A217: [x,y] = [1,2];
then x = 1 by XTUPLE_0:1;
hence thesis by A207,A217,XTUPLE_0:1;
end;
suppose
A218: [x,y] = [2,1];
then x = 2 by XTUPLE_0:1;
hence thesis by A210,A218,XTUPLE_0:1;
end;
suppose
A219: [x,y] = [2,3];
then x = 2 by XTUPLE_0:1;
hence thesis by A209,A219,XTUPLE_0:1;
end;
suppose
A220: [x,y] = [3,2];
then x = 3 by XTUPLE_0:1;
hence thesis by A212,A220,XTUPLE_0:1;
end;
end;
thus [f.x,f.y] in the InternalRel of H2 implies [x,y] in the
InternalRel of N4
proof
[f.x,f.y] in the InternalRel of S implies [x,y] in the
InternalRel of N4 by A137;
then
A221: [f.x,f.y] in (the InternalRel of H1) \/ (the InternalRel
of H2) implies [x,y] in the InternalRel of N4 by A138,Def2;
assume [f.x,f.y] in the InternalRel of H2;
hence thesis by A221,XBOOLE_0:def 3;
end;
end;
A222: f.3 in rng (the InternalRel of H2) by A209,XTUPLE_0:def 13;
rng f c= the carrier of H2
proof
let y be object;
assume y in rng f;
then consider x being object such that
A223: x in dom f and
A224: y = f.x by FUNCT_1:def 3;
per cases by A187,A223,Lm1,ENUMSET1:def 2;
suppose
x = 0;
hence thesis by A186,A224;
end;
suppose
x = 1;
hence thesis by A195,A197,A224;
end;
suppose
x = 2;
hence thesis by A195,A208,A224;
end;
suppose
x = 3;
hence thesis by A195,A222,A224;
end;
end;
then f is Function of the carrier of N4,the carrier of H2 by
FUNCT_2:6;
then H2 embeds N4 by A136,A213,NECKLACE:def 1;
hence thesis by A5,A18,A194,A204;
end;
end;
hence thesis by A19,A20;
end;
end;
assume R embeds N4;
then P[k] by A1;
then
A225: ex i being Nat st P[i];
P[0] from NAT_1:sch 7(A225,A2);
hence thesis;
end;