:: The Class of Series-Parallel Graphs, {I}
:: by Krzysztof Retel
::
:: Received November 18, 2002
:: Copyright (c) 2002-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, NAT_1, CARD_1, ZFMISC_1, XBOOLE_0, SUBSET_1, ARYTM_3,
FUNCT_3, FUNCT_1, RELAT_1, FUNCT_2, FUNCT_4, TARSKI, FUNCOP_1, ORDERS_2,
STRUCT_0, RELAT_2, XXREAL_0, ARYTM_1, WELLORD1, CAT_1, SEQM_3, FINSET_1,
ORDINAL1, CARD_2, SQUARE_1, NECKLACE, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_2, WELLORD1,
FINSET_1, SQUARE_1, QUIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1,
NAT_1, NAT_D, RELAT_1, RELAT_2, FUNCT_3, FUNCOP_1, RELSET_1, FUNCT_1,
PARTFUN1, FUNCT_2, FUNCT_4, BINOP_1, XXREAL_0, STRUCT_0, ORDERS_2,
WAYBEL_0, WAYBEL_1, ORDERS_3;
constructors WELLORD1, REAL_1, SQUARE_1, NAT_1, QUIN_1, CARD_2, REALSET1,
ORDERS_3, WAYBEL_1, NAT_D, RELSET_1, FUNCT_4;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, SQUARE_1, STRUCT_0, ORDERS_2, HILBERT3,
CARD_1, RELAT_1, QUIN_1, NAT_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions WAYBEL_0, WAYBEL_1, ORDERS_3, STRUCT_0, FUNCT_1, RELAT_1, RELAT_2,
XBOOLE_0, TARSKI;
equalities STRUCT_0, XBOOLE_0, SQUARE_1, FUNCOP_1, WELLORD1, SUBSET_1,
BINOP_1, ORDINAL1;
expansions WAYBEL_1, RELAT_2;
theorems FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, RELSET_1, ZFMISC_1, NAT_1,
AXIOMS, CARD_1, WAYBEL_0, SUBSET_1, XBOOLE_0, XBOOLE_1, QUIN_1, WELLORD2,
RELAT_1, FUNCT_3, TARSKI, FUNCOP_1, ORDERS_2, RELAT_2, ORDINAL1, CARD_2,
SQUARE_1, PARTFUN1, XREAL_1, XXREAL_0, FRECHET, XTUPLE_0;
schemes NAT_1, FRAENKEL, FUNCT_7;
begin :: Preliminaries
reserve i,j,k,n for Nat;
reserve x,x1,x2,x3,y1,y2,y3 for set;
theorem
4 = {0,1,2,3} by CARD_1:52;
theorem
[:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[
x2,y3],[x3,y1],[x3,y2],[x3,y3]}
proof
thus [:{x1,x2,x3},{y1,y2,y3}:] = [:{x1}\/{x2,x3}, {y1,y2,y3}:] by ENUMSET1:2
.= [:{x1}\/{x2,x3}, {y1}\/ {y2,y3}:] by ENUMSET1:2
.= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ [:{x2,x3},{
y2,y3}:] by ZFMISC_1:98
.= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,
y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:109
.= {[x1,y1]} \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,y3}
:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:29
.= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,y3}
:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ([:{x2},{y2,y3
}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,
y3]} \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
.= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,
y3]} \/ {[x3,y2],[x3,y3]}) by ZFMISC_1:30
.= {[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]}
\/ {[x3,y2],[x3,y3]}) by ENUMSET1:2
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[
x3,y2],[x3,y3]}) by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2]
,[x3,y3]} by ENUMSET1:5
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3], [x3,y2],[x3
,y3]} by ENUMSET1:81
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2]
,[x3,y3]} by ENUMSET1:80
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[
x3,y2],[x3,y3]}) by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[
x3,y2],[x3,y3]}) by ENUMSET1:59
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1],[x3,y2
],[x3,y3]}) by ENUMSET1:9
.= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3], [x3,y1],[x3,y2],[x3
,y3]} by ENUMSET1:80;
end;
::$CT
theorem Th3:
for x be non zero Nat holds 0 in x
proof
let x be non zero Nat;
reconsider n = x as Element of NAT by ORDINAL1:def 12;
n = {i where i is Nat: i < n} & 0 < n by AXIOMS:4;
hence thesis;
end;
registration
let X be set;
cluster delta X -> one-to-one;
coherence
proof
set f = delta X;
let x1,x2 be object;
assume that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
f.x1 = [x1,x1] & f.x2 = [x2,x2] by A1,FUNCT_3:def 6;
hence thesis by A2,XTUPLE_0:1;
end;
end;
theorem Th4:
for X being set holds card id X = card X
proof
let X be set;
id X in Funcs(X,X) by FUNCT_2:9;
hence thesis by CARD_2:3;
end;
registration
cluster trivial -> one-to-one for Function;
coherence
proof
let f be Function such that
A1: f is trivial;
let x1,x2 be object;
assume that
A2: x1 in dom f and
A3: x2 in dom f and
f.x1 = f.x2;
reconsider f as trivial Function by A1;
consider x being object such that
A4: dom f = {x} by A2,ZFMISC_1:131;
x1 = x by A2,A4,TARSKI:def 1;
hence thesis by A3,A4,TARSKI:def 1;
end;
end;
theorem
for f,g be Function st dom f misses dom g holds rng(f +* g) = rng f \/
rng g by FRECHET:35,PARTFUN1:56;
theorem Th6:
for f,g be one-to-one Function st dom f misses dom g & rng f
misses rng g holds (f+*g)" = f" +* g"
proof
let f,g be one-to-one Function such that
A1: dom f misses dom g and
A2: rng f misses rng g;
A3: (f+*g) is one-to-one by A2,FUNCT_4:92;
A4: for y,x being object
holds y in rng (f+*g) & x = (f" +* g").y iff x in dom(f+*g) & y = (f+*g).x
proof
let y,x be object;
thus y in rng (f+*g) & x = (f" +* g").y implies x in dom (f+*g) & y = (f+*
g).x
proof
A5: rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
assume that
A6: y in rng (f+*g) and
A7: x = (f" +* g").y;
per cases by A6,A5,XBOOLE_0:def 3;
suppose
A8: y in rng f;
then consider z being object such that
A9: z in dom f and
A10: y = f.z by FUNCT_1:def 3;
dom (f +* g) = dom f \/ dom g by FUNCT_4:def 1;
then
A11: z in dom (f +* g) by A9,XBOOLE_0:def 3;
A12: dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
y = (f +* g).z & z = f".y by A1,A9,A10,FUNCT_1:32,FUNCT_4:16;
hence thesis by A2,A7,A8,A11,A12,FUNCT_4:16;
end;
suppose
A13: y in rng g;
A14: dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
consider z being object such that
A15: z in dom g and
A16: y = g.z by A13,FUNCT_1:def 3;
z = g".y by A15,A16,FUNCT_1:32;
then z = (g" +* f").y by A2,A13,A14,FUNCT_4:16;
then
A17: z = x by A2,A7,A14,FUNCT_4:35;
dom (f +* g) = dom f \/ dom g & y = (g +* f).z by A1,A15,A16,FUNCT_4:16
,def 1;
hence thesis by A1,A15,A17,FUNCT_4:35,XBOOLE_0:def 3;
end;
end;
thus x in dom (f+*g) & y = (f+*g).x implies y in rng (f+*g) & x = (f" +* g
").y
proof
A18: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
assume that
A19: x in dom (f+*g) and
A20: y = (f+*g).x;
per cases by A19,A18,XBOOLE_0:def 3;
suppose
A21: x in dom f;
then not x in dom g by A1,XBOOLE_0:3;
then
A22: y = f.x by A20,FUNCT_4:11;
then
A23: x = f".y by A21,FUNCT_1:32;
A24: dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
A25: y in rng f by A21,A22,FUNCT_1:def 3;
then y in rng f \/ rng g by XBOOLE_0:def 3;
hence thesis by A1,A2,A25,A23,A24,FRECHET:35,FUNCT_4:16,PARTFUN1:56;
end;
suppose
A26: x in dom g;
then
A27: y = g.x by A20,FUNCT_4:13;
then
A28: y in rng g by A26,FUNCT_1:def 3;
then
A29: y in rng f \/ rng g by XBOOLE_0:def 3;
A30: dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
x = g".y by A26,A27,FUNCT_1:32;
then x = (g" +* f").y by A2,A28,A30,FUNCT_4:16;
hence thesis by A1,A2,A29,A30,FRECHET:35,FUNCT_4:35,PARTFUN1:56;
end;
end;
end;
dom (f" +* g") = dom (f") \/ dom (g") by FUNCT_4:def 1
.= rng f \/ dom (g") by FUNCT_1:33
.= rng f \/ rng g by FUNCT_1:33
.= rng (f +* g) by A1,FRECHET:35,PARTFUN1:56;
hence thesis by A3,A4,FUNCT_1:32;
end;
theorem
for A,a,b being set holds (A --> a) +* (A --> b) = A --> b
proof
let A,a,b be set;
set g = A --> b;
dom (A --> a) c= dom g;
hence thesis by FUNCT_4:19;
end;
theorem Th8:
for a,b being set holds (a .--> b)" = b .--> a
proof
let a,b be set;
set f = a .--> b, g = b .--> a;
A1: for y,x be object holds y in rng f & x = g.y iff x in dom f & y = f.x
proof
let y,x be object;
thus y in rng f & x = g.y implies x in dom f & y = f.x
proof
assume that
A2: y in rng f and
A3: x = g.y;
A4: y in {b} by A2,FUNCOP_1:8;
then
A5: x = g.b by A3,TARSKI:def 1
.= a by FUNCOP_1:72;
then
A6: x in {a} by TARSKI:def 1;
f.x = b by A5,FUNCOP_1:72
.= y by A4,TARSKI:def 1;
hence thesis by A6;
end;
assume that
A7: x in dom f and
A8: y = f.x;
A9: x in {a} by A7;
then
A10: y = f.a by A8,TARSKI:def 1
.= b by FUNCOP_1:72;
then
A11: y in {b} by TARSKI:def 1;
g.y = a by A10,FUNCOP_1:72
.= x by A9,TARSKI:def 1;
hence thesis by A11,FUNCOP_1:8;
end;
dom g = {b}
.= rng f by FUNCOP_1:8;
hence thesis by A1,FUNCT_1:32;
end;
theorem Th9:
for a,b,c,d being set st a = b iff c = d holds (a,b) --> (c,d)"
= (c,d) --> (a,b)
proof
let a,b,c,d being set such that
A1: a = b iff c = d;
per cases by A1;
suppose
A2: a = b & c = d;
(a,a) --> (d,d)" = (a .--> d)" by FUNCT_4:81
.= (d .--> a) by Th8
.= (d,d) --> (a,a) by FUNCT_4:81;
hence thesis by A2;
end;
suppose
A3: a <> b & c <> d;
set f = (a,b) --> (c,d), g = (c,d) --> (a,b);
A4: for y,x be object holds y in rng f & x = g.y iff x in dom f & y = f.x
proof
let y,x be object;
A5: x in dom f & y = f.x implies y in rng f & x = g.y
proof
assume that
A6: x in dom f and
A7: y = f.x;
A8: x in {a,b} by A6,FUNCT_4:62;
per cases by A8,TARSKI:def 2;
suppose
A9: x = a;
then
A10: y = c by A3,A7,FUNCT_4:63;
then y in {c,d} by TARSKI:def 2;
hence thesis by A3,A9,A10,FUNCT_4:63,64;
end;
suppose
A11: x = b;
then
A12: y = d by A7,FUNCT_4:63;
then y in {c,d} by TARSKI:def 2;
hence thesis by A3,A11,A12,FUNCT_4:63,64;
end;
end;
y in rng f & x = g.y implies x in dom f & y = f.x
proof
assume that
A13: y in rng f and
A14: x = g.y;
A15: y in {c,d} by A3,A13,FUNCT_4:64;
per cases by A15,TARSKI:def 2;
suppose
A16: y = c;
then
A17: x = a by A3,A14,FUNCT_4:63;
then x in {a,b} by TARSKI:def 2;
hence thesis by A3,A16,A17,FUNCT_4:62,63;
end;
suppose
A18: y = d;
then
A19: x = b by A14,FUNCT_4:63;
then x in {a,b} by TARSKI:def 2;
hence thesis by A18,A19,FUNCT_4:62,63;
end;
end;
hence thesis by A5;
end;
A20: f is one-to-one
proof
A21: dom f = {a,b} by FUNCT_4:62;
let x1,x2 being object such that
A22: x1 in dom f & x2 in dom f and
A23: f.x1 = f.x2;
per cases by A22,A21,TARSKI:def 2;
suppose
x1 = a & x2 = a or x1 = b & x2 = b;
hence thesis;
end;
suppose
A24: x1 = a & x2 = b;
then f.x1 = c by A3,FUNCT_4:63;
hence thesis by A3,A23,A24,FUNCT_4:63;
end;
suppose
A25: x1 = b & x2 = a;
then f.x1 = d by FUNCT_4:63;
hence thesis by A3,A23,A25,FUNCT_4:63;
end;
end;
dom g = {c,d} by FUNCT_4:62
.= rng f by A3,FUNCT_4:64;
hence thesis by A20,A4,FUNCT_1:32;
end;
end;
scheme
Convers{X()-> non empty set, R() -> Relation, F,G(set)-> set, P[set]}: R()~
={[F(x),G(x)] where x is Element of X(): P[x]}
provided
A1: R() = {[G(x),F(x)] where x is Element of X(): P[x]}
proof
set S = {[F(x),G(x)] where x is Element of X(): P[x]};
S is Relation-like
proof
let x being object;
assume x in S;
then ex y being Element of X() st x = [F(y),G(y)] & P[y];
hence thesis;
end;
then reconsider S9 = S as Relation;
A2: for x,y being object holds [y,x] in R() implies [x,y] in S9
proof
let x,y being object;
assume [y,x] in R();
then consider z being Element of X() such that
A3: [y,x] = [G(z),F(z)] and
A4: P[z] by A1;
y = G(z) & x = F(z) by A3,XTUPLE_0:1;
hence thesis by A4;
end;
for x,y being object holds [x,y] in S9 implies [y,x] in R()
proof
let x,y being object;
assume [x,y] in S9;
then consider z being Element of X() such that
A5: [x,y] = [F(z),G(z)] and
A6: P[z];
x = F(z) & y = G(z) by A5,XTUPLE_0:1;
hence thesis by A1,A6;
end;
hence thesis by A2,RELAT_1:def 7;
end;
theorem
for i,j,n be Nat holds i < j & j in Segm n implies i in Segm n
proof
let i,j,n be Nat;
assume that
A1: i < j and
A2: j in Segm n;
j < n by A2,NAT_1:44;
then i < n by A1,XXREAL_0:2;
hence thesis by NAT_1:44;
end;
begin :: Auxiliary Concepts
definition
let R,S be RelStr;
pred S embeds R means
ex f being Function of R,S st f is one-to-one &
for x,y being Element of R holds [x,y] in the InternalRel of R iff [f.x,f.y] in
the InternalRel of S;
end;
definition
let R,S be non empty RelStr;
redefine pred S embeds R; :: redefines embeds (NECKLACE, definition)
reflexivity
proof
let R be non empty RelStr;
set f = id the carrier of R;
reconsider f as Function of R,R;
take f;
thus f is one-to-one;
let x,y be Element of R;
thus thesis;
end;
end;
theorem Th11:
for R,S,T be non empty RelStr holds R embeds S & S embeds T
implies R embeds T
proof
let R,S,T be non empty RelStr;
assume R embeds S;
then consider f being Function of S,R such that
A1: f is one-to-one and
A2: for x,y being Element of S holds [x,y] in the InternalRel of S iff [
f.x,f.y] in the InternalRel of R;
assume S embeds T;
then consider g being Function of T,S such that
A3: g is one-to-one and
A4: for x,y being Element of T holds [x,y] in the InternalRel of T iff [
g.x,g.y] in the InternalRel of S;
reconsider h=f*g as Function of T,R;
take h;
thus h is one-to-one by A1,A3;
thus for x,y being Element of T holds [x,y] in the InternalRel of T iff [h.x
,h.y] in the InternalRel of R
proof
let x,y be Element of T;
thus [x,y] in the InternalRel of T implies [h.x,h.y] in the InternalRel of
R
proof
assume [x,y] in the InternalRel of T;
then
A5: [g.x,g.y] in the InternalRel of S by A4;
h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:15;
hence thesis by A2,A5;
end;
thus [h.x,h.y] in the InternalRel of R implies [x,y] in the InternalRel of
T
proof
A6: h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:15;
assume [h.x,h.y] in the InternalRel of R;
then [g.x,g.y] in the InternalRel of S by A2,A6;
hence thesis by A4;
end;
end;
end;
definition
let R,S be non empty RelStr;
pred R is_equimorphic_to S means
R embeds S & S embeds R;
reflexivity;
symmetry;
end;
theorem
for R,S,T be non empty RelStr holds R is_equimorphic_to S & S
is_equimorphic_to T implies R is_equimorphic_to T
by Th11;
notation
let R be non empty RelStr;
antonym R is parallel↑ for R is connected;
end;
definition
let R be RelStr;
attr R is symmetric means
:Def3:
the InternalRel of R is_symmetric_in the carrier of R;
end;
definition
let R be RelStr;
attr R is asymmetric means
the InternalRel of R is asymmetric;
end;
theorem
for R be RelStr st R is asymmetric holds the InternalRel of R misses (
the InternalRel of R)~
proof
let R be RelStr;
assume R is asymmetric;
then the InternalRel of R is asymmetric;
then
A1: the InternalRel of R is_asymmetric_in field (the InternalRel of R);
assume the InternalRel of R meets (the InternalRel of R)~;
then consider x being object such that
A2: x in the InternalRel of R and
A3: x in (the InternalRel of R)~ by XBOOLE_0:3;
consider y,z being object such that
A4: x = [y,z] by A3,RELAT_1:def 1;
A5: z in field the InternalRel of R by A2,A4,RELAT_1:15;
[z,y] in the InternalRel of R & y in field the InternalRel of R by A2,A3,A4,
RELAT_1:15,def 7;
hence contradiction by A2,A4,A1,A5;
end;
definition
let R be RelStr;
attr R is irreflexive means
for x being set st x in the carrier of R holds
not [x,x] in the InternalRel of R;
end;
definition
let n be Nat;
func n-SuccRelStr -> strict RelStr means
:Def6:
the carrier of it = n & the
InternalRel of it = {[i,i+1] where i is Element of NAT:i+1 < n};
existence
proof
set r = {[i,i+1] where i is Element of NAT:i+1 < n};
r c= [:n,n:]
proof
let x be object;
assume x in r;
then consider i be Element of NAT such that
A1: x = [i,i+1] and
A2: i+1 < n;
i <= i+1 by NAT_1:11;
then i < n by A2,XXREAL_0:2;
then
A3: i in Segm n by NAT_1:44;
i+1 in Segm n by A2,NAT_1:44;
hence thesis by A1,A3,ZFMISC_1:87;
end;
then reconsider r as Relation of n;
take RelStr (#n,r#);
thus thesis;
end;
uniqueness;
end;
theorem
for n be Nat holds n-SuccRelStr is asymmetric
proof
let n be Nat;
set S = n-SuccRelStr;
the InternalRel of S is_asymmetric_in field the InternalRel of S
proof
let x,y be object;
assume that
x in field the InternalRel of S and
y in field the InternalRel of S and
A1: [x,y] in the InternalRel of S;
A2: [x,y] in {[i,i+1] where i is Element of NAT:i+1 < n} by A1,Def6;
assume [y,x] in the InternalRel of S;
then [y,x] in {[i9,i9+1] where i9 is Element of NAT:i9+1 < n} by Def6;
then consider j be Element of NAT such that
A3: [y,x] = [j,j+1] and
j+1<n;
A4: y = j & x = j+1 by A3,XTUPLE_0:1;
consider i be Element of NAT such that
A5: [x,y] = [i,i+1] and
i+1<n by A2;
x = i & y = i+1 by A5,XTUPLE_0:1;
hence contradiction by A4;
end;
hence the InternalRel of S is asymmetric;
end;
theorem Th15:
n > 0 implies card the InternalRel of n-SuccRelStr = n-1
proof
deffunc F(Element of NAT) = [$1,$1+1];
defpred P[Element of NAT] means $1+1<n;
defpred Q[set] means $1 in Segm(n-'1);
A1: n-'1 c= NAT;
assume
A2: n > 0;
then
A3: n >= 0+1 by NAT_1:13;
A4: i in Segm(n-'1) implies i+1<n
proof
assume i in Segm(n-'1);
then
A5: i < n-'1 by NAT_1:44;
n >= 0+1 by A2,NAT_1:13;
then i < n-1 by A5,XREAL_1:233;
hence thesis by XREAL_1:20;
end;
A6: for i being Element of NAT holds P[i] iff Q[i]
proof
let i be Element of NAT;
thus i+1<n implies i in Segm(n-'1)
proof
assume i+1<n;
then i < n-1 by XREAL_1:20;
then i < n-'1 by A3,XREAL_1:233;
hence thesis by NAT_1:44;
end;
thus thesis by A4;
end;
A7: {F(i) where i is Element of NAT: P[i]} = {F(i) where i is Element of
NAT: Q[i]} from FRAENKEL:sch 3(A6);
deffunc F(Element of NAT) = [$1,$1+1];
A8: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1 = d2 by XTUPLE_0:1
;
A9: n-'1, {F(i) where i is Element of NAT: i in n-'1} are_equipotent from
FUNCT_7:sch 4(A1,A8);
thus card the InternalRel of n-SuccRelStr = card {[i,i+1] where i is Element
of NAT:i+1 < n} by Def6
.= card (n-'1) by A7,A9,CARD_1:5
.= n-'1
.= n-1 by A3,XREAL_1:233;
end;
definition
let R be RelStr;
func SymRelStr R -> strict RelStr means
:Def7:
the carrier of it = the
carrier of R & the InternalRel of it = (the InternalRel of R) \/ (the
InternalRel of R)~;
existence
proof
take RelStr (#the carrier of R, (the InternalRel of R) \/ (the InternalRel
of R)~ #);
thus thesis;
end;
uniqueness;
end;
registration
let R be RelStr;
cluster SymRelStr R -> symmetric;
coherence
proof
let x,y be object;
assume that
x in the carrier of SymRelStr R and
y in the carrier of SymRelStr R and
A1: [x,y] in the InternalRel of SymRelStr R;
A2: [x,y] in (the InternalRel of R) \/ (the InternalRel of R)~ by A1,Def7;
per cases by A2,XBOOLE_0:def 3;
suppose
[x,y] in the InternalRel of R;
then [y,x] in (the InternalRel of R)~ by RELAT_1:def 7;
then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~ by
XBOOLE_0:def 3;
hence thesis by Def7;
end;
suppose
[x,y] in (the InternalRel of R)~;
then [y,x] in the InternalRel of R by RELAT_1:def 7;
then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~ by
XBOOLE_0:def 3;
hence thesis by Def7;
end;
end;
end;
registration
cluster non empty symmetric for RelStr;
existence
proof
set R = {[0,0]};
R c= [:{0},{0}:] by ZFMISC_1:29;
then reconsider R = {[0,0]} as Relation of {0};
take S = RelStr (#{0},R#);
thus S is non empty;
thus the InternalRel of S is_symmetric_in the carrier of S
proof
let x,y be object;
assume that
x in the carrier of S and
y in the carrier of S and
A1: [x,y] in the InternalRel of S;
x = 0 & y = 0 by A1,ZFMISC_1:28;
then [y,x] in [:{0},{0}:] by ZFMISC_1:28;
hence thesis by ZFMISC_1:29;
end;
end;
end;
registration
let R be symmetric RelStr;
cluster the InternalRel of R -> symmetric;
coherence
proof
let x,y be object;
assume
A1: x in field the InternalRel of R & y in field the InternalRel of R
& [x,y ] in the InternalRel of R;
the InternalRel of R is_symmetric_in the carrier of R & field the
InternalRel of R c= (the carrier of R) \/ the carrier of R by Def3,RELSET_1:8;
hence thesis by A1;
end;
end;
Lm1: for S,R being non empty RelStr holds S,R are_isomorphic implies card (the
InternalRel of S) = card (the InternalRel of R)
proof
let S,R being non empty RelStr;
set A = the carrier of S, B = the carrier of R, C = the InternalRel of S, D
= the InternalRel of R;
reconsider C as set;
assume S,R are_isomorphic;
then consider f being Function of S,R such that
A1: f is isomorphic;
reconsider f9=f as one-to-one Function by A1,WAYBEL_0:def 38;
A2: [:f9,f9:] is one-to-one;
A3: dom f = A by FUNCT_2:def 1;
A4: rng f = B by A1,WAYBEL_0:66;
A5: f is monotone by A1,WAYBEL_0:def 38;
the InternalRel of S,the InternalRel of R are_equipotent
proof
set P = [:f,f:];
set F = [:f,f:]|C;
set L = dom F;
A6: dom F = dom ([:f,f:]) /\ C by RELAT_1:61
.= [:dom f, dom f:] /\ C by FUNCT_3:def 8
.= C by A3,XBOOLE_1:28;
A7: rng F c= D
proof
let a be object;
assume a in rng F;
then consider x being object such that
A8: x in dom F and
A9: a = F.x by FUNCT_1:def 3;
consider x1,x2 being object such that
A10: x = [x1,x2] by A8,RELAT_1:def 1;
A11: x in dom [:f,f:] by A8,RELAT_1:57;
then reconsider X1 = x1, X2 = x2 as Element of S by A10,ZFMISC_1:87;
X1 <= X2 by A8,A10,ORDERS_2:def 5;
then
A12: f.X1 <= f.X2 by A5;
A13: a = P.(x1,x2) by A8,A9,A10,FUNCT_1:47;
x1 in dom f & x2 in dom f by A3,A10,A11,ZFMISC_1:87;
then a = [f.x1,f.x2] by A13,FUNCT_3:def 8;
hence thesis by A12,ORDERS_2:def 5;
end;
then reconsider F as Function of L,[:B,B:] by FUNCT_2:2,XBOOLE_1:1;
reconsider F as Function of L,D by A7,FUNCT_2:6;
A14: rng F = D
proof
thus rng F c= D by A7;
let x be object;
assume
A15: x in D;
then consider x1,x2 being object such that
A16: x = [x1,x2] by RELAT_1:def 1;
reconsider x19 = x1, x29 = x2 as Element of B by A15,A16,ZFMISC_1:87;
x1 in B by A15,A16,ZFMISC_1:87;
then consider X1 being object such that
A17: X1 in dom f and
A18: x1 = f.X1 by A4,FUNCT_1:def 3;
x2 in B by A15,A16,ZFMISC_1:87;
then consider X2 being object such that
A19: X2 in dom f and
A20: x2 = f.X2 by A4,FUNCT_1:def 3;
reconsider X19 = X1, X29 = X2 as Element of S by A17,A19;
x19 <= x29 by A15,A16,ORDERS_2:def 5;
then X19 <= X29 by A1,A18,A20,WAYBEL_0:66;
then
A21: [X1,X2] in C by ORDERS_2:def 5;
set Pi = [X1,X2];
Pi in [:dom f,dom f:] by A17,A19,ZFMISC_1:87;
then x = [:f,f:].(X1,X2) by A16,A18,A20,FUNCT_3:65
.= F.[X1,X2] by A6,A21,FUNCT_1:47;
hence thesis by A6,A21,FUNCT_1:def 3;
end;
F is one-to-one by A2,FUNCT_1:52;
hence thesis by A6,A14,WELLORD2:def 4;
end;
hence thesis by CARD_1:5;
end;
definition
let R be RelStr;
func ComplRelStr R -> strict RelStr means
:Def8:
the carrier of it = the carrier of R &
the InternalRel of it = (the InternalRel of R)` \ id (the carrier of R);
existence
proof
reconsider r = (the InternalRel of R)` \ id (the carrier of R) as Relation
of the carrier of R;
take RelStr(#the carrier of R, r#);
thus thesis;
end;
uniqueness;
end;
registration
let R be non empty RelStr;
cluster ComplRelStr R -> non empty;
coherence
proof
the carrier of ComplRelStr R = the carrier of R by Def8;
hence the carrier of ComplRelStr R is non empty;
end;
end;
theorem Th16:
for S,R being RelStr holds S,R are_isomorphic implies card the
InternalRel of S = card the InternalRel of R
proof
let S,R be RelStr;
assume
A1: S,R are_isomorphic;
then
A2: ex f being Function of S,R st f is isomorphic;
per cases by A2,WAYBEL_0:def 38;
suppose
S is non empty & R is non empty;
hence thesis by A1,Lm1;
end;
suppose
S is empty & R is empty;
then reconsider S, R as empty RelStr;
the InternalRel of S = {} & the InternalRel of R = {};
hence thesis;
end;
end;
begin :: Necklace n
definition
let n be Nat;
func Necklace n -> strict RelStr equals
SymRelStr(n-SuccRelStr);
coherence;
end;
registration
let n be Nat;
cluster Necklace n -> symmetric;
coherence;
end;
theorem Th17:
the InternalRel of Necklace n = {[i,i+1] where i is Element of
NAT:i+1 < n} \/ {[i+1,i] where i is Element of NAT:i+1 < n}
proof
set I = {[i,i+1] where i is Element of NAT:i+1 < n};
I is Relation-like
proof
let x be object;
assume x in I;
then ex i being Element of NAT st x = [i,i+1] & i+1<n;
hence thesis;
end;
then reconsider I as Relation;
set B = n-SuccRelStr;
deffunc F(Element of NAT) = $1;
deffunc G(Element of NAT) = $1+1;
defpred P[Element of NAT] means $1+1 < n;
set R = {[G(i),F(i)] where i is Element of NAT: P[i]};
A1: I = {[F(i),G(i)] where i is Element of NAT: P[i]};
A2: I~ = R from Convers(A1);
the InternalRel of B = I by Def6;
hence thesis by A2,Def7;
end;
theorem Th18:
for x be set holds x in the InternalRel of Necklace n iff ex i
being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i])
proof
let x be set;
thus x in the InternalRel of Necklace n implies ex i being Element of NAT st
i+1< n & (x = [i,i+1] or x = [i+1,i])
proof
assume x in the InternalRel of Necklace n;
then
x in ({[i,i+1] where i is Element of NAT:i+1 < n} \/ {[i+1,i] where i
is Element of NAT:i+1 < n } ) by Th17;
then x in {[i,i+1] where i is Element of NAT:i+1 < n} or x in {[i+1,i]
where i is Element of NAT:i+1 < n} by XBOOLE_0:def 3;
then (ex i being Element of NAT st x = [i,i+1] & i+1<n) or ex i being
Element of NAT st x = [i+1,i] & i+1<n;
hence thesis;
end;
thus (ex i being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i]))
implies x in the InternalRel of Necklace n
proof
given i being Element of NAT such that
A1: i+1 < n &( x=[i,i+1] or x=[i+1,i]);
per cases by A1;
suppose
i+1 < n & x=[i,i+1];
then x in {[j,j+1] where j is Element of NAT:j+1 < n};
then
x in ({[j,j+1] where j is Element of NAT:j+1 < n} \/ {[j+1,j] where
j is Element of NAT:j+1 < n}) by XBOOLE_0:def 3;
hence thesis by Th17;
end;
suppose
i+1 < n & x=[i+1,i];
then x in {[j+1,j] where j is Element of NAT:j+1 < n};
then
x in ({[j+1,j] where j is Element of NAT:j+1 < n} \/ {[j,j+1] where
j is Element of NAT:j+1 < n}) by XBOOLE_0:def 3;
hence thesis by Th17;
end;
end;
end;
registration
let n be Nat;
cluster Necklace n -> irreflexive;
coherence
proof
let x be set;
set A = Necklace n;
assume x in the carrier of A;
A1: the InternalRel of Necklace n = {[i,i+1] where i is Element of NAT:i+1
< n} \/ {[i+1,i] where i is Element of NAT:i+1 < n} by Th17;
assume
A2: [x,x] in the InternalRel of A;
per cases by A2,A1,XBOOLE_0:def 3;
suppose
[x,x] in {[i,i+1] where i is Element of NAT:i+1 < n};
then consider i being Element of NAT such that
A3: [x,x] = [i,i+1] and
i+1 < n;
x = i & x = i+1 by A3,XTUPLE_0:1;
hence contradiction;
end;
suppose
[x,x] in {[i+1,i] where i is Element of NAT:i+1 < n};
then consider i being Element of NAT such that
A4: [x,x] = [i+1,i] and
i+1 < n;
x = i+1 & x = i by A4,XTUPLE_0:1;
hence contradiction;
end;
end;
end;
theorem Th19:
for n be Nat holds the carrier of Necklace n = n
proof
let n be Nat;
the carrier of Necklace n = the carrier of n-SuccRelStr by Def7
.= n by Def6;
hence thesis;
end;
registration
let n be non zero Nat;
cluster Necklace n -> non empty;
coherence by Th19;
end;
registration
let n be Nat;
cluster the carrier of Necklace n -> finite;
coherence by Th19;
end;
theorem Th20:
for n,i be Nat st i+1 < n holds [i,i+1] in the InternalRel of Necklace n
proof
let n,j be Nat such that
A1: j+1 < n;
reconsider j as Element of NAT by ORDINAL1:def 12;
A2: [j,j+1] in {[i,i+1] where i is Element of NAT:i+1 < n} by A1;
the InternalRel of Necklace n = {[i,i+1] where i is Element of NAT:i+1 <
n} \/ {[i+1,i] where i is Element of NAT:i+1 < n} by Th17;
hence thesis by A2,XBOOLE_0:def 3;
end;
theorem Th21:
for n be Nat, i being Nat st i in the carrier of Necklace n holds i < n
proof
let n be Nat, i being Nat;
assume i in the carrier of Necklace n;
then i in Segm n by Th19;
hence thesis by NAT_1:44;
end;
theorem
for n be non zero Nat holds Necklace n is connected
proof
let n be non zero Nat;
given X,Y being Subset of Necklace n such that
A1: X <> {} and
A2: Y <> {} and
A3: [#] Necklace n = X \/ Y and
A4: X misses Y and
A5: the InternalRel of Necklace n = (the InternalRel of Necklace n)|_2 X
\/ (the InternalRel of Necklace n) |_2 Y;
A6: the carrier of Necklace n = n & 0 in n by Th3,Th19;
per cases by A3,A6,XBOOLE_0:def 3;
suppose
A7: 0 in X;
defpred P[Nat] means $1 in Y;
consider x being Element of Necklace n such that
A8: x in Y by A2,SUBSET_1:4;
x in the carrier of Necklace n;
then x in Segm n by Th19;
then x is natural;
then
A9: ex x being Nat st P[x] by A8;
consider k being Nat such that
A10: P[k] and
A11: for i being Nat st P[i] holds k <= i from NAT_1:sch 5 (A9);
k <> 0 by A4,A7,A10,XBOOLE_0:3;
then consider i being Nat such that
A12: k = i+1 by NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
A13: not i in Y by A11,A12,XREAL_1:29;
A14: not i+1 in X by A4,A10,A12,XBOOLE_0:3;
A15: [i,i+1] in the InternalRel of Necklace n by A10,A12,Th20,Th21;
now
per cases by A5,A15,XBOOLE_0:def 3;
suppose
[i,i+1] in (the InternalRel of Necklace n) |_2 X;
then [i,i+1] in [:X,X:] by XBOOLE_0:def 4;
hence contradiction by A14,ZFMISC_1:87;
end;
suppose
[i,i+1] in (the InternalRel of Necklace n) |_2 Y;
then [i,i+1] in [:Y,Y:] by XBOOLE_0:def 4;
hence contradiction by A13,ZFMISC_1:87;
end;
end;
hence contradiction;
end;
suppose
A16: 0 in Y;
defpred P[Nat] means $1 in X;
consider y being Element of Necklace n such that
A17: y in X by A1,SUBSET_1:4;
y in the carrier of Necklace n;
then y in Segm n by Th19;
then y is natural;
then
A18: ex y being Nat st P[y] by A17;
consider k being Nat such that
A19: P[k] and
A20: for i being Nat st P[i] holds k <= i from NAT_1:sch 5 (A18);
k <> 0 by A4,A16,A19,XBOOLE_0:3;
then consider i being Nat such that
A21: k = i+1 by NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
A22: not i in X by A20,A21,XREAL_1:29;
A23: not i+1 in Y by A4,A19,A21,XBOOLE_0:3;
A24: [i,i+1] in the InternalRel of Necklace n by A19,A21,Th20,Th21;
now
per cases by A5,A24,XBOOLE_0:def 3;
suppose
[i,i+1] in (the InternalRel of Necklace n) |_2 Y;
then [i,i+1] in [:Y,Y:] by XBOOLE_0:def 4;
hence contradiction by A23,ZFMISC_1:87;
end;
suppose
[i,i+1] in (the InternalRel of Necklace n) |_2 X;
then [i,i+1] in [:X,X:] by XBOOLE_0:def 4;
hence contradiction by A22,ZFMISC_1:87;
end;
end;
hence thesis;
end;
end;
theorem Th23:
for i,j being Nat st [i,j] in the InternalRel of Necklace n
holds i = j + 1 or j = i + 1
proof
let i,j be Nat;
assume [i,j] in the InternalRel of Necklace n;
then
[i,j] in {[k,k+1] where k is Element of NAT:k+1 < n} \/ {[l+1,l] where l
is Element of NAT:l+1 < n} by Th17;
then
A1: [i,j] in {[k,k+1] where k is Element of NAT:k+1 < n} or [i,j] in {[k+1,k
] where k is Element of NAT:k+1 < n} by XBOOLE_0:def 3;
i + 1 = j or j + 1 = i
proof
per cases by A1;
suppose
ex k being Element of NAT st [i,j] = [k,k+1] & k+1 < n;
then consider k such that
A2: [i,j] = [k,k+1] and
k+1 < n;
i = k by A2,XTUPLE_0:1;
hence thesis by A2,XTUPLE_0:1;
end;
suppose
ex k being Element of NAT st [i,j] = [k+1,k] & k+1 < n;
then consider k such that
A3: [i,j] = [k+1,k] and
k+1 < n;
i = k+1 by A3,XTUPLE_0:1;
hence thesis by A3,XTUPLE_0:1;
end;
end;
hence thesis;
end;
theorem Th24:
for i,j being Nat st (i = j + 1 or j = i + 1) & i in the carrier
of Necklace n & j in the carrier of Necklace n holds [i,j] in the InternalRel
of Necklace n
proof
let i,j be Nat such that
A1: i = j + 1 or j = i + 1 and
A2: i in the carrier of Necklace n and
A3: j in the carrier of Necklace n;
per cases by A1;
suppose
A4: i=j+1;
then [j,j+1] in the InternalRel of Necklace n by A2,Th20,Th21;
then [j+1,j] in (the InternalRel of Necklace n)~ by RELAT_1:def 7;
hence thesis by A4,RELAT_2:13;
end;
suppose
j=i+1;
hence thesis by A3,Th20,Th21;
end;
end;
theorem Th25:
n > 0 implies card ({[i+1,i] where i is Element of NAT:i+1 < n}) = n-1
proof
deffunc F(Element of NAT) = [$1+1,$1];
defpred P[Element of NAT] means $1+1<n;
defpred Q[Element of NAT] means $1 in Segm(n-'1);
A1: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1=d2 by XTUPLE_0:1;
assume
A2: n > 0;
then
A3: n >= 0+1 by NAT_1:13;
A4: i in Segm(n-'1) implies i+1<n
proof
assume i in Segm(n-'1);
then
A5: i < n-'1 by NAT_1:44;
n >= 0+1 by A2,NAT_1:13;
then i < n-1 by A5,XREAL_1:233;
hence thesis by XREAL_1:20;
end;
A6: for i being Element of NAT holds P[i] iff Q[i]
proof
let i being Element of NAT;
thus i+1<n implies i in Segm(n-'1)
proof
assume i+1<n;
then i < n-1 by XREAL_1:20;
then i < n-'1 by A3,XREAL_1:233;
hence thesis by NAT_1:44;
end;
thus thesis by A4;
end;
A7: {F(i) where i is Element of NAT: P[i]} = {F(i) where i is Element of
NAT: Q[i]} from FRAENKEL:sch 3(A6);
A8: n-'1 c= NAT;
n-'1, {F(i) where i is Element of NAT: i in n-'1} are_equipotent from
FUNCT_7:sch 4 (A8,A1);
hence
card ({[i+1,i] where i is Element of NAT:i+1 < n}) = card (n-'1) by A7,
CARD_1:5
.= n-'1
.= n-1 by A3,XREAL_1:233;
end;
theorem Th26:
n > 0 implies card the InternalRel of Necklace n = 2*(n-1)
proof
deffunc G(Element of NAT) = $1+1;
deffunc F(Element of NAT) = $1;
defpred P[Element of NAT] means $1+1 < n;
set A = {[i,i+1] where i is Element of NAT:i+1 < n}, B = {[G(i),F(i)] where
i is Element of NAT:P[i]};
A1: A is Relation-like
proof
let x be object;
assume x in A;
then ex i being Element of NAT st x = [i,i+1] & i+1<n;
hence thesis;
end;
A2: the InternalRel of Necklace n = A \/ B by Th17;
assume
A3: n > 0;
then n >= 0+1 by NAT_1:13;
then
A4: n-'1 = n-1 by XREAL_1:233;
A = the InternalRel of n-SuccRelStr by Def6;
then
A5: card A = n-1 by A3,Th15;
reconsider A as Relation by A1;
A6: A = {[F(i),G(i)] where i is Element of NAT: P[i]};
A7: A~ = B from Convers(A6);
A8: A misses B
proof
assume A meets B;
then consider x being object such that
A9: x in A and
A10: x in B by XBOOLE_0:3;
consider y,z being object such that
A11: x = [y,z] by A9,RELAT_1:def 1;
[z,y] in A by A7,A10,A11,RELAT_1:def 7;
then consider j be Element of NAT such that
A12: [z,y] = [j,j+1] and
j+1<n;
A13: z = j & y = j+1 by A12,XTUPLE_0:1;
consider i be Element of NAT such that
A14: [y,z] = [i,i+1] and
i+1<n by A9,A11;
y = i & z = i+1 by A14,XTUPLE_0:1;
hence contradiction by A13;
end;
card B = n-1 by A3,Th25;
then
card the InternalRel of Necklace n = card (n-1) +` card (n-1) by A2,A5,A8,
CARD_2:35
.= card ((n-'1) + (n-'1)) by A4,CARD_2:38
.= 2*(n-1) by A4;
hence thesis;
end;
theorem
Necklace 1, ComplRelStr Necklace 1 are_isomorphic
proof
set f = 0 .--> 0;
set S = Necklace 1, T = ComplRelStr S;
A1: the carrier of S = the carrier of T by Def8;
A2: the carrier of S = {0} by Th19,CARD_1:49;
then dom f = the carrier of S & rng f c= the carrier of T
by A1,FUNCOP_1:13;
then f is Relation of the carrier of S, the carrier of T by RELSET_1:4;
then reconsider g = f as Function of S,T
by A2;
A3: rng g = {0} by FUNCOP_1:8;
for y,x being object holds y in rng g & x = g.y iff x in dom g & y = g.x
proof
let x,y being object;
A5: x in dom g & y=g.x implies y in rng g & x = g.y
proof
assume that
A6: x in dom g and
A7: y = g.x;
A8: x = 0 by A6,TARSKI:def 1;
y = 0 by A7;
hence thesis by A3,A8,TARSKI:def 1;
end;
y in rng g & x = g.y implies x in dom g & y=g.x
proof
assume that
A9: y in rng g and
A10: x = g.y;
A11: y = 0 by A3,A9,TARSKI:def 1;
x = 0 by A10;
hence thesis by A11,TARSKI:def 1;
end;
hence thesis by A3,A5;
end;
then reconsider h = g" as Function of T,S by A1,A3,FUNCT_1:32;
A12: h is monotone
proof
let x,y being Element of T;
assume x <= y;
then [x,y] in the InternalRel of T by ORDERS_2:def 5;
then [x,y] in (the InternalRel of S)` \ id (the carrier of S) by Def8;
then not [x,y] in id (the carrier of S) by XBOOLE_0:def 5;
then
A13: not x in (the carrier of S) or x <> y by RELAT_1:def 10;
let a,b being Element of S such that
a = h.x and
b = h.y;
A14: x in (the carrier of T);
A15: the carrier of T = Segm 1 by A1,Th19;
then x in Segm 1 & y in Segm 1;
then reconsider i = x, j = y as Nat;
A16: j = 0 by A15,CARD_1:49,TARSKI:def 1;
A17: i = 0 by A15,CARD_1:49,TARSKI:def 1;
A18: i + 1 <> j & j + 1 <> i & i <> j
proof
hereby
assume
A19: i+1=j or j+1=i;
per cases by A19;
suppose
i+1 = j;
hence contradiction by A15,A17,NAT_1:44;
end;
suppose
j+1=i;
hence contradiction by A15,A16,NAT_1:44;
end;
end;
thus thesis by A13,A14,Def8;
end;
A20: y = 0 by A15,CARD_1:49,TARSKI:def 1;
the carrier of T = {0} by A1,Th19,CARD_1:49;
hence thesis by A18,A20,TARSKI:def 1;
end;
g is monotone
proof
let x,y being Element of S;
assume x <= y;
then
A21: [x,y] in the InternalRel of S by ORDERS_2:def 5;
the carrier of S = Segm 1 by Th19;
then x in Segm 1 & y in Segm 1;
then reconsider i = x, j = y as Nat;
let a,b being Element of T such that
a = g.x and
b = g.y;
the carrier of S = {0} by Th19,CARD_1:49;
then
A22: x = 0 & y = 0 by TARSKI:def 1;
i = j + 1 or j = i + 1 by A21,Th23;
hence thesis by A22;
end;
then g is isomorphic by A12,WAYBEL_0:def 38;
hence thesis;
end;
theorem
Necklace 4, ComplRelStr Necklace 4 are_isomorphic
proof
set g = (0,1) --> (1,3), h = (2,3) --> (0,2), f = g +* h;
set S = Necklace 4, T = ComplRelStr Necklace 4;
A1: rng h = {0,2} by FUNCT_4:64;
A2: rng g = {1,3} by FUNCT_4:64;
A3: rng f c= the carrier of T
proof
let x be object;
assume
A4: x in rng f;
A5: rng f c= rng g \/ rng h by FUNCT_4:17;
rng g \/ rng h = {1,3,0,2} by A2,A1,ENUMSET1:5
.= {0,1,2,3} by ENUMSET1:69;
then x in 4 by A4,A5,CARD_1:52;
then x in the carrier of S by Th19;
hence thesis by Def8;
end;
A6: dom f = dom (0,1) --> (1,3) \/ dom (2,3) --> (0,2) by FUNCT_4:def 1
.= {0,1} \/ dom (2,3) --> (0,2) by FUNCT_4:62
.= {0,1} \/ {2,3} by FUNCT_4:62
.= {0,1,2,3} by ENUMSET1:5;
then
A7: dom f = the carrier of S by Th19,CARD_1:52;
then reconsider f as Function of S,T by A3,FUNCT_2:def 1,RELSET_1:4;
take f;
per cases;
case that
S is non empty and
T is non empty;
set A = the InternalRel of T;
A8: rng (0 .--> 1) misses rng (1 .--> 3)
proof
assume rng (0 .--> 1) meets rng (1 .--> 3);
then consider x being object such that
A9: x in rng (0 .--> 1) and
A10: x in rng (1 .--> 3) by XBOOLE_0:3;
rng (0 .--> 1) = {1} by FUNCOP_1:8;
then rng (1 .--> 3) = {3} & x = 1 by A9,FUNCOP_1:8,TARSKI:def 1;
hence contradiction by A10,TARSKI:def 1;
end;
A11: rng g misses rng h
proof
assume rng g meets rng h;
then consider x being object such that
A12: x in rng g and
A13: x in rng h by XBOOLE_0:3;
x = 1 or x = 3 by A2,A12,TARSKI:def 2;
hence contradiction by A1,A13,TARSKI:def 2;
end;
set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
A14: rng (2 .--> 0) misses rng (3 .--> 2)
proof
assume rng (2 .--> 0) meets rng (3 .--> 2);
then consider x being object such that
A15: x in rng (2 .--> 0) and
A16: x in rng (3 .--> 2) by XBOOLE_0:3;
rng (2 .--> 0) = {0} by FUNCOP_1:8;
then rng (3 .--> 2) = {2} & x = 0 by A15,FUNCOP_1:8,TARSKI:def 1;
hence contradiction by A16,TARSKI:def 1;
end;
h = (2 .--> 0) +* (3 .-->2) by FUNCT_4:def 4;
then
A17: h is one-to-one by A14,FUNCT_4:92;
A18: dom g misses dom h
proof
assume dom g meets dom h;
then consider x being object such that
A19: x in dom g and
A20: x in dom h by XBOOLE_0:3;
x = 0 or x = 1 by A19,TARSKI:def 2;
hence contradiction by A20,TARSKI:def 2;
end;
then
A21: rng f = rng g \/ rng h by FRECHET:35,PARTFUN1:56
.= {1,3,0,2} by A2,A1,ENUMSET1:5
.= {0,1,2,3} by ENUMSET1:69
.= the carrier of S by Th19,CARD_1:52
.= the carrier of T by Def8;
g = (0 .--> 1) +* (1 .-->3) by FUNCT_4:def 4;
then
A22: g is one-to-one by A8,FUNCT_4:92;
hence f is one-to-one by A17,A11,FUNCT_4:92;
then reconsider F = f" as Function of T,S by A21,FUNCT_2:25;
A23: B c= A
proof
set C = the carrier of S;
let x be object;
assume x in B;
then
A24: x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3] or x
= [3,0] by ENUMSET1:def 4;
A25: 2 in C & 3 in C by A6,A7,ENUMSET1:def 2;
0 in C & 1 in C by A6,A7,ENUMSET1:def 2;
then reconsider x9=x as Element of [:C,C:] by A24,A25,ZFMISC_1:87;
not x9 in the InternalRel of S
proof
assume x9 in the InternalRel of S;
then consider i being Element of NAT such that
i+1< 4 and
A26: x9= [i,i+1] or x9= [i+1,i] by Th18;
i=1 & i+1=3 or i=3 & i+1=1 or i=0 & i+1=2 or i=2 & i+1=0 or i=0 &
i+1=3 or i=3 & i+1=0 by A24,A26,XTUPLE_0:1;
hence contradiction;
end;
then
A27: x9 in (the InternalRel of S)` by SUBSET_1:29;
not x in id (the carrier of S) by A24,RELAT_1:def 10;
then x in (the InternalRel of S)` \ id (the carrier of S) by A27,
XBOOLE_0:def 5;
hence thesis by Def8;
end;
thus f is monotone
proof
A28: dom h = {2,3} by FUNCT_4:62;
then 2 in dom h by TARSKI:def 2;
then
A29: f.2 = h.2 by FUNCT_4:13
.= 0 by FUNCT_4:63;
3 in dom h by A28,TARSKI:def 2;
then
A30: f.3 = h.3 by FUNCT_4:13
.= 2 by FUNCT_4:63;
A31: dom g = {0,1} by FUNCT_4:62;
then 0 in dom g by TARSKI:def 2;
then
A32: f.0 = g.0 by A18,FUNCT_4:16
.= 1 by FUNCT_4:63;
1 in dom g by A31,TARSKI:def 2;
then
A33: f.1 = g.1 by A18,FUNCT_4:16
.= 3 by FUNCT_4:63;
let x,y being Element of S;
assume x <= y;
then
A34: [x,y] in the InternalRel of S by ORDERS_2:def 5;
the carrier of S = 4 by Th19;
then x in Segm 4 & y in Segm 4;
then reconsider i = x, j = y as Nat;
A35: i = j + 1 or j = i + 1 by A34,Th23;
let a,b being Element of T such that
A36: a = f.x & b = f.y;
per cases by A6,A7,ENUMSET1:def 2;
suppose
x = 0 & y = 0;
hence thesis by A35;
end;
suppose
x = 0 & y = 1;
then [a,b] in B by A36,A32,A33,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 0 & y = 2;
hence thesis by A35;
end;
suppose
x = 0 & y = 3;
hence thesis by A35;
end;
suppose
x = 1 & y = 0;
then [a,b] in B by A36,A32,A33,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 1 & y = 1;
hence thesis by A35;
end;
suppose
x = 1 & y = 2;
then [a,b] in B by A36,A33,A29,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 1 & y = 3;
hence thesis by A35;
end;
suppose
x = 2 & y = 0;
hence thesis by A35;
end;
suppose
x = 2 & y = 1;
then [a,b] in B by A36,A33,A29,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 2 & y = 2;
hence thesis by A35;
end;
suppose
x = 2 & y = 3;
then [a,b] in B by A36,A29,A30,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 3 & y = 0;
hence thesis by A35;
end;
suppose
x = 3 & y = 1;
hence thesis by A35;
end;
suppose
x = 3 & y = 2;
then [a,b] in B by A36,A29,A30,ENUMSET1:def 4;
hence thesis by A23,ORDERS_2:def 5;
end;
suppose
x = 3 & y = 3;
hence thesis by A35;
end;
end;
take F;
thus F = f";
thus F is monotone
proof
let x,y being Element of T;
assume x <= y;
then [x,y] in the InternalRel of T by ORDERS_2:def 5;
then
A37: [x,y] in (the InternalRel of S)` \ id (the carrier of S) by Def8;
then not [x,y] in id (the carrier of S) by XBOOLE_0:def 5;
then
A38: not x in (the carrier of S) or x <> y by RELAT_1:def 10;
[x,y] in (the InternalRel of S)` implies not [x,y] in (the
InternalRel of S) by XBOOLE_0:def 5;
then
A39: not [x,y] in ({[k,k+1] where k is Element of NAT:k+1 < 4} \/ {[l+1,
l] where l is Element of NAT:l+1 < 4}) by A37,Th17,XBOOLE_0:def 5;
then
A40: not [x,y] in {[k+1,k] where k is Element of NAT:k+1 < 4} by
XBOOLE_0:def 3;
A41: the carrier of T = the carrier of S by Def8
.= Segm 4 by Th19;
then x in Segm 4 & y in Segm 4;
then x is natural & y is natural;
then reconsider i = x, j = y as Element of NAT by ORDINAL1:def 12;
A42: x in (the carrier of T);
A43: not [x,y] in {[k,k+1] where k is Element of NAT:k+1 < 4} by A39,
XBOOLE_0:def 3;
A44: i + 1 <> j & j + 1 <> i & i <> j
proof
hereby
assume
A45: i+1=j or j+1=i;
per cases by A45;
suppose
A46: i+1 = j;
then i+1 < 4 by A41,NAT_1:44;
hence contradiction by A43,A46;
end;
suppose
A47: j+1=i;
then j+1 < 4 by A41,NAT_1:44;
hence contradiction by A40,A47;
end;
end;
thus thesis by A38,A42,Def8;
end;
A48: h" = (0,2) --> (2,3) by Th9;
then
A49: dom (h") = {0,2} by FUNCT_4:62;
then
A50: 0 in dom (h") by TARSKI:def 2;
A51: F.0 = (g" +* h").0 by A22,A17,A18,A11,Th6
.= h".0 by A50,FUNCT_4:13
.= 2 by A48,FUNCT_4:63;
A52: g" = (1,3) --> (0,1) by Th9;
then
A53: dom (g") = {1,3} by FUNCT_4:62;
then
A54: 1 in dom (g") by TARSKI:def 2;
A55: dom (g") misses dom (h")
proof
assume dom (g") meets dom (h");
then consider x being object such that
A56: x in dom (g") and
A57: x in dom (h") by XBOOLE_0:3;
x = 1 or x = 3 by A53,A56,TARSKI:def 2;
hence contradiction by A49,A57,TARSKI:def 2;
end;
A58: F.1 = (g" +* h").1 by A22,A17,A18,A11,Th6
.= g".1 by A55,A54,FUNCT_4:16
.= 0 by A52,FUNCT_4:63;
A59: 2 in dom (h") by A49,TARSKI:def 2;
A60: F.2 = (g" +* h").2 by A22,A17,A18,A11,Th6
.= h".2 by A59,FUNCT_4:13
.= 3 by A48,FUNCT_4:63;
A61: 3 in dom (g") by A53,TARSKI:def 2;
A62: F.3 = (g" +* h").3 by A22,A17,A18,A11,Th6
.= g".3 by A55,A61,FUNCT_4:16
.= 1 by A52,FUNCT_4:63;
let a,b being Element of S such that
A63: a = F.x and
A64: b = F.y;
per cases by A41,CARD_1:52,ENUMSET1:def 2;
suppose
x = 0 & y = 0;
hence thesis by A44;
end;
suppose
x = 0 & y = 1;
hence thesis by A44;
end;
suppose
A65: x = 0 & y = 2;
then b = 2+1 by A64,A60;
then [a,b] in the InternalRel of S by A63,A51,A65,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
A66: x = 0 & y = 3;
then a = 1+1 by A63,A51;
then [a,b] in the InternalRel of S by A64,A62,A66,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
x = 1 & y = 0;
hence thesis by A44;
end;
suppose
x = 1 & y = 1;
hence thesis by A44;
end;
suppose
x = 1 & y = 2;
hence thesis by A44;
end;
suppose
A67: x = 1 & y = 3;
then b = 0+1 by A64,A62;
then [a,b] in the InternalRel of S by A63,A58,A67,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
A68: x = 2 & y = 0;
then a = 2+1 by A63,A60;
then [a,b] in the InternalRel of S by A64,A51,A68,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
x = 2 & y = 1;
hence thesis by A44;
end;
suppose
x = 2 & y = 2;
hence thesis by A44;
end;
suppose
x = 2 & y = 3;
hence thesis by A44;
end;
suppose
A69: x = 3 & y = 0;
then b = 1+1 by A64,A51;
then [a,b] in the InternalRel of S by A63,A62,A69,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
A70: x = 3 & y = 1;
then a = 0+1 by A63,A62;
then [a,b] in the InternalRel of S by A64,A58,A70,Th24;
hence thesis by ORDERS_2:def 5;
end;
suppose
x = 3 & y = 2;
hence thesis by A44;
end;
suppose
x = 3 & y = 3;
hence thesis by A44;
end;
end;
end;
case
S is empty or T is empty;
hence thesis;
end;
end;
theorem
Necklace n, ComplRelStr Necklace n are_isomorphic implies n = 0 or n =
1 or n = 4
proof
assume
A1: Necklace n, ComplRelStr Necklace n are_isomorphic;
set S = Necklace n, T = ComplRelStr S;
card n = n;
then
A2: card [:n,n:] = n*n by CARD_2:46;
assume
A3: not thesis;
n <= 4 implies n = 0 or ... or n = 4;
then n = 2 or n = 3 or n > 4 by A3;
then
A4: card the InternalRel of S = 2*(n-1) by Th26;
A5: n*n - 2*(n-1) - n <> 2*(n-1)
proof
A6: delta(1,-5,4) = (-5)^2 - 4*1*4 by QUIN_1:def 1
.= 9;
assume not thesis;
then 1*n ^2 + (- 5)*n + 4 = 0;
then
n = (- (-5) - sqrt delta(1,-5,4))/(2 * 1) or n = (- (-5) + sqrt delta
(1,-5,4))/(2 * 1) by A6,QUIN_1:15;
then n = (5 - sqrt 3^2)/2 or n = (5 + sqrt 3^2)/2 by A6;
then
A7: n = (5 - 3)/2 or n = (5+3)/2 by SQUARE_1:22;
per cases by A7;
suppose
n =1;
hence contradiction by A3;
end;
suppose
n=4;
hence contradiction by A3;
end;
end;
A8: id (the carrier of S) misses (the InternalRel of S)
proof
assume not thesis;
then consider x being object such that
A9: x in id (the carrier of S) and
A10: x in the InternalRel of S by XBOOLE_0:3;
consider i being Element of NAT such that
i+1 < n and
A11: x = [i,i+1] or x = [i+1,i] by A10,Th18;
consider x1,x2 being object such that
A12: x = [x1,x2] by A9,RELAT_1:def 1;
A13: x1=x2 by A9,A12,RELAT_1:def 10;
per cases by A12,A11;
suppose
[x1,x2] = [i,i+1];
then x1 = i & x2 = i+1 by XTUPLE_0:1;
hence thesis by A13;
end;
suppose
[x1,x2] = [i+1,i];
then x1 = i+1 & x2 = i by XTUPLE_0:1;
hence thesis by A13;
end;
end;
the carrier of S = n by Th19;
then
A14: card (the InternalRel of S)` = n*n - 2*(n-1) by A4,A2,CARD_2:44;
the carrier of S = n & n = card n by Th19;
then
A15: card id (the carrier of S) = n by Th4;
card (the InternalRel of T) = card ((the InternalRel of S)` \ id (the
carrier of S)) by Def8
.= n*n - 2*(n-1) - n by A14,A15,A8,CARD_2:44,XBOOLE_1:86;
hence thesis by A1,A4,A5,Th16;
end;