glibpre0.miz
begin
theorem ::
GLIBPRE0:1
for X,Y,Z be
set st Z
c= X holds (X
\/ (Y
\ Z))
= (X
\/ Y)
proof
let X,Y,Z be
set;
assume
A1: Z
c= X;
A2: (X
\/ (Y
\ Z))
c= (X
\/ Y) by
XBOOLE_1: 9;
now
let x be
object;
assume x
in (X
\/ Y);
per cases by
XBOOLE_0:def 3;
suppose x
in X;
hence x
in (X
\/ (Y
\ Z)) by
XBOOLE_0:def 3;
end;
suppose x
in Y & not x
in Z;
then x
in (Y
\ Z) by
XBOOLE_0:def 5;
hence x
in (X
\/ (Y
\ Z)) by
XBOOLE_0:def 3;
end;
suppose x
in Y & x
in Z;
hence x
in (X
\/ (Y
\ Z)) by
A1,
XBOOLE_0:def 3;
end;
end;
then (X
\/ Y)
c= (X
\/ (Y
\ Z)) by
TARSKI:def 3;
hence thesis by
A2,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:2
Th2: for X,Y,Z be
set holds (X
/\ Z)
misses (Y
\ Z)
proof
let X,Y,Z be
set;
((X
/\ Z)
/\ (Y
\ Z))
= (X
/\ (Z
/\ (Y
\ Z))) by
XBOOLE_1: 16
.= (X
/\ ((Z
/\ Y)
\ (Z
/\ Z))) by
XBOOLE_1: 50
.= (X
/\
{} ) by
XBOOLE_1: 17,
XBOOLE_1: 37
.=
{} ;
hence thesis by
XBOOLE_0:def 7;
end;
theorem ::
GLIBPRE0:3
for x,y be
object holds (
{x, y}
\
{ the
Element of
{x, y}})
=
{} iff x
= y
proof
let x,y be
object;
set z = the
Element of
{x, y};
hereby
assume (
{x, y}
\
{z})
=
{} ;
then
{x, y}
c=
{z} by
XBOOLE_1: 37;
then x
= z & y
= z by
ZFMISC_1: 20;
hence x
= y;
end;
assume x
= y;
then
{x, y}
=
{x} by
ENUMSET1: 29;
then
{z}
=
{x, y} by
TARSKI:def 1;
hence thesis by
XBOOLE_1: 37;
end;
theorem ::
GLIBPRE0:4
for a,b,x,y be
object st a
<> b & x
= the
Element of
{a, b} & y
= the
Element of (
{a, b}
\
{ the
Element of
{a, b}}) holds x
= a & y
= b or x
= b & y
= a
proof
let a,b,x,y be
object;
assume
A1: a
<> b & x
= the
Element of
{a, b} & y
= the
Element of (
{a, b}
\
{ the
Element of
{a, b}});
per cases by
TARSKI:def 2;
suppose
A2: x
= a;
(
{a, b}
\
{a})
=
{b} by
A1,
ZFMISC_1: 17;
hence thesis by
A1,
A2,
TARSKI:def 1;
end;
suppose
A3: x
= b;
(
{a, b}
\
{b})
=
{a} by
A1,
ZFMISC_1: 17;
hence thesis by
A1,
A3,
TARSKI:def 1;
end;
end;
theorem ::
GLIBPRE0:5
for a,b,x,y be
object holds
{a, b}
=
{x, y} iff x
= a & y
= b or x
= b & y
= a by
ZFMISC_1: 22;
theorem ::
GLIBPRE0:6
for X be
set, Y be non
empty
set holds X
c< Y iff X is
proper
Subset of Y by
SUBSET_1:def 6,
XBOOLE_0:def 8;
registration
let X be non
empty
set;
cluster (
id X) -> non
irreflexive;
coherence
proof
ex x be
object st x
in (
field (
id X)) &
[x, x]
in (
id X)
proof
consider x be
object such that
A1: x
in X by
XBOOLE_0:def 1;
take x;
A2: (
field (
id X))
= ((
dom (
id X))
\/ (
rng (
id X))) by
RELAT_1:def 6;
thus x
in (
field (
id X)) by
A1,
A2;
thus
[x, x]
in (
id X) by
A1,
RELAT_1:def 10;
end;
hence (
id X) is non
irreflexive by
RELAT_2:def 2,
RELAT_2:def 10;
end;
cluster
[:X, X:] -> non
irreflexive non
asymmetric;
coherence
proof
ex x be
object st x
in (
field
[:X, X:]) &
[x, x]
in
[:X, X:]
proof
consider x be
object such that
A3: x
in X by
XBOOLE_0:def 1;
take x;
(
field
[:X, X:])
= (X
\/ X) by
WELLSET1: 2;
hence x
in (
field
[:X, X:]) by
A3;
thus
[x, x]
in
[:X, X:] by
A3,
ZFMISC_1:def 2;
end;
hence thesis by
RELAT_2:def 2,
RELAT_2:def 10;
end;
cluster non
irreflexive non
asymmetric for
Relation of X;
existence
proof
take R =
[:X, X:];
R
c= R;
hence thesis;
end;
cluster
symmetric
irreflexive non
total for
Relation of X;
existence
proof
take the
empty
Relation of X;
thus thesis;
end;
cluster
symmetric non
irreflexive non
empty for
Relation of X;
existence
proof
take (
id X);
thus thesis;
end;
end
registration
let X be non
trivial
set;
cluster (
id X) -> non
connected;
coherence
proof
set x = the
Element of X;
set y = the
Element of (X
\
{x});
[x, x]
in (
id X) &
[y, y]
in (
id X) by
RELAT_1:def 10;
then
A1: x
in (
field (
id X)) & y
in (
field (
id X)) by
RELAT_1: 15;
not y
in
{x} by
XBOOLE_0:def 5;
then
A2: y
<> x by
TARSKI:def 1;
then not
[x, y]
in (
id X) & not
[y, x]
in (
id X) by
RELAT_1:def 10;
hence thesis by
A1,
A2,
RELAT_2:def 6,
RELAT_2:def 14;
end;
cluster
symmetric non
connected for
Relation of X;
existence
proof
take (
id X);
thus thesis;
end;
cluster
[:X, X:] -> non
antisymmetric;
coherence
proof
set x = the
Element of X;
set y = the
Element of (X
\
{x});
A3:
[x, y]
in
[:X, X:] &
[y, x]
in
[:X, X:] by
ZFMISC_1: 87;
then
A4: x
in (
field
[:X, X:]) & y
in (
field
[:X, X:]) by
RELAT_1: 15;
not y
in
{x} by
XBOOLE_0:def 5;
then x
<> y by
TARSKI:def 1;
hence thesis by
A3,
A4,
RELAT_2:def 4,
RELAT_2:def 12;
end;
cluster non
antisymmetric for
Relation of X;
existence
proof
take
[:X, X:];
[:X, X:]
c=
[:X, X:];
hence thesis;
end;
end
theorem ::
GLIBPRE0:7
for R,S be
Relation, X be
set holds ((R
\/ S)
.: X)
= ((R
.: X)
\/ (S
.: X))
proof
let R,S be
Relation, X be
set;
now
let y be
object;
hereby
assume y
in ((R
\/ S)
.: X);
then
consider x be
object such that
A1:
[x, y]
in (R
\/ S) & x
in X by
RELAT_1:def 13;
per cases by
A1,
XBOOLE_0:def 3;
suppose
[x, y]
in R;
then y
in (R
.: X) by
A1,
RELAT_1:def 13;
hence y
in ((R
.: X)
\/ (S
.: X)) by
XBOOLE_0:def 3;
end;
suppose
[x, y]
in S;
then y
in (S
.: X) by
A1,
RELAT_1:def 13;
hence y
in ((R
.: X)
\/ (S
.: X)) by
XBOOLE_0:def 3;
end;
end;
assume y
in ((R
.: X)
\/ (S
.: X));
per cases by
XBOOLE_0:def 3;
suppose y
in (R
.: X);
then
consider x be
object such that
A2:
[x, y]
in R & x
in X by
RELAT_1:def 13;
[x, y]
in (R
\/ S) by
A2,
XBOOLE_0:def 3;
hence y
in ((R
\/ S)
.: X) by
A2,
RELAT_1:def 13;
end;
suppose y
in (S
.: X);
then
consider x be
object such that
A3:
[x, y]
in S & x
in X by
RELAT_1:def 13;
[x, y]
in (R
\/ S) by
A3,
XBOOLE_0:def 3;
hence y
in ((R
\/ S)
.: X) by
A3,
RELAT_1:def 13;
end;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:8
for R,S be
Relation, Y be
set holds ((R
\/ S)
" Y)
= ((R
" Y)
\/ (S
" Y))
proof
let R,S be
Relation, Y be
set;
now
let x be
object;
hereby
assume x
in ((R
\/ S)
" Y);
then
consider y be
object such that
A1:
[x, y]
in (R
\/ S) & y
in Y by
RELAT_1:def 14;
per cases by
A1,
XBOOLE_0:def 3;
suppose
[x, y]
in R;
then x
in (R
" Y) by
A1,
RELAT_1:def 14;
hence x
in ((R
" Y)
\/ (S
" Y)) by
XBOOLE_0:def 3;
end;
suppose
[x, y]
in S;
then x
in (S
" Y) by
A1,
RELAT_1:def 14;
hence x
in ((R
" Y)
\/ (S
" Y)) by
XBOOLE_0:def 3;
end;
end;
assume x
in ((R
" Y)
\/ (S
" Y));
per cases by
XBOOLE_0:def 3;
suppose x
in (R
" Y);
then
consider y be
object such that
A2:
[x, y]
in R & y
in Y by
RELAT_1:def 14;
[x, y]
in (R
\/ S) by
A2,
XBOOLE_0:def 3;
hence x
in ((R
\/ S)
" Y) by
A2,
RELAT_1:def 14;
end;
suppose x
in (S
" Y);
then
consider y be
object such that
A3:
[x, y]
in S & y
in Y by
RELAT_1:def 14;
[x, y]
in (R
\/ S) by
A3,
XBOOLE_0:def 3;
hence x
in ((R
\/ S)
" Y) by
A3,
RELAT_1:def 14;
end;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:9
for R be
Relation, X,Y be
set holds ((Y
|` R)
| X)
= ((Y
|` R)
/\ (R
| X))
proof
let R be
Relation, X,Y be
set;
now
let z be
object;
hereby
assume
A1: z
in ((Y
|` R)
| X);
then
consider x,y be
object such that
A2: z
=
[x, y] by
RELAT_1:def 1;
A3: z
in (Y
|` R) & x
in X by
A1,
A2,
RELAT_1:def 11;
then z
in R by
A2,
RELAT_1:def 12;
then z
in (R
| X) by
A2,
A3,
RELAT_1:def 11;
hence z
in ((Y
|` R)
/\ (R
| X)) by
A3,
XBOOLE_0:def 4;
end;
assume z
in ((Y
|` R)
/\ (R
| X));
then
A4: z
in (Y
|` R) & z
in (R
| X) by
XBOOLE_0:def 4;
then
consider x,y be
object such that
A5: z
=
[x, y] by
RELAT_1:def 1;
x
in X by
A4,
A5,
RELAT_1:def 11;
hence z
in ((Y
|` R)
| X) by
A4,
A5,
RELAT_1:def 11;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:10
for R be
symmetric
Relation, x be
object holds (
Im (R,x))
= (
Coim (R,x))
proof
let R be
symmetric
Relation, x be
object;
thus (
Im (R,x))
= (R
.:
{x}) by
RELAT_1:def 16
.= (R
"
{x}) by
FRIENDS1: 2
.= (
Coim (R,x)) by
RELAT_1:def 17;
end;
theorem ::
GLIBPRE0:11
for X be
set, R be
Relation of X holds R is
irreflexive iff (
id X)
misses R
proof
let X be
set, R be
Relation of X;
hereby
assume
A1: R is
irreflexive;
assume (
id X)
meets R;
then ((
id X)
/\ R)
<>
{} by
XBOOLE_0:def 7;
then
consider z be
object such that
A2: z
in ((
id X)
/\ R) by
XBOOLE_0:def 1;
consider x,y be
object such that
A3: z
=
[x, y] by
A2,
RELAT_1:def 1;
A4:
[x, y]
in (
id X) &
[x, y]
in R by
A2,
A3,
XBOOLE_0:def 4;
then x
= y & x
in (
field R) by
RELAT_1:def 10,
RELAT_1: 15;
hence contradiction by
A1,
A4,
RELAT_2:def 2,
RELAT_2:def 10;
end;
assume
A5: (
id X)
misses R;
(
field R)
c= (X
\/ X) by
RELSET_1: 8;
then (
id (
field R))
misses R by
A5,
FUNCT_4: 3,
XBOOLE_1: 63;
hence thesis by
RELAT_2: 2;
end;
theorem ::
GLIBPRE0:12
for x,y be
object holds (
{
[x, y]} qua
Relation
~ )
=
{
[y, x]}
proof
let x,y be
object;
set Z = (
{
[x, y]} qua
Relation
~ );
now
let a,b be
object;
hereby
assume
[a, b]
in Z;
then
[b, a]
in
{
[x, y]} by
RELAT_1:def 7;
then
[b, a]
=
[x, y] by
TARSKI:def 1;
then b
= x & a
= y by
XTUPLE_0: 1;
hence
[a, b]
in
{
[y, x]} by
TARSKI:def 1;
end;
assume
[a, b]
in
{
[y, x]};
then
[a, b]
=
[y, x] by
TARSKI:def 1;
then a
= y & b
= x by
XTUPLE_0: 1;
then
[b, a]
in
{
[x, y]} by
TARSKI:def 1;
hence
[a, b]
in Z by
RELAT_1:def 7;
end;
hence thesis by
RELAT_1:def 2;
end;
theorem ::
GLIBPRE0:13
for X be
set, x,y be
object, R be
symmetric
Relation of X holds
[x, y]
in R implies
[y, x]
in R
proof
let X be
set, x,y be
object, R be
symmetric
Relation of X;
assume
A1:
[x, y]
in R;
then x
in (
field R) & y
in (
field R) by
RELAT_1: 15;
hence thesis by
A1,
RELAT_2:def 3,
RELAT_2:def 11;
end;
registration
let a,b be
Cardinal;
cluster (a
/\ b) ->
cardinal;
coherence by
ORDINAL3: 13;
cluster (a
\/ b) ->
cardinal;
coherence by
ORDINAL3: 12;
end
registration
let X be
c=-linear
set;
cluster (
RelIncl X) ->
connected;
coherence
proof
now
let x,y be
object;
assume x
in (
field (
RelIncl X)) & y
in (
field (
RelIncl X)) & x
<> y;
then
A1: x
in X & y
in X by
WELLORD2:def 1;
reconsider A = x, B = y as
set by
TARSKI: 1;
per cases by
A1,
ORDINAL1:def 8,
XBOOLE_0:def 9;
suppose A
c= B;
hence
[x, y]
in (
RelIncl X) or
[y, x]
in (
RelIncl X) by
A1,
WELLORD2:def 1;
end;
suppose B
c= A;
hence
[x, y]
in (
RelIncl X) or
[y, x]
in (
RelIncl X) by
A1,
WELLORD2:def 1;
end;
end;
hence thesis by
RELAT_2:def 6,
RELAT_2:def 14;
end;
end
registration
let X be
c=-linear
set;
cluster (
InclPoset X) ->
connected;
coherence
proof
(
field (
RelIncl X))
= X by
ORDERS_1: 12;
hence thesis by
RELAT_2:def 14,
ORDERS_5:def 1;
end;
end
theorem ::
GLIBPRE0:14
Th15: for X be non
empty
set st for a be
set st a
in X holds a is
cardinal
number holds ex A be
Cardinal st A
in X & A
= (
meet X)
proof
let X be non
empty
set;
assume
A1: for a be
set st a
in X holds a is
cardinal
number;
defpred
P[
Ordinal] means $1
in X & $1 is
cardinal
number;
A2: ex A be
Ordinal st
P[A]
proof
consider A be
object such that
A3: A
in X by
XBOOLE_0:def 1;
reconsider A as
Ordinal by
A1,
A3;
take A;
thus thesis by
A1,
A3;
end;
consider A be
Ordinal such that
A4:
P[A] & for B be
Ordinal st
P[B] holds A
c= B from
ORDINAL1:sch 1(
A2);
reconsider A as
Cardinal by
A4;
take A;
thus A
in X by
A4;
A5: (
meet X)
c= A by
A4,
SETFAM_1: 3;
now
let x be
object;
assume
A6: x
in A;
now
let Y be
set;
assume
A7: Y
in X;
then
reconsider B = Y as
Ordinal by
A1;
B
in X & B is
cardinal
number by
A1,
A7;
then A
c= B by
A4;
hence x
in Y by
A6;
end;
hence x
in (
meet X) by
SETFAM_1:def 1;
end;
then A
c= (
meet X) by
TARSKI:def 3;
hence A
= (
meet X) by
A5,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:15
for X be
set st for a be
set st a
in X holds a is
cardinal
number holds (
meet X) is
cardinal
number
proof
let X be
set;
assume
A1: for a be
set st a
in X holds a is
cardinal
number;
per cases ;
suppose X
=
{} ;
hence thesis by
SETFAM_1:def 1;
end;
suppose X
<>
{} ;
then
consider A be
Cardinal such that
A2: A
in X & A
= (
meet X) by
A1,
Th15;
thus thesis by
A2;
end;
end;
registration
let f be
Cardinal-yielding
Function, x be
object;
cluster (f
. x) ->
cardinal;
coherence
proof
per cases ;
suppose x
in (
dom f);
hence thesis by
CARD_3:def 1;
end;
suppose not x
in (
dom f);
hence thesis by
FUNCT_1:def 2;
end;
end;
end
Th19: for X be
functional
set holds (
meet X) is
Function
proof
let X be
functional
set;
per cases ;
suppose
A1: X
<>
{} ;
consider Z be
object such that
A2: Z
in X by
A1,
XBOOLE_0:def 1;
reconsider Z as
set by
TARSKI: 1;
A3:
now
let x be
object;
assume x
in (
meet X);
then x
in Z by
A2,
SETFAM_1:def 1;
then
consider y,z be
object such that
A4: x
=
[y, z] by
A2,
RELAT_1:def 1;
take y, z;
thus x
=
[y, z] by
A4;
end;
now
let x,y1,y2 be
object;
assume
[x, y1]
in (
meet X) &
[x, y2]
in (
meet X);
then
[x, y1]
in Z &
[x, y2]
in Z by
A2,
SETFAM_1:def 1;
hence y1
= y2 by
A2,
FUNCT_1:def 1;
end;
hence thesis by
A3,
RELAT_1:def 1,
FUNCT_1:def 1;
end;
suppose X
=
{} ;
hence thesis by
SETFAM_1:def 1;
end;
end;
registration
let X be
functional
set;
cluster (
meet X) ->
Function-like
Relation-like;
coherence by
Th19;
end
theorem ::
GLIBPRE0:16
Th20: for X be
set holds 4
c= (
card X) iff ex w,x,y,z be
object st w
in X & x
in X & y
in X & z
in X & w
<> x & w
<> y & w
<> z & x
<> y & x
<> z & y
<> z
proof
let X be
set;
thus 4
c= (
card X) implies ex w,x,y,z be
object st w
in X & x
in X & y
in X & z
in X & w
<> x & w
<> y & w
<> z & x
<> y & x
<> z & y
<> z
proof
assume 4
c= (
card X);
then (
card 4)
c= (
card X);
then
consider f be
Function such that
A1: f is
one-to-one and
A2: (
dom f)
= 4 and
A3: (
rng f)
c= X by
CARD_1: 10;
take w = (f
.
0 );
take x = (f
. 1);
take y = (f
. 2);
take z = (f
. 3);
A4:
0
in (
dom f) by
A2,
ENUMSET1:def 2,
CARD_1: 52;
then (f
.
0 )
in (
rng f) by
FUNCT_1:def 3;
hence w
in X by
A3;
A5: 1
in (
dom f) by
A2,
ENUMSET1:def 2,
CARD_1: 52;
then (f
. 1)
in (
rng f) by
FUNCT_1:def 3;
hence x
in X by
A3;
A6: 2
in (
dom f) by
A2,
ENUMSET1:def 2,
CARD_1: 52;
then (f
. 2)
in (
rng f) by
FUNCT_1:def 3;
hence y
in X by
A3;
A7: 3
in (
dom f) by
A2,
ENUMSET1:def 2,
CARD_1: 52;
then (f
. 3)
in (
rng f) by
FUNCT_1:def 3;
hence z
in X by
A3;
thus w
<> x by
A1,
A4,
A5,
FUNCT_1:def 4;
thus w
<> y by
A1,
A4,
A6,
FUNCT_1:def 4;
thus w
<> z by
A1,
A4,
A7,
FUNCT_1:def 4;
thus x
<> y by
A1,
A5,
A6,
FUNCT_1:def 4;
thus x
<> z by
A1,
A5,
A7,
FUNCT_1:def 4;
thus thesis by
A1,
A6,
A7,
FUNCT_1:def 4;
end;
given w,x,y,z be
object such that
A8: w
in X & x
in X & y
in X & z
in X and
A9: w
<> x & w
<> y & w
<> z & x
<> y & x
<> z & y
<> z;
for a be
object st a
in
{w, x, y, z} holds a
in X by
A8,
ENUMSET1:def 2;
then (
card
{w, x, y, z})
c= (
card X) by
TARSKI:def 3,
CARD_1: 11;
hence thesis by
A9,
CARD_2: 59;
end;
theorem ::
GLIBPRE0:17
Th21: for X be
set st 4
c= (
card X) holds for w,x,y be
object holds ex z be
object st z
in X & w
<> z & x
<> z & y
<> z
proof
let X be
set;
assume 4
c= (
card X);
then
consider a,b,c,d be
object such that
A1: a
in X and
A2: b
in X and
A3: c
in X and
A4: d
in X and
A5: a
<> b & a
<> c & a
<> d & b
<> c & b
<> d & d
<> c by
Th20;
let w,x,y be
object;
per cases ;
suppose w
<> a & x
<> a & y
<> a;
hence thesis by
A1;
end;
suppose w
<> a & x
<> a & y
= a & w
<> b & x
<> b;
hence thesis by
A2,
A5;
end;
suppose w
<> a & x
<> a & y
= a & w
<> b & x
= b & w
<> c;
hence thesis by
A3,
A5;
end;
suppose w
<> a & x
<> a & y
= a & w
<> b & x
= b & w
= c;
hence thesis by
A4,
A5;
end;
suppose w
<> a & x
<> a & y
= a & w
= b & x
<> c;
hence thesis by
A3,
A5;
end;
suppose w
<> a & x
<> a & y
= a & w
= b & x
= c;
hence thesis by
A4,
A5;
end;
suppose w
<> a & x
= a & w
<> b & y
<> b;
hence thesis by
A2,
A5;
end;
suppose w
<> a & x
= a & w
<> b & y
= b & w
<> c;
hence thesis by
A3,
A5;
end;
suppose w
<> a & x
= a & w
<> b & y
= b & w
= c;
hence thesis by
A4,
A5;
end;
suppose w
<> a & x
= a & w
= b & y
<> c;
hence thesis by
A3,
A5;
end;
suppose w
<> a & x
= a & w
= b & y
= c;
hence thesis by
A4,
A5;
end;
suppose w
= a & x
<> b & y
<> b;
hence thesis by
A2,
A5;
end;
suppose w
= a & x
<> b & y
= b & x
<> c;
hence thesis by
A3,
A5;
end;
suppose w
= a & x
<> b & y
= b & x
= c;
hence thesis by
A4,
A5;
end;
suppose w
= a & x
= b & y
<> c;
hence thesis by
A3,
A5;
end;
suppose w
= a & x
= b & y
= c;
hence thesis by
A4,
A5;
end;
end;
theorem ::
GLIBPRE0:18
for X be
set holds (
singletons X)
misses (
2Set X)
proof
let X be
set;
assume (
singletons X)
meets (
2Set X);
then
consider x be
object such that
A1: x
in ((
singletons X)
/\ (
2Set X)) by
XBOOLE_0: 4;
A2: x
in (
singletons X) & x
in (
2Set X) by
A1,
XBOOLE_0:def 4;
then
consider Y be
Subset of X such that
A3: x
= Y & Y is 1
-element;
consider Z be
Subset of X such that
A4: x
= Z & (
card Z)
= 2 by
A2;
thus contradiction by
A3,
A4,
CARD_1:def 7;
end;
theorem ::
GLIBPRE0:19
Th23: for X,Y be
set st (
card X)
= (
card Y) holds (
card (
2Set X))
= (
card (
2Set Y))
proof
let X,Y be
set;
assume (
card X)
= (
card Y);
then
consider g be
Function such that
A1: g is
one-to-one & (
dom g)
= X & (
rng g)
= Y by
CARD_1: 5,
WELLORD2:def 4;
deffunc
E1(
set) = the
Element of $1;
deffunc
E2(
set) = the
Element of ($1
\
{
E1($1)});
deffunc
F(
object) =
{(g
.
E1(In)), (g
.
E2(In))};
consider f be
Function such that
A2: (
dom f)
= (
2Set X) & for x be
object st x
in (
2Set X) holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
now
let y be
object;
hereby
assume y
in (
rng f);
then
consider x be
object such that
A3: x
in (
dom f) & (f
. x)
= y by
FUNCT_1:def 3;
consider X9 be
Subset of X such that
A4: x
= X9 & (
card X9)
= 2 by
A2,
A3;
A5: y
=
{(g
.
E1(In)), (g
.
E2(In))} by
A2,
A3,
A4
.=
{(g
.
E1(X9)), (g
.
E2(X9))};
X9 is non
trivial
proof
assume
A6: X9 is
trivial;
per cases ;
suppose X9 is
empty;
hence contradiction by
A4;
end;
suppose X9 is non
empty;
then (
card X9)
= 1 by
A6,
CARD_1:def 7;
hence contradiction by
A4;
end;
end;
then X9
<>
{} & (X9
\
{
E1(X9)})
<>
{} by
ZFMISC_1: 139;
then
A7:
E1(X9)
in X9 &
E2(X9)
in (X9
\
{
E1(X9)});
then
E2(X9)
in X9 & not
E2(X9)
in
{
E1(X9)} by
XBOOLE_0:def 5;
then
E2(X9)
in X9 &
E1(X9)
<>
E2(X9) by
TARSKI:def 1;
then
A8: (g
.
E1(X9))
<> (g
.
E2(X9)) by
A1,
A7,
FUNCT_1:def 4;
(g
.
E1(X9))
in Y & (g
.
E2(X9))
in Y by
A1,
A7,
FUNCT_1: 3;
then
A9:
{(g
.
E1(X9)), (g
.
E2(X9))}
c= Y by
ZFMISC_1: 32;
(
card
{(g
.
E1(X9)), (g
.
E2(X9))})
= 2 by
A8,
CARD_2: 57;
hence y
in (
2Set Y) by
A5,
A9;
end;
assume y
in (
2Set Y);
then
consider Y9 be
Subset of Y such that
A10: y
= Y9 & (
card Y9)
= 2;
consider y1,y2 be
object such that
A11: y1
<> y2 & Y9
=
{y1, y2} by
A10,
CARD_2: 60;
y1
in Y9 & y2
in Y9 by
A11,
TARSKI:def 2;
then
A12: y1
in (
rng g) & y2
in (
rng g) by
A1;
then
consider x1 be
object such that
A13: x1
in (
dom g) & (g
. x1)
= y1 by
FUNCT_1:def 3;
consider x2 be
object such that
A14: x2
in (
dom g) & (g
. x2)
= y2 by
A12,
FUNCT_1:def 3;
A15: x1
<> x2 by
A11,
A13,
A14;
reconsider X9 =
{x1, x2} as
Subset of X by
A1,
A13,
A14,
ZFMISC_1: 32;
(
card X9)
= 2 by
A15,
CARD_2: 57;
then
A16: X9
in (
2Set X);
per cases by
TARSKI:def 2;
suppose
A17:
E1(X9)
= x1;
then (X9
\
{
E1(X9)})
=
{x2} by
A15,
ZFMISC_1: 17;
then
A18:
E2(X9)
= x2 by
TARSKI:def 1;
(f
. X9)
=
{(g
.
E1(In)), (g
.
E2(In))} by
A2,
A16
.= y by
A10,
A11,
A13,
A14,
A17,
A18;
hence y
in (
rng f) by
A2,
A16,
FUNCT_1: 3;
end;
suppose
A19:
E1(X9)
= x2;
then (X9
\
{
E1(X9)})
=
{x1} by
A15,
ZFMISC_1: 17;
then
A20:
E2(X9)
= x1 by
TARSKI:def 1;
(f
. X9)
=
{(g
.
E1(In)), (g
.
E2(In))} by
A2,
A16
.= y by
A10,
A11,
A13,
A14,
A19,
A20;
hence y
in (
rng f) by
A2,
A16,
FUNCT_1: 3;
end;
end;
then
A21: (
rng f)
= (
2Set Y) by
TARSKI: 2;
now
let x1,x2 be
object;
assume
A22: x1
in (
dom f) & x2
in (
dom f) & (f
. x1)
= (f
. x2);
then
consider X1 be
Subset of X such that
A23: x1
= X1 & (
card X1)
= 2 by
A2;
consider X2 be
Subset of X such that
A24: x2
= X2 & (
card X2)
= 2 by
A2,
A22;
A25: (f
. x1)
=
{(g
.
E1(In)), (g
.
E2(In))} by
A2,
A22,
A23
.=
{(g
.
E1(X1)), (g
.
E2(X1))};
A26: (f
. x2)
=
{(g
.
E1(In)), (g
.
E2(In))} by
A2,
A22,
A24
.=
{(g
.
E1(X2)), (g
.
E2(X2))};
X1 is non
trivial
proof
assume
A27: X1 is
trivial;
per cases ;
suppose X1 is
empty;
hence contradiction by
A23;
end;
suppose X1 is non
empty;
then (
card X1)
= 1 by
A27,
CARD_1:def 7;
hence contradiction by
A23;
end;
end;
then X1
<>
{} & (X1
\
{
E1(X1)})
<>
{} by
ZFMISC_1: 139;
then
A28:
E1(X1)
in X1 &
E2(X1)
in (X1
\
{
E1(X1)});
then
E2(X1)
in X1 & not
E2(X1)
in
{
E1(X1)} by
XBOOLE_0:def 5;
then
A29:
E2(X1)
in X1 &
E2(X1)
<>
E1(X1) by
TARSKI:def 1;
A30:
E1(X1)
in X &
E2(X1)
in X by
A28;
X2 is non
trivial
proof
assume
A31: X2 is
trivial;
per cases ;
suppose X2 is
empty;
hence contradiction by
A24;
end;
suppose X2 is non
empty;
then (
card X2)
= 1 by
A31,
CARD_1:def 7;
hence contradiction by
A24;
end;
end;
then X2
<>
{} & (X2
\
{
E1(X2)})
<>
{} by
ZFMISC_1: 139;
then
A32:
E1(X2)
in X2 &
E2(X2)
in (X2
\
{
E1(X2)});
then
E2(X2)
in X2 & not
E2(X2)
in
{
E1(X2)} by
XBOOLE_0:def 5;
then
A33:
E2(X2)
in X2 &
E2(X2)
<>
E1(X2) by
TARSKI:def 1;
A34:
E1(X2)
in X &
E2(X2)
in X by
A32;
A35: X1 is
finite & X2 is
finite by
A23,
A24;
{
E1(X1),
E2(X1)}
c= X1 & (
card
{
E1(X1),
E2(X1)})
= 2 by
A29,
ZFMISC_1: 32,
CARD_2: 57;
then
A36:
{
E1(X1),
E2(X1)}
= X1 by
A23,
A35,
CARD_2: 102;
{
E1(X2),
E2(X2)}
c= X2 & (
card
{
E1(X2),
E2(X2)})
= 2 by
A33,
ZFMISC_1: 32,
CARD_2: 57;
then
A37:
{
E1(X2),
E2(X2)}
= X2 by
A24,
A35,
CARD_2: 102;
A38: (f
. x1)
in (
rng f) & (f
. x2)
in (
rng f) by
A22,
FUNCT_1: 3;
then
consider Y1 be
Subset of Y such that
A39: (f
. x1)
= Y1 & (
card Y1)
= 2 by
A21;
consider Y2 be
Subset of Y such that
A40: (f
. x2)
= Y2 & (
card Y2)
= 2 by
A21,
A38;
A41: (g
.
E1(X1))
<> (g
.
E2(X1))
proof
assume (g
.
E1(X1))
= (g
.
E2(X1));
then (f
. x1)
=
{(g
.
E1(X1))} by
A25,
ENUMSET1: 29;
hence contradiction by
A39,
CARD_1: 30;
end;
A42: (g
.
E1(X2))
<> (g
.
E2(X2))
proof
assume (g
.
E1(X2))
= (g
.
E2(X2));
then (f
. x2)
=
{(g
.
E1(X2))} by
A26,
ENUMSET1: 29;
hence contradiction by
A40,
CARD_1: 30;
end;
A43:
{(g
.
E1(X1)), (g
.
E2(X1))}
=
{(g
.
E1(X2)), (g
.
E2(X2))} by
A22,
A25,
A26;
per cases by
ZFMISC_1: 6;
suppose
A44: (g
.
E1(X1))
= (g
.
E1(X2));
then
A45:
E1(X1)
=
E1(X2) by
A1,
A30,
A34,
FUNCT_1:def 4;
(
{(g
.
E1(X1)), (g
.
E2(X1))}
\
{(g
.
E1(X1))})
=
{(g
.
E2(X1))} by
A41,
ZFMISC_1: 17;
then
{(g
.
E2(X1))}
=
{(g
.
E2(X2))} by
A42,
A43,
A44,
ZFMISC_1: 17;
then
E2(X1)
=
E2(X2) by
A1,
A28,
A32,
FUNCT_1:def 4,
ZFMISC_1: 3;
hence x1
= x2 by
A23,
A24,
A36,
A37,
A45;
end;
suppose
A46: (g
.
E1(X1))
= (g
.
E2(X2));
then
A47:
E1(X1)
=
E2(X2) by
A1,
A28,
A32,
FUNCT_1:def 4;
(
{(g
.
E1(X1)), (g
.
E2(X1))}
\
{(g
.
E1(X1))})
=
{(g
.
E2(X1))} by
A41,
ZFMISC_1: 17;
then
{(g
.
E2(X1))}
=
{(g
.
E1(X2))} by
A42,
A43,
A46,
ZFMISC_1: 17;
then
E2(X1)
=
E1(X2) by
A1,
A28,
A32,
FUNCT_1:def 4,
ZFMISC_1: 3;
hence x1
= x2 by
A23,
A24,
A36,
A37,
A47;
end;
end;
hence thesis by
A2,
A21,
FUNCT_1:def 4,
CARD_1: 70;
end;
theorem ::
GLIBPRE0:20
for X be
finite
set holds (
card (
2Set X))
= ((
card X)
choose 2)
proof
let X be
finite
set;
(
card (
card X))
= (
card (
Seg (
card X))) by
FINSEQ_1: 55;
then (
card (
2Set X))
= (
card (
2Set (
Seg (
card X)))) by
Th23;
hence thesis by
MATRIX13: 10;
end;
begin
theorem ::
GLIBPRE0:21
Th25: for G be
_Graph, v be
Vertex of G, e,w be
object st v is
isolated holds not e
Joins (v,w,G)
proof
let G be
_Graph, v be
Vertex of G, e,w be
object;
assume v is
isolated;
then not e
in (v
.edgesInOut() ) by
GLIB_000:def 49;
hence thesis by
GLIB_000: 62;
end;
theorem ::
GLIBPRE0:22
Th26: for G be
_Graph, v be
Vertex of G, e,w be
object st v is
isolated holds not e
DJoins (v,w,G) & not e
DJoins (w,v,G)
proof
let G be
_Graph, v be
Vertex of G, e,w be
object;
assume
A1: v is
isolated;
assume e
DJoins (v,w,G) or e
DJoins (w,v,G);
per cases ;
suppose e
DJoins (v,w,G);
then e
Joins (v,w,G) by
GLIB_000: 16;
hence contradiction by
A1,
Th25;
end;
suppose e
DJoins (w,v,G);
then e
Joins (v,w,G) by
GLIB_000: 16;
hence contradiction by
A1,
Th25;
end;
end;
theorem ::
GLIBPRE0:23
for G be
_Graph, v be
Vertex of G holds v is
isolated iff not v
in ((
rng (
the_Source_of G))
\/ (
rng (
the_Target_of G)))
proof
let G be
_Graph, v be
Vertex of G;
hereby
assume
A1: v is
isolated;
assume v
in ((
rng (
the_Source_of G))
\/ (
rng (
the_Target_of G)));
per cases by
XBOOLE_0:def 3;
suppose v
in (
rng (
the_Source_of G));
then
consider e be
object such that
A2: e
in (
dom (
the_Source_of G)) & ((
the_Source_of G)
. e)
= v by
FUNCT_1:def 3;
e
DJoins (v,((
the_Target_of G)
. e),G) by
A2,
GLIB_000:def 14;
hence contradiction by
A1,
Th26;
end;
suppose v
in (
rng (
the_Target_of G));
then
consider e be
object such that
A3: e
in (
dom (
the_Target_of G)) & ((
the_Target_of G)
. e)
= v by
FUNCT_1:def 3;
e
DJoins (((
the_Source_of G)
. e),v,G) by
A3,
GLIB_000:def 14;
hence contradiction by
A1,
Th26;
end;
end;
assume
A4: not v
in ((
rng (
the_Source_of G))
\/ (
rng (
the_Target_of G)));
assume v is non
isolated;
then (v
.edgesInOut() )
<>
{} by
GLIB_000:def 49;
then
consider e be
object such that
A5: e
in (v
.edgesInOut() ) by
XBOOLE_0:def 1;
A6: e
in (
the_Edges_of G) & (((
the_Source_of G)
. e)
= v or ((
the_Target_of G)
. e)
= v) by
A5,
GLIB_000: 61;
per cases ;
suppose
A7: ((
the_Source_of G)
. e)
= v;
e
in (
dom (
the_Source_of G)) by
A6,
FUNCT_2:def 1;
then v
in (
rng (
the_Source_of G)) by
A7,
FUNCT_1: 3;
hence contradiction by
A4,
XBOOLE_0:def 3;
end;
suppose
A8: ((
the_Target_of G)
. e)
= v;
e
in (
dom (
the_Target_of G)) by
A6,
FUNCT_2:def 1;
then v
in (
rng (
the_Target_of G)) by
A8,
FUNCT_1: 3;
hence contradiction by
A4,
XBOOLE_0:def 3;
end;
end;
theorem ::
GLIBPRE0:24
for G be
_Graph, v be
Vertex of G, e be
object st v is
endvertex holds not e
Joins (v,v,G)
proof
let G be
_Graph, v be
Vertex of G, e be
object;
assume v is
endvertex;
then
consider e0 be
object such that
A1: (v
.edgesInOut() )
=
{e0} & not e0
Joins (v,v,G) by
GLIB_000:def 51;
assume
A2: e
Joins (v,v,G);
then e
in (v
.edgesInOut() ) by
GLIB_000: 62;
hence contradiction by
A1,
A2,
TARSKI:def 1;
end;
theorem ::
GLIBPRE0:25
for G be
_Graph, v be
Vertex of G holds (v
.edgesIn() )
= ((
the_Target_of G)
"
{v}) & (v
.edgesOut() )
= ((
the_Source_of G)
"
{v})
proof
let G be
_Graph, v be
Vertex of G;
now
let e be
object;
hereby
assume e
in (v
.edgesIn() );
then
A1: e
in (
the_Edges_of G) & ((
the_Target_of G)
. e)
= v by
GLIB_000: 56;
then
A2: e
in (
dom (
the_Target_of G)) by
FUNCT_2:def 1;
((
the_Target_of G)
. e)
in
{v} by
A1,
TARSKI:def 1;
hence e
in ((
the_Target_of G)
"
{v}) by
A2,
FUNCT_1:def 7;
end;
assume e
in ((
the_Target_of G)
"
{v});
then
A3: e
in (
dom (
the_Target_of G)) & ((
the_Target_of G)
. e)
in
{v} by
FUNCT_1:def 7;
then ((
the_Target_of G)
. e)
= v by
TARSKI:def 1;
hence e
in (v
.edgesIn() ) by
A3,
GLIB_000: 56;
end;
hence (v
.edgesIn() )
= ((
the_Target_of G)
"
{v}) by
TARSKI: 2;
now
let e be
object;
hereby
assume e
in (v
.edgesOut() );
then
A4: e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
= v by
GLIB_000: 58;
then
A5: e
in (
dom (
the_Source_of G)) by
FUNCT_2:def 1;
((
the_Source_of G)
. e)
in
{v} by
A4,
TARSKI:def 1;
hence e
in ((
the_Source_of G)
"
{v}) by
A5,
FUNCT_1:def 7;
end;
assume e
in ((
the_Source_of G)
"
{v});
then
A6: e
in (
dom (
the_Source_of G)) & ((
the_Source_of G)
. e)
in
{v} by
FUNCT_1:def 7;
then ((
the_Source_of G)
. e)
= v by
TARSKI:def 1;
hence e
in (v
.edgesOut() ) by
A6,
GLIB_000: 58;
end;
hence (v
.edgesOut() )
= ((
the_Source_of G)
"
{v}) by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:26
Th30: for G be
_trivial
_Graph, v be
Vertex of G holds (v
.edgesIn() )
= (
the_Edges_of G) & (v
.edgesOut() )
= (
the_Edges_of G) & (v
.edgesInOut() )
= (
the_Edges_of G)
proof
let G be
_trivial
_Graph, v be
Vertex of G;
consider v0 be
Vertex of G such that
A1: (
the_Vertices_of G)
=
{v0} by
GLIB_000: 22;
A2: v
= v0 by
A1,
TARSKI:def 1;
A3:
now
let e be
object;
assume
A4: e
in (
the_Edges_of G);
then e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 13;
then ((
the_Source_of G)
. e)
in (
the_Vertices_of G) & ((
the_Target_of G)
. e)
in (
the_Vertices_of G) by
GLIB_000: 13;
then ((
the_Source_of G)
. e)
= v0 & ((
the_Target_of G)
. e)
= v0 by
A1,
TARSKI:def 1;
hence e
DJoins (v,v,G) by
A2,
A4,
GLIB_000:def 14;
end;
for e be
object st e
in (
the_Edges_of G) holds e
in (v
.edgesIn() ) by
A3,
GLIB_000: 57;
then (
the_Edges_of G)
c= (v
.edgesIn() ) by
TARSKI:def 3;
hence
A5: (v
.edgesIn() )
= (
the_Edges_of G) by
XBOOLE_0:def 10;
for e be
object st e
in (
the_Edges_of G) holds e
in (v
.edgesOut() ) by
A3,
GLIB_000: 59;
then (
the_Edges_of G)
c= (v
.edgesOut() ) by
TARSKI:def 3;
hence (v
.edgesOut() )
= (
the_Edges_of G) by
XBOOLE_0:def 10;
hence (v
.edgesInOut() )
= (
the_Edges_of G) by
A5;
end;
theorem ::
GLIBPRE0:27
for G be
_trivial
_Graph, v be
Vertex of G holds (v
.inDegree() )
= (G
.size() ) & (v
.outDegree() )
= (G
.size() ) & (v
.degree() )
= ((G
.size() )
+` (G
.size() ))
proof
let G be
_trivial
_Graph, v be
Vertex of G;
thus (v
.inDegree() )
= (G
.size() ) & (v
.outDegree() )
= (G
.size() ) by
Th30;
hence (v
.degree() )
= ((G
.size() )
+` (G
.size() ));
end;
theorem ::
GLIBPRE0:28
Th32: for G be
_Graph, X,Y be
set holds (G
.edgesBetween (X,Y))
= ((G
.edgesDBetween (X,Y))
\/ (G
.edgesDBetween (Y,X)))
proof
let G be
_Graph, X,Y be
set;
now
let e be
object;
hereby
assume e
in ((G
.edgesDBetween (X,Y))
\/ (G
.edgesDBetween (Y,X)));
per cases by
XBOOLE_0:def 3;
suppose e
in (G
.edgesDBetween (X,Y));
then e
DSJoins (X,Y,G) by
GLIB_000:def 31;
hence e
SJoins (X,Y,G) by
GLIB_009: 11;
end;
suppose e
in (G
.edgesDBetween (Y,X));
then e
DSJoins (Y,X,G) by
GLIB_000:def 31;
hence e
SJoins (X,Y,G) by
GLIB_009: 11;
end;
end;
assume e
SJoins (X,Y,G);
per cases by
GLIB_009: 11;
suppose e
DSJoins (X,Y,G);
then e
in (G
.edgesDBetween (X,Y)) by
GLIB_000:def 31;
hence e
in ((G
.edgesDBetween (X,Y))
\/ (G
.edgesDBetween (Y,X))) by
XBOOLE_0:def 3;
end;
suppose e
DSJoins (Y,X,G);
then e
in (G
.edgesDBetween (Y,X)) by
GLIB_000:def 31;
hence e
in ((G
.edgesDBetween (X,Y))
\/ (G
.edgesDBetween (Y,X))) by
XBOOLE_0:def 3;
end;
end;
hence thesis by
GLIB_000:def 30;
end;
theorem ::
GLIBPRE0:29
Th33: for G be
_Graph, v be
Vertex of G holds (v
.edgesInOut() )
= (G
.edgesBetween ((
the_Vertices_of G),
{v}))
proof
let G be
_Graph, v be
Vertex of G;
thus (v
.edgesInOut() )
= ((v
.edgesIn() )
\/ (v
.edgesOut() ))
.= ((G
.edgesDBetween ((
the_Vertices_of G),
{v}))
\/ (v
.edgesOut() )) by
GLIB_000: 39
.= ((G
.edgesDBetween ((
the_Vertices_of G),
{v}))
\/ (G
.edgesDBetween (
{v},(
the_Vertices_of G)))) by
GLIB_000: 39
.= (G
.edgesBetween ((
the_Vertices_of G),
{v})) by
Th32;
end;
theorem ::
GLIBPRE0:30
for G be
_Graph, X,Y be
set holds (G
.edgesDBetween (X,Y))
= ((G
.edgesOutOf X)
/\ (G
.edgesInto Y))
proof
let G be
_Graph, X,Y be
set;
now
let e be
object;
hereby
assume e
in (G
.edgesDBetween (X,Y));
then e
DSJoins (X,Y,G) by
GLIB_000:def 31;
then e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
in X & ((
the_Target_of G)
. e)
in Y by
GLIB_000:def 16;
then e
in (G
.edgesOutOf X) & e
in (G
.edgesInto Y) by
GLIB_000:def 26,
GLIB_000:def 27;
hence e
in ((G
.edgesOutOf X)
/\ (G
.edgesInto Y)) by
XBOOLE_0:def 4;
end;
assume e
in ((G
.edgesOutOf X)
/\ (G
.edgesInto Y));
then e
in (G
.edgesOutOf X) & e
in (G
.edgesInto Y) by
XBOOLE_0:def 4;
then e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
in X & ((
the_Target_of G)
. e)
in Y by
GLIB_000:def 26,
GLIB_000:def 27;
then e
DSJoins (X,Y,G) by
GLIB_000:def 16;
hence e
in (G
.edgesDBetween (X,Y)) by
GLIB_000:def 31;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:31
for G be
_Graph, X,Y be
set holds (G
.edgesDBetween (X,Y))
c= (G
.edgesBetween (X,Y))
proof
let G be
_Graph, X,Y be
set;
now
let e be
object;
assume e
in (G
.edgesDBetween (X,Y));
then e
DSJoins (X,Y,G) by
GLIB_000:def 31;
then e
SJoins (X,Y,G) by
GLIB_009: 11;
hence e
in (G
.edgesBetween (X,Y)) by
GLIB_000:def 30;
end;
hence thesis by
TARSKI:def 3;
end;
theorem ::
GLIBPRE0:32
Th36: for G be
_Graph, v be
Vertex of G st for e be
object holds not e
Joins (v,v,G) holds (
card (v
.edgesInOut() ))
= (v
.degree() )
proof
let G be
_Graph, v be
Vertex of G;
assume
A1: for e be
object holds not e
Joins (v,v,G);
((v
.edgesIn() )
/\ (v
.edgesOut() ))
=
{}
proof
assume ((v
.edgesIn() )
/\ (v
.edgesOut() ))
<>
{} ;
then
consider e be
object such that
A2: e
in ((v
.edgesIn() )
/\ (v
.edgesOut() )) by
XBOOLE_0:def 1;
e
in (v
.edgesIn() ) & e
in (v
.edgesOut() ) by
A2,
XBOOLE_0:def 4;
then e
in (
the_Edges_of G) & ((
the_Target_of G)
. e)
= v & ((
the_Source_of G)
. e)
= v by
GLIB_000: 56,
GLIB_000: 58;
then e
Joins (v,v,G) by
GLIB_000:def 13;
hence contradiction by
A1;
end;
hence thesis by
CARD_2: 35,
XBOOLE_0:def 7;
end;
theorem ::
GLIBPRE0:33
Th37: for G be
_Graph, v be
Vertex of G holds v is
isolated iff (v
.edgesIn() )
=
{} & (v
.edgesOut() )
=
{}
proof
let G be
_Graph, v be
Vertex of G;
hereby
assume v is
isolated;
then (v
.edgesInOut() )
=
{} by
GLIB_000:def 49;
hence (v
.edgesIn() )
=
{} & (v
.edgesOut() )
=
{} ;
end;
assume (v
.edgesIn() )
=
{} & (v
.edgesOut() )
=
{} ;
then (v
.edgesInOut() )
=
{} ;
hence v is
isolated by
GLIB_000:def 49;
end;
theorem ::
GLIBPRE0:34
Th38: for G be
_Graph, v be
Vertex of G holds v is
isolated iff (v
.inDegree() )
=
0 & (v
.outDegree() )
=
0
proof
let G be
_Graph, v be
Vertex of G;
hereby
assume v is
isolated;
then (v
.edgesIn() )
=
{} & (v
.edgesOut() )
=
{} by
Th37;
hence (v
.inDegree() )
=
0 & (v
.outDegree() )
=
0 ;
end;
assume (v
.inDegree() )
=
0 & (v
.outDegree() )
=
0 ;
then (v
.edgesIn() )
=
{} & (v
.edgesOut() )
=
{} ;
hence v is
isolated by
Th37;
end;
theorem ::
GLIBPRE0:35
Th39: for G be
_Graph, v be
Vertex of G holds v is
isolated iff (v
.degree() )
=
0
proof
let G be
_Graph, v be
Vertex of G;
hereby
assume v is
isolated;
then (v
.inDegree() )
=
0 & (v
.outDegree() )
=
0 by
Th38;
hence (v
.degree() )
= (
0
+`
0 )
.=
0 ;
end;
assume
A1: (v
.degree() )
=
0 ;
(v
.inDegree() )
c= (v
.degree() ) & (v
.outDegree() )
c= (v
.degree() ) by
CARD_2: 94;
then (v
.inDegree() )
=
0 & (v
.outDegree() )
=
0 by
A1;
hence thesis by
Th38;
end;
theorem ::
GLIBPRE0:36
for G be
_Graph, X be
set holds (G
.edgesInto X)
= (
union { (v
.edgesIn() ) where v be
Vertex of G : v
in X })
proof
let G be
_Graph, X be
set;
set S = { (v
.edgesIn() ) where v be
Vertex of G : v
in X };
now
let e be
object;
hereby
assume e
in (G
.edgesInto X);
then
A1: e
in (
the_Edges_of G) & ((
the_Target_of G)
. e)
in X by
GLIB_000:def 26;
then e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 13;
then
reconsider v = ((
the_Target_of G)
. e) as
Vertex of G by
GLIB_000: 13;
A2: e
in (v
.edgesIn() ) by
A1,
GLIB_000: 56;
(v
.edgesIn() )
in S by
A1;
hence e
in (
union S) by
A2,
TARSKI:def 4;
end;
assume e
in (
union S);
then
consider E be
set such that
A3: e
in E & E
in S by
TARSKI:def 4;
consider v be
Vertex of G such that
A4: E
= (v
.edgesIn() ) & v
in X by
A3;
e
in (
the_Edges_of G) & ((
the_Target_of G)
. e)
= v by
A3,
A4,
GLIB_000: 56;
hence e
in (G
.edgesInto X) by
A4,
GLIB_000:def 26;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:37
for G be
_Graph, X be
set holds (G
.edgesOutOf X)
= (
union { (v
.edgesOut() ) where v be
Vertex of G : v
in X })
proof
let G be
_Graph, X be
set;
set S = { (v
.edgesOut() ) where v be
Vertex of G : v
in X };
now
let e be
object;
hereby
assume e
in (G
.edgesOutOf X);
then
A1: e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
in X by
GLIB_000:def 27;
then e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 13;
then
reconsider v = ((
the_Source_of G)
. e) as
Vertex of G by
GLIB_000: 13;
A2: e
in (v
.edgesOut() ) by
A1,
GLIB_000: 58;
(v
.edgesOut() )
in S by
A1;
hence e
in (
union S) by
A2,
TARSKI:def 4;
end;
assume e
in (
union S);
then
consider E be
set such that
A3: e
in E & E
in S by
TARSKI:def 4;
consider v be
Vertex of G such that
A4: E
= (v
.edgesOut() ) & v
in X by
A3;
e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
= v by
A3,
A4,
GLIB_000: 58;
hence e
in (G
.edgesOutOf X) by
A4,
GLIB_000:def 27;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:38
for G be
_Graph, X be
set holds (G
.edgesInOut X)
= (
union { (v
.edgesInOut() ) where v be
Vertex of G : v
in X })
proof
let G be
_Graph, X be
set;
set S = { (v
.edgesInOut() ) where v be
Vertex of G : v
in X };
now
let e be
object;
hereby
assume e
in (G
.edgesInOut X);
then
A1: e
in (
the_Edges_of G) & (((
the_Source_of G)
. e)
in X or ((
the_Target_of G)
. e)
in X) by
GLIB_000: 28;
then
A2: e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 13;
per cases by
A1;
suppose
A3: ((
the_Source_of G)
. e)
in X;
reconsider v = ((
the_Source_of G)
. e) as
Vertex of G by
A2,
GLIB_000: 13;
A4: e
in (v
.edgesInOut() ) by
A1,
GLIB_000: 61;
(v
.edgesInOut() )
in S by
A3;
hence e
in (
union S) by
A4,
TARSKI:def 4;
end;
suppose
A5: ((
the_Target_of G)
. e)
in X;
reconsider v = ((
the_Target_of G)
. e) as
Vertex of G by
A2,
GLIB_000: 13;
A6: e
in (v
.edgesInOut() ) by
A1,
GLIB_000: 61;
(v
.edgesInOut() )
in S by
A5;
hence e
in (
union S) by
A6,
TARSKI:def 4;
end;
end;
assume e
in (
union S);
then
consider E be
set such that
A7: e
in E & E
in S by
TARSKI:def 4;
consider v be
Vertex of G such that
A8: E
= (v
.edgesInOut() ) & v
in X by
A7;
e
in (
the_Edges_of G) & (((
the_Source_of G)
. e)
= v or ((
the_Target_of G)
. e)
= v) by
A7,
A8,
GLIB_000: 61;
hence e
in (G
.edgesInOut X) by
A8,
GLIB_000: 28;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:39
for G be
_Graph, X,Y be
set holds (G
.edgesDBetween (X,Y))
= (
union { ((v
.edgesOut() )
/\ (w
.edgesIn() )) where v,w be
Vertex of G : v
in X & w
in Y })
proof
let G be
_Graph, X,Y be
set;
set S = { ((v
.edgesOut() )
/\ (w
.edgesIn() )) where v,w be
Vertex of G : v
in X & w
in Y };
now
let e be
object;
hereby
assume e
in (G
.edgesDBetween (X,Y));
then e
DSJoins (X,Y,G) by
GLIB_000:def 31;
then
A1: e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
in X & ((
the_Target_of G)
. e)
in Y by
GLIB_000:def 16;
then
A2: e
DJoins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 14;
then e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000: 16;
then
reconsider v = ((
the_Source_of G)
. e), w = ((
the_Target_of G)
. e) as
Vertex of G by
GLIB_000: 13;
e
DJoins (v,w,G) & e is
set by
A2,
TARSKI: 1;
then e
in (v
.edgesOut() ) & e
in (w
.edgesIn() ) by
GLIB_000: 57,
GLIB_000: 59;
then
A3: e
in ((v
.edgesOut() )
/\ (w
.edgesIn() )) by
XBOOLE_0:def 4;
((v
.edgesOut() )
/\ (w
.edgesIn() ))
in S by
A1;
hence e
in (
union S) by
A3,
TARSKI:def 4;
end;
assume e
in (
union S);
then
consider E be
set such that
A4: e
in E & E
in S by
TARSKI:def 4;
consider v,w be
Vertex of G such that
A5: E
= ((v
.edgesOut() )
/\ (w
.edgesIn() )) & v
in X & w
in Y by
A4;
e
in (v
.edgesOut() ) & e
in (w
.edgesIn() ) by
A4,
A5,
XBOOLE_0:def 4;
then e
in (
the_Edges_of G) & ((
the_Source_of G)
. e)
= v & ((
the_Target_of G)
. e)
= w by
GLIB_000: 56,
GLIB_000: 58;
then e
DJoins (v,w,G) by
GLIB_000:def 14;
then e
DSJoins (X,Y,G) by
A5,
GLIB_009: 7;
hence e
in (G
.edgesDBetween (X,Y)) by
GLIB_000:def 31;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:40
Th44: for G be
_Graph, X,Y be
set holds (G
.edgesBetween (X,Y))
c= (
union { ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) where v,w be
Vertex of G : v
in X & w
in Y })
proof
let G be
_Graph, X,Y be
set;
set S = { ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) where v,w be
Vertex of G : v
in X & w
in Y };
now
let e be
object;
assume e
in (G
.edgesBetween (X,Y));
then e
SJoins (X,Y,G) by
GLIB_000:def 30;
then
A1: e
in (
the_Edges_of G) & (((
the_Source_of G)
. e)
in X & ((
the_Target_of G)
. e)
in Y or ((
the_Source_of G)
. e)
in Y & ((
the_Target_of G)
. e)
in X) by
GLIB_000:def 15;
then
A2: e
Joins (((
the_Source_of G)
. e),((
the_Target_of G)
. e),G) by
GLIB_000:def 13;
then
reconsider v = ((
the_Source_of G)
. e), w = ((
the_Target_of G)
. e) as
Vertex of G by
GLIB_000: 13;
e
Joins (v,w,G) & e
Joins (w,v,G) & e is
set by
A2,
GLIB_000: 14,
TARSKI: 1;
then e
in (v
.edgesInOut() ) & e
in (w
.edgesInOut() ) by
GLIB_000: 64;
then
A3: e
in ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) by
XBOOLE_0:def 4;
((v
.edgesInOut() )
/\ (w
.edgesInOut() ))
in S by
A1;
hence e
in (
union S) by
A3,
TARSKI:def 4;
end;
hence thesis by
TARSKI:def 3;
end;
theorem ::
GLIBPRE0:41
for G be
_Graph, X,Y be
set st X
misses Y holds (G
.edgesBetween (X,Y))
= (
union { ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) where v,w be
Vertex of G : v
in X & w
in Y })
proof
let G be
_Graph, X,Y be
set;
assume
A1: X
misses Y;
set S = { ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) where v,w be
Vertex of G : v
in X & w
in Y };
now
let e be
object;
assume e
in (
union S);
then
consider E be
set such that
A2: e
in E & E
in S by
TARSKI:def 4;
consider v,w be
Vertex of G such that
A3: E
= ((v
.edgesInOut() )
/\ (w
.edgesInOut() )) & v
in X & w
in Y by
A2;
A4: e
in (v
.edgesInOut() ) & e
in (w
.edgesInOut() ) by
A2,
A3,
XBOOLE_0:def 4;
then
consider v2 be
Vertex of G such that
A5: e
Joins (v,v2,G) by
GLIB_000: 64;
consider w2 be
Vertex of G such that
A6: e
Joins (w,w2,G) by
A4,
GLIB_000: 64;
A7: v
= w & v2
= w2 or v
= w2 & v2
= w by
A5,
A6,
GLIB_000: 15;
v
<> w
proof
assume v
= w;
then v
in (X
/\ Y) by
A3,
XBOOLE_0:def 4;
hence contradiction by
A1,
XBOOLE_0:def 7;
end;
then e
SJoins (X,Y,G) by
A3,
A5,
A7,
GLIB_000: 17;
hence e
in (G
.edgesBetween (X,Y)) by
GLIB_000:def 30;
end;
then
A8: (
union S)
c= (G
.edgesBetween (X,Y)) by
TARSKI:def 3;
(G
.edgesBetween (X,Y))
c= (
union S) by
Th44;
hence thesis by
A8,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:42
for G1 be
_Graph, E be
set, G2 be
removeEdges of G1, E holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.edgesIn() )
= ((v1
.edgesIn() )
\ E) & (v2
.edgesOut() )
= ((v1
.edgesOut() )
\ E) & (v2
.edgesInOut() )
= ((v1
.edgesInOut() )
\ E)
proof
let G1 be
_Graph, E be
set, G2 be
removeEdges of G1, E;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
A2: (
the_Edges_of G2)
= ((
the_Edges_of G1)
\ E) by
GLIB_000: 53;
now
let e be
object;
hereby
assume
A3: e
in (v2
.edgesIn() );
then
A4: e
in (v1
.edgesIn() ) by
A1,
GLIB_000: 78,
TARSKI:def 3;
not e
in E by
A2,
A3,
XBOOLE_0:def 5;
hence e
in ((v1
.edgesIn() )
\ E) by
A4,
XBOOLE_0:def 5;
end;
assume e
in ((v1
.edgesIn() )
\ E);
then
A5: e
in (v1
.edgesIn() ) & not e
in E by
XBOOLE_0:def 5;
then
A6: e
in (
the_Edges_of G2) by
A2,
XBOOLE_0:def 5;
v1
= ((
the_Target_of G1)
. e) by
A5,
GLIB_000: 56
.= ((
the_Target_of G2)
. e) by
A6,
GLIB_000:def 32;
hence e
in (v2
.edgesIn() ) by
A1,
A6,
GLIB_000: 56;
end;
hence
A7: (v2
.edgesIn() )
= ((v1
.edgesIn() )
\ E) by
TARSKI: 2;
now
let e be
object;
hereby
assume
A8: e
in (v2
.edgesOut() );
then
A9: e
in (v1
.edgesOut() ) by
A1,
GLIB_000: 78,
TARSKI:def 3;
not e
in E by
A2,
A8,
XBOOLE_0:def 5;
hence e
in ((v1
.edgesOut() )
\ E) by
A9,
XBOOLE_0:def 5;
end;
assume e
in ((v1
.edgesOut() )
\ E);
then
A10: e
in (v1
.edgesOut() ) & not e
in E by
XBOOLE_0:def 5;
then
A11: e
in (
the_Edges_of G2) by
A2,
XBOOLE_0:def 5;
v1
= ((
the_Source_of G1)
. e) by
A10,
GLIB_000: 58
.= ((
the_Source_of G2)
. e) by
A11,
GLIB_000:def 32;
hence e
in (v2
.edgesOut() ) by
A1,
A11,
GLIB_000: 58;
end;
hence
A12: (v2
.edgesOut() )
= ((v1
.edgesOut() )
\ E) by
TARSKI: 2;
thus (v2
.edgesInOut() )
= ((v1
.edgesInOut() )
\ E) by
A7,
A12,
XBOOLE_1: 42;
end;
theorem ::
GLIBPRE0:43
for G1,G2 be
_Graph, V be
set holds G2 is
removeVertices of G1, V iff G2 is
removeVertices of G1, (V
/\ (
the_Vertices_of G1))
proof
let G1,G2 be
_Graph, V be
set;
((
the_Vertices_of G1)
\ V)
= ((
the_Vertices_of G1)
\ (V
/\ (
the_Vertices_of G1))) by
XBOOLE_1: 47;
hence thesis;
end;
theorem ::
GLIBPRE0:44
Th48: for G1 be
_Graph, V be
set, G2 be
removeVertices of G1, V holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st V
c< (
the_Vertices_of G1) & v1
= v2 holds (v2
.edgesIn() )
= ((v1
.edgesIn() )
\ (G1
.edgesOutOf V)) & (v2
.edgesOut() )
= ((v1
.edgesOut() )
\ (G1
.edgesInto V)) & (v2
.edgesInOut() )
= ((v1
.edgesInOut() )
\ (G1
.edgesInOut V))
proof
let G1 be
_Graph, V be
set, G2 be
removeVertices of G1, V;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: V
c< (
the_Vertices_of G1) & v1
= v2;
then
A2: (
the_Edges_of G2)
= (G1
.edgesBetween ((
the_Vertices_of G1)
\ V)) by
GLIB_000: 49;
(
the_Vertices_of G2)
= ((
the_Vertices_of G1)
\ V) by
A1,
GLIB_000: 49;
then
A3: not v2
in V by
XBOOLE_0:def 5;
now
let e be
object;
hereby
assume
A4: e
in (v2
.edgesIn() );
then
A5: e
in (v1
.edgesIn() ) by
A1,
GLIB_000: 78,
TARSKI:def 3;
e
in (G1
.edgesOutOf ((
the_Vertices_of G1)
\ V)) by
A2,
A4,
XBOOLE_0:def 4;
then ((
the_Source_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
GLIB_000:def 27;
then not ((
the_Source_of G1)
. e)
in V by
XBOOLE_0:def 5;
then not e
in (G1
.edgesOutOf V) by
GLIB_000:def 27;
hence e
in ((v1
.edgesIn() )
\ (G1
.edgesOutOf V)) by
A5,
XBOOLE_0:def 5;
end;
assume e
in ((v1
.edgesIn() )
\ (G1
.edgesOutOf V));
then
A6: e
in (v1
.edgesIn() ) & not e
in (G1
.edgesOutOf V) by
XBOOLE_0:def 5;
then
A7: not ((
the_Source_of G1)
. e)
in V by
GLIB_000:def 27;
e
Joins (((
the_Source_of G1)
. e),((
the_Target_of G1)
. e),G1) by
A6,
GLIB_000:def 13;
then
A8: ((
the_Source_of G1)
. e)
in (
the_Vertices_of G1) & ((
the_Target_of G1)
. e)
in (
the_Vertices_of G1) by
GLIB_000: 13;
then ((
the_Source_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
A7,
XBOOLE_0:def 5;
then
A9: e
in (G1
.edgesOutOf ((
the_Vertices_of G1)
\ V)) by
A6,
GLIB_000:def 27;
not ((
the_Target_of G1)
. e)
in V by
A1,
A3,
A6,
GLIB_000: 56;
then ((
the_Target_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
A8,
XBOOLE_0:def 5;
then e
in (G1
.edgesInto ((
the_Vertices_of G1)
\ V)) by
A6,
GLIB_000:def 26;
then
A10: e
in (
the_Edges_of G2) by
A2,
A9,
XBOOLE_0:def 4;
v1
= ((
the_Target_of G1)
. e) by
A6,
GLIB_000: 56
.= ((
the_Target_of G2)
. e) by
A10,
GLIB_000:def 32;
hence e
in (v2
.edgesIn() ) by
A1,
A10,
GLIB_000: 56;
end;
hence
A11: (v2
.edgesIn() )
= ((v1
.edgesIn() )
\ (G1
.edgesOutOf V)) by
TARSKI: 2;
now
let e be
object;
hereby
assume
A12: e
in (v2
.edgesOut() );
then
A13: e
in (v1
.edgesOut() ) by
A1,
GLIB_000: 78,
TARSKI:def 3;
e
in (G1
.edgesInto ((
the_Vertices_of G1)
\ V)) by
A2,
A12,
XBOOLE_0:def 4;
then ((
the_Target_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
GLIB_000:def 26;
then not ((
the_Target_of G1)
. e)
in V by
XBOOLE_0:def 5;
then not e
in (G1
.edgesInto V) by
GLIB_000:def 26;
hence e
in ((v1
.edgesOut() )
\ (G1
.edgesInto V)) by
A13,
XBOOLE_0:def 5;
end;
assume e
in ((v1
.edgesOut() )
\ (G1
.edgesInto V));
then
A14: e
in (v1
.edgesOut() ) & not e
in (G1
.edgesInto V) by
XBOOLE_0:def 5;
then
A15: not ((
the_Target_of G1)
. e)
in V by
GLIB_000:def 26;
e
Joins (((
the_Source_of G1)
. e),((
the_Target_of G1)
. e),G1) by
A14,
GLIB_000:def 13;
then
A16: ((
the_Source_of G1)
. e)
in (
the_Vertices_of G1) & ((
the_Target_of G1)
. e)
in (
the_Vertices_of G1) by
GLIB_000: 13;
then ((
the_Target_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
A15,
XBOOLE_0:def 5;
then
A17: e
in (G1
.edgesInto ((
the_Vertices_of G1)
\ V)) by
A14,
GLIB_000:def 26;
not ((
the_Source_of G1)
. e)
in V by
A1,
A3,
A14,
GLIB_000: 58;
then ((
the_Source_of G1)
. e)
in ((
the_Vertices_of G1)
\ V) by
A16,
XBOOLE_0:def 5;
then e
in (G1
.edgesOutOf ((
the_Vertices_of G1)
\ V)) by
A14,
GLIB_000:def 27;
then
A18: e
in (
the_Edges_of G2) by
A2,
A17,
XBOOLE_0:def 4;
v1
= ((
the_Source_of G1)
. e) by
A14,
GLIB_000: 58
.= ((
the_Source_of G2)
. e) by
A18,
GLIB_000:def 32;
hence e
in (v2
.edgesOut() ) by
A1,
A18,
GLIB_000: 58;
end;
hence
A19: (v2
.edgesOut() )
= ((v1
.edgesOut() )
\ (G1
.edgesInto V)) by
TARSKI: 2;
((v1
.edgesOut() )
/\ (G1
.edgesOutOf V))
=
{}
proof
assume ((v1
.edgesOut() )
/\ (G1
.edgesOutOf V))
<>
{} ;
then
consider e be
object such that
A20: e
in ((v1
.edgesOut() )
/\ (G1
.edgesOutOf V)) by
XBOOLE_0:def 1;
e
in (v1
.edgesOut() ) & e
in (G1
.edgesOutOf V) by
A20,
XBOOLE_0:def 4;
then ((
the_Source_of G1)
. e)
= v1 & ((
the_Source_of G1)
. e)
in V by
GLIB_000:def 27,
GLIB_000: 58;
hence contradiction by
A1,
A3;
end;
then (v1
.edgesOut() )
misses (G1
.edgesOutOf V) by
XBOOLE_0:def 7;
then
A21: ((v1
.edgesOut() )
\ (G1
.edgesInto V))
misses (G1
.edgesOutOf V) by
XBOOLE_1: 36,
XBOOLE_1: 63;
((v1
.edgesIn() )
/\ (G1
.edgesInto V))
=
{}
proof
assume ((v1
.edgesIn() )
/\ (G1
.edgesInto V))
<>
{} ;
then
consider e be
object such that
A22: e
in ((v1
.edgesIn() )
/\ (G1
.edgesInto V)) by
XBOOLE_0:def 1;
e
in (v1
.edgesIn() ) & e
in (G1
.edgesInto V) by
A22,
XBOOLE_0:def 4;
then ((
the_Target_of G1)
. e)
= v1 & ((
the_Target_of G1)
. e)
in V by
GLIB_000:def 26,
GLIB_000: 56;
hence contradiction by
A1,
A3;
end;
then
A23: (v1
.edgesIn() )
misses (G1
.edgesInto V) by
XBOOLE_0:def 7;
thus (v2
.edgesInOut() )
= (((v1
.edgesIn() )
\/ ((v1
.edgesOut() )
\ (G1
.edgesInto V)))
\ (G1
.edgesOutOf V)) by
A11,
A19,
A21,
XBOOLE_1: 87
.= (((v1
.edgesInOut() )
\ (G1
.edgesInto V))
\ (G1
.edgesOutOf V)) by
A23,
XBOOLE_1: 87
.= ((v1
.edgesInOut() )
\ (G1
.edgesInOut V)) by
XBOOLE_1: 41;
end;
theorem ::
GLIBPRE0:45
for G1 be non
_trivial
_Graph, v be
Vertex of G1 holds for G2 be
removeVertex of G1, v holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.edgesIn() )
= ((v1
.edgesIn() )
\ (v
.edgesOut() )) & (v2
.edgesOut() )
= ((v1
.edgesOut() )
\ (v
.edgesIn() )) & (v2
.edgesInOut() )
= ((v1
.edgesInOut() )
\ (v
.edgesInOut() ))
proof
let G1 be non
_trivial
_Graph, v be
Vertex of G1;
let G2 be
removeVertex of G1, v;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
((
the_Vertices_of G1)
\
{v})
<>
{} by
GLIB_000: 20;
then (
the_Vertices_of G1)
<>
{v} by
XBOOLE_1: 37;
then
{v}
c< (
the_Vertices_of G1) by
XBOOLE_0:def 8;
hence thesis by
A1,
Th48;
end;
begin
theorem ::
GLIBPRE0:46
for G be
_Graph, C be
Component of G holds for v1 be
Vertex of G, v2 be
Vertex of C st v1
= v2 holds (v1
.edgesIn() )
= (v2
.edgesIn() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.edgesOut() )
= (v2
.edgesOut() ) & (v1
.outDegree() )
= (v2
.outDegree() ) & (v1
.edgesInOut() )
= (v2
.edgesInOut() ) & (v1
.degree() )
= (v2
.degree() )
proof
let G be
_Graph, C be
Component of G;
let v1 be
Vertex of G, v2 be
Vertex of C;
assume
A1: v1
= v2;
then
A2: (v2
.edgesIn() )
c= (v1
.edgesIn() ) & (v2
.edgesOut() )
c= (v1
.edgesOut() ) by
GLIB_000: 78;
now
let e be
object;
assume e
in (v1
.edgesIn() );
then
consider x be
set such that
A3: e
DJoins (x,v1,G) by
GLIB_000: 57;
set W = (G
.walkOf (v1,e,x));
A4: e
Joins (v1,x,G) by
A3,
GLIB_000: 16;
then W
is_Walk_from (v1,x) by
GLIB_001: 15;
then
A5: x
in (G
.reachableFrom v1) by
GLIB_002:def 5;
A6: e
Joins (v2,x,G) & e
DJoins (x,v2,G) by
A1,
A3,
A4;
(
the_Vertices_of C)
= (G
.reachableFrom v1) by
A1,
GLIB_002: 33;
then e
in (G
.edgesBetween (
the_Vertices_of C)) by
A5,
A6,
GLIB_000: 32;
then e
in (
the_Edges_of C) by
GLIB_002: 31;
then e
DJoins (x,v2,C) & e is
set by
A6,
GLIB_000: 73;
hence e
in (v2
.edgesIn() ) by
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v2
.edgesIn() ) by
TARSKI:def 3;
hence
A7: (v1
.edgesIn() )
= (v2
.edgesIn() ) by
A2,
XBOOLE_0:def 10;
hence
A8: (v1
.inDegree() )
= (v2
.inDegree() );
now
let e be
object;
assume e
in (v1
.edgesOut() );
then
consider x be
set such that
A9: e
DJoins (v1,x,G) by
GLIB_000: 59;
set W = (G
.walkOf (v1,e,x));
A10: e
Joins (v1,x,G) by
A9,
GLIB_000: 16;
then W
is_Walk_from (v1,x) by
GLIB_001: 15;
then
A11: x
in (G
.reachableFrom v1) by
GLIB_002:def 5;
A12: e
Joins (v2,x,G) & e
DJoins (v2,x,G) by
A1,
A9,
A10;
(
the_Vertices_of C)
= (G
.reachableFrom v1) by
A1,
GLIB_002: 33;
then e
in (G
.edgesBetween (
the_Vertices_of C)) by
A11,
A12,
GLIB_000: 32;
then e
in (
the_Edges_of C) by
GLIB_002: 31;
then e
DJoins (v2,x,C) & e is
set by
A12,
GLIB_000: 73;
hence e
in (v2
.edgesOut() ) by
GLIB_000: 59;
end;
then (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
TARSKI:def 3;
hence
A13: (v1
.edgesOut() )
= (v2
.edgesOut() ) by
A2,
XBOOLE_0:def 10;
hence
A14: (v1
.outDegree() )
= (v2
.outDegree() );
thus (v1
.edgesInOut() )
= (v2
.edgesInOut() ) by
A7,
A13;
thus (v1
.degree() )
= (v2
.degree() ) by
A8,
A14;
end;
begin
theorem ::
GLIBPRE0:47
for G2 be
_Graph, V be
set, G1 be
addVertices of G2, V holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v1
.edgesIn() )
= (v2
.edgesIn() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.edgesOut() )
= (v2
.edgesOut() ) & (v1
.outDegree() )
= (v2
.outDegree() ) & (v1
.edgesInOut() )
= (v2
.edgesInOut() ) & (v1
.degree() )
= (v2
.degree() )
proof
let G2 be
_Graph, V be
set, G1 be
addVertices of G2, V;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
A2: G2 is
Subgraph of G1 by
GLIB_006: 57;
then
A3: (v2
.edgesIn() )
c= (v1
.edgesIn() ) by
A1,
GLIB_000: 78;
now
let e be
object;
assume e
in (v1
.edgesIn() );
then
consider x be
set such that
A4: e
DJoins (x,v1,G1) by
GLIB_000: 57;
e
DJoins (x,v2,G2) & e is
set by
A1,
A4,
GLIB_006: 85,
TARSKI: 1;
hence e
in (v2
.edgesIn() ) by
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v2
.edgesIn() ) by
TARSKI:def 3;
hence
A5: (v1
.edgesIn() )
= (v2
.edgesIn() ) by
A3,
XBOOLE_0:def 10;
hence
A6: (v1
.inDegree() )
= (v2
.inDegree() );
A7: (v2
.edgesOut() )
c= (v1
.edgesOut() ) by
A1,
A2,
GLIB_000: 78;
now
let e be
object;
assume e
in (v1
.edgesOut() );
then
consider x be
set such that
A8: e
DJoins (v1,x,G1) by
GLIB_000: 59;
e
DJoins (v2,x,G2) & e is
set by
A1,
A8,
GLIB_006: 85,
TARSKI: 1;
hence e
in (v2
.edgesOut() ) by
GLIB_000: 59;
end;
then (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
TARSKI:def 3;
hence
A9: (v1
.edgesOut() )
= (v2
.edgesOut() ) by
A7,
XBOOLE_0:def 10;
hence
A10: (v1
.outDegree() )
= (v2
.outDegree() );
thus (v1
.edgesInOut() )
= (v2
.edgesInOut() ) by
A5,
A9;
thus (v1
.degree() )
= (v2
.degree() ) by
A6,
A10;
end;
theorem ::
GLIBPRE0:48
for G2 be
_Graph, v,w,e be
object, G1 be
addEdge of G2, v, e, w holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 & v2
<> v & v2
<> w holds (v1
.edgesIn() )
= (v2
.edgesIn() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.edgesOut() )
= (v2
.edgesOut() ) & (v1
.outDegree() )
= (v2
.outDegree() ) & (v1
.edgesInOut() )
= (v2
.edgesInOut() ) & (v1
.degree() )
= (v2
.degree() )
proof
let G2 be
_Graph, v,w,e be
object, G1 be
addEdge of G2, v, e, w;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2 & v2
<> v & v2
<> w;
per cases ;
suppose
A2: v
in (
the_Vertices_of G2) & w
in (
the_Vertices_of G2) & not e
in (
the_Edges_of G2);
A3: G2 is
Subgraph of G1 by
GLIB_006: 57;
A4: (v2
.edgesIn() )
c= (v1
.edgesIn() ) by
A1,
A3,
GLIB_000: 78;
now
let f be
object;
assume f
in (v1
.edgesIn() );
then
consider x be
set such that
A5: f
DJoins (x,v1,G1) by
GLIB_000: 57;
f
in (
the_Edges_of G2)
proof
assume
A7: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A5,
GLIB_000: 16;
hence contradiction by
A1,
A2,
A7,
GLIB_006: 107;
end;
hence f
in (v2
.edgesIn() ) by
A1,
A5,
GLIB_006: 71,
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v2
.edgesIn() ) by
TARSKI:def 3;
hence
A8: (v1
.edgesIn() )
= (v2
.edgesIn() ) by
A4,
XBOOLE_0:def 10;
hence (v1
.inDegree() )
= (v2
.inDegree() );
A9: (v2
.edgesOut() )
c= (v1
.edgesOut() ) by
A1,
A3,
GLIB_000: 78;
now
let f be
object;
assume f
in (v1
.edgesOut() );
then
consider x be
set such that
A10: f
DJoins (v1,x,G1) by
GLIB_000: 59;
f
in (
the_Edges_of G2)
proof
assume
A12: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A10,
GLIB_000: 16;
hence contradiction by
A1,
A2,
A12,
GLIB_006: 107;
end;
hence f
in (v2
.edgesOut() ) by
A1,
A10,
GLIB_006: 71,
GLIB_000: 59;
end;
then (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
TARSKI:def 3;
hence
A13: (v1
.edgesOut() )
= (v2
.edgesOut() ) by
A9,
XBOOLE_0:def 10;
hence (v1
.outDegree() )
= (v2
.outDegree() );
thus thesis by
A8,
A13;
end;
suppose not (v
in (
the_Vertices_of G2) & w
in (
the_Vertices_of G2) & not e
in (
the_Edges_of G2));
then G1
== G2 by
GLIB_006:def 11;
hence thesis by
A1,
GLIB_000: 96;
end;
end;
theorem ::
GLIBPRE0:49
for G2 be
_Graph, v,w be
Vertex of G2, e be
object holds for G1 be
addEdge of G2, v, e, w holds for v1 be
Vertex of G1 st not e
in (
the_Edges_of G2) & v1
= v & v
<> w holds (v1
.edgesIn() )
= (v
.edgesIn() ) & (v1
.inDegree() )
= (v
.inDegree() ) & (v1
.edgesOut() )
= ((v
.edgesOut() )
\/
{e}) & (v1
.outDegree() )
= ((v
.outDegree() )
+` 1) & (v1
.edgesInOut() )
= ((v
.edgesInOut() )
\/
{e}) & (v1
.degree() )
= ((v
.degree() )
+` 1)
proof
let G2 be
_Graph, v,w be
Vertex of G2, e be
object;
let G1 be
addEdge of G2, v, e, w, v1 be
Vertex of G1;
assume
A1: not e
in (
the_Edges_of G2) & v1
= v & v
<> w;
A2: G2 is
Subgraph of G1 by
GLIB_006: 57;
A3: (v
.edgesIn() )
c= (v1
.edgesIn() ) by
A1,
A2,
GLIB_000: 78;
now
let f be
object;
assume f
in (v1
.edgesIn() );
then
consider x be
set such that
A4: f
DJoins (x,v1,G1) by
GLIB_000: 57;
f
in (
the_Edges_of G2)
proof
assume
A6: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A4,
GLIB_000: 16;
then f
= e by
A1,
A6,
GLIB_006: 106;
then f
DJoins (v,w,G1) by
A1,
GLIB_006: 105;
hence contradiction by
A1,
A4,
GLIB_009: 6;
end;
hence f
in (v
.edgesIn() ) by
A1,
A4,
GLIB_006: 71,
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v
.edgesIn() ) by
TARSKI:def 3;
hence
A7: (v1
.edgesIn() )
= (v
.edgesIn() ) by
A3,
XBOOLE_0:def 10;
hence
A8: (v1
.inDegree() )
= (v
.inDegree() );
now
let f be
object;
thus f
in (v1
.edgesOut() ) implies f
in ((v
.edgesOut() )
\/
{e})
proof
assume f
in (v1
.edgesOut() );
then
consider x be
set such that
A9: f
DJoins (v1,x,G1) by
GLIB_000: 59;
per cases by
A9,
GLIB_006: 71;
suppose
A10: f
DJoins (v1,x,G2);
f is
set by
TARSKI: 1;
then f
in (v
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
hence thesis by
XBOOLE_0:def 3;
end;
suppose
A11: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A9,
GLIB_000: 16;
then f
= e by
A1,
A11,
GLIB_006: 106;
then f
in
{e} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
end;
assume f
in ((v
.edgesOut() )
\/
{e});
per cases by
XBOOLE_0:def 3;
suppose f
in (v
.edgesOut() );
hence f
in (v1
.edgesOut() ) by
A1,
A2,
GLIB_000: 78,
TARSKI:def 3;
end;
suppose f
in
{e};
then f
= e & f is
set by
TARSKI:def 1;
hence f
in (v1
.edgesOut() ) by
A1,
GLIB_000: 59,
GLIB_006: 105;
end;
end;
hence
A12: (v1
.edgesOut() )
= ((v
.edgesOut() )
\/
{e}) by
TARSKI: 2;
not e
in (v
.edgesOut() ) by
A1;
then
A13: (v
.edgesOut() )
misses
{e} by
ZFMISC_1: 50;
thus
A14: (v1
.outDegree() )
= ((
card (v
.edgesOut() ))
+` (
card
{e})) by
A12,
A13,
CARD_2: 35
.= ((v
.outDegree() )
+` 1) by
CARD_1: 30;
thus (v1
.edgesInOut() )
= ((v
.edgesInOut() )
\/
{e}) by
A7,
A12,
XBOOLE_1: 4;
thus (v1
.degree() )
= ((v
.degree() )
+` 1) by
A8,
A14,
CARD_2: 19;
end;
theorem ::
GLIBPRE0:50
for G2 be
_Graph, v,w be
Vertex of G2, e be
object holds for G1 be
addEdge of G2, v, e, w holds for w1 be
Vertex of G1 st not e
in (
the_Edges_of G2) & w1
= w & v
<> w holds (w1
.edgesIn() )
= ((w
.edgesIn() )
\/
{e}) & (w1
.inDegree() )
= ((w
.inDegree() )
+` 1) & (w1
.edgesOut() )
= (w
.edgesOut() ) & (w1
.outDegree() )
= (w
.outDegree() ) & (w1
.edgesInOut() )
= ((w
.edgesInOut() )
\/
{e}) & (w1
.degree() )
= ((w
.degree() )
+` 1)
proof
let G2 be
_Graph, v,w be
Vertex of G2, e be
object;
let G1 be
addEdge of G2, v, e, w, w1 be
Vertex of G1;
assume
A1: not e
in (
the_Edges_of G2) & w1
= w & v
<> w;
A2: G2 is
Subgraph of G1 by
GLIB_006: 57;
now
let f be
object;
thus f
in (w1
.edgesIn() ) implies f
in ((w
.edgesIn() )
\/
{e})
proof
assume f
in (w1
.edgesIn() );
then
consider x be
set such that
A3: f
DJoins (x,w1,G1) by
GLIB_000: 57;
per cases by
A3,
GLIB_006: 71;
suppose
A4: f
DJoins (x,w1,G2);
f is
set by
TARSKI: 1;
then f
in (w
.edgesIn() ) by
A1,
A4,
GLIB_000: 57;
hence thesis by
XBOOLE_0:def 3;
end;
suppose
A5: not f
in (
the_Edges_of G2);
f
Joins (x,w1,G1) by
A3,
GLIB_000: 16;
then f
= e by
A1,
A5,
GLIB_006: 106;
then f
in
{e} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
end;
assume f
in ((w
.edgesIn() )
\/
{e});
per cases by
XBOOLE_0:def 3;
suppose f
in (w
.edgesIn() );
hence f
in (w1
.edgesIn() ) by
A1,
A2,
GLIB_000: 78,
TARSKI:def 3;
end;
suppose f
in
{e};
then f
= e by
TARSKI:def 1;
then
A6: f
DJoins (v,w,G1) by
A1,
GLIB_006: 105;
f is
set by
TARSKI: 1;
hence f
in (w1
.edgesIn() ) by
A1,
A6,
GLIB_000: 57;
end;
end;
hence
A7: (w1
.edgesIn() )
= ((w
.edgesIn() )
\/
{e}) by
TARSKI: 2;
not e
in (w
.edgesIn() ) by
A1;
then
A8: (w
.edgesIn() )
misses
{e} by
ZFMISC_1: 50;
thus
A9: (w1
.inDegree() )
= ((
card (w
.edgesIn() ))
+` (
card
{e})) by
A7,
A8,
CARD_2: 35
.= ((w
.inDegree() )
+` 1) by
CARD_1: 30;
A10: (w
.edgesOut() )
c= (w1
.edgesOut() ) by
A1,
A2,
GLIB_000: 78;
now
let f be
object;
assume f
in (w1
.edgesOut() );
then
consider x be
set such that
A11: f
DJoins (w1,x,G1) by
GLIB_000: 59;
f
in (
the_Edges_of G2)
proof
assume
A13: not f
in (
the_Edges_of G2);
f
Joins (x,w1,G1) by
A11,
GLIB_000: 16;
then f
= e by
A1,
A13,
GLIB_006: 106;
then f
DJoins (v,w,G1) by
A1,
GLIB_006: 105;
hence contradiction by
A1,
A11,
GLIB_009: 6;
end;
hence f
in (w
.edgesOut() ) by
A1,
A11,
GLIB_000: 59,
GLIB_006: 71;
end;
then (w1
.edgesOut() )
c= (w
.edgesOut() ) by
TARSKI:def 3;
hence
A14: (w1
.edgesOut() )
= (w
.edgesOut() ) by
A10,
XBOOLE_0:def 10;
hence
A15: (w1
.outDegree() )
= (w
.outDegree() );
thus (w1
.edgesInOut() )
= ((w
.edgesInOut() )
\/
{e}) by
A7,
A14,
XBOOLE_1: 4;
thus (w1
.degree() )
= ((w
.degree() )
+` 1) by
A9,
A15,
CARD_2: 19;
end;
theorem ::
GLIBPRE0:51
for G2 be
_Graph, v be
Vertex of G2, e be
object holds for G1 be
addEdge of G2, v, e, v holds for v1 be
Vertex of G1 st not e
in (
the_Edges_of G2) & v1
= v holds (v1
.edgesIn() )
= ((v
.edgesIn() )
\/
{e}) & (v1
.inDegree() )
= ((v
.inDegree() )
+` 1) & (v1
.edgesOut() )
= ((v
.edgesOut() )
\/
{e}) & (v1
.outDegree() )
= ((v
.outDegree() )
+` 1) & (v1
.edgesInOut() )
= ((v
.edgesInOut() )
\/
{e}) & (v1
.degree() )
= ((v
.degree() )
+` 2)
proof
let G2 be
_Graph, v be
Vertex of G2, e be
object;
let G1 be
addEdge of G2, v, e, v, v1 be
Vertex of G1;
assume
A1: not e
in (
the_Edges_of G2) & v1
= v;
A2: G2 is
Subgraph of G1 by
GLIB_006: 57;
now
let f be
object;
thus f
in (v1
.edgesIn() ) implies f
in ((v
.edgesIn() )
\/
{e})
proof
assume f
in (v1
.edgesIn() );
then
consider x be
set such that
A3: f
DJoins (x,v1,G1) by
GLIB_000: 57;
per cases by
A3,
GLIB_006: 71;
suppose
A4: f
DJoins (x,v1,G2);
f is
set by
TARSKI: 1;
then f
in (v
.edgesIn() ) by
A1,
A4,
GLIB_000: 57;
hence thesis by
XBOOLE_0:def 3;
end;
suppose
A5: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A3,
GLIB_000: 16;
then f
= e by
A1,
A5,
GLIB_006: 106;
then f
in
{e} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
end;
assume f
in ((v
.edgesIn() )
\/
{e});
per cases by
XBOOLE_0:def 3;
suppose f
in (v
.edgesIn() );
hence f
in (v1
.edgesIn() ) by
A1,
A2,
GLIB_000: 78,
TARSKI:def 3;
end;
suppose f
in
{e};
then f
= e & f is
set by
TARSKI:def 1;
hence f
in (v1
.edgesIn() ) by
A1,
GLIB_000: 57,
GLIB_006: 105;
end;
end;
hence
A6: (v1
.edgesIn() )
= ((v
.edgesIn() )
\/
{e}) by
TARSKI: 2;
not e
in (v
.edgesIn() ) by
A1;
then
A7: (v
.edgesIn() )
misses
{e} by
ZFMISC_1: 50;
thus
A8: (v1
.inDegree() )
= ((
card (v
.edgesIn() ))
+` (
card
{e})) by
A6,
A7,
CARD_2: 35
.= ((v
.inDegree() )
+` 1) by
CARD_1: 30;
now
let f be
object;
thus f
in (v1
.edgesOut() ) implies f
in ((v
.edgesOut() )
\/
{e})
proof
assume f
in (v1
.edgesOut() );
then
consider x be
set such that
A9: f
DJoins (v1,x,G1) by
GLIB_000: 59;
per cases by
A9,
GLIB_006: 71;
suppose
A10: f
DJoins (v1,x,G2);
f is
set by
TARSKI: 1;
then f
in (v
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
hence thesis by
XBOOLE_0:def 3;
end;
suppose
A11: not f
in (
the_Edges_of G2);
f
Joins (x,v1,G1) by
A9,
GLIB_000: 16;
then f
= e by
A1,
A11,
GLIB_006: 106;
then f
in
{e} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
end;
assume f
in ((v
.edgesOut() )
\/
{e});
per cases by
XBOOLE_0:def 3;
suppose f
in (v
.edgesOut() );
hence f
in (v1
.edgesOut() ) by
A1,
A2,
GLIB_000: 78,
TARSKI:def 3;
end;
suppose f
in
{e};
then f
= e & f is
set by
TARSKI:def 1;
hence f
in (v1
.edgesOut() ) by
A1,
GLIB_000: 59,
GLIB_006: 105;
end;
end;
hence
A12: (v1
.edgesOut() )
= ((v
.edgesOut() )
\/
{e}) by
TARSKI: 2;
not e
in (v
.edgesOut() ) by
A1;
then
A13: (v
.edgesOut() )
misses
{e} by
ZFMISC_1: 50;
thus
A14: (v1
.outDegree() )
= ((
card (v
.edgesOut() ))
+` (
card
{e})) by
A12,
A13,
CARD_2: 35
.= ((v
.outDegree() )
+` 1) by
CARD_1: 30;
thus (v1
.edgesInOut() )
= ((v
.edgesInOut() )
\/
{e}) by
A6,
A12,
XBOOLE_1: 5;
thus (v1
.degree() )
= ((((v
.inDegree() )
+` 1)
+` (v
.outDegree() ))
+` 1) by
A8,
A14,
CARD_2: 19
.= ((((v
.inDegree() )
+` (v
.outDegree() ))
+` 1)
+` 1) by
CARD_2: 19
.= ((v
.degree() )
+` (1
+` 1)) by
CARD_2: 19
.= ((v
.degree() )
+` 2);
end;
begin
theorem ::
GLIBPRE0:52
for G3 be
_Graph, E be
set, G4 be
reverseEdgeDirections of G3, E holds for G1 be
Supergraph of G3, G2 be
reverseEdgeDirections of G1, E st E
c= (
the_Edges_of G3) holds G2 is
Supergraph of G4
proof
let G3 be
_Graph, E be
set, G4 be
reverseEdgeDirections of G3, E;
let G1 be
Supergraph of G3, G2 be
reverseEdgeDirections of G1, E;
assume
A1: E
c= (
the_Edges_of G3);
(
the_Edges_of G3)
c= (
the_Edges_of G1) by
GLIB_006:def 9;
then
A2: E
c= (
the_Edges_of G1) by
A1,
XBOOLE_1: 1;
now
(
the_Vertices_of G2)
= (
the_Vertices_of G1) & (
the_Vertices_of G3)
= (
the_Vertices_of G4) by
GLIB_007: 4;
hence (
the_Vertices_of G4)
c= (
the_Vertices_of G2) by
GLIB_006:def 9;
(
the_Edges_of G4)
= (
the_Edges_of G3) & (
the_Edges_of G2)
= (
the_Edges_of G1) by
GLIB_007: 4;
hence (
the_Edges_of G4)
c= (
the_Edges_of G2) by
GLIB_006:def 9;
let e be
set;
assume
A3: e
in (
the_Edges_of G4);
set v4 = ((
the_Source_of G4)
. e), w4 = ((
the_Target_of G4)
. e);
per cases ;
suppose
A4: e
in E;
e
DJoins (v4,w4,G4) by
A3,
GLIB_000:def 14;
then e
DJoins (w4,v4,G3) by
A1,
A4,
GLIB_007: 7;
then e
DJoins (w4,v4,G1) by
GLIB_006: 70;
then e
DJoins (v4,w4,G2) by
A2,
A4,
GLIB_007: 7;
hence ((
the_Source_of G4)
. e)
= ((
the_Source_of G2)
. e) & ((
the_Target_of G4)
. e)
= ((
the_Target_of G2)
. e) by
GLIB_000:def 14;
end;
suppose
A5: not e
in E;
e
DJoins (v4,w4,G4) by
A3,
GLIB_000:def 14;
then e
DJoins (v4,w4,G3) by
A1,
A5,
GLIB_007: 8;
then e
DJoins (v4,w4,G1) by
GLIB_006: 70;
then e
DJoins (v4,w4,G2) by
A2,
A5,
GLIB_007: 8;
hence ((
the_Source_of G4)
. e)
= ((
the_Source_of G2)
. e) & ((
the_Target_of G4)
. e)
= ((
the_Target_of G2)
. e) by
GLIB_000:def 14;
end;
end;
hence G2 is
Supergraph of G4 by
GLIB_006:def 9;
end;
theorem ::
GLIBPRE0:53
for G2 be
_Graph, v be
object, G1 be
addVertex of G2, v holds G1 is
addAdjVertexAll of G2, v,
{}
proof
let G2 be
_Graph, v be
object, G1 be
addVertex of G2, v;
per cases ;
suppose
A1: not v
in (
the_Vertices_of G2);
A2:
{}
c= (
the_Vertices_of G2) by
XBOOLE_1: 2;
now
thus (
the_Vertices_of G1)
= ((
the_Vertices_of G2)
\/
{v}) by
GLIB_006:def 10;
hereby
let e be
object;
not e
Joins (v,v,G2) by
A1,
GLIB_000: 13;
hence not e
Joins (v,v,G1) by
GLIB_006: 87;
let v1 be
object;
hereby
assume not v1
in
{} ;
not e
Joins (v1,v,G2) by
A1,
GLIB_000: 13;
hence not e
Joins (v1,v,G1) by
GLIB_006: 87;
end;
let v2 be
object;
assume v1
<> v & v2
<> v & e
DJoins (v1,v2,G1);
hence e
DJoins (v1,v2,G2) by
GLIB_006: 85;
end;
take E =
{} ;
thus (
card
{} )
= (
card E);
thus E
misses (
the_Edges_of G2) by
XBOOLE_1: 65;
thus (
the_Edges_of G1)
= ((
the_Edges_of G2)
\/ E) by
GLIB_006:def 10;
let v1 be
object;
assume v1
in
{} ;
hence ex e1 be
object st e1
in E & e1
Joins (v1,v,G1) & for e2 be
object st e2
Joins (v1,v,G1) holds e1
= e2;
end;
hence thesis by
A1,
A2,
GLIB_007:def 4;
end;
suppose
A3: v
in (
the_Vertices_of G2);
then G1
== G2 by
ZFMISC_1: 31,
GLIB_006: 78;
hence thesis by
A3,
GLIB_007:def 4;
end;
end;
theorem ::
GLIBPRE0:54
Th58: for G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 & E
c= (
the_Edges_of G1) holds (v2
.edgesIn() )
= (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E)) & (v2
.edgesOut() )
= (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E))
proof
let G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2 & E
c= (
the_Edges_of G1);
now
let e be
object;
A2: e is
set by
TARSKI: 1;
hereby
assume e
in (v2
.edgesIn() );
then
consider x be
set such that
A3: e
DJoins (x,v2,G2) by
GLIB_000: 57;
per cases ;
suppose
A4: e
in E;
then e
DJoins (v2,x,G1) by
A1,
A3,
GLIB_007: 7;
then e
in (v1
.edgesOut() ) by
A1,
A2,
GLIB_000: 59;
then e
in ((v1
.edgesOut() )
/\ E) by
A4,
XBOOLE_0:def 4;
hence e
in (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E)) by
XBOOLE_0:def 3;
end;
suppose
A5: not e
in E;
then e
DJoins (x,v2,G1) by
A1,
A3,
GLIB_007: 8;
then e
in (v1
.edgesIn() ) by
A1,
A2,
GLIB_000: 57;
then e
in ((v1
.edgesIn() )
\ E) by
A5,
XBOOLE_0:def 5;
hence e
in (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E)) by
XBOOLE_0:def 3;
end;
end;
assume e
in (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E));
per cases by
XBOOLE_0:def 3;
suppose e
in ((v1
.edgesIn() )
\ E);
then
A6: e
in (v1
.edgesIn() ) & not e
in E by
XBOOLE_0:def 5;
then
consider x be
set such that
A7: e
DJoins (x,v1,G1) by
GLIB_000: 57;
e
DJoins (x,v1,G2) by
A1,
A6,
A7,
GLIB_007: 8;
hence e
in (v2
.edgesIn() ) by
A1,
A2,
GLIB_000: 57;
end;
suppose e
in ((v1
.edgesOut() )
/\ E);
then
A8: e
in (v1
.edgesOut() ) & e
in E by
XBOOLE_0:def 4;
then
consider x be
set such that
A9: e
DJoins (v1,x,G1) by
GLIB_000: 59;
e
DJoins (x,v1,G2) by
A1,
A8,
A9,
GLIB_007: 7;
hence e
in (v2
.edgesIn() ) by
A1,
A2,
GLIB_000: 57;
end;
end;
hence (v2
.edgesIn() )
= (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E)) by
TARSKI: 2;
now
let e be
object;
A10: e is
set by
TARSKI: 1;
hereby
assume e
in (v2
.edgesOut() );
then
consider x be
set such that
A11: e
DJoins (v2,x,G2) by
GLIB_000: 59;
per cases ;
suppose
A12: e
in E;
then e
DJoins (x,v2,G1) by
A1,
A11,
GLIB_007: 7;
then e
in (v1
.edgesIn() ) by
A1,
A10,
GLIB_000: 57;
then e
in ((v1
.edgesIn() )
/\ E) by
A12,
XBOOLE_0:def 4;
hence e
in (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)) by
XBOOLE_0:def 3;
end;
suppose
A13: not e
in E;
then e
DJoins (v2,x,G1) by
A1,
A11,
GLIB_007: 8;
then e
in (v1
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
then e
in ((v1
.edgesOut() )
\ E) by
A13,
XBOOLE_0:def 5;
hence e
in (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)) by
XBOOLE_0:def 3;
end;
end;
assume e
in (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E));
per cases by
XBOOLE_0:def 3;
suppose e
in ((v1
.edgesOut() )
\ E);
then
A14: e
in (v1
.edgesOut() ) & not e
in E by
XBOOLE_0:def 5;
then
consider x be
set such that
A15: e
DJoins (v1,x,G1) by
GLIB_000: 59;
e
DJoins (v1,x,G2) by
A1,
A14,
A15,
GLIB_007: 8;
hence e
in (v2
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
end;
suppose e
in ((v1
.edgesIn() )
/\ E);
then
A16: e
in (v1
.edgesIn() ) & e
in E by
XBOOLE_0:def 4;
then
consider x be
set such that
A17: e
DJoins (x,v1,G1) by
GLIB_000: 57;
e
DJoins (v1,x,G2) by
A1,
A16,
A17,
GLIB_007: 7;
hence e
in (v2
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
end;
end;
hence (v2
.edgesOut() )
= (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)) by
TARSKI: 2;
end;
theorem ::
GLIBPRE0:55
for G1 be
_Graph, G2 be
reverseEdgeDirections of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.edgesIn() )
= (v1
.edgesOut() ) & (v2
.inDegree() )
= (v1
.outDegree() ) & (v2
.edgesOut() )
= (v1
.edgesIn() ) & (v2
.outDegree() )
= (v1
.inDegree() )
proof
let G1 be
_Graph, G2 be
reverseEdgeDirections of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
now
let e be
object;
hereby
assume
A2: e
in (v2
.edgesIn() );
A3: e is
set by
TARSKI: 1;
consider x be
set such that
A4: e
DJoins (x,v2,G2) by
A2,
GLIB_000: 57;
e
in (
the_Edges_of G2) by
A4,
GLIB_000:def 14;
then e
in (
the_Edges_of G1) by
GLIB_007: 4;
then e
DJoins (v1,x,G1) by
A1,
A4,
GLIB_007: 7;
hence e
in (v1
.edgesOut() ) by
A3,
GLIB_000: 59;
end;
assume
A5: e
in (v1
.edgesOut() );
A6: e is
set by
TARSKI: 1;
consider x be
set such that
A7: e
DJoins (v1,x,G1) by
A5,
GLIB_000: 59;
e
in (
the_Edges_of G1) by
A7,
GLIB_000:def 14;
then e
DJoins (x,v2,G2) by
A1,
A7,
GLIB_007: 7;
hence e
in (v2
.edgesIn() ) by
A6,
GLIB_000: 57;
end;
hence (v2
.edgesIn() )
= (v1
.edgesOut() ) by
TARSKI: 2;
hence (v2
.inDegree() )
= (v1
.outDegree() );
now
let e be
object;
hereby
assume
A8: e
in (v2
.edgesOut() );
A9: e is
set by
TARSKI: 1;
consider x be
set such that
A10: e
DJoins (v2,x,G2) by
A8,
GLIB_000: 59;
e
in (
the_Edges_of G2) by
A10,
GLIB_000:def 14;
then e
in (
the_Edges_of G1) by
GLIB_007: 4;
then e
DJoins (x,v1,G1) by
A1,
A10,
GLIB_007: 7;
hence e
in (v1
.edgesIn() ) by
A9,
GLIB_000: 57;
end;
assume
A11: e
in (v1
.edgesIn() );
A12: e is
set by
TARSKI: 1;
consider x be
set such that
A13: e
DJoins (x,v1,G1) by
A11,
GLIB_000: 57;
e
in (
the_Edges_of G1) by
A13,
GLIB_000:def 14;
then e
DJoins (v2,x,G2) by
A1,
A13,
GLIB_007: 7;
hence e
in (v2
.edgesOut() ) by
A12,
GLIB_000: 59;
end;
hence (v2
.edgesOut() )
= (v1
.edgesIn() ) by
TARSKI: 2;
hence (v2
.outDegree() )
= (v1
.inDegree() );
end;
theorem ::
GLIBPRE0:56
Th60: for G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.edgesInOut() )
= (v1
.edgesInOut() ) & (v2
.degree() )
= (v1
.degree() )
proof
let G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
per cases ;
suppose E
c= (
the_Edges_of G1);
then
A2: (v2
.edgesIn() )
= (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E)) & (v2
.edgesOut() )
= (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)) by
A1,
Th58;
thus (v2
.edgesInOut() )
= (((((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesOut() )
/\ E))
\/ ((v1
.edgesIn() )
/\ E))
\/ ((v1
.edgesOut() )
\ E)) by
A2,
XBOOLE_1: 4
.= (((((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesIn() )
/\ E))
\/ ((v1
.edgesOut() )
/\ E))
\/ ((v1
.edgesOut() )
\ E)) by
XBOOLE_1: 4
.= (((v1
.edgesIn() )
\/ ((v1
.edgesOut() )
/\ E))
\/ ((v1
.edgesOut() )
\ E)) by
XBOOLE_1: 51
.= ((v1
.edgesIn() )
\/ (((v1
.edgesOut() )
/\ E)
\/ ((v1
.edgesOut() )
\ E))) by
XBOOLE_1: 4
.= (v1
.edgesInOut() ) by
XBOOLE_1: 51;
thus (v2
.degree() )
= (((
card ((v1
.edgesIn() )
\ E))
+` (
card ((v1
.edgesOut() )
/\ E)))
+` (
card (((v1
.edgesOut() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)))) by
A2,
Th2,
CARD_2: 35
.= (((
card ((v1
.edgesIn() )
\ E))
+` (
card ((v1
.edgesOut() )
/\ E)))
+` ((
card ((v1
.edgesOut() )
\ E))
+` (
card ((v1
.edgesIn() )
/\ E)))) by
Th2,
CARD_2: 35
.= ((((
card ((v1
.edgesIn() )
\ E))
+` (
card ((v1
.edgesOut() )
/\ E)))
+` (
card ((v1
.edgesIn() )
/\ E)))
+` (
card ((v1
.edgesOut() )
\ E))) by
CARD_2: 19
.= ((((
card ((v1
.edgesIn() )
\ E))
+` (
card ((v1
.edgesIn() )
/\ E)))
+` (
card ((v1
.edgesOut() )
/\ E)))
+` (
card ((v1
.edgesOut() )
\ E))) by
CARD_2: 19
.= (((
card (((v1
.edgesIn() )
\ E)
\/ ((v1
.edgesIn() )
/\ E)))
+` (
card ((v1
.edgesOut() )
/\ E)))
+` (
card ((v1
.edgesOut() )
\ E))) by
Th2,
CARD_2: 35
.= (((v1
.inDegree() )
+` (
card ((v1
.edgesOut() )
/\ E)))
+` (
card ((v1
.edgesOut() )
\ E))) by
XBOOLE_1: 51
.= ((v1
.inDegree() )
+` ((
card ((v1
.edgesOut() )
/\ E))
+` (
card ((v1
.edgesOut() )
\ E)))) by
CARD_2: 19
.= ((v1
.inDegree() )
+` (
card (((v1
.edgesOut() )
/\ E)
\/ ((v1
.edgesOut() )
\ E)))) by
Th2,
CARD_2: 35
.= (v1
.degree() ) by
XBOOLE_1: 51;
end;
suppose not E
c= (
the_Edges_of G1);
then G1
== G2 by
GLIB_007:def 1;
hence thesis by
A1,
GLIB_000: 96;
end;
end;
theorem ::
GLIBPRE0:57
for G2 be
_Graph, v be
object, V be
set holds for G1 be
addAdjVertexAll of G2, v, V, w be
Vertex of G1 st V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2) & v
= w holds (w
.allNeighbors() )
= V & (w
.degree() )
= (
card V)
proof
let G2 be
_Graph, v be
object, V be
set;
let G1 be
addAdjVertexAll of G2, v, V, w be
Vertex of G1;
assume
A1: V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2) & v
= w;
then
consider E be
set such that
A2: (
card V)
= (
card E) & E
misses (
the_Edges_of G2) and
A3: (
the_Edges_of G1)
= ((
the_Edges_of G2)
\/ E) and
A4: for v1 be
object st v1
in V holds ex e1 be
object st e1
in E & e1
Joins (v1,v,G1) & for e2 be
object st e2
Joins (v1,v,G1) holds e1
= e2 by
GLIB_007:def 4;
now
let x be
object;
hereby
assume x
in (w
.allNeighbors() );
then
consider e be
object such that
A5: e
Joins (w,x,G1) by
GLIB_000: 71;
not e
in (
the_Edges_of G2)
proof
assume e
in (
the_Edges_of G2);
then e
Joins (w,x,G2) by
A5,
GLIB_006: 72;
hence contradiction by
A1,
GLIB_000: 13;
end;
then w
= v & x
in V or x
= v & w
in V by
A1,
A2,
A3,
A5,
GLIB_007: 51;
hence x
in V by
A1;
end;
assume x
in V;
then
consider e1 be
object such that
A6: e1
in E & e1
Joins (x,v,G1) and for e2 be
object st e2
Joins (x,v,G1) holds e1
= e2 by
A4;
x is
set by
TARSKI: 1;
hence x
in (w
.allNeighbors() ) by
A1,
A6,
GLIB_000: 14,
GLIB_000: 71;
end;
hence (w
.allNeighbors() )
= V by
TARSKI: 2;
per cases ;
suppose
A7: V
<>
{} ;
V
c= V;
then
consider f be
Function of V, (G1
.edgesBetween (V,
{v})) such that
A8: f is
one-to-one
onto and
A9: for u be
object st u
in V holds (f
. u)
Joins (u,v,G1) by
A1,
GLIB_007: 57;
A10: (
rng f)
= (G1
.edgesBetween (V,
{w})) by
A1,
A8,
FUNCT_2:def 3;
(
the_Vertices_of G2)
c= (
the_Vertices_of G1) by
GLIB_006:def 9;
then V
c= (
the_Vertices_of G1) by
A1,
XBOOLE_1: 1;
then
A11: (G1
.edgesBetween (V,
{w}))
c= (G1
.edgesBetween ((
the_Vertices_of G1),
{w})) by
GLIB_000: 37;
now
let e be
object;
assume e
in (G1
.edgesBetween ((
the_Vertices_of G1),
{w}));
then
A12: e
SJoins ((
the_Vertices_of G1),
{w},G1) by
GLIB_000:def 30;
ex u be
object st e
Joins (u,w,G1)
proof
per cases by
A12,
GLIB_000:def 15;
suppose
A13: ((
the_Source_of G1)
. e)
in (
the_Vertices_of G1) & ((
the_Target_of G1)
. e)
in
{w};
take ((
the_Source_of G1)
. e);
A14: ((
the_Target_of G1)
. e)
= w by
A13,
TARSKI:def 1;
e
in (
the_Edges_of G1) by
A12,
GLIB_000:def 15;
hence e
Joins (((
the_Source_of G1)
. e),w,G1) by
A14,
GLIB_000:def 13;
end;
suppose
A15: ((
the_Target_of G1)
. e)
in (
the_Vertices_of G1) & ((
the_Source_of G1)
. e)
in
{w};
take ((
the_Target_of G1)
. e);
A16: ((
the_Source_of G1)
. e)
= w by
A15,
TARSKI:def 1;
e
in (
the_Edges_of G1) by
A12,
GLIB_000:def 15;
hence e
Joins (((
the_Target_of G1)
. e),w,G1) by
A16,
GLIB_000:def 13;
end;
end;
then
consider u be
object such that
A17: e
Joins (u,w,G1);
u
in V & w
in
{w} by
A1,
A17,
GLIB_007:def 4,
TARSKI:def 1;
then e
SJoins (V,
{w},G1) by
A17,
GLIB_000: 17;
hence e
in (G1
.edgesBetween (V,
{w})) by
GLIB_000:def 30;
end;
then (G1
.edgesBetween ((
the_Vertices_of G1),
{w}))
c= (G1
.edgesBetween (V,
{w})) by
TARSKI:def 3;
then (G1
.edgesBetween (V,
{w}))
= (G1
.edgesBetween ((
the_Vertices_of G1),
{w})) by
A11,
XBOOLE_0:def 10;
then
A18: (
rng f)
= (w
.edgesInOut() ) by
A10,
Th33;
set u = the
Element of V;
A19: u
in V & v
in
{v} by
A7,
TARSKI:def 1;
then (f
. u)
Joins (u,v,G1) by
A9;
then (f
. u)
SJoins (V,
{v},G1) by
A19,
GLIB_000: 17;
then (f
. u)
in (G1
.edgesBetween (V,
{v})) by
GLIB_000:def 30;
then (
dom f)
= V by
FUNCT_2:def 1;
then
A20: (
card V)
= (
card (w
.edgesInOut() )) by
A8,
A18,
CARD_1: 70;
for e be
object holds not e
Joins (w,w,G1) by
A1,
GLIB_007:def 4;
hence (w
.degree() )
= (
card V) by
A20,
Th36;
end;
suppose
A21: V
=
{} ;
then
A22: G1 is
addVertex of G2, v by
GLIB_007: 55;
(
{w}
\ (
the_Vertices_of G2))
=
{w} by
A1,
ZFMISC_1: 59;
then w
in (
{v}
\ (
the_Vertices_of G2)) by
A1,
TARSKI:def 1;
hence (w
.degree() )
= (
card V) by
A21,
A22,
Th39,
GLIB_006: 88;
end;
end;
theorem ::
GLIBPRE0:58
Th62: for G2 be
_Graph, v be
object, V be
set holds for G1 be
addAdjVertexAll of G2, v, V holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 & not v2
in V holds (v1
.edgesIn() )
= (v2
.edgesIn() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.edgesOut() )
= (v2
.edgesOut() ) & (v1
.outDegree() )
= (v2
.outDegree() ) & (v1
.edgesInOut() )
= (v2
.edgesInOut() ) & (v1
.degree() )
= (v2
.degree() )
proof
let G2 be
_Graph, v be
object, V be
set;
let G1 be
addAdjVertexAll of G2, v, V;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2 & not v2
in V;
per cases ;
suppose
A2: V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2);
A3: G2 is
Subgraph of G1 by
GLIB_006: 57;
then
A4: (v2
.edgesIn() )
c= (v1
.edgesIn() ) by
A1,
GLIB_000: 78;
now
let e be
object;
A5: e is
set by
TARSKI: 1;
assume e
in (v1
.edgesIn() );
then
consider x be
set such that
A6: e
DJoins (x,v1,G1) by
GLIB_000: 57;
A7: x
<> v
proof
assume x
= v;
then e
Joins (v1,v,G1) by
A6,
GLIB_000: 16;
hence contradiction by
A1,
A2,
GLIB_007:def 4;
end;
v1
<> v by
A1,
A2;
then e
DJoins (x,v1,G2) by
A2,
A6,
A7,
GLIB_007:def 4;
hence e
in (v2
.edgesIn() ) by
A1,
A5,
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v2
.edgesIn() ) by
TARSKI:def 3;
hence
A8: (v1
.edgesIn() )
= (v2
.edgesIn() ) by
A4,
XBOOLE_0:def 10;
hence (v1
.inDegree() )
= (v2
.inDegree() );
A9: (v2
.edgesOut() )
c= (v1
.edgesOut() ) by
A1,
A3,
GLIB_000: 78;
now
let e be
object;
A10: e is
set by
TARSKI: 1;
assume e
in (v1
.edgesOut() );
then
consider x be
set such that
A11: e
DJoins (v1,x,G1) by
GLIB_000: 59;
A12: x
<> v
proof
assume x
= v;
then e
Joins (v1,v,G1) by
A11,
GLIB_000: 16;
hence contradiction by
A1,
A2,
GLIB_007:def 4;
end;
v1
<> v by
A1,
A2;
then e
DJoins (v1,x,G2) by
A2,
A11,
A12,
GLIB_007:def 4;
hence e
in (v2
.edgesOut() ) by
A1,
A10,
GLIB_000: 59;
end;
then (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
TARSKI:def 3;
hence
A13: (v1
.edgesOut() )
= (v2
.edgesOut() ) by
A9,
XBOOLE_0:def 10;
hence (v1
.outDegree() )
= (v2
.outDegree() );
thus thesis by
A8,
A13;
end;
suppose not (V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2));
then G1
== G2 by
GLIB_007:def 4;
hence thesis by
A1,
GLIB_000: 96;
end;
end;
theorem ::
GLIBPRE0:59
for G2 be
_Graph, v be
object, V be
Subset of (
the_Vertices_of G2) holds for G1 be
addAdjVertexAll of G2, v, V holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st not v
in (
the_Vertices_of G2) & v1
= v2 & v2
in V holds (v1
.allNeighbors() )
= ((v2
.allNeighbors() )
\/
{v}) & (v1
.degree() )
= ((v2
.degree() )
+` 1)
proof
let G2 be
_Graph, v be
object, V be
Subset of (
the_Vertices_of G2);
let G1 be
addAdjVertexAll of G2, v, V;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
A1: v is
set by
TARSKI: 1;
assume
A2: not v
in (
the_Vertices_of G2) & v1
= v2 & v2
in V;
A3: G2 is
Subgraph of G1 by
GLIB_006: 57;
then
A4: (v2
.allNeighbors() )
c= (v1
.allNeighbors() ) by
A2,
GLIB_000: 82;
consider E be
set such that
A5: (
card V)
= (
card E) & E
misses (
the_Edges_of G2) and (
the_Edges_of G1)
= ((
the_Edges_of G2)
\/ E) and
A6: for w1 be
object st w1
in V holds ex e1 be
object st e1
in E & e1
Joins (w1,v,G1) & for e2 be
object st e2
Joins (w1,v,G1) holds e1
= e2 by
A2,
GLIB_007:def 4;
consider e1 be
object such that
A7: e1
in E & e1
Joins (v2,v,G1) and
A8: for e2 be
object st e2
Joins (v2,v,G1) holds e1
= e2 by
A2,
A6;
e1
Joins (v1,v,G1) & v is
set by
A2,
A7,
TARSKI: 1;
then
{v}
c= (v1
.allNeighbors() ) by
GLIB_000: 71,
ZFMISC_1: 31;
then
A9: ((v2
.allNeighbors() )
\/
{v})
c= (v1
.allNeighbors() ) by
A4,
XBOOLE_1: 8;
now
let x be
object;
assume x
in (v1
.allNeighbors() );
then
consider e2 be
object such that
A10: e2
Joins (v1,x,G1) by
GLIB_000: 71;
per cases ;
suppose x
<> v;
then v1
<> v & x
<> v by
A2;
then e2
Joins (v2,x,G2) & x is
set by
A2,
A10,
GLIB_007: 49,
TARSKI: 1;
then x
in (v2
.allNeighbors() ) by
GLIB_000: 71;
hence x
in ((v2
.allNeighbors() )
\/
{v}) by
XBOOLE_0:def 3;
end;
suppose x
= v;
then x
in
{v} by
TARSKI:def 1;
hence x
in ((v2
.allNeighbors() )
\/
{v}) by
XBOOLE_0:def 3;
end;
end;
then (v1
.allNeighbors() )
c= ((v2
.allNeighbors() )
\/
{v}) by
TARSKI:def 3;
hence (v1
.allNeighbors() )
= ((v2
.allNeighbors() )
\/
{v}) by
A9,
XBOOLE_0:def 10;
A11: (v2
.edgesOut() )
c= (v1
.edgesOut() ) & (v2
.edgesIn() )
c= (v1
.edgesIn() ) by
A2,
A3,
GLIB_000: 78;
A12: e1 is
set by
TARSKI: 1;
per cases by
A7,
GLIB_000: 16;
suppose
A13: e1
DJoins (v2,v,G1);
then
{e1}
c= (v1
.edgesOut() ) by
A1,
A2,
A12,
GLIB_000: 59,
ZFMISC_1: 31;
then
A14: ((v2
.edgesOut() )
\/
{e1})
c= (v1
.edgesOut() ) by
A11,
XBOOLE_1: 8;
now
let e2 be
object;
assume e2
in (v1
.edgesOut() );
then
consider x be
set such that
A15: e2
DJoins (v1,x,G1) by
GLIB_000: 59;
per cases ;
suppose x
<> v;
then
A16: x
<> v & v1
<> v & e2 is
set by
A2,
TARSKI: 1;
then e2
DJoins (v1,x,G2) by
A2,
A15,
GLIB_007:def 4;
then e2
in (v2
.edgesOut() ) by
A2,
A16,
GLIB_000: 59;
hence e2
in ((v2
.edgesOut() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
suppose x
= v;
then e2
Joins (v2,v,G1) by
A2,
A15,
GLIB_000: 16;
then e1
= e2 by
A8;
then e2
in
{e1} by
TARSKI:def 1;
hence e2
in ((v2
.edgesOut() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
end;
then (v1
.edgesOut() )
c= ((v2
.edgesOut() )
\/
{e1}) by
TARSKI:def 3;
then
A17: (v1
.edgesOut() )
= ((v2
.edgesOut() )
\/
{e1}) by
A14,
XBOOLE_0:def 10;
now
let e2 be
object;
assume e2
in (v1
.edgesIn() );
then
consider x be
set such that
A18: e2
DJoins (x,v1,G1) by
GLIB_000: 57;
A19: e2 is
set & v1
<> v by
A2,
TARSKI: 1;
x
<> v
proof
assume
A20: x
= v;
then e2
Joins (v2,v,G1) by
A2,
A18,
GLIB_000: 16;
then e1
= e2 by
A8;
then x
= v1 by
A2,
A13,
A18,
GLIB_009: 6;
hence contradiction by
A2,
A20;
end;
then e2
DJoins (x,v1,G2) by
A2,
A18,
A19,
GLIB_007:def 4;
hence e2
in (v2
.edgesIn() ) by
A2,
A19,
GLIB_000: 57;
end;
then (v1
.edgesIn() )
c= (v2
.edgesIn() ) by
TARSKI:def 3;
then
A21: (v1
.edgesIn() )
= (v2
.edgesIn() ) by
A11,
XBOOLE_0:def 10;
not e1
in (
the_Edges_of G2)
proof
assume e1
in (
the_Edges_of G2);
then e1
in (E
/\ (
the_Edges_of G2)) by
A7,
XBOOLE_0:def 4;
hence contradiction by
A5,
XBOOLE_0: 4;
end;
then not e1
in (v2
.edgesOut() );
then
A22:
{e1}
misses (v2
.edgesOut() ) by
ZFMISC_1: 50;
thus (v1
.degree() )
= ((v2
.inDegree() )
+` ((
card (v2
.edgesOut() ))
+` (
card
{e1}))) by
A17,
A21,
A22,
CARD_2: 35
.= ((v2
.inDegree() )
+` ((v2
.outDegree() )
+` 1)) by
CARD_1: 30
.= ((v2
.degree() )
+` 1) by
CARD_2: 19;
end;
suppose
A23: e1
DJoins (v,v2,G1);
then
{e1}
c= (v1
.edgesIn() ) by
A1,
A2,
A12,
GLIB_000: 57,
ZFMISC_1: 31;
then
A24: ((v2
.edgesIn() )
\/
{e1})
c= (v1
.edgesIn() ) by
A11,
XBOOLE_1: 8;
now
let e2 be
object;
assume e2
in (v1
.edgesIn() );
then
consider x be
set such that
A25: e2
DJoins (x,v1,G1) by
GLIB_000: 57;
per cases ;
suppose x
<> v;
then
A26: x
<> v & v1
<> v & e2 is
set by
A2,
TARSKI: 1;
then e2
DJoins (x,v1,G2) by
A2,
A25,
GLIB_007:def 4;
then e2
in (v2
.edgesIn() ) by
A2,
A26,
GLIB_000: 57;
hence e2
in ((v2
.edgesIn() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
suppose x
= v;
then e2
Joins (v2,v,G1) by
A2,
A25,
GLIB_000: 16;
then e1
= e2 by
A8;
then e2
in
{e1} by
TARSKI:def 1;
hence e2
in ((v2
.edgesIn() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
end;
then (v1
.edgesIn() )
c= ((v2
.edgesIn() )
\/
{e1}) by
TARSKI:def 3;
then
A27: (v1
.edgesIn() )
= ((v2
.edgesIn() )
\/
{e1}) by
A24,
XBOOLE_0:def 10;
now
let e2 be
object;
assume e2
in (v1
.edgesOut() );
then
consider x be
set such that
A28: e2
DJoins (v1,x,G1) by
GLIB_000: 59;
A29: e2 is
set & v1
<> v by
A2,
TARSKI: 1;
x
<> v
proof
assume
A30: x
= v;
then e2
Joins (v2,v,G1) by
A2,
A28,
GLIB_000: 16;
then e1
= e2 by
A8;
then x
= v1 by
A2,
A23,
A28,
GLIB_009: 6;
hence contradiction by
A2,
A30;
end;
then e2
DJoins (v1,x,G2) by
A2,
A28,
A29,
GLIB_007:def 4;
hence e2
in (v2
.edgesOut() ) by
A2,
A29,
GLIB_000: 59;
end;
then (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
TARSKI:def 3;
then
A31: (v1
.edgesOut() )
= (v2
.edgesOut() ) by
A11,
XBOOLE_0:def 10;
not e1
in (
the_Edges_of G2)
proof
assume e1
in (
the_Edges_of G2);
then e1
in (E
/\ (
the_Edges_of G2)) by
A7,
XBOOLE_0:def 4;
hence contradiction by
A5,
XBOOLE_0: 4;
end;
then not e1
in (v2
.edgesIn() );
then
A32:
{e1}
misses (v2
.edgesIn() ) by
ZFMISC_1: 50;
thus (v1
.degree() )
= ((v2
.outDegree() )
+` ((
card (v2
.edgesIn() ))
+` (
card
{e1}))) by
A27,
A31,
A32,
CARD_2: 35
.= ((v2
.outDegree() )
+` ((v2
.inDegree() )
+` 1)) by
CARD_1: 30
.= ((v2
.degree() )
+` 1) by
CARD_2: 19;
end;
end;
theorem ::
GLIBPRE0:60
for G2 be
_Graph, v be
object, V be
set holds for G1 be
addAdjVertexAll of G2, v, V holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v1
.degree() )
c= ((v2
.degree() )
+` 1) & (v1
.inDegree() )
c= ((v2
.inDegree() )
+` 1) & (v1
.outDegree() )
c= ((v2
.outDegree() )
+` 1)
proof
let G2 be
_Graph, v be
object, V be
set;
let G1 be
addAdjVertexAll of G2, v, V;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
per cases ;
suppose
A2: V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2) & v2
in V;
then
consider E be
set such that
A3: (
card V)
= (
card E) & E
misses (
the_Edges_of G2) and (
the_Edges_of G1)
= ((
the_Edges_of G2)
\/ E) and
A4: for v3 be
object st v3
in V holds ex e1 be
object st e1
in E & e1
Joins (v3,v,G1) & for e2 be
object st e2
Joins (v3,v,G1) holds e1
= e2 by
GLIB_007:def 4;
consider e1 be
object such that
A5: e1
in E & e1
Joins (v2,v,G1) and
A6: for e2 be
object st e2
Joins (v2,v,G1) holds e1
= e2 by
A2,
A4;
A7: v2
<> v by
A2;
now
let e2 be
object;
assume e2
in (v1
.edgesIn() );
then
consider x be
set such that
A8: e2
DJoins (x,v1,G1) by
GLIB_000: 57;
per cases ;
suppose x
= v;
then e2
Joins (v1,v,G1) by
A8,
GLIB_000: 16;
then e2
= e1 by
A1,
A6;
then e2
in
{e1} by
TARSKI:def 1;
hence e2
in ((v2
.edgesIn() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
suppose x
<> v;
then
A9: e2
DJoins (x,v1,G2) by
A1,
A2,
A7,
A8,
GLIB_007:def 4;
e2 is
set by
TARSKI: 1;
then e2
in (v2
.edgesIn() ) by
A1,
A9,
GLIB_000: 57;
hence e2
in ((v2
.edgesIn() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
end;
then
A10: (v1
.edgesIn() )
c= ((v2
.edgesIn() )
\/
{e1}) by
TARSKI:def 3;
now
let e2 be
object;
assume e2
in (v1
.edgesOut() );
then
consider x be
set such that
A11: e2
DJoins (v1,x,G1) by
GLIB_000: 59;
per cases ;
suppose x
= v;
then e2
Joins (v1,v,G1) by
A11,
GLIB_000: 16;
then e2
= e1 by
A1,
A6;
then e2
in
{e1} by
TARSKI:def 1;
hence e2
in ((v2
.edgesOut() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
suppose x
<> v;
then
A12: e2
DJoins (v1,x,G2) by
A1,
A2,
A7,
A11,
GLIB_007:def 4;
e2 is
set by
TARSKI: 1;
then e2
in (v2
.edgesOut() ) by
A1,
A12,
GLIB_000: 59;
hence e2
in ((v2
.edgesOut() )
\/
{e1}) by
XBOOLE_0:def 3;
end;
end;
then
A13: (v1
.edgesOut() )
c= ((v2
.edgesOut() )
\/
{e1}) by
TARSKI:def 3;
A14: (v1
.edgesIn() )
= (v2
.edgesIn() ) or (v1
.edgesOut() )
= (v2
.edgesOut() )
proof
assume
A15: (v1
.edgesIn() )
<> (v2
.edgesIn() ) & (v1
.edgesOut() )
<> (v2
.edgesOut() );
G2 is
Subgraph of G1 by
GLIB_006: 57;
then (v2
.edgesIn() )
c= (v1
.edgesIn() ) & (v2
.edgesOut() )
c= (v1
.edgesOut() ) by
A1,
GLIB_000: 78;
then not (v1
.edgesIn() )
c= (v2
.edgesIn() ) & not (v1
.edgesOut() )
c= (v2
.edgesOut() ) by
A15,
XBOOLE_0:def 10;
then
A16: ((v1
.edgesIn() )
\ (v2
.edgesIn() ))
<>
{} & ((v1
.edgesOut() )
\ (v2
.edgesOut() ))
<>
{} by
XBOOLE_1: 37;
then
consider i be
object such that
A17: i
in ((v1
.edgesIn() )
\ (v2
.edgesIn() )) by
XBOOLE_0:def 1;
consider o be
object such that
A18: o
in ((v1
.edgesOut() )
\ (v2
.edgesOut() )) by
A16,
XBOOLE_0:def 1;
A19: i
in (v1
.edgesIn() ) & not i
in (v2
.edgesIn() ) & o
in (v1
.edgesOut() ) & not o
in (v2
.edgesOut() ) by
A17,
A18,
XBOOLE_0:def 5;
then i
in
{e1} & o
in
{e1} by
A10,
A13,
XBOOLE_0:def 3;
then
A20: i
= e1 & o
= e1 by
TARSKI:def 1;
then
consider j be
set such that
A21: e1
DJoins (j,v1,G1) by
A19,
GLIB_000: 57;
consider p be
set such that
A22: e1
DJoins (v1,p,G1) by
A19,
A20,
GLIB_000: 59;
j
= v1 & v1
= p by
A21,
A22,
GLIB_009: 6;
then e1
Joins (v1,v1,G1) by
A21,
GLIB_000: 16;
hence contradiction by
A1,
A5,
A7,
GLIB_000: 15;
end;
{e1}
misses (
the_Edges_of G2) by
A3,
A5,
ZFMISC_1: 31,
XBOOLE_1: 63;
then
A23:
{e1}
misses (v2
.edgesIn() ) &
{e1}
misses (v2
.edgesOut() ) by
XBOOLE_1: 63;
then
A24: (
card ((v2
.edgesOut() )
\/
{e1}))
= ((v2
.outDegree() )
+` (
card
{e1})) by
CARD_2: 35
.= ((v2
.outDegree() )
+` 1) by
CARD_1: 30;
A25: (
card ((v2
.edgesIn() )
\/
{e1}))
= ((v2
.inDegree() )
+` (
card
{e1})) by
A23,
CARD_2: 35
.= ((v2
.inDegree() )
+` 1) by
CARD_1: 30;
thus (v1
.degree() )
c= ((v2
.degree() )
+` 1)
proof
per cases by
A14;
suppose (v1
.edgesIn() )
= (v2
.edgesIn() );
then
A26: (v1
.inDegree() )
= (v2
.inDegree() );
(v1
.outDegree() )
c= ((v2
.outDegree() )
+` 1) by
A13,
A24,
CARD_1: 11;
then (v1
.degree() )
c= ((v2
.inDegree() )
+` ((v2
.outDegree() )
+` 1)) by
A26,
CARD_2: 84;
hence thesis by
CARD_2: 19;
end;
suppose (v1
.edgesOut() )
= (v2
.edgesOut() );
then
A27: (v1
.outDegree() )
= (v2
.outDegree() );
(v1
.inDegree() )
c= ((v2
.inDegree() )
+` 1) by
A10,
A25,
CARD_1: 11;
then (v1
.degree() )
c= ((v2
.outDegree() )
+` ((v2
.inDegree() )
+` 1)) by
A27,
CARD_2: 84;
hence thesis by
CARD_2: 19;
end;
end;
thus thesis by
A10,
A13,
A24,
A25,
CARD_1: 11;
end;
suppose not v2
in V;
then (v1
.degree() )
= (v2
.degree() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.outDegree() )
= (v2
.outDegree() ) by
A1,
Th62;
hence thesis by
CARD_2: 94;
end;
suppose not (V
c= (
the_Vertices_of G2) & not v
in (
the_Vertices_of G2));
then G1
== G2 by
GLIB_007:def 4;
then (v1
.degree() )
= (v2
.degree() ) & (v1
.inDegree() )
= (v2
.inDegree() ) & (v1
.outDegree() )
= (v2
.outDegree() ) by
A1,
GLIB_000: 96;
hence thesis by
CARD_2: 94;
end;
end;
begin
theorem ::
GLIBPRE0:61
Th65: for G be
_Graph holds G is
edgeless iff for v,w be
Vertex of G holds not (v,w)
are_adjacent
proof
let G be
_Graph;
hereby
assume
A1: G is
edgeless;
let v,w be
Vertex of G;
not ex e be
object st e
Joins (v,w,G) by
A1,
GLIB_008: 50;
hence not (v,w)
are_adjacent by
CHORD:def 3;
end;
assume
A2: for v,w be
Vertex of G holds not (v,w)
are_adjacent ;
assume G is non
edgeless;
then
consider e be
object such that
A3: e
in (
the_Edges_of G) by
XBOOLE_0:def 1;
set v = ((
the_Source_of G)
. e), w = ((
the_Target_of G)
. e);
reconsider v, w as
Vertex of G by
A3,
FUNCT_2: 5;
e
Joins (v,w,G) by
A3,
GLIB_000:def 13;
hence contradiction by
A2,
CHORD:def 3;
end;
theorem ::
GLIBPRE0:62
for G be
loopless
_Graph holds G is
edgeless iff for v,w be
Vertex of G st v
<> w holds not (v,w)
are_adjacent
proof
let G be
loopless
_Graph;
thus G is
edgeless implies for v,w be
Vertex of G st v
<> w holds not (v,w)
are_adjacent by
Th65;
assume
A1: for v,w be
Vertex of G st v
<> w holds not (v,w)
are_adjacent ;
assume G is non
edgeless;
then
consider e be
object such that
A2: e
in (
the_Edges_of G) by
XBOOLE_0:def 1;
set v = ((
the_Source_of G)
. e), w = ((
the_Target_of G)
. e);
reconsider v, w as
Vertex of G by
A2,
FUNCT_2: 5;
A3: e
Joins (v,w,G) by
A2,
GLIB_000:def 13;
then v
<> w by
GLIB_000: 18;
hence contradiction by
A1,
A3,
CHORD:def 3;
end;
begin
theorem ::
GLIBPRE0:63
Th67: for G be
_Graph holds (G
.loops() )
= (
dom ((
the_Source_of G)
/\ (
the_Target_of G)))
proof
let G be
_Graph;
now
let e be
object;
hereby
assume e
in (G
.loops() );
then
consider v be
object such that
A1: e
DJoins (v,v,G) by
GLIB_009: 45;
e
in (
the_Edges_of G) by
A1,
GLIB_000:def 14;
then
A2: e
in (
dom (
the_Source_of G)) & e
in (
dom (
the_Target_of G)) by
FUNCT_2:def 1;
((
the_Source_of G)
. e)
= v & ((
the_Target_of G)
. e)
= v by
A1,
GLIB_000:def 14;
then
[e, v]
in (
the_Source_of G) &
[e, v]
in (
the_Target_of G) by
A2,
FUNCT_1:def 2;
then
[e, v]
in ((
the_Source_of G)
/\ (
the_Target_of G)) by
XBOOLE_0:def 4;
hence e
in (
dom ((
the_Source_of G)
/\ (
the_Target_of G))) by
FUNCT_1: 1;
end;
set v = (((
the_Source_of G)
/\ (
the_Target_of G))
. e);
assume e
in (
dom ((
the_Source_of G)
/\ (
the_Target_of G)));
then
[e, v]
in ((
the_Source_of G)
/\ (
the_Target_of G)) by
FUNCT_1:def 2;
then
A3:
[e, v]
in (
the_Source_of G) &
[e, v]
in (
the_Target_of G) by
XBOOLE_0:def 4;
then
A4: e
in (
dom (
the_Source_of G)) & e
in (
dom (
the_Target_of G)) by
FUNCT_1: 1;
then ((
the_Source_of G)
. e)
= v & ((
the_Target_of G)
. e)
= v by
A3,
FUNCT_1:def 2;
hence e
in (G
.loops() ) by
A4,
GLIB_000:def 14,
GLIB_009: 45;
end;
hence thesis by
TARSKI: 2;
end;
Lm1: for G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E holds G2 is
reverseEdgeDirections of G1, (E
\ (G1
.loops() ))
proof
let G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E;
per cases ;
suppose
A1: E
c= (
the_Edges_of G1);
then
A2: (
the_Vertices_of G1)
= (
the_Vertices_of G2) & (
the_Edges_of G1)
= (
the_Edges_of G2) by
GLIB_007:def 1;
A3: (E
\ (G1
.loops() ))
c= (
the_Edges_of G1) by
A1,
XBOOLE_1: 1;
set S = (
the_Source_of G1), T = (
the_Target_of G1);
(
dom (T
| (E
/\ (G1
.loops() ))))
c= (
dom T) by
RELAT_1: 60;
then (
dom (T
| (E
/\ (G1
.loops() ))))
c= (
the_Edges_of G1) by
FUNCT_2:def 1;
then
A4: (
dom (T
| (E
/\ (G1
.loops() ))))
c= (
dom S) by
FUNCT_2:def 1;
now
let x be
object;
assume x
in ((
dom S)
/\ (
dom (T
| (E
/\ (G1
.loops() )))));
then
A5: x
in (
dom (T
| (E
/\ (G1
.loops() )))) by
A4,
XBOOLE_1: 28;
then x
in (G1
.loops() ) by
XBOOLE_0:def 4;
then
A6: x
in (
dom (S
/\ T)) by
Th67;
thus (S
. x)
= ((S
/\ T)
. x) by
A6,
GRFUNC_1: 11
.= (T
. x) by
A6,
GRFUNC_1: 11
.= ((T
| (E
/\ (G1
.loops() )))
. x) by
A5,
FUNCT_1: 47;
end;
then
A7: S
tolerates (T
| (E
/\ (G1
.loops() ))) by
PARTFUN1:def 4;
A8: (
the_Source_of G2)
= (S
+* (T
| E)) by
A1,
GLIB_007:def 1
.= (S
+* (T
| ((E
/\ (G1
.loops() ))
\/ (E
\ (G1
.loops() ))))) by
XBOOLE_1: 51
.= (S
+* ((T
| (E
/\ (G1
.loops() )))
+* (T
| (E
\ (G1
.loops() ))))) by
FUNCT_4: 78
.= ((S
+* (T
| (E
/\ (G1
.loops() ))))
+* (T
| (E
\ (G1
.loops() )))) by
FUNCT_4: 14
.= (((T
| (E
/\ (G1
.loops() )))
+* S)
+* (T
| (E
\ (G1
.loops() )))) by
A7,
FUNCT_4: 34
.= (S
+* (T
| (E
\ (G1
.loops() )))) by
A4,
FUNCT_4: 19;
(
dom (S
| (E
/\ (G1
.loops() ))))
c= (
dom S) by
RELAT_1: 60;
then (
dom (S
| (E
/\ (G1
.loops() ))))
c= (
the_Edges_of G1) by
FUNCT_2:def 1;
then
A9: (
dom (S
| (E
/\ (G1
.loops() ))))
c= (
dom T) by
FUNCT_2:def 1;
now
let x be
object;
assume x
in ((
dom T)
/\ (
dom (S
| (E
/\ (G1
.loops() )))));
then
A10: x
in (
dom (S
| (E
/\ (G1
.loops() )))) by
A9,
XBOOLE_1: 28;
then x
in (G1
.loops() ) by
XBOOLE_0:def 4;
then
A11: x
in (
dom (S
/\ T)) by
Th67;
thus (T
. x)
= ((S
/\ T)
. x) by
A11,
GRFUNC_1: 11
.= (S
. x) by
A11,
GRFUNC_1: 11
.= ((S
| (E
/\ (G1
.loops() )))
. x) by
A10,
FUNCT_1: 47;
end;
then
A12: T
tolerates (S
| (E
/\ (G1
.loops() ))) by
PARTFUN1:def 4;
(
the_Target_of G2)
= (T
+* (S
| E)) by
A1,
GLIB_007:def 1
.= (T
+* (S
| ((E
/\ (G1
.loops() ))
\/ (E
\ (G1
.loops() ))))) by
XBOOLE_1: 51
.= (T
+* ((S
| (E
/\ (G1
.loops() )))
+* (S
| (E
\ (G1
.loops() ))))) by
FUNCT_4: 78
.= ((T
+* (S
| (E
/\ (G1
.loops() ))))
+* (S
| (E
\ (G1
.loops() )))) by
FUNCT_4: 14
.= (((S
| (E
/\ (G1
.loops() )))
+* T)
+* (S
| (E
\ (G1
.loops() )))) by
A12,
FUNCT_4: 34
.= (T
+* (S
| (E
\ (G1
.loops() )))) by
A9,
FUNCT_4: 19;
hence thesis by
A2,
A3,
A8,
GLIB_007:def 1;
end;
suppose
A13: not E
c= (
the_Edges_of G1);
then
A14: G1
== G2 by
GLIB_007:def 1;
consider e be
object such that
A15: e
in E & not e
in (
the_Edges_of G1) by
A13,
TARSKI:def 3;
not e
in (G1
.loops() ) by
A15;
then e
in (E
\ (G1
.loops() )) by
A15,
XBOOLE_0:def 5;
then not (E
\ (G1
.loops() ))
c= (
the_Edges_of G1) by
A15;
hence thesis by
A14,
GLIB_007:def 1;
end;
end;
Lm2: for G1 be
_Graph, E be
set holds for G2 be
reverseEdgeDirections of G1, (E
\ (G1
.loops() )) holds G2 is
reverseEdgeDirections of G1, E
proof
let G1 be
_Graph, E be
set;
let G2 be
reverseEdgeDirections of G1, (E
\ (G1
.loops() ));
per cases ;
suppose
A1: (E
\ (G1
.loops() ))
c= (
the_Edges_of G1);
then
A2: (
the_Vertices_of G1)
= (
the_Vertices_of G2) & (
the_Edges_of G1)
= (
the_Edges_of G2) by
GLIB_007:def 1;
E
c= ((
the_Edges_of G1)
\/ (G1
.loops() )) by
A1,
XBOOLE_1: 44;
then
A3: E
c= (
the_Edges_of G1) by
XBOOLE_1: 12;
set S = (
the_Source_of G1), T = (
the_Target_of G1);
(
dom (T
| (E
/\ (G1
.loops() ))))
c= (
dom T) by
RELAT_1: 60;
then (
dom (T
| (E
/\ (G1
.loops() ))))
c= (
the_Edges_of G1) by
FUNCT_2:def 1;
then
A4: (
dom (T
| (E
/\ (G1
.loops() ))))
c= (
dom S) by
FUNCT_2:def 1;
now
let x be
object;
assume x
in ((
dom S)
/\ (
dom (T
| (E
/\ (G1
.loops() )))));
then
A5: x
in (
dom (T
| (E
/\ (G1
.loops() )))) by
A4,
XBOOLE_1: 28;
then x
in (G1
.loops() ) by
XBOOLE_0:def 4;
then
A6: x
in (
dom (S
/\ T)) by
Th67;
thus (S
. x)
= ((S
/\ T)
. x) by
A6,
GRFUNC_1: 11
.= (T
. x) by
A6,
GRFUNC_1: 11
.= ((T
| (E
/\ (G1
.loops() )))
. x) by
A5,
FUNCT_1: 47;
end;
then
A7: S
tolerates (T
| (E
/\ (G1
.loops() ))) by
PARTFUN1:def 4;
A8: (
the_Source_of G2)
= (S
+* (T
| (E
\ (G1
.loops() )))) by
A1,
GLIB_007:def 1
.= (((T
| (E
/\ (G1
.loops() )))
+* S)
+* (T
| (E
\ (G1
.loops() )))) by
A4,
FUNCT_4: 19
.= ((S
+* (T
| (E
/\ (G1
.loops() ))))
+* (T
| (E
\ (G1
.loops() )))) by
A7,
FUNCT_4: 34
.= (S
+* ((T
| (E
/\ (G1
.loops() )))
+* (T
| (E
\ (G1
.loops() ))))) by
FUNCT_4: 14
.= (S
+* (T
| ((E
/\ (G1
.loops() ))
\/ (E
\ (G1
.loops() ))))) by
FUNCT_4: 78
.= (S
+* (T
| E)) by
XBOOLE_1: 51;
(
dom (S
| (E
/\ (G1
.loops() ))))
c= (
dom S) by
RELAT_1: 60;
then (
dom (S
| (E
/\ (G1
.loops() ))))
c= (
the_Edges_of G1) by
FUNCT_2:def 1;
then
A9: (
dom (S
| (E
/\ (G1
.loops() ))))
c= (
dom T) by
FUNCT_2:def 1;
now
let x be
object;
assume x
in ((
dom T)
/\ (
dom (S
| (E
/\ (G1
.loops() )))));
then
A10: x
in (
dom (S
| (E
/\ (G1
.loops() )))) by
A9,
XBOOLE_1: 28;
then x
in (G1
.loops() ) by
XBOOLE_0:def 4;
then
A11: x
in (
dom (S
/\ T)) by
Th67;
thus (T
. x)
= ((S
/\ T)
. x) by
A11,
GRFUNC_1: 11
.= (S
. x) by
A11,
GRFUNC_1: 11
.= ((S
| (E
/\ (G1
.loops() )))
. x) by
A10,
FUNCT_1: 47;
end;
then
A12: T
tolerates (S
| (E
/\ (G1
.loops() ))) by
PARTFUN1:def 4;
(
the_Target_of G2)
= (T
+* (S
| (E
\ (G1
.loops() )))) by
A1,
GLIB_007:def 1
.= (((S
| (E
/\ (G1
.loops() )))
+* T)
+* (S
| (E
\ (G1
.loops() )))) by
A9,
FUNCT_4: 19
.= ((T
+* (S
| (E
/\ (G1
.loops() ))))
+* (S
| (E
\ (G1
.loops() )))) by
A12,
FUNCT_4: 34
.= (T
+* ((S
| (E
/\ (G1
.loops() )))
+* (S
| (E
\ (G1
.loops() ))))) by
FUNCT_4: 14
.= (T
+* (S
| ((E
/\ (G1
.loops() ))
\/ (E
\ (G1
.loops() ))))) by
FUNCT_4: 78
.= (T
+* (S
| E)) by
XBOOLE_1: 51;
hence thesis by
A3,
A2,
A8,
GLIB_007:def 1;
end;
suppose
A13: not (E
\ (G1
.loops() ))
c= (
the_Edges_of G1);
A14: not E
c= (
the_Edges_of G1) by
A13,
XBOOLE_1: 1;
G1
== G2 by
A13,
GLIB_007:def 1;
hence thesis by
A14,
GLIB_007:def 1;
end;
end;
theorem ::
GLIBPRE0:64
for G1,G2 be
_Graph, E be
set holds G2 is
reverseEdgeDirections of G1, E iff G2 is
reverseEdgeDirections of G1, (E
\ (G1
.loops() )) by
Lm1,
Lm2;
theorem ::
GLIBPRE0:65
Th69: for G1 be
_Graph, G2 be
removeLoops of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.inNeighbors() )
= ((v1
.inNeighbors() )
\
{v1}) & (v2
.outNeighbors() )
= ((v1
.outNeighbors() )
\
{v1}) & (v2
.allNeighbors() )
= ((v1
.allNeighbors() )
\
{v1})
proof
let G1 be
_Graph, G2 be
removeLoops of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
now
let x be
object;
hereby
assume
A2: x
in (v2
.inNeighbors() );
then
A3: x
in (v1
.inNeighbors() ) by
A1,
GLIB_000: 82,
TARSKI:def 3;
consider e be
object such that
A4: e
DJoins (x,v2,G2) by
A2,
GLIB_000: 69;
x
<> v2 by
A4,
GLIB_009: 17;
then not x
in
{v1} by
A1,
TARSKI:def 1;
hence x
in ((v1
.inNeighbors() )
\
{v1}) by
A3,
XBOOLE_0:def 5;
end;
assume x
in ((v1
.inNeighbors() )
\
{v1});
then
A5: x
in (v1
.inNeighbors() ) & not x
in
{v1} by
XBOOLE_0:def 5;
then
consider e be
object such that
A6: e
DJoins (x,v1,G1) by
GLIB_000: 69;
A7: e
Joins (x,v1,G1) by
A6,
GLIB_000: 16;
x
<> v1 by
A5,
TARSKI:def 1;
then
A8: not e
in (G1
.loops() ) by
A7,
GLIB_009: 46;
e
in (
the_Edges_of G1) by
A6,
GLIB_000:def 14;
then e
in ((
the_Edges_of G1)
\ (G1
.loops() )) by
A8,
XBOOLE_0:def 5;
then
A9: e
in (
the_Edges_of G2) by
GLIB_000: 53;
A10: x is
set & e is
set by
TARSKI: 1;
then e
DJoins (x,v1,G2) by
A6,
A9,
GLIB_000: 73;
hence x
in (v2
.inNeighbors() ) by
A1,
A10,
GLIB_000: 69;
end;
hence
A11: (v2
.inNeighbors() )
= ((v1
.inNeighbors() )
\
{v1}) by
TARSKI: 2;
now
let x be
object;
hereby
assume
A12: x
in (v2
.outNeighbors() );
then
A13: x
in (v1
.outNeighbors() ) by
A1,
GLIB_000: 82,
TARSKI:def 3;
consider e be
object such that
A14: e
DJoins (v2,x,G2) by
A12,
GLIB_000: 70;
x
<> v2 by
A14,
GLIB_009: 17;
then not x
in
{v1} by
A1,
TARSKI:def 1;
hence x
in ((v1
.outNeighbors() )
\
{v1}) by
A13,
XBOOLE_0:def 5;
end;
assume x
in ((v1
.outNeighbors() )
\
{v1});
then
A15: x
in (v1
.outNeighbors() ) & not x
in
{v1} by
XBOOLE_0:def 5;
then
consider e be
object such that
A16: e
DJoins (v1,x,G1) by
GLIB_000: 70;
A17: e
Joins (v1,x,G1) by
A16,
GLIB_000: 16;
x
<> v1 by
A15,
TARSKI:def 1;
then
A18: not e
in (G1
.loops() ) by
A17,
GLIB_009: 46;
e
in (
the_Edges_of G1) by
A16,
GLIB_000:def 14;
then e
in ((
the_Edges_of G1)
\ (G1
.loops() )) by
A18,
XBOOLE_0:def 5;
then
A19: e
in (
the_Edges_of G2) by
GLIB_000: 53;
A20: x is
set & e is
set by
TARSKI: 1;
then e
DJoins (v1,x,G2) by
A16,
A19,
GLIB_000: 73;
hence x
in (v2
.outNeighbors() ) by
A1,
A20,
GLIB_000: 70;
end;
hence
A21: (v2
.outNeighbors() )
= ((v1
.outNeighbors() )
\
{v1}) by
TARSKI: 2;
thus (v2
.allNeighbors() )
= ((v1
.allNeighbors() )
\
{v1}) by
A11,
A21,
XBOOLE_1: 42;
end;
theorem ::
GLIBPRE0:66
Th70: for G1 be
_Graph, G2 be
removeParallelEdges of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.allNeighbors() )
= (v1
.allNeighbors() )
proof
let G1 be
_Graph, G2 be
removeParallelEdges of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
consider E be
RepEdgeSelection of G1 such that
A2: G2 is
inducedSubgraph of G1, (
the_Vertices_of G1), E by
GLIB_009:def 7;
(
the_Edges_of G1)
= (G1
.edgesBetween (
the_Vertices_of G1)) by
GLIB_000: 34;
then E
c= (G1
.edgesBetween (
the_Vertices_of G1)) & (
the_Vertices_of G1)
c= (
the_Vertices_of G1);
then
A3: (
the_Edges_of G2)
= E by
A2,
GLIB_000:def 37;
A4: (v2
.allNeighbors() )
c= (v1
.allNeighbors() ) by
A1,
GLIB_000: 82;
now
let x be
object;
assume x
in (v1
.allNeighbors() );
then
consider e0 be
object such that
A5: e0
Joins (v1,x,G1) by
GLIB_000: 71;
consider e be
object such that
A6: e
Joins (v1,x,G1) & e
in E and for e9 be
object st e9
Joins (v1,x,G1) & e9
in E holds e9
= e by
A5,
GLIB_009:def 5;
A7: x is
set & e is
set by
TARSKI: 1;
then e
Joins (v1,x,G2) by
A3,
A6,
GLIB_000: 73;
hence x
in (v2
.allNeighbors() ) by
A1,
A7,
GLIB_000: 71;
end;
then (v1
.allNeighbors() )
c= (v2
.allNeighbors() ) by
TARSKI:def 3;
hence (v2
.allNeighbors() )
= (v1
.allNeighbors() ) by
A4,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:67
Th71: for G1 be
_Graph, G2 be
removeDParallelEdges of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.inNeighbors() )
= (v1
.inNeighbors() ) & (v2
.outNeighbors() )
= (v1
.outNeighbors() ) & (v2
.allNeighbors() )
= (v1
.allNeighbors() )
proof
let G1 be
_Graph, G2 be
removeDParallelEdges of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
consider E be
RepDEdgeSelection of G1 such that
A2: G2 is
inducedSubgraph of G1, (
the_Vertices_of G1), E by
GLIB_009:def 8;
(
the_Edges_of G1)
= (G1
.edgesBetween (
the_Vertices_of G1)) by
GLIB_000: 34;
then E
c= (G1
.edgesBetween (
the_Vertices_of G1)) & (
the_Vertices_of G1)
c= (
the_Vertices_of G1);
then
A3: (
the_Edges_of G2)
= E by
A2,
GLIB_000:def 37;
A4: (v2
.inNeighbors() )
c= (v1
.inNeighbors() ) by
A1,
GLIB_000: 82;
now
let x be
object;
assume x
in (v1
.inNeighbors() );
then
consider e0 be
object such that
A5: e0
DJoins (x,v1,G1) by
GLIB_000: 69;
consider e be
object such that
A6: e
DJoins (x,v1,G1) & e
in E and for e9 be
object st e9
DJoins (x,v1,G1) & e9
in E holds e9
= e by
A5,
GLIB_009:def 6;
A7: x is
set & e is
set by
TARSKI: 1;
then e
DJoins (x,v1,G2) by
A3,
A6,
GLIB_000: 73;
hence x
in (v2
.inNeighbors() ) by
A1,
A7,
GLIB_000: 69;
end;
then (v1
.inNeighbors() )
c= (v2
.inNeighbors() ) by
TARSKI:def 3;
hence
A8: (v2
.inNeighbors() )
= (v1
.inNeighbors() ) by
A4,
XBOOLE_0:def 10;
A9: (v2
.outNeighbors() )
c= (v1
.outNeighbors() ) by
A1,
GLIB_000: 82;
now
let x be
object;
assume x
in (v1
.outNeighbors() );
then
consider e0 be
object such that
A10: e0
DJoins (v1,x,G1) by
GLIB_000: 70;
consider e be
object such that
A11: e
DJoins (v1,x,G1) & e
in E and for e9 be
object st e9
DJoins (v1,x,G1) & e9
in E holds e9
= e by
A10,
GLIB_009:def 6;
A12: x is
set & e is
set by
TARSKI: 1;
then e
DJoins (v1,x,G2) by
A3,
A11,
GLIB_000: 73;
hence x
in (v2
.outNeighbors() ) by
A1,
A12,
GLIB_000: 70;
end;
then (v1
.outNeighbors() )
c= (v2
.outNeighbors() ) by
TARSKI:def 3;
hence
A13: (v2
.outNeighbors() )
= (v1
.outNeighbors() ) by
A9,
XBOOLE_0:def 10;
thus (v2
.allNeighbors() )
= (v1
.allNeighbors() ) by
A8,
A13;
end;
theorem ::
GLIBPRE0:68
for G1 be
_Graph, G2 be
SimpleGraph of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.allNeighbors() )
= ((v1
.allNeighbors() )
\
{v1})
proof
let G1 be
_Graph, G2 be
SimpleGraph of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
consider G9 be
removeParallelEdges of G1 such that
A2: G2 is
removeLoops of G9 by
GLIB_009: 119;
reconsider v3 = v2 as
Vertex of G9 by
A2,
GLIB_000: 53;
thus (v2
.allNeighbors() )
= ((v3
.allNeighbors() )
\
{v3}) by
A2,
Th69
.= ((v1
.allNeighbors() )
\
{v1}) by
A1,
Th70;
end;
theorem ::
GLIBPRE0:69
for G1 be
_Graph, G2 be
DSimpleGraph of G1 holds for v1 be
Vertex of G1, v2 be
Vertex of G2 st v1
= v2 holds (v2
.inNeighbors() )
= ((v1
.inNeighbors() )
\
{v1}) & (v2
.outNeighbors() )
= ((v1
.outNeighbors() )
\
{v1}) & (v2
.allNeighbors() )
= ((v1
.allNeighbors() )
\
{v1})
proof
let G1 be
_Graph, G2 be
DSimpleGraph of G1;
let v1 be
Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1
= v2;
consider G9 be
removeDParallelEdges of G1 such that
A2: G2 is
removeLoops of G9 by
GLIB_009: 120;
reconsider v3 = v2 as
Vertex of G9 by
A2,
GLIB_000: 53;
thus (v2
.inNeighbors() )
= ((v3
.inNeighbors() )
\
{v3}) by
A2,
Th69
.= ((v1
.inNeighbors() )
\
{v1}) by
A1,
Th71;
thus (v2
.outNeighbors() )
= ((v3
.outNeighbors() )
\
{v3}) by
A2,
Th69
.= ((v1
.outNeighbors() )
\
{v1}) by
A1,
Th71;
thus (v2
.allNeighbors() )
= ((v3
.allNeighbors() )
\
{v3}) by
A2,
Th69
.= ((v1
.allNeighbors() )
\
{v1}) by
A1,
Th71;
end;
registration
let G be non
loopless
_Graph;
cluster -> non
loopless for
removeParallelEdges of G;
coherence
proof
let H be
removeParallelEdges of G;
consider E be
RepEdgeSelection of G such that
A1: H is
inducedSubgraph of G, (
the_Vertices_of G), E by
GLIB_009:def 7;
consider v be
object such that
A2: ex e be
object st e
Joins (v,v,G) by
GLIB_000: 18;
consider e0 be
object such that
A3: e0
Joins (v,v,G) by
A2;
consider e be
object such that
A4: e
Joins (v,v,G) & e
in E and for e9 be
object st e9
Joins (v,v,G) & e9
in E holds e9
= e by
A3,
GLIB_009:def 5;
A5: (
the_Edges_of G)
= (G
.edgesBetween (
the_Vertices_of G)) by
GLIB_000: 34;
(
the_Vertices_of G)
c= (
the_Vertices_of G);
then
A6: e
in (
the_Edges_of H) by
A1,
A4,
A5,
GLIB_000:def 37;
v is
set & e is
set by
TARSKI: 1;
then e
Joins (v,v,H) by
A4,
A6,
GLIB_000: 73;
hence thesis by
GLIB_000: 18;
end;
cluster -> non
loopless for
removeDParallelEdges of G;
coherence
proof
let H be
removeDParallelEdges of G;
consider E be
RepDEdgeSelection of G such that
A7: H is
inducedSubgraph of G, (
the_Vertices_of G), E by
GLIB_009:def 8;
consider v be
object such that
A8: ex e be
object st e
DJoins (v,v,G) by
GLIB_009: 17;
consider e0 be
object such that
A9: e0
DJoins (v,v,G) by
A8;
consider e be
object such that
A10: e
DJoins (v,v,G) & e
in E and for e9 be
object st e9
DJoins (v,v,G) & e9
in E holds e9
= e by
A9,
GLIB_009:def 6;
A11: (
the_Edges_of G)
= (G
.edgesBetween (
the_Vertices_of G)) by
GLIB_000: 34;
(
the_Vertices_of G)
c= (
the_Vertices_of G);
then
A12: e
in (
the_Edges_of H) by
A7,
A10,
A11,
GLIB_000:def 37;
v is
set & e is
set by
TARSKI: 1;
then e
DJoins (v,v,H) by
A10,
A12,
GLIB_000: 73;
hence thesis by
GLIB_009: 17;
end;
end
registration
let G be non
edgeless
_Graph;
cluster -> non
edgeless for
removeParallelEdges of G;
coherence
proof
let H be
removeParallelEdges of G;
consider E be
RepEdgeSelection of G such that
A1: H is
inducedSubgraph of G, (
the_Vertices_of G), E by
GLIB_009:def 7;
A4: (
the_Edges_of G)
= (G
.edgesBetween (
the_Vertices_of G)) by
GLIB_000: 34;
(
the_Vertices_of G)
c= (
the_Vertices_of G);
then (
the_Edges_of H)
= E by
A1,
A4,
GLIB_000:def 37;
hence thesis;
end;
cluster -> non
edgeless for
removeDParallelEdges of G;
coherence
proof
let H be
removeDParallelEdges of G;
consider E be
RepDEdgeSelection of G such that
A5: H is
inducedSubgraph of G, (
the_Vertices_of G), E by
GLIB_009:def 8;
A8: (
the_Edges_of G)
= (G
.edgesBetween (
the_Vertices_of G)) by
GLIB_000: 34;
(
the_Vertices_of G)
c= (
the_Vertices_of G);
then (
the_Edges_of H)
= E by
A5,
A8,
GLIB_000:def 37;
hence thesis;
end;
end
theorem ::
GLIBPRE0:70
for G be
_Graph, E be
RepEdgeSelection of G holds (
card E)
= (
card (
Class (
EdgeAdjEqRel G)))
proof
let G be
_Graph, E be
RepEdgeSelection of G;
deffunc
F(
object) = (
Class ((
EdgeAdjEqRel G),$1));
consider f be
Function such that
A1: (
dom f)
= E & for x be
object st x
in E holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
now
let y be
object;
hereby
assume y
in (
rng f);
then
consider x be
object such that
A2: x
in (
dom f) & (f
. x)
= y by
FUNCT_1:def 3;
y
= (
Class ((
EdgeAdjEqRel G),x)) by
A1,
A2;
hence y
in (
Class (
EdgeAdjEqRel G)) by
A1,
A2,
EQREL_1:def 3;
end;
assume y
in (
Class (
EdgeAdjEqRel G));
then
consider x be
object such that
A3: x
in (
the_Edges_of G) & y
= (
Class ((
EdgeAdjEqRel G),x)) by
EQREL_1:def 3;
set v = ((
the_Source_of G)
. x), w = ((
the_Target_of G)
. x);
A4: x
Joins (v,w,G) by
A3,
GLIB_000:def 13;
then
consider e be
object such that
A5: e
Joins (v,w,G) & e
in E and for e9 be
object st e9
Joins (v,w,G) & e9
in E holds e9
= e by
GLIB_009:def 5;
[x, e]
in (
EdgeAdjEqRel G) by
A4,
A5,
GLIB_009:def 3;
then e
in (
Class ((
EdgeAdjEqRel G),x)) by
EQREL_1: 18;
then y
= (
Class ((
EdgeAdjEqRel G),e)) by
A3,
EQREL_1: 23
.= (f
. e) by
A1,
A5;
hence y
in (
rng f) by
A1,
A5,
FUNCT_1: 3;
end;
then
A6: (
rng f)
= (
Class (
EdgeAdjEqRel G)) by
TARSKI: 2;
now
let x1,x2 be
object;
assume
A7: x1
in (
dom f) & x2
in (
dom f) & (f
. x1)
= (f
. x2);
then (f
. x1)
= (
Class ((
EdgeAdjEqRel G),x1)) & (f
. x2)
= (
Class ((
EdgeAdjEqRel G),x2)) by
A1;
then x2
in (
Class ((
EdgeAdjEqRel G),x1)) by
A1,
A7,
EQREL_1: 23;
then
[x1, x2]
in (
EdgeAdjEqRel G) by
EQREL_1: 18;
then
consider v,w be
object such that
A8: x1
Joins (v,w,G) & x2
Joins (v,w,G) by
GLIB_009:def 3;
consider e be
object such that e
Joins (v,w,G) & e
in E and
A9: for e9 be
object st e9
Joins (v,w,G) & e9
in E holds e9
= e by
A8,
GLIB_009:def 5;
x1
= e & x2
= e by
A1,
A7,
A8,
A9;
hence x1
= x2;
end;
hence thesis by
A1,
A6,
FUNCT_1:def 4,
CARD_1: 70;
end;
theorem ::
GLIBPRE0:71
for G be
_Graph, E be
RepDEdgeSelection of G holds (
card E)
= (
card (
Class (
DEdgeAdjEqRel G)))
proof
let G be
_Graph, E be
RepDEdgeSelection of G;
deffunc
F(
object) = (
Class ((
DEdgeAdjEqRel G),$1));
consider f be
Function such that
A1: (
dom f)
= E & for x be
object st x
in E holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
now
let y be
object;
hereby
assume y
in (
rng f);
then
consider x be
object such that
A2: x
in (
dom f) & (f
. x)
= y by
FUNCT_1:def 3;
y
= (
Class ((
DEdgeAdjEqRel G),x)) by
A1,
A2;
hence y
in (
Class (
DEdgeAdjEqRel G)) by
A1,
A2,
EQREL_1:def 3;
end;
assume y
in (
Class (
DEdgeAdjEqRel G));
then
consider x be
object such that
A3: x
in (
the_Edges_of G) & y
= (
Class ((
DEdgeAdjEqRel G),x)) by
EQREL_1:def 3;
set v = ((
the_Source_of G)
. x), w = ((
the_Target_of G)
. x);
A4: x
DJoins (v,w,G) by
A3,
GLIB_000:def 14;
then
consider e be
object such that
A5: e
DJoins (v,w,G) & e
in E and for e9 be
object st e9
DJoins (v,w,G) & e9
in E holds e9
= e by
GLIB_009:def 6;
[x, e]
in (
DEdgeAdjEqRel G) by
A4,
A5,
GLIB_009:def 4;
then e
in (
Class ((
DEdgeAdjEqRel G),x)) by
EQREL_1: 18;
then y
= (
Class ((
DEdgeAdjEqRel G),e)) by
A3,
EQREL_1: 23
.= (f
. e) by
A1,
A5;
hence y
in (
rng f) by
A1,
A5,
FUNCT_1: 3;
end;
then
A6: (
rng f)
= (
Class (
DEdgeAdjEqRel G)) by
TARSKI: 2;
now
let x1,x2 be
object;
assume
A7: x1
in (
dom f) & x2
in (
dom f) & (f
. x1)
= (f
. x2);
then (f
. x1)
= (
Class ((
DEdgeAdjEqRel G),x1)) & (f
. x2)
= (
Class ((
DEdgeAdjEqRel G),x2)) by
A1;
then x2
in (
Class ((
DEdgeAdjEqRel G),x1)) by
A1,
A7,
EQREL_1: 23;
then
[x1, x2]
in (
DEdgeAdjEqRel G) by
EQREL_1: 18;
then
consider v,w be
object such that
A8: x1
DJoins (v,w,G) & x2
DJoins (v,w,G) by
GLIB_009:def 4;
consider e be
object such that e
DJoins (v,w,G) & e
in E and
A9: for e9 be
object st e9
DJoins (v,w,G) & e9
in E holds e9
= e by
A8,
GLIB_009:def 6;
x1
= e & x2
= e by
A1,
A7,
A8,
A9;
hence x1
= x2;
end;
hence thesis by
A1,
A6,
CARD_1: 70,
FUNCT_1:def 4;
end;
Lm3: for G be
_Graph, X be
set, E be
Subset of (
the_Edges_of G) holds for H be
reverseEdgeDirections of G, X holds E is
RepEdgeSelection of G implies E is
RepEdgeSelection of H
proof
let G be
_Graph, X be
set, E be
Subset of (
the_Edges_of G);
let H be
reverseEdgeDirections of G, X;
assume
A1: E is
RepEdgeSelection of G;
A2: E is
Subset of (
the_Edges_of H) by
GLIB_007: 4;
now
let v,w,e0 be
object;
assume e0
Joins (v,w,H);
then
consider e be
object such that
A3: e
Joins (v,w,G) & e
in E and
A4: for e9 be
object st e9
Joins (v,w,G) & e9
in E holds e9
= e by
A1,
GLIB_007: 9,
GLIB_009:def 5;
take e;
thus e
Joins (v,w,H) & e
in E by
A3,
GLIB_007: 9;
let e9 be
object;
assume e9
Joins (v,w,H) & e9
in E;
hence e9
= e by
A4,
GLIB_007: 9;
end;
hence thesis by
A2,
GLIB_009:def 5;
end;
theorem ::
GLIBPRE0:72
for G be
_Graph, X be
set, E be
Subset of (
the_Edges_of G) holds for H be
reverseEdgeDirections of G, X holds E is
RepEdgeSelection of G iff E is
RepEdgeSelection of H
proof
let G be
_Graph, X be
set, E be
Subset of (
the_Edges_of G);
let H be
reverseEdgeDirections of G, X;
thus E is
RepEdgeSelection of G implies E is
RepEdgeSelection of H by
Lm3;
A1: G is
reverseEdgeDirections of H, X by
GLIB_007: 3;
assume E is
RepEdgeSelection of H;
hence thesis by
A1,
Lm3;
end;
theorem ::
GLIBPRE0:73
for G be
_Graph, V be non
empty
Subset of (
the_Vertices_of G) holds for H be
inducedSubgraph of G, V, E be
RepEdgeSelection of G holds (E
/\ (G
.edgesBetween V)) is
RepEdgeSelection of H
proof
let G be
_Graph, V be non
empty
Subset of (
the_Vertices_of G);
let H be
inducedSubgraph of G, V, E be
RepEdgeSelection of G;
(G
.edgesBetween V)
= (
the_Edges_of H) by
GLIB_000:def 37;
then
reconsider E9 = (E
/\ (G
.edgesBetween V)) as
Subset of (
the_Edges_of H) by
XBOOLE_1: 17;
now
let v,w,e0 be
object;
A1: v is
set & w is
set by
TARSKI: 1;
assume
A2: e0
Joins (v,w,H);
then e0
Joins (v,w,G) by
A1,
GLIB_000: 72;
then
consider e be
object such that
A3: e
Joins (v,w,G) & e
in E and
A4: for e9 be
object st e9
Joins (v,w,G) & e9
in E holds e9
= e by
GLIB_009:def 5;
take e;
v
in (
the_Vertices_of H) & w
in (
the_Vertices_of H) by
A2,
GLIB_000: 13;
then v
in V & w
in V by
GLIB_000:def 37;
then
A5: e
in (G
.edgesBetween V) by
A3,
GLIB_000: 32;
then e
in (
the_Edges_of H) by
GLIB_000:def 37;
hence e
Joins (v,w,H) by
A1,
A3,
GLIB_000: 73;
thus e
in E9 by
A3,
A5,
XBOOLE_0:def 4;
let e9 be
object;
assume e9
Joins (v,w,H) & e9
in E9;
then e9
Joins (v,w,G) & e9
in E by
A1,
GLIB_000: 72,
XBOOLE_0:def 4;
hence e9
= e by
A4;
end;
hence thesis by
GLIB_009:def 5;
end;
theorem ::
GLIBPRE0:74
for G be
_Graph, V be non
empty
Subset of (
the_Vertices_of G) holds for H be
inducedSubgraph of G, V, E be
RepDEdgeSelection of G holds (E
/\ (G
.edgesBetween V)) is
RepDEdgeSelection of H
proof
let G be
_Graph, V be non
empty
Subset of (
the_Vertices_of G);
let H be
inducedSubgraph of G, V, E be
RepDEdgeSelection of G;
(G
.edgesBetween V)
= (
the_Edges_of H) by
GLIB_000:def 37;
then
reconsider E9 = (E
/\ (G
.edgesBetween V)) as
Subset of (
the_Edges_of H) by
XBOOLE_1: 17;
now
let v,w,e0 be
object;
A1: v is
set & w is
set by
TARSKI: 1;
assume
A2: e0
DJoins (v,w,H);
then e0
DJoins (v,w,G) by
A1,
GLIB_000: 72;
then
consider e be
object such that
A3: e
DJoins (v,w,G) & e
in E and
A4: for e9 be
object st e9
DJoins (v,w,G) & e9
in E holds e9
= e by
GLIB_009:def 6;
take e;
e0
Joins (v,w,H) by
A2,
GLIB_000: 16;
then v
in (
the_Vertices_of H) & w
in (
the_Vertices_of H) by
GLIB_000: 13;
then
A5: v
in V & w
in V by
GLIB_000:def 37;
e
Joins (v,w,G) by
A3,
GLIB_000: 16;
then
A6: e
in (G
.edgesBetween V) by
A5,
GLIB_000: 32;
then e
in (
the_Edges_of H) by
GLIB_000:def 37;
hence e
DJoins (v,w,H) by
A1,
A3,
GLIB_000: 73;
thus e
in E9 by
A3,
A6,
XBOOLE_0:def 4;
let e9 be
object;
assume e9
DJoins (v,w,H) & e9
in E9;
then e9
DJoins (v,w,G) & e9
in E by
A1,
GLIB_000: 72,
XBOOLE_0:def 4;
hence e9
= e by
A4;
end;
hence thesis by
GLIB_009:def 6;
end;
theorem ::
GLIBPRE0:75
for G be
_Graph, V be
set, H be
addVertices of G, V holds for E be
Subset of (
the_Edges_of G) holds E is
RepEdgeSelection of G iff E is
RepEdgeSelection of H
proof
let G be
_Graph, V be
set, H be
addVertices of G, V;
let E be
Subset of (
the_Edges_of G);
A1: (
the_Edges_of G)
= (
the_Edges_of H) by
GLIB_006:def 10;
hereby
assume
A2: E is
RepEdgeSelection of G;
now
let v,w,e0 be
object;
A3: v is
set & w is
set by
TARSKI: 1;
assume e0
Joins (v,w,H);
then
consider e be
object such that
A4: e
Joins (v,w,G) & e
in E and
A5: for e9 be
object st e9
Joins (v,w,G) & e9
in E holds e9
= e by
A2,
A3,
GLIB_009: 41,
GLIB_009:def 5;
take e;
thus e
Joins (v,w,H) & e
in E by
A3,
A4,
GLIB_009: 41;
let e9 be
object;
assume e9
Joins (v,w,H) & e9
in E;
hence e9
= e by
A3,
A5,
GLIB_009: 41;
end;
hence E is
RepEdgeSelection of H by
A1,
GLIB_009:def 5;
end;
assume
A6: E is
RepEdgeSelection of H;
now
let v,w,e0 be
object;
A7: v is
set & w is
set by
TARSKI: 1;
assume e0
Joins (v,w,G);
then
consider e be
object such that
A8: e
Joins (v,w,H) & e
in E and
A9: for e9 be
object st e9
Joins (v,w,H) & e9
in E holds e9
= e by
A6,
A7,
GLIB_009: 41,
GLIB_009:def 5;
take e;
thus e
Joins (v,w,G) & e
in E by
A7,
A8,
GLIB_009: 41;
let e9 be
object;
assume e9
Joins (v,w,G) & e9
in E;
hence e9
= e by
A7,
A9,
GLIB_009: 41;
end;
hence E is
RepEdgeSelection of G by
GLIB_009:def 5;
end;
theorem ::
GLIBPRE0:76
for G be
_Graph, V be
set, H be
addVertices of G, V holds for E be
Subset of (
the_Edges_of G) holds E is
RepDEdgeSelection of G iff E is
RepDEdgeSelection of H
proof
let G be
_Graph, V be
set, H be
addVertices of G, V;
let E be
Subset of (
the_Edges_of G);
A1: (
the_Edges_of G)
= (
the_Edges_of H) by
GLIB_006:def 10;
hereby
assume
A2: E is
RepDEdgeSelection of G;
now
let v,w,e0 be
object;
A3: v is
set & w is
set by
TARSKI: 1;
assume e0
DJoins (v,w,H);
then
consider e be
object such that
A4: e
DJoins (v,w,G) & e
in E and
A5: for e9 be
object st e9
DJoins (v,w,G) & e9
in E holds e9
= e by
A2,
A3,
GLIB_009: 41,
GLIB_009:def 6;
take e;
thus e
DJoins (v,w,H) & e
in E by
A3,
A4,
GLIB_009: 41;
let e9 be
object;
assume e9
DJoins (v,w,H) & e9
in E;
hence e9
= e by
A3,
A5,
GLIB_009: 41;
end;
hence E is
RepDEdgeSelection of H by
A1,
GLIB_009:def 6;
end;
assume
A6: E is
RepDEdgeSelection of H;
now
let v,w,e0 be
object;
A7: v is
set & w is
set by
TARSKI: 1;
assume e0
DJoins (v,w,G);
then
consider e be
object such that
A8: e
DJoins (v,w,H) & e
in E and
A9: for e9 be
object st e9
DJoins (v,w,H) & e9
in E holds e9
= e by
A6,
A7,
GLIB_009: 41,
GLIB_009:def 6;
take e;
thus e
DJoins (v,w,G) & e
in E by
A7,
A8,
GLIB_009: 41;
let e9 be
object;
assume e9
DJoins (v,w,G) & e9
in E;
hence e9
= e by
A7,
A9,
GLIB_009: 41;
end;
hence E is
RepDEdgeSelection of G by
GLIB_009:def 6;
end;
registration
cluster non
non-multi
non-Dmulti for
_Graph;
existence
proof
set G0 = the
_trivial
edgeless
_Graph, v = the
Vertex of G0;
set w = (
the_Vertices_of G0), e = (
the_Edges_of G0);
set G1 = the
addAdjVertex of G0, v, e, w;
A1: not e
in (
the_Edges_of G0) & not w
in (
the_Vertices_of G0);
reconsider v1 = v, w1 = w as
Vertex of G1 by
A1,
GLIB_006: 68,
GLIB_006: 129;
set f = (
the_Edges_of G1), G2 = the
addEdge of G1, w1, f, v1;
take G2;
A3: e
DJoins (v,w,G2) by
A1,
GLIB_006: 70,
GLIB_006: 131;
A4: not f
in (
the_Edges_of G1);
then
A5: f
DJoins (w1,v1,G2) by
GLIB_006: 105;
ex e1,e2,v1,v2 be
object st e1
Joins (v1,v2,G2) & e2
Joins (v1,v2,G2) & e1
<> e2
proof
take e, f, v, w;
thus e
Joins (v,w,G2) by
A3,
GLIB_000: 16;
thus f
Joins (v,w,G2) by
A5,
GLIB_000: 16;
thus e
<> f;
end;
hence G2 is non
non-multi by
GLIB_000:def 20;
for e1,e2,v1,v2 be
object st e1
DJoins (v1,v2,G2) & e2
DJoins (v1,v2,G2) holds e1
= e2
proof
let e1,e2,v1,v2 be
object;
assume
A6: e1
DJoins (v1,v2,G2) & e2
DJoins (v1,v2,G2);
then
A7: e1
in (
the_Edges_of G2) & e2
in (
the_Edges_of G2) by
GLIB_000:def 14;
(
the_Edges_of G2)
= ((
the_Edges_of G1)
\/
{f}) by
A4,
GLIB_006:def 11
.= (((
the_Edges_of G0)
\/
{e})
\/
{f}) by
A1,
GLIB_006:def 12
.=
{e, f} by
ENUMSET1: 1;
per cases by
A7,
TARSKI:def 2;
suppose e1
= e & e2
= e;
hence thesis;
end;
suppose e1
= e & e2
= f;
then v1
= v & v2
= w & v1
= w & v2
= v by
A3,
A5,
A6,
GLIB_009: 6;
then v
= w & v
in w;
hence thesis;
end;
suppose e1
= f & e2
= e;
then v1
= v & v2
= w & v1
= w & v2
= v by
A3,
A5,
A6,
GLIB_009: 6;
then v
= w & v
in w;
hence thesis;
end;
suppose e1
= f & e2
= f;
hence thesis;
end;
end;
hence thesis by
GLIB_000:def 21;
end;
end
definition
let GF be
Graph-yielding
Function;
::
GLIBPRE0:def1
attr GF is
plain means
:
Def1: for x be
object st x
in (
dom GF) holds ex G be
_Graph st (GF
. x)
= G & G is
plain;
end
registration
let G be
plain
_Graph;
cluster
<*G*> ->
plain;
coherence
proof
let x be
object;
assume
A1: x
in (
dom
<*G*>);
then
reconsider n = x as
Nat;
1
<= n
<= (
len
<*G*>) by
A1,
FINSEQ_3: 25;
then 1
<= n
<= 1 by
FINSEQ_1: 40;
then n
= 1 by
XXREAL_0: 1;
hence thesis by
FINSEQ_1: 40;
end;
cluster (
NAT
--> G) ->
plain;
coherence by
FUNCOP_1: 7;
end
definition
let GF be non
empty
Graph-yielding
Function;
:: original:
plain
redefine
::
GLIBPRE0:def2
attr GF is
plain means
:
Def2: for x be
Element of (
dom GF) holds (GF
. x) is
plain;
compatibility
proof
hereby
assume
A1: GF is
plain;
let x be
Element of (
dom GF);
consider G be
_Graph such that
A2: (GF
. x)
= G & G is
plain by
A1;
thus (GF
. x) is
plain by
A2;
end;
assume
A3: for x be
Element of (
dom GF) holds (GF
. x) is
plain;
let x be
object;
assume x
in (
dom GF);
then
reconsider y = x as
Element of (
dom GF);
take (GF
. y);
thus thesis by
A3;
end;
end
Lm4: for F be
ManySortedSet of
NAT , n be
object holds n is
Nat iff n
in (
dom F)
proof
let F be
ManySortedSet of
NAT , n be
object;
hereby
assume n is
Nat;
then n
in
NAT by
ORDINAL1:def 12;
hence n
in (
dom F) by
PARTFUN1:def 2;
end;
assume n
in (
dom F);
hence n is
Nat;
end;
definition
let GSq be
GraphSeq;
:: original:
plain
redefine
::
GLIBPRE0:def3
attr GSq is
plain means
:
Def3: for n be
Nat holds (GSq
. n) is
plain;
compatibility
proof
hereby
assume
A1: GSq is
plain;
let x be
Nat;
x
in (
dom GSq) by
Lm4;
hence (GSq
. x) is
plain by
A1;
end;
assume
A2: for x be
Nat holds (GSq
. x) is
plain;
let x be
Element of (
dom GSq);
thus thesis by
A2;
end;
end
registration
cluster
empty ->
plain for
Graph-yielding
Function;
coherence ;
end
registration
cluster
plain for
GraphSeq;
existence
proof
take (
NAT
--> the
plain
_Graph);
thus thesis;
end;
cluster non
empty
plain for
Graph-yielding
FinSequence;
existence
proof
take
<* the
plain
_Graph*>;
thus thesis;
end;
end
registration
let GF be
plain non
empty
Graph-yielding
Function, x be
Element of (
dom GF);
cluster (GF
. x) ->
plain;
coherence by
Def2;
end
registration
let GSq be
plain
GraphSeq, x be
Nat;
cluster (GSq
. x) ->
plain;
coherence by
Def3;
end
registration
let p be
plain
Graph-yielding
FinSequence, n be
Nat;
cluster (p
| n) ->
plain;
coherence
proof
A1: (p
| n)
= (p
| (
Seg n)) by
FINSEQ_1:def 15;
now
let x be
object;
assume
A2: x
in (
dom (p
| n));
then x
in (
dom p) by
A1,
RELAT_1: 60,
TARSKI:def 3;
then
consider G be
_Graph such that
A3: (p
. x)
= G & G is
plain by
Def1;
take G;
thus ((p
| n)
. x)
= G & G is
plain by
A1,
A3,
A2,
FUNCT_1: 47;
end;
hence thesis;
end;
cluster (p
/^ n) ->
plain;
coherence
proof
per cases ;
suppose
A4: n
<= (
len p);
now
let x be
object;
assume
A5: x
in (
dom (p
/^ n));
then
reconsider i = x as
Nat;
(n
+ i)
in (
dom p) by
A5,
FINSEQ_5: 26;
then
consider G be
_Graph such that
A6: (p
. (n
+ i))
= G & G is
plain by
Def1;
take G;
thus ((p
/^ n)
. x)
= G & G is
plain by
A4,
A5,
A6,
RFINSEQ:def 1;
end;
hence thesis;
end;
suppose not (n
<= (
len p));
hence thesis by
RFINSEQ:def 1;
end;
end;
let m be
Nat;
cluster (
smid (p,m,n)) ->
plain;
coherence
proof
(
smid (p,m,n))
= ((p
/^ (m
-' 1))
| ((n
+ 1)
-' m)) by
FINSEQ_8:def 1;
hence thesis;
end;
cluster ((m,n)
-cut p) ->
plain;
coherence
proof
per cases ;
suppose 1
<= m & m
<= n & n
<= (
len p);
then 1
<= m & m
<= (
len p) & 1
<= n & n
<= (
len p) by
XXREAL_0: 2;
then m
in (
dom p) & n
in (
dom p) by
FINSEQ_3: 25;
then (
smid (p,m,n))
= ((m,n)
-cut p) by
FINSEQ_8: 29;
hence thesis;
end;
suppose not (1
<= m & m
<= n & n
<= (
len p));
hence thesis by
FINSEQ_6:def 4;
end;
end;
end
registration
let p,q be
plain
Graph-yielding
FinSequence;
cluster (p
^ q) ->
plain;
coherence
proof
for x be
object st x
in (
dom (p
^ q)) holds ex G be
_Graph st G
= ((p
^ q)
. x) & G is
plain
proof
let x be
object;
assume
A1: x
in (
dom (p
^ q));
then
reconsider k = x as
Nat;
per cases by
A1,
FINSEQ_1: 25;
suppose k
in (
dom p);
then ((p
^ q)
. k)
= (p
. k) & ex G be
_Graph st (p
. k)
= G & G is
plain by
Def1,
FINSEQ_1:def 7;
hence ex G be
_Graph st ((p
^ q)
. x)
= G & G is
plain;
end;
suppose ex n be
Nat st n
in (
dom q) & k
= ((
len p)
+ n);
then
consider n be
Nat such that
A2: n
in (
dom q) & k
= ((
len p)
+ n);
((p
^ q)
. ((
len p)
+ n))
= (q
. n) & ex G be
_Graph st (q
. n)
= G & G is
plain by
A2,
Def1,
FINSEQ_1:def 7;
hence ex G be
_Graph st ((p
^ q)
. x)
= G & G is
plain by
A2;
end;
end;
hence thesis;
end;
cluster (p
^' q) ->
plain;
coherence
proof
(p
^' q)
= (p
^ ((2,(
len q))
-cut q)) by
FINSEQ_6:def 5;
hence thesis;
end;
end
registration
let G1,G2 be
plain
_Graph;
cluster
<*G1, G2*> ->
plain;
coherence
proof
<*G1, G2*>
= (
<*G1*>
^
<*G2*>) by
FINSEQ_1:def 9;
hence thesis;
end;
let G3 be
plain
_Graph;
cluster
<*G1, G2, G3*> ->
plain;
coherence
proof
<*G1, G2, G3*>
= ((
<*G1*>
^
<*G2*>)
^
<*G3*>) by
FINSEQ_1:def 10;
hence thesis;
end;
end
begin
theorem ::
GLIBPRE0:77
Th81: for G1,G2 be
_Graph st G1
== G2 holds ex F be
PGraphMapping of G1, G2 st F
= (
id G1) & F is
Disomorphism
proof
let G1,G2 be
_Graph;
assume
A1: G1
== G2;
then
reconsider F = (
id G1) as
PGraphMapping of G1, G2 by
GLIB_010: 11;
take F;
thus F
= (
id G1);
(
dom (F
_V ))
= (
the_Vertices_of G1) & (
dom (F
_E ))
= (
the_Edges_of G1);
then
A2: F is
total by
GLIB_010:def 11;
(
rng (F
_V ))
= (
the_Vertices_of G2) & (
rng (F
_E ))
= (
the_Edges_of G2) by
A1,
GLIB_000:def 34;
then
A3: F is
onto by
GLIB_010:def 12;
(F
_V ) is
one-to-one & (F
_E ) is
one-to-one;
then
A4: F is
one-to-one by
GLIB_010:def 13;
now
let e,v,w be
object;
assume
A5: e
in (
dom (F
_E )) & v
in (
dom (F
_V )) & w
in (
dom (F
_V ));
assume e
DJoins (v,w,G1);
then (((
id G1)
_E )
. e)
DJoins ((((
id G1)
_V )
. v),(((
id G1)
_V )
. w),G1) by
A5,
GLIB_010:def 14;
hence ((F
_E )
. e)
DJoins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
GLIB_000: 88;
end;
then F is
directed by
GLIB_010:def 14;
hence F is
Disomorphism by
A2,
A3,
A4;
end;
theorem ::
GLIBPRE0:78
for G1,G2 be
_Graph st G1
== G2 holds G2 is G1
-Disomorphic
proof
let G1,G2 be
_Graph;
assume G1
== G2;
then
consider F be
PGraphMapping of G1, G2 such that
A1: F
= (
id G1) & F is
Disomorphism by
Th81;
thus thesis by
A1,
GLIB_010:def 24;
end;
theorem ::
GLIBPRE0:79
Th83: for G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E holds ex F be
PGraphMapping of G1, G2 st F
= (
id G1) & F is
isomorphism
proof
let G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E;
reconsider F = (
id G1) as
PGraphMapping of G1, G2 by
GLIB_010: 12;
take F;
thus F
= (
id G1);
(
dom (F
_V ))
= (
the_Vertices_of G1) & (
dom (F
_E ))
= (
the_Edges_of G1);
then
A1: F is
total by
GLIB_010:def 11;
(
rng (F
_V ))
= (
the_Vertices_of G2) & (
rng (F
_E ))
= (
the_Edges_of G2) by
GLIB_007: 4;
then
A2: F is
onto by
GLIB_010:def 12;
(F
_V ) is
one-to-one & (F
_E ) is
one-to-one;
then F is
one-to-one by
GLIB_010:def 13;
hence F is
isomorphism by
A1,
A2;
end;
theorem ::
GLIBPRE0:80
for G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E holds G2 is G1
-isomorphic
proof
let G1 be
_Graph, E be
set, G2 be
reverseEdgeDirections of G1, E;
consider F be
PGraphMapping of G1, G2 such that
A1: F
= (
id G1) & F is
isomorphism by
Th83;
thus thesis by
A1,
GLIB_010:def 23;
end;
theorem ::
GLIBPRE0:81
for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 st F is
Dcontinuous
isomorphism holds (G1 is
non-Dmulti iff G2 is
non-Dmulti) & (G1 is
Dsimple iff G2 is
Dsimple)
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
assume
A1: F is
Dcontinuous
isomorphism;
then
reconsider F0 = F as
one-to-one
PGraphMapping of G1, G2;
(F0
" ) is
Dcontinuous
isomorphism by
A1,
GLIB_010: 74,
GLIB_010: 75;
hence thesis by
A1,
GLIB_010: 50;
end;
theorem ::
GLIBPRE0:82
Th86: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st v
in (
dom (F
_V )) holds ((F
_E )
.: (v
.edgesInOut() ))
c= (((F
_V )
/. v)
.edgesInOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: v
in (
dom (F
_V ));
now
let e be
object;
assume e
in ((F
_E )
.: (v
.edgesInOut() ));
then
consider e0 be
object such that
A2: e0
in (
dom (F
_E )) & e0
in (v
.edgesInOut() ) & e
= ((F
_E )
. e0) by
FUNCT_1:def 6;
per cases by
A2,
GLIB_000: 61;
suppose
A3: ((
the_Source_of G1)
. e0)
= v;
set w = ((
the_Target_of G1)
. e0);
A4: w
in (
dom (F
_V )) by
A2,
GLIB_010: 5;
e0
Joins (v,w,G1) by
A2,
A3,
GLIB_000:def 13;
then ((F
_E )
. e0)
Joins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A2,
A4,
GLIB_010: 4;
then ((F
_E )
. e0)
Joins (((F
_V )
/. v),((F
_V )
. w),G2) by
A1,
PARTFUN1:def 6;
hence e
in (((F
_V )
/. v)
.edgesInOut() ) by
A2,
GLIB_000: 62;
end;
suppose
A5: ((
the_Target_of G1)
. e0)
= v;
set w = ((
the_Source_of G1)
. e0);
A6: w
in (
dom (F
_V )) by
A2,
GLIB_010: 5;
e0
Joins (v,w,G1) by
A2,
A5,
GLIB_000:def 13;
then ((F
_E )
. e0)
Joins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A2,
A6,
GLIB_010: 4;
then ((F
_E )
. e0)
Joins (((F
_V )
/. v),((F
_V )
. w),G2) by
A1,
PARTFUN1:def 6;
hence e
in (((F
_V )
/. v)
.edgesInOut() ) by
A2,
GLIB_000: 62;
end;
end;
hence thesis by
TARSKI:def 3;
end;
theorem ::
GLIBPRE0:83
Th87: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
directed & v
in (
dom (F
_V )) holds ((F
_E )
.: (v
.edgesIn() ))
c= (((F
_V )
/. v)
.edgesIn() ) & ((F
_E )
.: (v
.edgesOut() ))
c= (((F
_V )
/. v)
.edgesOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: F is
directed & v
in (
dom (F
_V ));
now
let e be
object;
assume e
in ((F
_E )
.: (v
.edgesIn() ));
then
consider e0 be
object such that
A2: e0
in (
dom (F
_E )) & e0
in (v
.edgesIn() ) & e
= ((F
_E )
. e0) by
FUNCT_1:def 6;
A3: ((
the_Target_of G1)
. e0)
= v by
A2,
GLIB_000: 56;
set w = ((
the_Source_of G1)
. e0);
A4: w
in (
dom (F
_V )) by
A2,
GLIB_010: 5;
e0
DJoins (w,v,G1) by
A2,
A3,
GLIB_000:def 14;
then ((F
_E )
. e0)
DJoins (((F
_V )
. w),((F
_V )
. v),G2) by
A1,
A2,
A4,
GLIB_010:def 14;
then ((F
_E )
. e0)
DJoins (((F
_V )
. w),((F
_V )
/. v),G2) by
A1,
PARTFUN1:def 6;
hence e
in (((F
_V )
/. v)
.edgesIn() ) by
A2,
GLIB_000: 57;
end;
hence ((F
_E )
.: (v
.edgesIn() ))
c= (((F
_V )
/. v)
.edgesIn() ) by
TARSKI:def 3;
now
let e be
object;
assume e
in ((F
_E )
.: (v
.edgesOut() ));
then
consider e0 be
object such that
A5: e0
in (
dom (F
_E )) & e0
in (v
.edgesOut() ) & e
= ((F
_E )
. e0) by
FUNCT_1:def 6;
A6: ((
the_Source_of G1)
. e0)
= v by
A5,
GLIB_000: 58;
set w = ((
the_Target_of G1)
. e0);
A7: w
in (
dom (F
_V )) by
A5,
GLIB_010: 5;
e0
DJoins (v,w,G1) by
A5,
A6,
GLIB_000:def 14;
then ((F
_E )
. e0)
DJoins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A5,
A7,
GLIB_010:def 14;
then ((F
_E )
. e0)
DJoins (((F
_V )
/. v),((F
_V )
. w),G2) by
A1,
PARTFUN1:def 6;
hence e
in (((F
_V )
/. v)
.edgesOut() ) by
A5,
GLIB_000: 59;
end;
hence ((F
_E )
.: (v
.edgesOut() ))
c= (((F
_V )
/. v)
.edgesOut() ) by
TARSKI:def 3;
end;
theorem ::
GLIBPRE0:84
Th88: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
onto
semi-continuous & v
in (
dom (F
_V )) holds ((F
_E )
.: (v
.edgesInOut() ))
= (((F
_V )
/. v)
.edgesInOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume
A1: F is
onto
semi-continuous & v
in (
dom (F
_V ));
then
A2: ((F
_E )
.: (v
.edgesInOut() ))
c= (((F
_V )
/. v)
.edgesInOut() ) by
Th86;
now
let e9 be
object;
assume
A3: e9
in (((F
_V )
/. v)
.edgesInOut() );
then e9
in (
the_Edges_of G2);
then e9
in (
rng (F
_E )) by
A1,
GLIB_010:def 12;
then
consider e be
object such that
A4: e
in (
dom (F
_E )) & ((F
_E )
. e)
= e9 by
FUNCT_1:def 3;
per cases by
A3,
GLIB_000: 61;
suppose
A5: ((
the_Source_of G2)
. e9)
= ((F
_V )
/. v);
set w9 = ((
the_Target_of G2)
. e9);
A6: ((F
_E )
. e)
Joins (((F
_V )
/. v),w9,G2) by
A3,
A4,
A5,
GLIB_000:def 13;
then w9
in (
the_Vertices_of G2) by
GLIB_000: 13;
then w9
in (
rng (F
_V )) by
A1,
GLIB_010:def 12;
then
consider w be
object such that
A7: w
in (
dom (F
_V )) & ((F
_V )
. w)
= w9 by
FUNCT_1:def 3;
((F
_E )
. e)
Joins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A6,
A7,
PARTFUN1:def 6;
then e
in (v
.edgesInOut() ) by
A1,
A4,
A7,
GLIB_010:def 15,
GLIB_000: 62;
hence e9
in ((F
_E )
.: (v
.edgesInOut() )) by
A4,
FUNCT_1:def 6;
end;
suppose
A8: ((
the_Target_of G2)
. e9)
= ((F
_V )
/. v);
set w9 = ((
the_Source_of G2)
. e9);
A9: ((F
_E )
. e)
Joins (((F
_V )
/. v),w9,G2) by
A3,
A4,
A8,
GLIB_000:def 13;
then w9
in (
the_Vertices_of G2) by
GLIB_000: 13;
then w9
in (
rng (F
_V )) by
A1,
GLIB_010:def 12;
then
consider w be
object such that
A10: w
in (
dom (F
_V )) & ((F
_V )
. w)
= w9 by
FUNCT_1:def 3;
((F
_E )
. e)
Joins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A9,
A10,
PARTFUN1:def 6;
then e
in (v
.edgesInOut() ) by
A1,
A4,
A10,
GLIB_010:def 15,
GLIB_000: 62;
hence e9
in ((F
_E )
.: (v
.edgesInOut() )) by
A4,
FUNCT_1:def 6;
end;
end;
then (((F
_V )
/. v)
.edgesInOut() )
c= ((F
_E )
.: (v
.edgesInOut() )) by
TARSKI:def 3;
hence thesis by
A2,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:85
Th89: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
onto
semi-Dcontinuous & v
in (
dom (F
_V )) holds ((F
_E )
.: (v
.edgesIn() ))
= (((F
_V )
/. v)
.edgesIn() ) & ((F
_E )
.: (v
.edgesOut() ))
= (((F
_V )
/. v)
.edgesOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume
A1: F is
onto
semi-Dcontinuous & v
in (
dom (F
_V ));
then
A2: ((F
_E )
.: (v
.edgesIn() ))
c= (((F
_V )
/. v)
.edgesIn() ) & ((F
_E )
.: (v
.edgesOut() ))
c= (((F
_V )
/. v)
.edgesOut() ) by
Th87;
now
let e9 be
object;
assume
A3: e9
in (((F
_V )
/. v)
.edgesIn() );
then e9
in (
the_Edges_of G2);
then e9
in (
rng (F
_E )) by
A1,
GLIB_010:def 12;
then
consider e be
object such that
A4: e
in (
dom (F
_E )) & ((F
_E )
. e)
= e9 by
FUNCT_1:def 3;
A5: ((
the_Target_of G2)
. e9)
= ((F
_V )
/. v) by
A3,
GLIB_000: 56;
set w9 = ((
the_Source_of G2)
. e9);
A6: ((F
_E )
. e)
DJoins (w9,((F
_V )
/. v),G2) by
A3,
A4,
A5,
GLIB_000:def 14;
then ((F
_E )
. e)
Joins (w9,((F
_V )
/. v),G2) by
GLIB_000: 16;
then w9
in (
the_Vertices_of G2) by
GLIB_000: 13;
then w9
in (
rng (F
_V )) by
A1,
GLIB_010:def 12;
then
consider w be
object such that
A7: w
in (
dom (F
_V )) & ((F
_V )
. w)
= w9 by
FUNCT_1:def 3;
((F
_E )
. e)
DJoins (((F
_V )
. w),((F
_V )
. v),G2) by
A1,
A6,
A7,
PARTFUN1:def 6;
then
A8: e
DJoins (w,v,G1) by
A1,
A4,
A7,
GLIB_010:def 17;
e is
set & w is
set by
TARSKI: 1;
then e
in (v
.edgesIn() ) by
A8,
GLIB_000: 57;
hence e9
in ((F
_E )
.: (v
.edgesIn() )) by
A4,
FUNCT_1:def 6;
end;
then (((F
_V )
/. v)
.edgesIn() )
c= ((F
_E )
.: (v
.edgesIn() )) by
TARSKI:def 3;
hence ((F
_E )
.: (v
.edgesIn() ))
= (((F
_V )
/. v)
.edgesIn() ) by
A2,
XBOOLE_0:def 10;
now
let e9 be
object;
assume
A9: e9
in (((F
_V )
/. v)
.edgesOut() );
then e9
in (
the_Edges_of G2);
then e9
in (
rng (F
_E )) by
A1,
GLIB_010:def 12;
then
consider e be
object such that
A10: e
in (
dom (F
_E )) & ((F
_E )
. e)
= e9 by
FUNCT_1:def 3;
A11: ((
the_Source_of G2)
. e9)
= ((F
_V )
/. v) by
A9,
GLIB_000: 58;
set w9 = ((
the_Target_of G2)
. e9);
A12: ((F
_E )
. e)
DJoins (((F
_V )
/. v),w9,G2) by
A9,
A10,
A11,
GLIB_000:def 14;
then ((F
_E )
. e)
Joins (((F
_V )
/. v),w9,G2) by
GLIB_000: 16;
then w9
in (
the_Vertices_of G2) by
GLIB_000: 13;
then w9
in (
rng (F
_V )) by
A1,
GLIB_010:def 12;
then
consider w be
object such that
A13: w
in (
dom (F
_V )) & ((F
_V )
. w)
= w9 by
FUNCT_1:def 3;
((F
_E )
. e)
DJoins (((F
_V )
. v),((F
_V )
. w),G2) by
A1,
A12,
A13,
PARTFUN1:def 6;
then
A14: e
DJoins (v,w,G1) by
A1,
A10,
A13,
GLIB_010:def 17;
e is
set & w is
set by
TARSKI: 1;
then e
in (v
.edgesOut() ) by
A14,
GLIB_000: 59;
hence e9
in ((F
_E )
.: (v
.edgesOut() )) by
A10,
FUNCT_1:def 6;
end;
then (((F
_V )
/. v)
.edgesOut() )
c= ((F
_E )
.: (v
.edgesOut() )) by
TARSKI:def 3;
hence ((F
_E )
.: (v
.edgesOut() ))
= (((F
_V )
/. v)
.edgesOut() ) by
A2,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:86
for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
isomorphism holds ((F
_E )
.: (v
.edgesInOut() ))
= (((F
_V )
/. v)
.edgesInOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: F is
isomorphism;
then (
dom (F
_V ))
= (
the_Vertices_of G1) by
GLIB_010:def 11;
hence thesis by
A1,
Th88;
end;
theorem ::
GLIBPRE0:87
for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
Disomorphism holds ((F
_E )
.: (v
.edgesIn() ))
= (((F
_V )
/. v)
.edgesIn() ) & ((F
_E )
.: (v
.edgesOut() ))
= (((F
_V )
/. v)
.edgesOut() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: F is
Disomorphism;
then (
dom (F
_V ))
= (
the_Vertices_of G1) by
GLIB_010:def 11;
hence thesis by
A1,
Th89;
end;
registration
let G1 be
_Graph, G2 be
edgeless
_Graph;
cluster ->
directed for
PGraphMapping of G1, G2;
coherence
proof
let F be
PGraphMapping of G1, G2;
for e,v,w be
object st e
in (
dom (F
_E )) & v
in (
dom (F
_V )) & w
in (
dom (F
_V )) holds e
DJoins (v,w,G1) implies ((F
_E )
. e)
DJoins (((F
_V )
. v),((F
_V )
. w),G2);
hence thesis by
GLIB_010:def 14;
end;
end
theorem ::
GLIBPRE0:88
Th92: for G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2 st (F0
_E ) is
one-to-one holds ex E be
Subset of (
the_Edges_of G2) st for G3 be
reverseEdgeDirections of G2, E holds ex F be
PGraphMapping of G1, G3 st F
= F0 & F is
directed & (F0 is non
empty implies F is non
empty) & (F0 is
total implies F is
total) & (F0 is
one-to-one implies F is
one-to-one) & (F0 is
onto implies F is
onto) & (F0 is
semi-continuous implies F is
semi-continuous) & (F0 is
continuous implies F is
continuous)
proof
let G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2;
assume
A1: (F0
_E ) is
one-to-one;
per cases ;
suppose (
the_Edges_of G2)
<>
{} ;
set E = { e9 where e9 be
Element of (
the_Edges_of G2) : e9
in (
rng (F0
_E )) & for e be
object st e
in (
dom (F0
_E )) & ((F0
_E )
. e)
= e9 holds e9
DJoins (((F0
_V )
. ((
the_Target_of G1)
. e)),((F0
_V )
. ((
the_Source_of G1)
. e)),G2) };
now
let x be
object;
assume x
in E;
then
consider e9 be
Element of (
the_Edges_of G2) such that
A2: x
= e9 and
A3: e9
in (
rng (F0
_E )) and for e be
object st e
in (
dom (F0
_E )) & ((F0
_E )
. e)
= e9 holds e9
DJoins (((F0
_V )
. ((
the_Target_of G1)
. e)),((F0
_V )
. ((
the_Source_of G1)
. e)),G2);
e9
in (
the_Edges_of G2) by
A3;
hence x
in (
the_Edges_of G2) by
A2;
end;
then
reconsider E as
Subset of (
the_Edges_of G2) by
TARSKI:def 3;
take E;
let G3 be
reverseEdgeDirections of G2, E;
consider F9 be
PGraphMapping of G2, G3 such that
A4: F9
= (
id G2) & F9 is
isomorphism by
Th83;
take (F9
* F0);
thus
A5: (F9
* F0)
= ((
id G2)
* F0) by
A4
.= F0 by
GLIB_010: 116;
now
let e,v,w be
object;
assume e
in (
dom ((F9
* F0)
_E )) & v
in (
dom ((F9
* F0)
_V )) & w
in (
dom ((F9
* F0)
_V ));
then
A6: e
in (
dom (F0
_E )) & v
in (
dom (F0
_V )) & w
in (
dom (F0
_V )) by
A5;
assume
A7: e
DJoins (v,w,G1);
A8: ((F0
_E )
. e)
in (
rng (F0
_E )) by
A6,
FUNCT_1: 3;
then
reconsider e9 = ((F0
_E )
. e) as
Element of (
the_Edges_of G2);
per cases ;
suppose
A11: e9
in E;
then
consider e8 be
Element of (
the_Edges_of G2) such that
A12: e8
= e9 & e8
in (
rng (F0
_E )) and
A13: for e0 be
object st e0
in (
dom (F0
_E )) & ((F0
_E )
. e0)
= e8 holds e8
DJoins (((F0
_V )
. ((
the_Target_of G1)
. e0)),((F0
_V )
. ((
the_Source_of G1)
. e0)),G2);
A14: e9
DJoins (((F0
_V )
. ((
the_Target_of G1)
. e)),((F0
_V )
. ((
the_Source_of G1)
. e)),G2) by
A6,
A12,
A13;
((
the_Source_of G1)
. e)
= v & ((
the_Target_of G1)
. e)
= w by
A7,
GLIB_000:def 14;
then ((F0
_E )
. e)
DJoins (((F0
_V )
. v),((F0
_V )
. w),G3) by
A11,
A14,
GLIB_007: 7;
hence (((F9
* F0)
_E )
. e)
DJoins ((((F9
* F0)
_V )
. v),(((F9
* F0)
_V )
. w),G3) by
A5;
end;
suppose
A15: not e9
in E;
e
Joins (v,w,G1) by
A7,
GLIB_000: 16;
then
A16: ((F0
_E )
. e)
Joins (((F0
_V )
. v),((F0
_V )
. w),G2) by
A6,
GLIB_010: 4;
not ((F0
_E )
. e)
DJoins (((F0
_V )
. w),((F0
_V )
. v),G2)
proof
assume
A17: ((F0
_E )
. e)
DJoins (((F0
_V )
. w),((F0
_V )
. v),G2);
for e0 be
object st e0
in (
dom (F0
_E )) & ((F0
_E )
. e0)
= e9 holds e9
DJoins (((F0
_V )
. ((
the_Target_of G1)
. e0)),((F0
_V )
. ((
the_Source_of G1)
. e0)),G2)
proof
let e0 be
object;
assume e0
in (
dom (F0
_E )) & ((F0
_E )
. e0)
= e9;
then e
= e0 by
A1,
A6,
FUNCT_1:def 4;
then ((
the_Source_of G1)
. e0)
= v & ((
the_Target_of G1)
. e0)
= w by
A7,
GLIB_000:def 14;
hence thesis by
A17;
end;
hence contradiction by
A8,
A15;
end;
then ((F0
_E )
. e)
DJoins (((F0
_V )
. v),((F0
_V )
. w),G2) by
A16,
GLIB_000: 16;
then ((F0
_E )
. e)
DJoins (((F0
_V )
. v),((F0
_V )
. w),G3) by
A15,
GLIB_007: 8;
hence (((F9
* F0)
_E )
. e)
DJoins ((((F9
* F0)
_V )
. v),(((F9
* F0)
_V )
. w),G3) by
A5;
end;
end;
hence (F9
* F0) is
directed by
GLIB_010:def 14;
thus F0 is non
empty implies (F9
* F0) is non
empty by
A5;
thus thesis by
A4,
GLIB_010: 104,
GLIB_010: 106;
end;
suppose
A18: (
the_Edges_of G2)
=
{} ;
take E = (
{} (
the_Edges_of G2));
let G3 be
reverseEdgeDirections of G2, E;
consider F9 be
PGraphMapping of G2, G3 such that
A19: F9
= (
id G2) & F9 is
isomorphism by
Th83;
take (F9
* F0);
thus
A20: (F9
* F0)
= ((
id G2)
* F0) by
A19
.= F0 by
GLIB_010: 116;
(
the_Edges_of G3)
=
{} by
A18,
GLIB_007: 4;
then G3 is
edgeless;
hence (F9
* F0) is
directed;
thus F0 is non
empty implies (F9
* F0) is non
empty by
A20;
thus thesis by
A19,
GLIB_010: 104,
GLIB_010: 106;
end;
end;
theorem ::
GLIBPRE0:89
Th93: for G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2 st (F0
_E ) is
one-to-one holds ex E be
Subset of (
the_Edges_of G2) st for G3 be
reverseEdgeDirections of G2, E holds ex F be
PGraphMapping of G1, G3 st F
= F0 & F is
directed & (F0 is
weak_SG-embedding implies F is
weak_SG-embedding) & (F0 is
strong_SG-embedding implies F is
strong_SG-embedding) & (F0 is
isomorphism implies F is
isomorphism)
proof
let G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2;
assume (F0
_E ) is
one-to-one;
then
consider E be
Subset of (
the_Edges_of G2) such that
A1: for G3 be
reverseEdgeDirections of G2, E holds ex F be
PGraphMapping of G1, G3 st F
= F0 & F is
directed & (F0 is non
empty implies F is non
empty) & (F0 is
total implies F is
total) & (F0 is
one-to-one implies F is
one-to-one) & (F0 is
onto implies F is
onto) & (F0 is
semi-continuous implies F is
semi-continuous) & (F0 is
continuous implies F is
continuous) by
Th92;
take E;
let G3 be
reverseEdgeDirections of G2, E;
consider F be
PGraphMapping of G1, G3 such that
A2: F
= F0 & F is
directed and F0 is non
empty implies F is non
empty and
A3: F0 is
total implies F is
total and
A4: F0 is
one-to-one implies F is
one-to-one and
A5: F0 is
onto implies F is
onto and F0 is
semi-continuous implies F is
semi-continuous and
A6: F0 is
continuous implies F is
continuous by
A1;
take F;
thus F
= F0 & F is
directed by
A2;
thus thesis by
A3,
A4,
A5,
A6;
end;
theorem ::
GLIBPRE0:90
Th94: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
directed
weak_SG-embedding holds (v
.inDegree() )
c= (((F
_V )
/. v)
.inDegree() ) & (v
.outDegree() )
c= (((F
_V )
/. v)
.outDegree() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume
A1: F is
directed
weak_SG-embedding;
then
A2: (
dom (F
_E ))
= (
the_Edges_of G1) by
GLIB_010:def 11;
set f = ((F
_E )
| (v
.edgesIn() ));
A3: (
dom f)
= ((
dom (F
_E ))
/\ (v
.edgesIn() )) by
RELAT_1: 61
.= (v
.edgesIn() ) by
A2,
XBOOLE_1: 28;
A4: (
rng f)
= ((F
_E )
.: (v
.edgesIn() )) by
RELAT_1: 115;
(
dom (F
_V ))
= (
the_Vertices_of G1) by
A1,
GLIB_010:def 11;
then ((F
_E )
.: (v
.edgesIn() ))
c= (((F
_V )
/. v)
.edgesIn() ) by
A1,
Th87;
then
A5: (
card ((F
_E )
.: (v
.edgesIn() )))
c= (
card (((F
_V )
/. v)
.edgesIn() )) by
CARD_1: 11;
f is
one-to-one by
A1,
FUNCT_1: 52;
hence (v
.inDegree() )
c= (((F
_V )
/. v)
.inDegree() ) by
A3,
A4,
A5,
CARD_1: 70;
set f = ((F
_E )
| (v
.edgesOut() ));
A6: (
dom f)
= ((
dom (F
_E ))
/\ (v
.edgesOut() )) by
RELAT_1: 61
.= (v
.edgesOut() ) by
A2,
XBOOLE_1: 28;
A7: (
rng f)
= ((F
_E )
.: (v
.edgesOut() )) by
RELAT_1: 115;
(
dom (F
_V ))
= (
the_Vertices_of G1) by
A1,
GLIB_010:def 11;
then ((F
_E )
.: (v
.edgesOut() ))
c= (((F
_V )
/. v)
.edgesOut() ) by
A1,
Th87;
then
A8: (
card ((F
_E )
.: (v
.edgesOut() )))
c= (
card (((F
_V )
/. v)
.edgesOut() )) by
CARD_1: 11;
f is
one-to-one by
A1,
FUNCT_1: 52;
hence (v
.outDegree() )
c= (((F
_V )
/. v)
.outDegree() ) by
A6,
A7,
A8,
CARD_1: 70;
end;
Lm5: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
directed
weak_SG-embedding holds (v
.degree() )
c= (((F
_V )
/. v)
.degree() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume F is
directed
weak_SG-embedding;
then (v
.inDegree() )
c= (((F
_V )
/. v)
.inDegree() ) & (v
.outDegree() )
c= (((F
_V )
/. v)
.outDegree() ) by
Th94;
hence thesis by
CARD_2: 83;
end;
theorem ::
GLIBPRE0:91
for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
weak_SG-embedding holds (v
.degree() )
c= (((F
_V )
/. v)
.degree() )
proof
let G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume
A1: F0 is
weak_SG-embedding;
then (F0
_E ) is
one-to-one;
then
consider E be
Subset of (
the_Edges_of G2) such that
A2: for G3 be
reverseEdgeDirections of G2, E holds ex F be
PGraphMapping of G1, G3 st F
= F0 & F is
directed & (F0 is
weak_SG-embedding implies F is
weak_SG-embedding) & (F0 is
strong_SG-embedding implies F is
strong_SG-embedding) & (F0 is
isomorphism implies F is
isomorphism) by
Th93;
set G3 = the
reverseEdgeDirections of G2, E;
consider F be
PGraphMapping of G1, G3 such that
A3: F
= F0 & F is
directed and
A4: F0 is
weak_SG-embedding implies F is
weak_SG-embedding and (F0 is
strong_SG-embedding implies F is
strong_SG-embedding) & (F0 is
isomorphism implies F is
isomorphism) by
A2;
A5: (v
.degree() )
c= (((F
_V )
/. v)
.degree() ) by
A1,
A3,
A4,
Lm5;
(
dom (F
_V ))
= (
the_Vertices_of G1) by
A1,
A4,
GLIB_010:def 11;
then
A6: v
in (
dom (F
_V )) & v
in (
dom (F0
_V )) by
A3;
((F0
_V )
/. v)
= ((F0
_V )
. v) by
A6,
PARTFUN1:def 6
.= ((F
_V )
/. v) by
A3,
A6,
PARTFUN1:def 6;
hence thesis by
A5,
Th60;
end;
theorem ::
GLIBPRE0:92
Th96: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
onto
semi-Dcontinuous & v
in (
dom (F
_V )) holds (((F
_V )
/. v)
.inDegree() )
c= (v
.inDegree() ) & (((F
_V )
/. v)
.outDegree() )
c= (v
.outDegree() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume F is
onto
semi-Dcontinuous & v
in (
dom (F
_V ));
then ((F
_E )
.: (v
.edgesIn() ))
= (((F
_V )
/. v)
.edgesIn() ) & ((F
_E )
.: (v
.edgesOut() ))
= (((F
_V )
/. v)
.edgesOut() ) by
Th89;
hence thesis by
CARD_1: 67;
end;
theorem ::
GLIBPRE0:93
for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
onto
semi-Dcontinuous & v
in (
dom (F
_V )) holds (((F
_V )
/. v)
.degree() )
c= (v
.degree() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2, v be
Vertex of G1;
assume F is
onto
semi-Dcontinuous & v
in (
dom (F
_V ));
then (((F
_V )
/. v)
.inDegree() )
c= (v
.inDegree() ) & (((F
_V )
/. v)
.outDegree() )
c= (v
.outDegree() ) by
Th96;
hence thesis by
CARD_2: 83;
end;
theorem ::
GLIBPRE0:94
Th98: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
Disomorphism holds (v
.inDegree() )
= (((F
_V )
/. v)
.inDegree() ) & (v
.outDegree() )
= (((F
_V )
/. v)
.outDegree() )
proof
let G1,G2 be
_Graph, F be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: F is
Disomorphism;
then (
dom (F
_V ))
= (
the_Vertices_of G1) by
GLIB_010:def 11;
then
A2: (((F
_V )
/. v)
.inDegree() )
c= (v
.inDegree() ) & (((F
_V )
/. v)
.outDegree() )
c= (v
.outDegree() ) by
A1,
Th96;
(v
.inDegree() )
c= (((F
_V )
/. v)
.inDegree() ) & (v
.outDegree() )
c= (((F
_V )
/. v)
.outDegree() ) by
A1,
Th94;
hence thesis by
A2,
XBOOLE_0:def 10;
end;
theorem ::
GLIBPRE0:95
Th99: for G1,G2 be
_Graph, F be
PGraphMapping of G1, G2 holds for v be
Vertex of G1 st F is
isomorphism holds (v
.degree() )
= (((F
_V )
/. v)
.degree() )
proof
let G1,G2 be
_Graph, F0 be
PGraphMapping of G1, G2;
let v be
Vertex of G1;
assume
A1: F0 is
isomorphism;
then (F0
_E ) is
one-to-one;
then
consider E be
Subset of (
the_Edges_of G2) such that
A2: for G3 be
reverseEdgeDirections of G2, E holds ex F be
PGraphMapping of G1, G3 st F
= F0 & F is
directed & (F0 is
weak_SG-embedding implies F is
weak_SG-embedding) & (F0 is
strong_SG-embedding implies F is
strong_SG-embedding) & (F0 is
isomorphism implies F is
isomorphism) by
Th93;
set G3 = the
reverseEdgeDirections of G2, E;
consider F be
PGraphMapping of G1, G3 such that
A3: F
= F0 & F is
directed and (F0 is
weak_SG-embedding implies F is
weak_SG-embedding) & (F0 is
strong_SG-embedding implies F is
strong_SG-embedding) and
A4: (F0 is
isomorphism implies F is
isomorphism) by
A2;
(v
.inDegree() )
= (((F
_V )
/. v)
.inDegree() ) & (v
.outDegree() )
= (((F
_V )
/. v)
.outDegree() ) by
A1,
A3,
A4,
Th98;
then
A5: (((F
_V )
/. v)
.degree() )
= (v
.degree() );
F0 is
total & (
dom (F
_V ))
= (
dom (F0
_V )) & v
in (
the_Vertices_of G1) by
A1,
A3;
then
A6: v
in (
dom (F0
_V )) & v
in (
dom (F
_V )) by
GLIB_010:def 11;
((F0
_V )
/. v)
= ((F0
_V )
. v) by
A6,
PARTFUN1:def 6
.= ((F
_V )
/. v) by
A3,
A6,
PARTFUN1:def 6;
hence thesis by
A5,
Th60;
end;
begin
theorem ::
GLIBPRE0:96
Th100: for G be
_Graph, u,v,w be
Vertex of G st v is
endvertex & u
<> w holds not (u,v)
are_adjacent or not (v,w)
are_adjacent
proof
let G be
_Graph, u,v,w be
Vertex of G;
assume
A1: v is
endvertex & u
<> w;
assume
A2: (u,v)
are_adjacent ;
consider e be
object such that
A3: (v
.edgesInOut() )
=
{e} & not e
Joins (v,v,G) by
A1,
GLIB_000:def 51;
e
in (v
.edgesInOut() ) by
A3,
TARSKI:def 1;
then
consider v9 be
Vertex of G such that
A4: e
Joins (v,v9,G) by
GLIB_000: 64;
consider e8 be
object such that
A5: e8
Joins (v,u,G) by
A2,
CHORD:def 3;
e8 is
set by
TARSKI: 1;
then e8
in (v
.edgesInOut() ) by
A5,
GLIB_000: 64;
then e8
= e by
A3,
TARSKI:def 1;
then
A6: v
= v & v9
= u or v
= u & v9
= v by
A4,
A5,
GLIB_000: 15;
not ex e9 be
object st e9
Joins (v,w,G)
proof
given e9 be
object such that
A7: e9
Joins (v,w,G);
e9 is
set by
TARSKI: 1;
then e9
in (v
.edgesInOut() ) by
A7,
GLIB_000: 64;
then e9
= e by
A3,
TARSKI:def 1;
then v
= v & w
= v9 or v
= v9 & w
= v by
A4,
A7,
GLIB_000: 15;
hence contradiction by
A1,
A6;
end;
hence not (v,w)
are_adjacent by
CHORD:def 3;
end;
theorem ::
GLIBPRE0:97
Th101: for G be
_Graph, v be
Vertex of G st 3
c= (G
.order() ) & v is
endvertex holds ex u,w be
Vertex of G st u
<> v & w
<> v & u
<> w & (u,v)
are_adjacent & not (v,w)
are_adjacent
proof
let G be
_Graph, v be
Vertex of G;
assume
A1: 3
c= (G
.order() ) & v is
endvertex;
then
A2: 3
c= (
card (
the_Vertices_of G));
consider e be
object such that
A3: (v
.edgesInOut() )
=
{e} & not e
Joins (v,v,G) by
A1,
GLIB_000:def 51;
e
in (v
.edgesInOut() ) by
A3,
TARSKI:def 1;
then
consider u be
Vertex of G such that
A4: e
Joins (v,u,G) by
GLIB_000: 64;
consider w be
object such that
A5: w
in (
the_Vertices_of G) & w
<> v & w
<> u by
A2,
PENCIL_1: 6;
reconsider w as
Vertex of G by
A5;
take u, w;
thus u
<> v & w
<> v & u
<> w by
A3,
A4,
A5;
thus (u,v)
are_adjacent by
A4,
CHORD:def 3;
hence not (v,w)
are_adjacent by
A1,
A5,
Th100;
end;
theorem ::
GLIBPRE0:98
for G be
_Graph, v be
Vertex of G st 4
c= (G
.order() ) & v is
endvertex holds ex x,y,z be
Vertex of G st v
<> x & v
<> y & v
<> z & x
<> y & x
<> z & y
<> z & (v,x)
are_adjacent & not (v,y)
are_adjacent & not (v,z)
are_adjacent
proof
let G be
_Graph, v be
Vertex of G;
assume
A1: 4
c= (G
.order() ) & v is
endvertex;
(
Segm 3)
c= (
Segm 4) by
NAT_1: 39;
then
consider x,y be
Vertex of G such that
A2: x
<> v & y
<> v & x
<> y & (x,v)
are_adjacent & not (v,y)
are_adjacent by
A1,
Th101,
XBOOLE_1: 1;
consider z be
object such that
A3: z
in (
the_Vertices_of G) & v
<> z & x
<> z & y
<> z by
A1,
Th21;
reconsider z as
Vertex of G by
A3;
take x, y, z;
thus v
<> x & v
<> y & v
<> z & x
<> y & x
<> z & y
<> z by
A2,
A3;
thus (v,x)
are_adjacent by
A2;
thus not (v,y)
are_adjacent by
A2;
thus not (v,z)
are_adjacent by
A1,
A2,
A3,
Th100;
end;
definition
let GF be
Graph-yielding
Function;
::
GLIBPRE0:def4
attr GF is
chordal means
:
Def4: for x be
object st x
in (
dom GF) holds ex G be
_Graph st (GF
. x)
= G & G is
chordal;
end
registration
let G be
chordal
_Graph;
cluster
<*G*> ->
chordal;
coherence
proof
let x be
object;
assume
A1: x
in (
dom
<*G*>);
then
reconsider n = x as
Nat;
1
<= n
<= (
len
<*G*>) by
A1,
FINSEQ_3: 25;
then 1
<= n
<= 1 by
FINSEQ_1: 40;
then n
= 1 by
XXREAL_0: 1;
hence thesis by
FINSEQ_1: 40;
end;
cluster (
NAT
--> G) ->
chordal;
coherence by
FUNCOP_1: 7;
end
definition
let GF be non
empty
Graph-yielding
Function;
:: original:
chordal
redefine
::
GLIBPRE0:def5
attr GF is
chordal means
:
Def5: for x be
Element of (
dom GF) holds (GF
. x) is
chordal;
compatibility
proof
hereby
assume
A1: GF is
chordal;
let x be
Element of (
dom GF);
ex G be
_Graph st (GF
. x)
= G & G is
chordal by
A1;
hence (GF
. x) is
chordal;
end;
assume
A3: for x be
Element of (
dom GF) holds (GF
. x) is
chordal;
let x be
object;
assume x
in (
dom GF);
then
reconsider y = x as
Element of (
dom GF);
take (GF
. y);
thus thesis by
A3;
end;
end
definition
let GSq be
GraphSeq;
:: original:
chordal
redefine
::
GLIBPRE0:def6
attr GSq is
chordal means
:
Def6: for n be
Nat holds (GSq
. n) is
chordal;
compatibility
proof
hereby
assume
A1: GSq is
chordal;
let x be
Nat;
x
in (
dom GSq) by
Lm4;
hence (GSq
. x) is
chordal by
A1;
end;
assume
A2: for x be
Nat holds (GSq
. x) is
chordal;
let x be
Element of (
dom GSq);
thus thesis by
A2;
end;
end
registration
cluster
empty ->
chordal for
Graph-yielding
Function;
coherence ;
end
registration
cluster
chordal for
GraphSeq;
existence
proof
take (
NAT
--> the
chordal
_Graph);
thus thesis;
end;
cluster non
empty
chordal for
Graph-yielding
FinSequence;
existence
proof
take
<* the
chordal
_Graph*>;
thus thesis;
end;
end
registration
let GF be
chordal non
empty
Graph-yielding
Function, x be
Element of (
dom GF);
cluster (GF
. x) ->
chordal;
coherence by
Def5;
end
registration
let GSq be
chordal
GraphSeq, x be
Nat;
cluster (GSq
. x) ->
chordal;
coherence by
Def6;
end
registration
let p be
chordal
Graph-yielding
FinSequence, n be
Nat;
cluster (p
| n) ->
chordal;
coherence
proof
A1: (p
| n)
= (p
| (
Seg n)) by
FINSEQ_1:def 15;
now
let x be
object;
assume
A2: x
in (
dom (p
| n));
then x
in (
dom p) by
A1,
RELAT_1: 60,
TARSKI:def 3;
then
consider G be
_Graph such that
A3: (p
. x)
= G & G is
chordal by
Def4;
take G;
thus ((p
| n)
. x)
= G & G is
chordal by
A1,
A3,
A2,
FUNCT_1: 47;
end;
hence thesis;
end;
cluster (p
/^ n) ->
chordal;
coherence
proof
per cases ;
suppose
A4: n
<= (
len p);
now
let x be
object;
assume
A5: x
in (
dom (p
/^ n));
then
reconsider i = x as
Nat;
(n
+ i)
in (
dom p) by
A5,
FINSEQ_5: 26;
then
consider G be
_Graph such that
A6: (p
. (n
+ i))
= G & G is
chordal by
Def4;
take G;
thus ((p
/^ n)
. x)
= G & G is
chordal by
A4,
A5,
A6,
RFINSEQ:def 1;
end;
hence thesis;
end;
suppose not (n
<= (
len p));
hence thesis by
RFINSEQ:def 1;
end;
end;
let m be
Nat;
cluster (
smid (p,m,n)) ->
chordal;
coherence
proof
(
smid (p,m,n))
= ((p
/^ (m
-' 1))
| ((n
+ 1)
-' m)) by
FINSEQ_8:def 1;
hence thesis;
end;
cluster ((m,n)
-cut p) ->
chordal;
coherence
proof
per cases ;
suppose 1
<= m & m
<= n & n
<= (
len p);
then 1
<= m & m
<= (
len p) & 1
<= n & n
<= (
len p) by
XXREAL_0: 2;
then m
in (
dom p) & n
in (
dom p) by
FINSEQ_3: 25;
then (
smid (p,m,n))
= ((m,n)
-cut p) by
FINSEQ_8: 29;
hence thesis;
end;
suppose not (1
<= m & m
<= n & n
<= (
len p));
hence thesis by
FINSEQ_6:def 4;
end;
end;
end
registration
let p,q be
chordal
Graph-yielding
FinSequence;
cluster (p
^ q) ->
chordal;
coherence
proof
for x be
object st x
in (
dom (p
^ q)) holds ex G be
_Graph st G
= ((p
^ q)
. x) & G is
chordal
proof
let x be
object;
assume
A1: x
in (
dom (p
^ q));
then
reconsider k = x as
Nat;
per cases by
A1,
FINSEQ_1: 25;
suppose k
in (
dom p);
then ((p
^ q)
. k)
= (p
. k) & ex G be
_Graph st (p
. k)
= G & G is
chordal by
Def4,
FINSEQ_1:def 7;
hence ex G be
_Graph st ((p
^ q)
. x)
= G & G is
chordal;
end;
suppose ex n be
Nat st n
in (
dom q) & k
= ((
len p)
+ n);
then
consider n be
Nat such that
A2: n
in (
dom q) & k
= ((
len p)
+ n);
((p
^ q)
. ((
len p)
+ n))
= (q
. n) & ex G be
_Graph st (q
. n)
= G & G is
chordal by
A2,
Def4,
FINSEQ_1:def 7;
hence ex G be
_Graph st ((p
^ q)
. x)
= G & G is
chordal by
A2;
end;
end;
hence thesis;
end;
cluster (p
^' q) ->
chordal;
coherence
proof
(p
^' q)
= (p
^ ((2,(
len q))
-cut q)) by
FINSEQ_6:def 5;
hence thesis;
end;
end
registration
let G1,G2 be
chordal
_Graph;
cluster
<*G1, G2*> ->
chordal;
coherence
proof
<*G1, G2*>
= (
<*G1*>
^
<*G2*>) by
FINSEQ_1:def 9;
hence thesis;
end;
let G3 be
chordal
_Graph;
cluster
<*G1, G2, G3*> ->
chordal;
coherence
proof
<*G1, G2, G3*>
= ((
<*G1*>
^
<*G2*>)
^
<*G3*>) by
FINSEQ_1:def 10;
hence thesis;
end;
end
begin
theorem ::
GLIBPRE0:99
for G1,G2 be
non-Dmulti
_Graph, f be
directed
PVertexMapping of G1, G2 holds for v be
Vertex of G1 st f is
Disomorphism holds (v
.inDegree() )
= ((f
/. v)
.inDegree() ) & (v
.outDegree() )
= ((f
/. v)
.outDegree() )
proof
let G1,G2 be
non-Dmulti
_Graph, f be
directed
PVertexMapping of G1, G2;
let v be
Vertex of G1;
assume f is
Disomorphism;
then
A1: (
DPVM2PGM f) is
Disomorphism by
GLIB_011: 48;
thus (v
.inDegree() )
= ((((
DPVM2PGM f)
_V )
/. v)
.inDegree() ) by
A1,
Th98
.= ((f
/. v)
.inDegree() );
thus (v
.outDegree() )
= ((((
DPVM2PGM f)
_V )
/. v)
.outDegree() ) by
A1,
Th98
.= ((f
/. v)
.outDegree() );
end;
theorem ::
GLIBPRE0:100
for G1,G2 be
non-multi
_Graph, f be
PVertexMapping of G1, G2 holds for v be
Vertex of G1 st f is
isomorphism holds (v
.degree() )
= ((f
/. v)
.degree() )
proof
let G1,G2 be
non-multi
_Graph, f be
PVertexMapping of G1, G2;
let v be
Vertex of G1;
assume f is
isomorphism;
hence (v
.degree() )
= ((((
PVM2PGM f)
_V )
/. v)
.degree() ) by
Th99,
GLIB_011: 47
.= ((f
/. v)
.degree() );
end;