:: About Supergraphs, Part {II}
:: by Sebastian Koch
::
:: Received June 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI,
ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, FINSET_1,
ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, GLIB_001, FUNCT_4, GLIB_006,
ABIAN, REWRITE1, CHORD, RCOMP_1, WAYBEL_0, MCART_1, GRAPH_1, CARD_2,
FUNCT_2, GLIB_007;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1,
FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, RVSUM_1, FUNCT_7, ABIAN,
GLIB_000, FINSEQ_8, GRAPH_2, GRAPH_5, GLIB_001, GLIB_002, CHORD,
GLIB_006;
constructors DOMAIN_1, BINOP_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5,
ABIAN, WELLORD2, FUNCT_2, FIB_NUM2, FINSEQ_8, GLIB_001, GLIB_002,
RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2,
FUNCT_7, FINSEQ_1, SUBSET_1, GLIB_006;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN,
XREAL_0, NAT_1, GLIB_000, GLIB_001, GLIB_002, CHORD, INT_1, CARD_1,
FUNCT_2, PARTFUN1, RELSET_1, FUNCT_4, SUBSET_1, GLIB_006;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
theorems TARSKI, XBOOLE_0, XBOOLE_1, XXREAL_0, RELAT_1, XREGULAR, CARD_1,
CARD_2, FUNCT_2, FUNCOP_1, FUNCT_3, FUNCT_4, NAT_D, ZFMISC_1, FUNCT_1,
GLIB_000, GLIB_001, GLIB_002, CHORD, POLYFORM, NAT_1, XREAL_1, ABIAN,
FINSEQ_1, FINSEQ_3, INT_1, BINOP_1, WELLORD2, ENUMSET1, GLIB_006;
schemes FUNCT_2;
begin :: Reversing Edge Directions
reserve G, G2 for _Graph, V, E for set,
v for object;
definition
let G, E;
mode reverseEdgeDirections of G, E -> _Graph means
:Def1:
the_Vertices_of it = the_Vertices_of G &
the_Edges_of it = the_Edges_of G &
the_Source_of it = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of it = the_Target_of G +* ((the_Source_of G) | E)
if E c= the_Edges_of G
otherwise it == G;
existence
proof
hereby
assume E c= the_Edges_of G;
set V = the_Vertices_of G;
set E1 = the_Edges_of G;
set S = the_Source_of G +* ((the_Target_of G) | E);
reconsider S as Function of E1,V;
set T = the_Target_of G +* ((the_Source_of G) | E);
reconsider T as Function of E1,V;
set G1 = createGraph(V,E1,S,T);
take G1;
thus the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G &
the_Source_of G1 = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of G1 = the_Target_of G +* ((the_Source_of G) | E);
end;
assume not E c= the_Edges_of G;
take G;
thus thesis;
end;
consistency;
end;
definition
let G;
:: a.k.a. the transpose, converse or reverse of G
mode reverseEdgeDirections of G
is reverseEdgeDirections of G, the_Edges_of G;
end;
theorem
for G, E for G1, G2 being reverseEdgeDirections of G, E holds G1 == G2
proof
let G,E;
let G1,G2 be reverseEdgeDirections of G, E;
per cases;
suppose A1: E c= the_Edges_of G;
A2: the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G &
the_Source_of G1 = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of G1 = the_Target_of G +* ((the_Source_of G) | E) by A1, Def1;
the_Vertices_of G2 = the_Vertices_of G &
the_Edges_of G2 = the_Edges_of G &
the_Source_of G2 = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of G2 = the_Target_of G +* ((the_Source_of G) | E) by A1, Def1;
hence thesis by A2, GLIB_000:def 34;
end;
suppose not E c= the_Edges_of G;
then G1 == G & G2 == G by Def1;
hence thesis by GLIB_000:85;
end;
end;
theorem Th2:
for G, G2, E for G1 being reverseEdgeDirections of G, E
st G1 == G2 holds G2 is reverseEdgeDirections of G, E
proof
let G, G2, E;
let G1 be reverseEdgeDirections of G, E;
assume A1: G1 == G2;
per cases;
suppose A2: E c= the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G &
the_Source_of G1 = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of G1 = the_Target_of G +* ((the_Source_of G) | E) by Def1;
then the_Vertices_of G2 = the_Vertices_of G &
the_Edges_of G2 = the_Edges_of G &
the_Source_of G2 = the_Source_of G +* ((the_Target_of G) | E) &
the_Target_of G2 = the_Target_of G +* ((the_Source_of G) | E)
by A1, GLIB_000:def 34;
hence thesis by A2, Def1;
end;
suppose A3: not E c= the_Edges_of G;
then G == G1 by Def1;
then G == G2 by A1, GLIB_000:85;
hence thesis by A3, Def1;
end;
end;
theorem Th3:
for G2, E for G1 being reverseEdgeDirections of G2, E
holds G2 is reverseEdgeDirections of G1, E
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
per cases;
suppose A1: E c= the_Edges_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 +* ((the_Target_of G2) | E) &
the_Target_of G1 = the_Target_of G2 +* ((the_Source_of G2) | E) by Def1;
set S1 = the_Source_of G1;
set S2 = the_Source_of G2;
set T1 = the_Target_of G1;
set T2 = the_Target_of G2;
A3: dom S1 = the_Edges_of G1 & dom T1 = the_Edges_of G1 &
dom S2 = the_Edges_of G2 & dom T2 = the_Edges_of G2 by FUNCT_2:def 1;
A4: dom (S2|E) = E by A3, A1, RELAT_1:62;
A5: dom (T2|E) = E by A3, A1, RELAT_1:62;
A6: S2 = S2 +* (S2|E) by FUNCT_4:75
.= S2 +* (T2|E) +* (S2|E) by A4, A5, FUNCT_4:74
.= S1 +* (T1|E) by A2, A4;
T2 = T2 +* (T2|E) by FUNCT_4:75
.= T2 +* (S2|E) +* (T2|E) by A4, A5, FUNCT_4:74
.= T1 +* (S1|E) by A2, A5;
hence thesis by A1, A2, A6, Def1;
end;
suppose A7: not E c= the_Edges_of G2;
then A8: G1 == G2 by Def1;
then the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
hence thesis by A7, A8, Def1;
end;
end;
theorem Th4:
for G2, E for G1 being reverseEdgeDirections of G2, E
holds the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
per cases;
suppose E c= the_Edges_of G2;
hence thesis by Def1;
end;
suppose not E c= the_Edges_of G2;
then G1 == G2 by Def1;
hence thesis by GLIB_000:def 34;
end;
end;
theorem Th5:
for G2 for G1 being reverseEdgeDirections of G2
holds G2 is reverseEdgeDirections of G1
proof
let G2;
let G1 be reverseEdgeDirections of G2;
the_Edges_of G1 = the_Edges_of G2 by Th4;
hence thesis by Th3;
end;
theorem Th6:
for G2 being _trivial _Graph, E being set, G1 being _Graph
holds G1 == G2 iff G1 is reverseEdgeDirections of G2, E
proof
let G2 be _trivial _Graph, E be set, G1 be _Graph;
per cases;
suppose A1: E c= the_Edges_of G2;
consider v being Vertex of G2 such that
the_Vertices_of G2 = {v} and
A2: the_Source_of G2 = the_Edges_of G2 --> v &
the_Target_of G2 = the_Edges_of G2 --> v by GLIB_000:106;
A3: the_Source_of G2 +* ((the_Target_of G2)|E) = the_Edges_of G2 --> v
by A2, FUNCT_4:75;
hereby
assume G1 == G2;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by GLIB_000:def 34;
hence G1 is reverseEdgeDirections of G2, E by A1, A2, A3, Def1;
end;
assume G1 is reverseEdgeDirections of G2, E;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 +* ((the_Target_of G2)|E) &
the_Target_of G1 = the_Target_of G2 +* ((the_Source_of G2)|E)
by A1, Def1;
hence G1 == G2 by A2, A3, GLIB_000:def 34;
end;
suppose not E c= the_Edges_of G2;
hence thesis by Def1;
end;
end;
Lm1:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object
st E c= the_Edges_of G2 & e in E
holds (e DJoins v1,v2,G2 implies e DJoins v2,v1,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1,e,v2 be object;
assume A1: E c= the_Edges_of G2 & e in E;
set S1 = the_Source_of G1;
set T1 = the_Target_of G1;
set S2 = the_Source_of G2;
set T2 = the_Target_of G2;
assume e DJoins v1,v2,G2;
then A2: e in the_Edges_of G2 & S2.e = v1 & T2.e = v2 by GLIB_000:def 14;
E c= dom S2 & E c= dom T2 by A1, FUNCT_2:def 1;
then A3: e in dom(S2|E) & e in dom(T2|E) by A1, RELAT_1:62;
A4: S1.e = (S2+*(T2|E)).e by A1, Def1
.= (T2|E).e by A3, FUNCT_4:13
.= v2 by A2, A3, FUNCT_1:47;
A5: T1.e = (T2+*(S2|E)).e by A1, Def1
.= (S2|E).e by A3, FUNCT_4:13
.= v1 by A2, A3, FUNCT_1:47;
e in the_Edges_of G1 by A2, Th4;
hence thesis by A4, A5, GLIB_000:def 14;
end;
theorem Th7:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object
st E c= the_Edges_of G2 & e in E
holds (e DJoins v1,v2,G2 iff e DJoins v2,v1,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1,e,v2 be object;
assume A1: E c= the_Edges_of G2 & e in E;
hence e DJoins v1,v2,G2 implies e DJoins v2,v1,G1 by Lm1;
reconsider G3=G2 as reverseEdgeDirections of G1,E by Th3;
E c= the_Edges_of G1 by Th4, A1;
then e DJoins v2,v1,G1 implies e DJoins v1,v2,G3 by A1, Lm1;
hence thesis;
end;
Lm2:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object
st E c= the_Edges_of G2 & not e in E
holds (e DJoins v1,v2,G2 implies e DJoins v1,v2,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1,e,v2 be object;
assume A1: E c= the_Edges_of G2 & not e in E;
set S1 = the_Source_of G1;
set T1 = the_Target_of G1;
set S2 = the_Source_of G2;
set T2 = the_Target_of G2;
assume e DJoins v1,v2,G2;
then A2: e in the_Edges_of G2 & S2.e = v1 & T2.e = v2 by GLIB_000:def 14;
A3: not e in dom(S2|E) & not e in dom(T2|E) by A1;
A4: S1.e = (S2+*(T2|E)).e by A1, Def1
.= v1 by A2, A3, FUNCT_4:11;
A5: T1.e = (T2+*(S2|E)).e by A1, Def1
.= v2 by A2, A3, FUNCT_4:11;
e in the_Edges_of G1 by A2, Th4;
hence thesis by A4, A5, GLIB_000:def 14;
end;
theorem Th8:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object
st E c= the_Edges_of G2 & not e in E
holds (e DJoins v1,v2,G2 iff e DJoins v1,v2,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1,e,v2 be object;
assume A1: E c= the_Edges_of G2 & not e in E;
hence e DJoins v1,v2,G2 implies e DJoins v1,v2,G1 by Lm2;
reconsider G3=G2 as reverseEdgeDirections of G1,E by Th3;
E c= the_Edges_of G1 by Th4, A1;
then e DJoins v1,v2,G1 implies e DJoins v1,v2,G3 by A1, Lm2;
hence thesis;
end;
Lm3:
for G2, E for G1 being reverseEdgeDirections of G2, E st E c= the_Edges_of G2
for v1,e,v2 being object
holds (e Joins v1,v2,G2 implies e Joins v1,v2,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
assume A1: E c= the_Edges_of G2;
let v1,e,v2 be object;
assume A2: e Joins v1,v2,G2;
per cases;
suppose A3: e in E;
then A4: e in the_Edges_of G2 by A1;
then e in dom the_Source_of G2 & e in dom the_Target_of G2
by FUNCT_2:def 1;
then A5: e in dom ((the_Source_of G2) | E) &
e in dom ((the_Target_of G2) | E) by A3, RELAT_1:57;
A6: (the_Source_of G1).e
= (the_Source_of G2 +* ((the_Target_of G2) | E)).e by A1, Def1
.= ((the_Target_of G2) | E).e by A5, FUNCT_4:13
.= (the_Target_of G2).e by A3, FUNCT_1:49;
A7: (the_Target_of G1).e
= (the_Target_of G2 +* ((the_Source_of G2) | E)).e by A1, Def1
.= ((the_Source_of G2) | E).e by A5, FUNCT_4:13
.= (the_Source_of G2).e by A3, FUNCT_1:49;
A8: e in the_Edges_of G1 by A4, Th4;
per cases by A2, GLIB_000:def 13;
suppose (the_Source_of G2).e = v1 & (the_Target_of G2).e = v2;
hence e Joins v1,v2,G1 by A6, A7, A8, GLIB_000:def 13;
end;
suppose (the_Source_of G2).e = v2 & (the_Target_of G2).e = v1;
hence e Joins v1,v2,G1 by A6, A7, A8, GLIB_000:def 13;
end;
end;
suppose A9: not e in E;
then A10: not e in dom ((the_Target_of G2) | E);
A11: (the_Source_of G1).e
= (the_Source_of G2 +* ((the_Target_of G2) | E)).e by A1, Def1
.= (the_Source_of G2).e by A10, FUNCT_4:11;
A12: not e in dom ((the_Source_of G2) | E) by A9;
A13: (the_Target_of G1).e
= (the_Target_of G2 +* ((the_Source_of G2) | E)).e by A1, Def1
.= (the_Target_of G2).e by A12, FUNCT_4:11;
e in the_Edges_of G2 by A2, GLIB_000:def 13;
then A14: e in the_Edges_of G1 by Th4;
per cases by A2, GLIB_000:def 13;
suppose (the_Source_of G2).e = v1 & (the_Target_of G2).e = v2;
hence e Joins v1,v2,G1 by A11, A13, A14, GLIB_000:def 13;
end;
suppose (the_Source_of G2).e = v2 & (the_Target_of G2).e = v1;
hence e Joins v1,v2,G1 by A11, A13, A14, GLIB_000:def 13;
end;
end;
end;
theorem Th9:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object
holds (e Joins v1,v2,G2 iff e Joins v1,v2,G1)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
per cases;
suppose A1: E c= the_Edges_of G2;
let v1,e,v2 be object;
thus e Joins v1,v2,G2 implies e Joins v1,v2,G1 by A1, Lm3;
reconsider G3 = G2 as reverseEdgeDirections of G1, E by Th3;
assume A2: e Joins v1,v2,G1;
E c= the_Edges_of G1 by A1, Def1;
then e Joins v1,v2,G3 by A2, Lm3;
hence thesis;
end;
suppose not (E c= the_Edges_of G2);
then G1 == G2 by Def1;
hence thesis by GLIB_000:88;
end;
end;
theorem Th10:
for G2, E, v for G1 being reverseEdgeDirections of G2, E
holds v is Vertex of G1 iff v is Vertex of G2 by Th4;
theorem Th11:
for G2, E, V for G1 being reverseEdgeDirections of G2, E
holds G1.edgesBetween(V) = G2.edgesBetween(V)
proof
let G2, E, V;
let G1 be reverseEdgeDirections of G2, E;
for e being object holds e in G1.edgesBetween(V) iff e in G2.edgesBetween(V)
proof
let e be object;
set x1 = (the_Source_of G1).e, y1 = (the_Target_of G1).e;
set x2 = (the_Source_of G2).e, y2 = (the_Target_of G2).e;
hereby
assume A1: e in G1.edgesBetween(V);
then e Joins x1,y1,G1 by GLIB_000:def 13;
then e Joins x1,y1,G2 by Th9;
then e in the_Edges_of G2 & ((x1=x2 & y1=y2) or (x1=y2 & y1=x2))
by GLIB_000:def 13;
then e in the_Edges_of G2 & x2 in V & y2 in V by A1, GLIB_000:31;
hence e in G2.edgesBetween(V) by GLIB_000:31;
end;
assume A2: e in G2.edgesBetween(V);
then e Joins x2,y2,G2 by GLIB_000:def 13;
then e Joins x2,y2,G1 by Th9;
then e in the_Edges_of G1 & ((x1=x2 & y1=y2) or (x1=y2 & y1=x2))
by GLIB_000:def 13;
then e in the_Edges_of G1 & x1 in V & y1 in V by A2, GLIB_000:31;
hence e in G1.edgesBetween(V) by GLIB_000:31;
end;
hence thesis by TARSKI:2;
end;
theorem Th12:
for G2, E, V for G1 being reverseEdgeDirections of G2, E
holds G1.edgesInOut(V) = G2.edgesInOut(V)
proof
let G2, E, V;
let G1 be reverseEdgeDirections of G2, E;
for e being object holds e in G1.edgesInOut(V) iff e in G2.edgesInOut(V)
proof
let e be object;
set x1 = (the_Source_of G1).e, y1 = (the_Target_of G1).e;
set x2 = (the_Source_of G2).e, y2 = (the_Target_of G2).e;
hereby
assume A1: e in G1.edgesInOut(V);
then e Joins x1,y1,G1 by GLIB_000:def 13;
then e Joins x1,y1,G2 by Th9;
then e in the_Edges_of G2 & ((x1=x2 & y1=y2) or (x1=y2 & y1=x2))
by GLIB_000:def 13;
then e in the_Edges_of G2 & (x2 in V or y2 in V) by A1, GLIB_000:28;
hence e in G2.edgesInOut(V) by GLIB_000:28;
end;
assume A2: e in G2.edgesInOut(V);
then e Joins x2,y2,G2 by GLIB_000:def 13;
then e Joins x2,y2,G1 by Th9;
then e in the_Edges_of G1 & ((x1=x2 & y1=y2) or (x1=y2 & y1=x2))
by GLIB_000:def 13;
then e in the_Edges_of G1 & (x1 in V or y1 in V) by A2, GLIB_000:28;
hence e in G1.edgesInOut(V) by GLIB_000:28;
end;
hence thesis by TARSKI:2;
end;
theorem Th13:
for G2, E, V for G1 being reverseEdgeDirections of G2, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v1.edgesInOut() = v2.edgesInOut()
proof
let G2, E, V;
let G1 be reverseEdgeDirections of G2, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
thus v1.edgesInOut() = G1.edgesInOut( {v1} ) by GLIB_000:def 40
.= G2.edgesInOut( {v2} ) by A1, Th12
.= v2.edgesInOut() by GLIB_000:def 40;
end;
theorem Th14:
for G2, E for G1 being reverseEdgeDirections of G2, E, W2 being Walk of G2
holds W2 is Walk of G1
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let W2 be Walk of G2;
per cases;
suppose E c= the_Edges_of G2;
W2 is FinSequence of the_Vertices_of G1 \/ the_Edges_of G2 by Th4;
then A1: W2 is FinSequence of the_Vertices_of G1 \/ the_Edges_of G1
by Th4;
W2.1 in the_Vertices_of G2 by GLIB_001:def 3;
then A2: W2.1 in the_Vertices_of G1 by Th4;
for n being odd Element of NAT st n < len W2 holds
W2.(n+1) Joins W2.n, W2.(n+2), G1 by Th9, GLIB_001:def 3;
hence thesis by A1, A2, GLIB_001:def 3;
end;
suppose not (E c= the_Edges_of G2);
then G1 == G2 by Def1;
hence thesis by GLIB_001:179;
end;
end;
theorem Th15:
for G2, E for G1 being reverseEdgeDirections of G2, E, W1 being Walk of G1
holds W1 is Walk of G2
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let W1 be Walk of G1;
reconsider G3 = G2 as reverseEdgeDirections of G1, E by Th3;
W1 is Walk of G3 by Th14;
hence thesis;
end;
theorem Th16:
for G2, E for G1 being reverseEdgeDirections of G2, E
for W2 being Walk of G2, W1 being Walk of G1
st E c= the_Edges_of G2 & W1 = W2 & W2.edges() c= E
holds (W1 is directed iff W2.reverse() is directed)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let W2 be Walk of G2, W1 be Walk of G1;
assume that
A1: E c= the_Edges_of G2 and
A2: W1 = W2 and
A3: W2.edges() c= E;
A4: for n being odd Element of NAT st n < len W2 holds W2.(n+1) in E
by A3, GLIB_001:100, TARSKI:def 3;
hereby
assume W1 is directed;
then A5: for m being odd Element of NAT st m < len W1
holds W1.(m+1) DJoins W1.m, W1.(m+2), G1 by GLIB_001:122;
for n being odd Element of NAT st n < len W2.reverse()
holds W2.reverse().(n+1) DJoins W2.reverse().n, W2.reverse().(n+2), G2
proof
let n be odd Element of NAT;
assume A6: n < len W2.reverse();
A7: n+2 <= len W2.reverse() by A6, GLIB_001:1;
A8: 1 <= n by ABIAN:12;
A10: 1+0 <= n+1+1 by XREAL_1:6;
A11: n+1 <= len W2.reverse() by A6, NAT_1:13;
(n+2)-(n+1) <= len W2.reverse() - (n+1) by A7, XREAL_1:9;
then (n+2)-(n+1) <= len W2 - (n+1) by GLIB_001:21;
then reconsider m = len W2 - n - 1 as Element of NAT by INT_1:3;
reconsider m as odd Element of NAT;
n in dom W2.reverse() & n+1 in dom W2.reverse() &
n+2 in dom W2.reverse() by A6,A7,A8,XREAL_1:6,A10,A11,FINSEQ_3:25;
then a12: W2.reverse().n = W2.(len W2-n+1) & len W2-n+1 in dom W2 &
W2.reverse().(n+1) = W2.(len W2-(n+1)+1) &
W2.reverse().(n+2) = W2.(len W2-(n+2)+1) by GLIB_001:25;
then m+2 <= len W1 by FINSEQ_3:25,A2;
then A13: m < len W1 by GLIB_001:1;
then A14: W1.(m+1) in E by A2, A4;
W1.(m+1) DJoins W1.m, W1.(m+2), G1 by A5, A13;
hence thesis by A1, A2, a12, A14, Th7;
end;
hence W2.reverse() is directed by GLIB_001:122;
end;
assume W2.reverse() is directed;
then A15: for m being odd Element of NAT st m < len W2.reverse()
holds W2.reverse().(m+1) DJoins W2.reverse().m, W2.reverse().(m+2), G2
by GLIB_001:122;
for n being odd Element of NAT st n < len W1
holds W1.(n+1) DJoins W1.n, W1.(n+2), G1
proof
let n be odd Element of NAT;
assume A16: n < len W1;
then A17: n < len W2 by A2;
A18: n+2 <= len W2 by A16,A2, GLIB_001:1;
A19: 1 <= n by ABIAN:12;
A21: 1+0 <= n+1+1 by XREAL_1:6;
A22: n+1 <= len W2 by NAT_1:13,A2, A16;
(n+2)-(n+1) <= len W2 - (n+1) by A18, XREAL_1:9;
then reconsider m = len W2 - n - 1 as Element of NAT by INT_1:3;
reconsider m as odd Element of NAT;
n in dom W2 & n+1 in dom W2 &
n+2 in dom W2 by A2,A16,A18,A19,XREAL_1:6,A21,A22,FINSEQ_3:25; then
a23: W2.n = W2.reverse().(len W2-n+1) & len W2-n+1 in dom W2.reverse() &
W2.(n+1) = W2.reverse().(len W2-(n+1)+1) &
W2.(n+2) = W2.reverse().(len W2-(n+2)+1) by GLIB_001:24;
then A23: W1.n = W2.reverse().(m+2) & m+2 in dom W2.reverse() &
W1.(n+1) = W2.reverse().(m+1) &
W1.(n+2) = W2.reverse().m by A2;
m+2 <= len W2.reverse() by a23, FINSEQ_3:25;
then A24: m < len W2.reverse() by GLIB_001:1;
A25: W1.(n+1) in E by A17, A2, A4;
W1.(n+1) DJoins W1.(n+2), W1.n, G2 by A23, A15,A24;
hence W1.(n+1) DJoins W1.n, W1.(n+2), G1 by A1, A25, Th7;
end;
hence thesis by GLIB_001:122;
end;
theorem
for G2 for G1 being reverseEdgeDirections of G2
for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2
holds (W1 is directed iff W2.reverse() is directed)
proof
let G2;
let G1 be reverseEdgeDirections of G2;
let W2 be Walk of G2, W1 be Walk of G1;
assume A1: W1 = W2;
W2.edges() c= the_Edges_of G2;
hence thesis by A1, Th16;
end;
Lm4:
for G2, E for G1 being reverseEdgeDirections of G2, E
for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2
holds (W1 is chordal implies W2 is chordal)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let W2 be Walk of G2, W1 be Walk of G1;
assume A1: W1 = W2;
assume W1 is chordal;
then consider m, n being odd Nat such that
A2: m+2 < n & n <= len W1 & W1.m <> W1.n and
A3: ex e being object st e Joins W1.m,W1.n,G1 and
A4: for f being object st f in W1.edges() holds not f Joins W1.m,W1.n,G1
by CHORD:def 10;
ex k, l being odd Nat st k+2 < l & l <= len W2 & W2.k <> W2.l &
(ex e being object st e Joins W2.k,W2.l,G2) &
for f being object st f in W2.edges() holds not f Joins W2.k,W2.l,G2
proof
take m, n;
thus m+2 < n & n <= len W2 & W2.m <> W2.n by A1, A2;
thus ex e being object st e Joins W2.m,W2.n,G2 by A1, A3, Th9;
let f be object;
assume f in W2.edges();
then f in W1.edges() by A1, GLIB_001:110;
hence not f Joins W2.m,W2.n,G2 by A1, Th9, A4;
end;
hence thesis by CHORD:def 10;
end;
theorem Th18:
for G2, E for G1 being reverseEdgeDirections of G2, E
for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2
holds (W1 is chordal iff W2 is chordal)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let W2 be Walk of G2, W1 be Walk of G1;
assume A1: W1 = W2;
hence W1 is chordal implies W2 is chordal by Lm4;
assume A2: W2 is chordal;
reconsider G3 = G2 as reverseEdgeDirections of G1, E by Th3;
reconsider W3 = W2 as Walk of G3;
W3 is chordal by A2;
hence W1 is chordal by A1, Lm4;
end;
theorem Th19:
for G2, E for G1 being reverseEdgeDirections of G2, E, v1, v2 being object
holds (ex W1 being Walk of G1 st W1 is_Walk_from v1,v2) iff
(ex W2 being Walk of G2 st W2 is_Walk_from v1,v2)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1, v2 be object;
hereby
given W1 being Walk of G1 such that
A1: W1 is_Walk_from v1,v2;
reconsider W2=W1 as Walk of G2 by Th15;
take W2;
thus W2 is_Walk_from v1,v2 by A1, GLIB_001:19;
end;
given W2 being Walk of G2 such that
A2: W2 is_Walk_from v1,v2;
reconsider W1=W2 as Walk of G1 by Th14;
take W1;
thus thesis by A2, GLIB_001:19;
end;
theorem Th20:
for G2, E for G1 being reverseEdgeDirections of G2, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
for v being object holds
v in G1.reachableFrom(v1) iff v in G2.reachableFrom(v2)
proof
let v be object;
hereby
assume v in G1.reachableFrom(v1);
then ex W being Walk of G1 st W is_Walk_from v1,v by GLIB_002:def 5;
then ex W being Walk of G2 st W is_Walk_from v2,v by A1, Th19;
hence v in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
assume v in G2.reachableFrom(v2);
then ex W being Walk of G2 st W is_Walk_from v2,v by GLIB_002:def 5;
then ex W being Walk of G1 st W is_Walk_from v1,v by A1, Th19;
hence v in G1.reachableFrom(v1) by GLIB_002:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th21:
for G2, E for G1 being reverseEdgeDirections of G2, E
holds G1.componentSet() = G2.componentSet() &
G1.numComponents() = G2.numComponents()
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
for V being object holds V in G1.componentSet() iff V in G2.componentSet()
proof
let V be object;
hereby
assume V in G1.componentSet();
then consider v being Vertex of G1 such that
A1: V = G1.reachableFrom(v) by GLIB_002:def 8;
reconsider w = v as Vertex of G2 by Th10;
V = G2.reachableFrom(w) by A1, Th20;
hence V in G2.componentSet() by GLIB_002:def 8;
end;
assume V in G2.componentSet();
then consider v being Vertex of G2 such that
A2: V = G2.reachableFrom(v) by GLIB_002:def 8;
reconsider w = v as Vertex of G1 by Th10;
V = G1.reachableFrom(w) by A2, Th20;
hence V in G1.componentSet() by GLIB_002:def 8;
end;
hence A3: G1.componentSet() = G2.componentSet() by TARSKI:2;
thus G1.numComponents() = card G2.componentSet() by A3, GLIB_002:def 9
.= G2.numComponents() by GLIB_002:def 9;
end;
registration
let G be _trivial _Graph, E be set;
cluster -> _trivial for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
A1: the_Vertices_of G1 = the_Vertices_of G by Th4;
card the_Vertices_of G = 1 by GLIB_000:def 19;
hence thesis by A1, GLIB_000:def 19;
end;
end;
registration
let G be non _trivial _Graph, E be set;
cluster -> non _trivial for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is _trivial;
then G2 is _trivial;
hence contradiction;
end;
end;
:: More theorems of this kind can be produced with other
:: subgraph modes. This particular example was needed
:: to show that the cut-vertex property prevails in graphs
:: with (partially) reversed edge directions
theorem Th22:
for G2, E for G1 being reverseEdgeDirections of G2, E, v being set
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is reverseEdgeDirections of G3, E \ G1.edgesInOut({v})
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v be set;
let G3 be removeVertex of G1,v, G4 be removeVertex of G2,v;
per cases;
suppose A1: E c= the_Edges_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 +* ((the_Target_of G2) | E) &
the_Target_of G1 = the_Target_of G2 +* ((the_Source_of G2) | E) by Def1;
then
A4: G1.edgesBetween(the_Vertices_of G1 \ {v})
= G2.edgesBetween(the_Vertices_of G2 \ {v}) by Th11;
per cases;
suppose A5: not v in the_Vertices_of G2;
then the_Vertices_of G1 \ {v} = the_Vertices_of G1 &
the_Vertices_of G2 \ {v} = the_Vertices_of G2 by A2, ZFMISC_1:57;
then A6: G1 == G3 & G2 == G4 by GLIB_000:94;
{v} /\ the_Vertices_of G1 = {} by XBOOLE_0:def 7,A2,A5, ZFMISC_1:50;
then a7: G1.edgesInOut({v}) = {} by GLIB_000:103;
G3 is reverseEdgeDirections of G2,E by A6, Th2;
then G2 is reverseEdgeDirections of G3,E by Th3;
hence thesis by A6, a7, Th2;
end;
suppose A8: v in the_Vertices_of G2;
then A9: v in the_Vertices_of G1 by A2;
per cases;
suppose A10: G2 is non _trivial;
then A11: the_Vertices_of G4 = the_Vertices_of G2 \ {v} &
the_Edges_of G4 = G2.edgesBetween(the_Vertices_of G2 \ {v})
by A8, GLIB_000:47;
A12: the_Vertices_of G3 = the_Vertices_of G1 \ {v} &
the_Edges_of G3 = G1.edgesBetween(the_Vertices_of G1 \ {v})
by A2, A8, GLIB_000:47, A10;
then A13: the_Vertices_of G4 = the_Vertices_of G3 &
the_Edges_of G4 = the_Edges_of G3 by A11, A2, A4;
A14: dom the_Source_of G4 = the_Edges_of G4 &
dom the_Target_of G4 = the_Edges_of G4 by GLIB_000:4;
for e being object holds
e in E \ G1.edgesInOut({v}) implies e in the_Edges_of G3
proof
let e be object;
assume e in E \ G1.edgesInOut({v});
then A15: e in E & not e in G1.edgesInOut({v}) by XBOOLE_0:def 5;
then A16: e in the_Edges_of G1 by A1, A2;
A17: not (the_Source_of G1).e in {v} &
not (the_Target_of G1).e in {v} by A15, A1,A2, GLIB_000:28;
e Joins (the_Source_of G1).e, (the_Target_of G1).e, G1
by A1, A2, A15, GLIB_000:def 13;
then (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} &
(the_Target_of G1).e in the_Vertices_of G1 \ {v}
by A17, XBOOLE_0:def 5;
hence thesis by A12,A16,GLIB_000:31;
end;
then A18: E \ G1.edgesInOut({v}) c= the_Edges_of G3 by TARSKI:def 3;
A19: for e being object holds
e in the_Edges_of G4 implies not e in G1.edgesInOut({v})
proof
let e be object;
assume e in the_Edges_of G4;
then A20: e in the_Edges_of G3 by A13;
assume e in G1.edgesInOut({v});
then e in the_Edges_of G1 & (
(the_Source_of G1).e in {v} or
(the_Target_of G1).e in {v}) by GLIB_000:28;
then A21: (the_Source_of G3).e in {v} or (the_Target_of G3).e in {v}
by A20, GLIB_000:def 32;
e Joins (the_Source_of G3).e,(the_Target_of G3).e, G3
by A20, GLIB_000:def 13;
then (the_Source_of G3).e in the_Vertices_of G3
& (the_Target_of G3).e in the_Vertices_of G3 by GLIB_000:13;
hence contradiction by A21, A12, XBOOLE_0:def 5;
end;
set S = the_Source_of G3 +*
((the_Target_of G3) | (E \ G1.edgesInOut({v})));
A22: dom ((the_Target_of G3) | (E\G1.edgesInOut({v})))
= (dom the_Target_of G3 /\ (E \ G1.edgesInOut({v}))) by RELAT_1:61
.= (the_Edges_of G3 /\ (E \ G1.edgesInOut({v}))) by GLIB_000:4;
A23: dom S = dom the_Source_of G3 \/
dom ((the_Target_of G3) | (E\G1.edgesInOut({v}))) by FUNCT_4:def 1
.= the_Edges_of G3 \/
dom ((the_Target_of G3) | (E \ G1.edgesInOut({v}))) by GLIB_000:4
.= dom the_Source_of G4 by A13, A14, A22, XBOOLE_1:22;
set T = the_Target_of G3 +*
((the_Source_of G3) | (E \ G1.edgesInOut({v})));
A24: dom ((the_Source_of G3) | (E \ G1.edgesInOut({v})))
= (dom the_Source_of G3 /\ (E \ G1.edgesInOut({v}))) by RELAT_1:61
.= (the_Edges_of G3 /\ (E \ G1.edgesInOut({v}))) by GLIB_000:4;
A25: dom T = dom the_Target_of G3 \/
dom ((the_Source_of G3) | (E\G1.edgesInOut({v}))) by FUNCT_4:def 1
.= the_Edges_of G3 \/
dom ((the_Source_of G3) | (E \ G1.edgesInOut({v}))) by GLIB_000:4
.= dom the_Target_of G4 by A13, A14, A24, XBOOLE_1:22;
for e being object st e in dom the_Source_of G4 holds
(the_Source_of G4).e = S.e
proof
let e be object;
assume e in dom the_Source_of G4;
then A26: e in the_Edges_of G4;
per cases;
suppose A27: e in E \ G1.edgesInOut({v});
then A28: e in E;
A29: e in the_Edges_of G3 by A27, A18;
A30: e in dom ((the_Target_of G3) | (E\G1.edgesInOut({v})))
by A27, A18, A22, XBOOLE_0:def 4;
e in the_Edges_of G2 by A26;
then e in dom the_Source_of G2 by GLIB_000:4;
then e in (dom the_Source_of G2) /\ E by A28, XBOOLE_0:def 4;
then A31: e in dom ((the_Source_of G2)|E) by RELAT_1:61;
thus S.e = ((the_Target_of G3) | (E\G1.edgesInOut({v}))).e
by A30, FUNCT_4:13
.= (the_Target_of G3).e by A27, FUNCT_1:49
.= (the_Target_of G1).e by A29, GLIB_000:def 32
.= ((the_Source_of G2)|E).e by A2, A31, FUNCT_4:13
.= (the_Source_of G2).e by A28, FUNCT_1:49
.= (the_Source_of G4).e by A26, GLIB_000:def 32;
end;
suppose A32: not e in E \ G1.edgesInOut({v});
not e in G1.edgesInOut({v}) by A26, A19;
then A33: not e in dom ((the_Target_of G2)|E)
by A32, XBOOLE_0:def 5;
A34: not e in dom ((the_Target_of G3)|(E\G1.edgesInOut({v})))
by A32;
thus S.e = (the_Source_of G3).e by A34, FUNCT_4:11
.= (the_Source_of G1).e by A13, A26, GLIB_000:def 32
.= (the_Source_of G2).e by A2, A33, FUNCT_4:11
.= (the_Source_of G4).e by A26, GLIB_000:def 32;
end;
end;
then A35: the_Source_of G4 = S by A23, FUNCT_1:2;
:: Proof is analog
for e being object st e in dom the_Target_of G4 holds
(the_Target_of G4).e = T.e
proof
let e be object;
assume e in dom the_Target_of G4;
then A36: e in the_Edges_of G4;
per cases;
suppose A37: e in E \ G1.edgesInOut({v});
then A38: e in E;
A39: e in the_Edges_of G3 by A37, A18;
A40: e in dom ((the_Source_of G3) | (E\G1.edgesInOut({v})))
by A37, A18, A24, XBOOLE_0:def 4;
e in the_Edges_of G2 by A36;
then e in dom the_Target_of G2 by GLIB_000:4;
then e in (dom the_Target_of G2) /\ E by A38, XBOOLE_0:def 4;
then A41: e in dom ((the_Target_of G2)|E) by RELAT_1:61;
thus T.e = ((the_Source_of G3) | (E\G1.edgesInOut({v}))).e
by A40, FUNCT_4:13
.= (the_Source_of G3).e by A37, FUNCT_1:49
.= (the_Source_of G1).e by A39, GLIB_000:def 32
.= ((the_Target_of G2)|E).e by A2, A41, FUNCT_4:13
.= (the_Target_of G2).e by A38, FUNCT_1:49
.= (the_Target_of G4).e by A36, GLIB_000:def 32;
end;
suppose A42: not e in E \ G1.edgesInOut({v});
not e in G1.edgesInOut({v}) by A36, A19;
then A43: not e in dom ((the_Source_of G2)|E)
by A42, XBOOLE_0:def 5;
not e in dom ((the_Source_of G3)|(E\G1.edgesInOut({v})))
by A42;
hence T.e = (the_Target_of G3).e by FUNCT_4:11
.= (the_Target_of G1).e by A13, A36, GLIB_000:def 32
.= (the_Target_of G2).e by A2, A43, FUNCT_4:11
.= (the_Target_of G4).e by A36, GLIB_000:def 32;
end;
end;
then the_Target_of G4 = T by A25, FUNCT_1:2;
hence thesis by A13, A18, A35, Def1;
end;
suppose A45: G2 is _trivial; then
consider v1 being Vertex of G1 such that
A47: the_Vertices_of G1 = {v1} by GLIB_000:22;
v = v1 by A9, A47, TARSKI:def 1;
then the_Vertices_of G1 \ {v} is empty &
the_Vertices_of G2 \ {v} is empty by XBOOLE_1:37,A2,A47;
then A48: G1 == G3 & G2 == G4 by GLIB_000:def 37;
G3 is reverseEdgeDirections of G2,E by A48, Th2;
then G3 == G2 by A45, Th6;
hence thesis by Th6, A45,A48, GLIB_000:85;
end;
end;
end;
suppose A50: not E c= the_Edges_of G2;
then A51: G1 == G2 by Def1;
then A52: the_Vertices_of G1 \ {v} = the_Vertices_of G2 \ {v}
by GLIB_000:def 34;
then A53: G1.edgesBetween(the_Vertices_of G1 \ {v})
= G2.edgesBetween(the_Vertices_of G2 \ {v}) by A51, GLIB_000:90;
A54: not E \ G1.edgesInOut({v}) c= the_Edges_of G3
proof
assume E \ G1.edgesInOut({v}) c= the_Edges_of G3;
then E \ G1.edgesInOut({v}) c= the_Edges_of G1 by XBOOLE_1:1;
then (E \ G1.edgesInOut({v})) \/ G1.edgesInOut({v}) c= the_Edges_of G1
by XBOOLE_1:8;
then A55: E \/ G1.edgesInOut({v}) c= the_Edges_of G1 by XBOOLE_1:39;
not E c= the_Edges_of G1 by A50, A51, GLIB_000:def 34;
hence contradiction by A55, XBOOLE_1:11;
end;
G4 is removeVertex of G1,v by A51, A52, A53, GLIB_000:95;
then G3 == G4 by GLIB_000:93;
hence thesis by A54, Def1;
end;
end;
Lm5:
for G2, E for G1 being reverseEdgeDirections of G2, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds (v1 is isolated implies v2 is isolated) &
(v1 is endvertex implies v2 is endvertex) &
(v1 is cut-vertex implies v2 is cut-vertex)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
hereby
assume v1 is isolated;
then v1.edgesInOut() = {} by GLIB_000:def 49;
then v2.edgesInOut() = {} by A1, Th13;
hence v2 is isolated by GLIB_000:def 49;
end;
hereby
assume v1 is endvertex;
then consider e being object such that
A2: v1.edgesInOut() = {e} & not e Joins v1,v1,G1 by GLIB_000:def 51;
A3: not e Joins v2,v2,G2 by A1, A2, Th9;
v2.edgesInOut() = {e} by A1, A2, Th13;
hence v2 is endvertex by A3, GLIB_000:def 51;
end;
assume A4: v1 is cut-vertex;
for G4 being removeVertex of G2, v2 holds
G2.numComponents() in G4.numComponents()
proof
let G4 be removeVertex of G2, v2;
set G3 = the removeVertex of G1, v1;
G4 is reverseEdgeDirections of G3, E \ G1.edgesInOut({v2}) by A1, Th22;
then A5: G4.numComponents() = G3.numComponents() by Th21;
G1.numComponents() in G3.numComponents() by A4, GLIB_002:def 10;
hence thesis by A5, Th21;
end;
hence v2 is cut-vertex by GLIB_002:def 10;
end;
theorem
for G2, E for G1 being reverseEdgeDirections of G2, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds (v1 is isolated iff v2 is isolated) &
(v1 is endvertex iff v2 is endvertex) &
(v1 is cut-vertex iff v2 is cut-vertex)
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
G2 is reverseEdgeDirections of G1, E by Th3;
hence thesis by A1, Lm5;
end;
theorem
for G2, E for G1 being reverseEdgeDirections of G2, E
holds G1.order() = G2.order() & G1.size() = G2.size()
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
A1: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by Th4;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= G2.order() by A1, GLIB_000:def 24;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= G2.size() by A1, GLIB_000:def 25;
end;
theorem Th25:
for G2, E for G1 being reverseEdgeDirections of G2, E
st E c= the_Edges_of G2 & G2 is non-Dmulti &
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2
holds (e1 in E & e2 in E) or (not e1 in E & not e2 in E)
holds G1 is non-Dmulti
proof
let G2, E;
let G1 be reverseEdgeDirections of G2, E;
assume that
A1: E c= the_Edges_of G2 and
A2: G2 is non-Dmulti and
A3: for e1,e2,v1,v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2
holds (e1 in E & e2 in E) or (not e1 in E & not e2 in E);
for e1,e2,v1,v2 being object holds e1 DJoins
v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume A4: e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1;
then e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 by GLIB_000:16;
then e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 by Th9;
then per cases by A3;
suppose e1 in E & e2 in E;
then e1 DJoins v2,v1,G2 & e2 DJoins v2,v1,G2 by A1, A4, Th7;
hence thesis by A2, GLIB_000:def 21;
end;
suppose (not e1 in E & not e2 in E);
then e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 by A1, A4, Th8;
hence thesis by A2, GLIB_000:def 21;
end;
end;
hence thesis by GLIB_000:def 21;
end;
registration
let G be non-Dmulti _Graph;
cluster -> non-Dmulti for reverseEdgeDirections of G;
coherence
proof
let G1 be reverseEdgeDirections of G;
set E = the_Edges_of G;
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G
holds (e1 in E & e2 in E) or (not e1 in E & not e2 in E)
by GLIB_000:def 13;
hence thesis by Th25;
end;
end;
registration
let G be non non-Dmulti _Graph;
cluster -> non non-Dmulti for reverseEdgeDirections of G;
coherence
proof
let G1 be reverseEdgeDirections of G;
reconsider G2 = G as reverseEdgeDirections of G1 by Th5;
assume G1 is non-Dmulti;
then G2 is non-Dmulti;
hence contradiction;
end;
end;
registration
let G be non-multi _Graph, E be set;
cluster -> non-multi for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
for e1,e2,v1,v2 being object holds e1 Joins
v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G by Th9;
hence thesis by GLIB_000:def 20;
end;
hence thesis by GLIB_000:def 20;
end;
end;
registration
let G be non non-multi _Graph, E be set;
cluster -> non non-multi for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is non-multi;
then G2 is non-multi;
hence contradiction;
end;
end;
registration
let G be loopless _Graph, E be set;
cluster -> loopless for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
for v being object holds not ex e being object st e Joins v,v,G1
by Th9, GLIB_000:18;
hence thesis by GLIB_000:18;
end;
end;
registration
let G be non loopless _Graph, E be set;
cluster -> non loopless for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is loopless;
then G2 is loopless;
hence contradiction;
end;
end;
registration
let G be connected _Graph, E be set;
cluster -> connected for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
for v1,v2 being Vertex of G1 holds
ex W1 being Walk of G1 st W1 is_Walk_from v1,v2
proof
let v1,v2 be Vertex of G1;
reconsider w1=v1,w2=v2 as Vertex of G by Th10;
ex W being Walk of G st W is_Walk_from w1,w2 by GLIB_002:def 1;
hence thesis by Th19;
end;
hence thesis by GLIB_002:def 1;
end;
end;
registration
let G be non connected _Graph, E be set;
cluster -> non connected for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is connected;
then G2 is connected;
hence contradiction;
end;
end;
registration
let G be acyclic _Graph, E be set;
cluster -> acyclic for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
not ex W1 being Walk of G1 st W1 is Cycle-like
proof
given W1 being Walk of G1 such that
A1: W1 is Cycle-like;
reconsider W=W1 as Walk of G by Th15;
W is Cycle-like by A1, GLIB_006:24;
hence contradiction by GLIB_002:def 2;
end;
hence thesis by GLIB_002:def 2;
end;
end;
registration
let G be non acyclic _Graph, E be set;
cluster -> non acyclic for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is acyclic;
then G2 is acyclic;
hence contradiction;
end;
end;
registration
let G be complete _Graph, E be set;
cluster -> complete for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
for v1,v2 being Vertex of G1 st v1 <> v2 holds v1,v2 are_adjacent
proof
let v1,v2 be Vertex of G1;
assume A1: v1 <> v2;
reconsider u1=v1, u2=v2 as Vertex of G by Th10;
consider e being object such that
A2: e Joins u1,u2,G by A1, CHORD:def 6, CHORD:def 3;
thus thesis by CHORD:def 3, A2, Th9;
end;
hence thesis by CHORD:def 6;
end;
end;
registration
let G be non complete _Graph, E be set;
cluster -> non complete for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is complete;
then G2 is complete;
hence contradiction;
end;
end;
registration
let G be chordal _Graph, E be set;
cluster -> chordal for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
for W1 being Walk of G1 st W1.length() > 3 & W1 is Cycle-like
holds W1 is chordal
proof
let W1 be Walk of G1;
reconsider W=W1 as Walk of G by Th15;
assume W1.length() > 3 & W1 is Cycle-like;
then W.length() > 3 & W is Cycle-like by GLIB_006:24, GLIB_001:114;
then W is chordal by CHORD:def 11;
hence thesis by Th18;
end;
hence thesis by CHORD:def 11;
end;
end;
:: "non"-version of this cluster has to wait
:: because non chordal existence will be proven with cycle graphs
registration
let G be _finite _Graph, E be set;
cluster -> _finite for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G by Th4;
hence thesis by GLIB_000:def 17;
end;
end;
registration
let G be non _finite _Graph, E be set;
cluster -> non _finite for reverseEdgeDirections of G, E;
coherence
proof
let G1 be reverseEdgeDirections of G, E;
reconsider G2 = G as reverseEdgeDirections of G1, E by Th3;
assume G1 is _finite;
then G2 is _finite;
hence contradiction;
end;
end;
theorem Th26:
for G2 for G1 being reverseEdgeDirections of G2
holds the_Source_of G1 = the_Target_of G2 &
the_Target_of G1 = the_Source_of G2
proof
let G2;
let G1 be reverseEdgeDirections of G2;
A1: dom the_Target_of G2 = the_Edges_of G2 &
dom the_Source_of G2 = the_Edges_of G2 by FUNCT_2:def 1;
thus the_Source_of G1 = the_Source_of G2 +* (
(the_Target_of G2) | the_Edges_of G2) by Def1
.= the_Target_of G2 by A1, FUNCT_4:19;
thus the_Target_of G1 = the_Target_of G2 +* (
(the_Source_of G2) | the_Edges_of G2) by Def1
.= the_Source_of G2 by A1, FUNCT_4:19;
end;
theorem
for G2 for G1 being reverseEdgeDirections of G2
for v1,e,v2 being object
holds (e DJoins v1,v2,G2 iff e DJoins v2,v1,G1)
proof
let G2;
let G1 be reverseEdgeDirections of G2;
let v1,e,v2 be object;
hereby
assume e DJoins v1,v2,G2;
then e in the_Edges_of G2 & (the_Source_of G2).e = v1 &
(the_Target_of G2).e = v2 by GLIB_000:def 14;
then e in the_Edges_of G1 & (the_Target_of G1).e = v1 &
(the_Source_of G1).e = v2 by Th26,Def1;
hence e DJoins v2,v1,G1 by GLIB_000:def 14;
end;
assume e DJoins v2,v1,G1;
then e in the_Edges_of G1 & (the_Source_of G1).e = v2 &
(the_Target_of G1).e = v1 by GLIB_000:def 14;
then e in the_Edges_of G2 & (the_Target_of G2).e = v2 &
(the_Source_of G2).e = v1 by Th26,Def1;
hence e DJoins v1,v2,G2 by GLIB_000:def 14;
end;
begin :: Adding a Vertex and several Edges to a Graph
Lm6:
for X, Y being set holds X /\ (Y --> X) = {}
proof
let X, Y be set;
assume X /\ (Y --> X) <> {};
then consider Z being object such that
A1: Z in X /\ (Y --> X) by XBOOLE_0:def 1;
reconsider Z as set by TARSKI:1;
consider y, x being object such that
A2: y in Y & x in {X} & Z = [y,x] by ZFMISC_1:def 2, A1;
x = X by A2, TARSKI:def 1;
then Z = { {y,X}, {y} } by A2,TARSKI:def 5;
then A3: {y, X} in Z by TARSKI:def 2;
X in {y,X} & Z in X by A1, XBOOLE_0:def 4, TARSKI:def 2;
hence contradiction by A3, XREGULAR:7;
end;
Lm7:
for X,Y being set, x being object st X /\ Y = {} & x in X holds not x in Y
by XBOOLE_0:def 4;
:: we need a lot of edges, so we take the freedom
:: to specify them within the definition
definition
let G, v, V;
mode addAdjVertexToAll of G,v,V -> Supergraph of G means :Def2:
the_Vertices_of it = the_Vertices_of G \/ {v} &
the_Edges_of it = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of it = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of it = the_Target_of G +* pr1(V,{the_Edges_of G})
if V c= the_Vertices_of G & not v in the_Vertices_of G
otherwise it == G;
existence
proof
hereby
assume A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
set V1 = the_Vertices_of G \/ {v};
reconsider V1 as non empty set;
set E1 = the_Edges_of G \/ (V --> the_Edges_of G);
set S1 = the_Source_of G +* ((V --> the_Edges_of G) --> v);
A2: dom S1 = dom (the_Source_of G) \/
dom ((V --> the_Edges_of G) --> v) by FUNCT_4:def 1
.= the_Edges_of G \/
dom ((V --> the_Edges_of G) --> v) by FUNCT_2:def 1
.= E1;
A3: rng the_Source_of G \/ rng ((V --> the_Edges_of G) --> v) c= V1
by XBOOLE_1:13;
rng S1 c= rng the_Source_of G \/ rng ((V --> the_Edges_of G) --> v)
by FUNCT_4:17;
then reconsider S1 as Function of E1, V1 by A2, FUNCT_2:2,A3,XBOOLE_1:1;
set T1 = the_Target_of G +* pr1(V,{the_Edges_of G});
A4: dom T1 = dom the_Target_of G \/
dom pr1(V,{the_Edges_of G}) by FUNCT_4:def 1
.= the_Edges_of G \/ dom pr1(V,{the_Edges_of G}) by FUNCT_2:def 1
.= the_Edges_of G \/ [: V, {the_Edges_of G} :] by FUNCT_3:def 4
.= E1 by FUNCOP_1:def 2;
rng pr1(V,{the_Edges_of G}) c= the_Vertices_of G by A1, XBOOLE_1:1;
then rng the_Target_of G \/ rng pr1(V,{the_Edges_of G})
c= the_Vertices_of G by XBOOLE_1:8;
then A5: rng the_Target_of G \/ rng pr1(V,{the_Edges_of G}) c= V1
by XBOOLE_1:10;
rng T1 c= rng the_Target_of G \/ rng pr1(V,{the_Edges_of G})
by FUNCT_4:17;
then reconsider T1 as Function of E1, V1 by A4,FUNCT_2:2,A5, XBOOLE_1:1;
set G1 = createGraph(V1,E1,S1,T1);
the_Vertices_of G c= V1 & the_Edges_of G c= E1 by XBOOLE_1:7;
then A6: the_Vertices_of G c= the_Vertices_of G1
& the_Edges_of G c= the_Edges_of G1;
for e being set st e in the_Edges_of G holds
(the_Source_of G).e = (the_Source_of G1).e &
(the_Target_of G).e = (the_Target_of G1).e
proof
let e be set;
assume A7: e in the_Edges_of G;
then e in dom the_Source_of G by FUNCT_2:def 1;
then A8: e in dom the_Source_of G \/
dom ((V --> the_Edges_of G) --> v) by XBOOLE_1:7, TARSKI:def 3;
a9: the_Edges_of G /\ (V --> the_Edges_of G) = {} by Lm6;
then A9: not e in (V --> the_Edges_of G) by A7, Lm7;
not e in dom ((V --> the_Edges_of G) --> v) by A7, Lm7, a9;
then A10: S1.e = (the_Source_of G).e by A8, FUNCT_4:def 1;
e in dom the_Target_of G by A7, FUNCT_2:def 1;
then A11: e in dom the_Target_of G \/ dom pr1(V,{the_Edges_of G})
by XBOOLE_1:7, TARSKI:def 3;
not e in [: V, {the_Edges_of G} :] by A9, FUNCOP_1:def 2;
then not e in dom pr1(V,{the_Edges_of G});
then T1.e = (the_Target_of G).e by A11, FUNCT_4:def 1;
hence thesis by A10;
end;
then reconsider G1 as Supergraph of G by A6, GLIB_006:def 9;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of G1 = the_Target_of G +* pr1(V,{the_Edges_of G});
end;
assume not (V c= the_Vertices_of G & not v in the_Vertices_of G);
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take G1;
thus thesis;
end;
consistency;
end;
definition
let G, v, V;
mode addAdjVertexFromAll of G,v,V -> Supergraph of G means
:Def3:
the_Vertices_of it = the_Vertices_of G \/ {v} &
the_Edges_of it = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of it = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of it = the_Target_of G +* ((V --> the_Edges_of G) --> v)
if V c= the_Vertices_of G & not v in the_Vertices_of G
otherwise it == G;
existence
proof
hereby
assume A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
set V1 = the_Vertices_of G \/ {v};
reconsider V1 as non empty set;
set E1 = the_Edges_of G \/ (V --> the_Edges_of G);
set T1 = the_Target_of G +* ((V --> the_Edges_of G) --> v);
A2: dom T1 = dom (the_Target_of G) \/
dom ((V --> the_Edges_of G) --> v) by FUNCT_4:def 1
.= the_Edges_of G \/
dom ((V --> the_Edges_of G) --> v) by FUNCT_2:def 1
.= E1;
A3: rng the_Target_of G \/ rng ((V --> the_Edges_of G) --> v) c= V1
by XBOOLE_1:13;
rng T1 c= rng the_Target_of G \/ rng ((V --> the_Edges_of G) --> v)
by FUNCT_4:17;
then reconsider T1 as Function of E1, V1 by A2,FUNCT_2:2,A3, XBOOLE_1:1;
set S1 = the_Source_of G +* pr1(V,{the_Edges_of G});
A4: dom S1 = dom the_Source_of G \/
dom pr1(V,{the_Edges_of G}) by FUNCT_4:def 1
.= the_Edges_of G \/ dom pr1(V,{the_Edges_of G}) by FUNCT_2:def 1
.= the_Edges_of G \/ [: V, {the_Edges_of G} :] by FUNCT_3:def 4
.= E1 by FUNCOP_1:def 2;
rng pr1(V,{the_Edges_of G}) c= the_Vertices_of G by A1, XBOOLE_1:1;
then rng the_Source_of G \/ rng pr1(V,{the_Edges_of G})
c= the_Vertices_of G by XBOOLE_1:8;
then A5: rng the_Source_of G \/ rng pr1(V,{the_Edges_of G}) c= V1
by XBOOLE_1:10;
rng S1 c= rng the_Source_of G \/ rng pr1(V,{the_Edges_of G})
by FUNCT_4:17;
then reconsider S1 as Function of E1, V1 by A4, FUNCT_2:2,
A5, XBOOLE_1:1;
set G1 = createGraph(V1,E1,S1,T1);
the_Vertices_of G c= V1 & the_Edges_of G c= E1 by XBOOLE_1:7;
then A6: the_Vertices_of G c= the_Vertices_of G1
& the_Edges_of G c= the_Edges_of G1;
for e being set st e in the_Edges_of G holds
(the_Source_of G).e = (the_Source_of G1).e &
(the_Target_of G).e = (the_Target_of G1).e
proof
let e be set;
assume A7: e in the_Edges_of G;
then e in dom the_Target_of G by FUNCT_2:def 1;
then A8: e in dom the_Target_of G \/
dom ((V --> the_Edges_of G) --> v) by XBOOLE_1:7, TARSKI:def 3;
a9: the_Edges_of G /\ (V --> the_Edges_of G) = {} by Lm6;
then A9: not e in (V --> the_Edges_of G) by A7, Lm7;
not e in dom ((V --> the_Edges_of G) --> v) by A7,Lm7,a9;
then A10: T1.e = (the_Target_of G).e by A8, FUNCT_4:def 1;
e in dom the_Source_of G by A7, FUNCT_2:def 1;
then A11: e in dom the_Source_of G \/ dom pr1(V,{the_Edges_of G})
by XBOOLE_1:7, TARSKI:def 3;
not e in [: V, {the_Edges_of G} :] by A9, FUNCOP_1:def 2;
then not e in dom pr1(V,{the_Edges_of G});
then S1.e = (the_Source_of G).e by A11, FUNCT_4:def 1;
hence thesis by A10;
end;
then reconsider G1 as Supergraph of G by GLIB_006:def 9, A6;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of G1 = the_Target_of G +* ((V --> the_Edges_of G) --> v);
end;
assume not (V c= the_Vertices_of G & not v in the_Vertices_of G);
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take G1;
thus thesis;
end;
consistency;
end;
definition
let G, v;
mode addAdjVertexToAll of G, v is
addAdjVertexToAll of G, v, the_Vertices_of G;
correctness;
mode addAdjVertexFromAll of G, v is
addAdjVertexFromAll of G,v, the_Vertices_of G;
correctness;
end;
theorem
for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V
holds G1 == G2
proof
let G, v, V;
let G1, G2 be addAdjVertexToAll of G,v,V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then
the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of G1 = the_Target_of G +* pr1(V,{the_Edges_of G}) &
the_Vertices_of G2 = the_Vertices_of G \/ {v} &
the_Edges_of G2 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G2 = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of G2 = the_Target_of G +* pr1(V,{the_Edges_of G}) by Def2;
hence thesis by GLIB_000:def 34;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 & G == G2 by Def2;
hence thesis by GLIB_000:85;
end;
end;
theorem
for G, v, V for G1, G2 being addAdjVertexFromAll of G,v,V
holds G1 == G2
proof
let G, v, V;
let G1, G2 be addAdjVertexFromAll of G,v,V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then
the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of G1 = the_Target_of G +* ((V --> the_Edges_of G) --> v) &
the_Vertices_of G2 = the_Vertices_of G \/ {v} &
the_Edges_of G2 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G2 = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of G2 = the_Target_of G +* ((V --> the_Edges_of G) --> v)
by Def3;
hence thesis by GLIB_000:def 34;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 & G == G2 by Def3;
hence thesis by GLIB_000:85;
end;
end;
theorem
for G, G2, v, V for G1 being addAdjVertexToAll of G,v,V
st G1 == G2 holds G2 is addAdjVertexToAll of G,v,V
proof
let G, G2, v, V;
let G1 be addAdjVertexToAll of G,v,V;
assume A1: G1 == G2;
per cases;
suppose A2: V c= the_Vertices_of G & not v in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of G1 = the_Target_of G +* pr1(V,{the_Edges_of G}) by Def2;
then A3: the_Vertices_of G2 = the_Vertices_of G \/ {v} &
the_Edges_of G2 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G2 = the_Source_of G +* ((V --> the_Edges_of G) --> v) &
the_Target_of G2 = the_Target_of G +* pr1(V,{the_Edges_of G})
by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, GLIB_006:59;
then G2 is Supergraph of G by GLIB_006:62;
hence thesis by A2, A3, Def2;
end;
suppose A4: not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 by Def2;
then A5: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by GLIB_006:59;
hence thesis by A4, A5, Def2;
end;
end;
theorem
for G, G2, v, V for G1 being addAdjVertexFromAll of G,v,V
st G1 == G2 holds G2 is addAdjVertexFromAll of G,v,V
proof
let G, G2, v, V;
let G1 be addAdjVertexFromAll of G,v,V;
assume A1: G1 == G2;
per cases;
suppose A2: V c= the_Vertices_of G & not v in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G1 = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of G1 = the_Target_of G +* ((V --> the_Edges_of G) --> v)
by Def3;
then A3: the_Vertices_of G2 = the_Vertices_of G \/ {v} &
the_Edges_of G2 = the_Edges_of G \/ (V --> the_Edges_of G) &
the_Source_of G2 = the_Source_of G +* pr1(V,{the_Edges_of G}) &
the_Target_of G2 = the_Target_of G +* ((V --> the_Edges_of G) --> v)
by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, GLIB_006:59;
then G2 is Supergraph of G by GLIB_006:62;
hence thesis by A2, A3, Def3;
end;
suppose A4: not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 by Def3;
then A5: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by GLIB_006:59;
hence thesis by A4, A5, Def3;
end;
end;
theorem Th32:
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
holds the_Vertices_of G1 = the_Vertices_of G2
& the_Edges_of G1 = the_Edges_of G2
proof
let G,v,V;
let G1 be addAdjVertexToAll of G,v,V;
let G2 be addAdjVertexFromAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v}
& the_Edges_of G1 = the_Edges_of G \/ (V --> the_Edges_of G) by Def2;
hence thesis by A1,Def3;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 & G == G2 by Def2, Def3;
then G1 == G2 by GLIB_000:85;
hence thesis by GLIB_000:def 34;
end;
end;
theorem Th33:
for G2, v, V for G1 being addAdjVertexToAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.edgesOutOf({v}) = V --> the_Edges_of G2
proof
let G2, v, V;
let G1 be addAdjVertexToAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def2;
for e being object holds e in G1.edgesOutOf({v}) iff
e in V --> the_Edges_of G2
proof
let e be object;
reconsider e1=e as set by TARSKI:1;
hereby
assume e in G1.edgesOutOf({v});
then A3: e1 in the_Edges_of G1 & (the_Source_of G1).e1 in {v}
by GLIB_000:def 27;
not e in the_Edges_of G2
proof
assume A4: e in the_Edges_of G2;
then (the_Source_of G2).e1 = (the_Source_of G1).e1 by GLIB_006:def 9
.= v by A3, TARSKI:def 1;
hence contradiction by A1, A4, FUNCT_2:5;
end;
hence e in V --> the_Edges_of G2 by A2, A3, XBOOLE_0:def 3;
end;
assume A5: e in V --> the_Edges_of G2;
then e in dom ((V --> the_Edges_of G2) --> v);
then (the_Source_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A2, FUNCT_4:13
.= v by A5, FUNCOP_1:7;
then A6: (the_Source_of G1).e in {v} by TARSKI:def 1;
e in the_Edges_of G1 by A5, A2, XBOOLE_0:def 3;
hence thesis by A6, GLIB_000:def 27;
end;
hence thesis by TARSKI:2;
end;
theorem Th34:
for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.edgesInto({v}) = V --> the_Edges_of G2
proof
let G2, v, V;
let G1 be addAdjVertexFromAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Target_of G1 = the_Target_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def3;
for e being object holds e in G1.edgesInto({v}) iff
e in V --> the_Edges_of G2
proof
let e be object;
reconsider e1=e as set by TARSKI:1;
hereby
assume e in G1.edgesInto({v});
then A3: e1 in the_Edges_of G1 & (the_Target_of G1).e1 in {v}
by GLIB_000:def 26;
then A4: (the_Target_of G1).e = v by TARSKI:def 1;
not e in the_Edges_of G2
proof
assume A5: e in the_Edges_of G2;
then (the_Target_of G2).e1 = v by A4, GLIB_006:def 9;
hence contradiction by A1, A5, FUNCT_2:5;
end;
hence e in V --> the_Edges_of G2 by A2, A3, XBOOLE_0:def 3;
end;
assume A6: e in V --> the_Edges_of G2;
then e in dom ((V --> the_Edges_of G2) --> v);
then (the_Target_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A2, FUNCT_4:13
.= v by A6, FUNCOP_1:7;
then A7: (the_Target_of G1).e in {v} by TARSKI:def 1;
e in the_Edges_of G1 by A6, A2, XBOOLE_0:def 3;
hence thesis by A7, GLIB_000:def 26;
end;
hence thesis by TARSKI:2;
end;
theorem Th35:
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
st V c= the_Vertices_of G & not v in the_Vertices_of G
holds G2 is reverseEdgeDirections of G1, G1.edgesOutOf({v})
& G1 is reverseEdgeDirections of G2, G2.edgesInto({v})
proof
let G, v, V;
let G1 be addAdjVertexToAll of G,v,V;
let G2 be addAdjVertexFromAll of G,v,V;
set E = V --> the_Edges_of G;
assume A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
then A2: G1.edgesOutOf({v}) = E & G2.edgesInto({v}) = E by Th33, Th34;
A3: the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Edges_of G1 = the_Edges_of G \/ E &
the_Source_of G1 = the_Source_of G +* (E --> v) &
the_Target_of G1 = the_Target_of G +* pr1(V, {the_Edges_of G})
by A1, Def2;
A4: the_Vertices_of G2 = the_Vertices_of G \/ {v} &
the_Edges_of G2 = the_Edges_of G \/ E &
the_Source_of G2 = the_Source_of G +* pr1(V, {the_Edges_of G}) &
the_Target_of G2 = the_Target_of G +* (E --> v)
by A1, Def3;
A5: dom (E --> v) = E;
A6: dom pr1(V, {the_Edges_of G}) = [: V, {the_Edges_of G} :] by FUNCT_3:def 4
.= E by FUNCOP_1:def 2;
A9: the_Source_of G2 = the_Source_of G1 +* (pr1(V, {the_Edges_of G}) | E)
by A3, A4, A5, A6, FUNCT_4:74
.= the_Source_of G1 +* ((the_Target_of G1) | E) by A6, A3;
A11: the_Target_of G2 = the_Target_of G1 +* ((E --> v) | E)
by A3, A4, A5, A6, FUNCT_4:74
.= the_Target_of G1 +* ((the_Source_of G1) | E) by A5, A3;
A13: the_Source_of G1 = the_Source_of G2 +* ((E --> v) | E)
by A3, A4, A5, A6, FUNCT_4:74
.= the_Source_of G2 +* ((the_Target_of G2) | E) by A5, A4;
A15: the_Target_of G1 = the_Target_of G2 +* (pr1(V, {the_Edges_of G}) | E)
by A3, A4, A5, A6, FUNCT_4:74
.= the_Target_of G2 +* ((the_Source_of G2) | E) by A6, A4;
thus G2 is reverseEdgeDirections of G1, G1.edgesOutOf({v})
by A2, A3, A4, A9, A11, Def1;
thus thesis by A2, A3, A4, A13, A15, Def1;
end;
theorem
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for v1,e,v2 being object
holds (e Joins v1,v2,G1 iff e Joins v1,v2,G2)
proof
let G,v,V;
let G1 be addAdjVertexToAll of G,v,V;
let G2 be addAdjVertexFromAll of G,v,V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then G2 is reverseEdgeDirections of G1, G1.edgesOutOf({v}) by Th35;
hence thesis by Th9;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 & G == G2 by Def2, Def3;
then G1 == G2 by GLIB_000:85;
hence thesis by GLIB_000:88;
end;
end;
theorem
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V, w being object
holds (w is Vertex of G1 iff w is Vertex of G2) by Th32;
theorem Th38:
for G2, v, V for G1 being addAdjVertexToAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
for e1, u being object
holds not e1 DJoins u,v,G1 & (not u in V implies not e1 DJoins v,u,G1) &
for e2 being object
holds e1 DJoins v,u,G1 & e2 DJoins v,u,G1 implies e1 = e2
proof
let G2, v, V;
let G1 be addAdjVertexToAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} &
the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* ((V --> the_Edges_of G2) --> v) &
the_Target_of G1 = the_Target_of G2 +* pr1(V,{the_Edges_of G2})
by Def2;
let e1, u be object;
thus not e1 DJoins u,v,G1
proof
assume e1 DJoins u,v,G1;
then A3: e1 in the_Edges_of G1 & (the_Source_of G1).e1 = u &
(the_Target_of G1).e1 = v by GLIB_000:def 14;
not e1 in the_Edges_of G2
proof
reconsider e3=e1 as set by TARSKI:1;
assume A4: e1 in the_Edges_of G2;
then (the_Target_of G2).e3 = v by A3, GLIB_006:def 9;
hence contradiction by A1, A4, FUNCT_2:5;
end;
then e1 in V --> the_Edges_of G2 by A2, A3, XBOOLE_0:def 3;
then A5: e1 in [:V,{the_Edges_of G2}:];
then A6: e1 in dom pr1(V,{the_Edges_of G2}) by FUNCT_3:def 4;
consider x1,y1 being object such that
A7: x1 in V & y1 in {the_Edges_of G2} and
A8: e1 = [x1,y1] by A5, ZFMISC_1:def 2;
v = pr1(V,{the_Edges_of G2}).e1 by A6, A2, A3, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x1,y1) by A8, BINOP_1:def 1
.= x1 by A7, FUNCT_3:def 4;
hence contradiction by A1,A7;
end;
thus not u in V implies not e1 DJoins v,u,G1
proof
assume A9: not u in V;
assume e1 DJoins v,u,G1;
then A10: e1 in the_Edges_of G1 &
(the_Source_of G1).e1 = v & (the_Target_of G1).e1 = u by GLIB_000:def 14;
not e1 in dom pr1(V, {the_Edges_of G2})
proof
assume A11: e1 in dom pr1(V, {the_Edges_of G2});
then consider x,y being object such that
A12: x in V & y in {the_Edges_of G2} & e1=[x,y] by ZFMISC_1:def 2;
u = pr1(V, {the_Edges_of G2}).e1 by A2, A10, A11, FUNCT_4:13
.= pr1(V, {the_Edges_of G2}).(x,y) by A12, BINOP_1:def 1
.= x by A12, FUNCT_3:def 4;
hence contradiction by A9, A12;
end;
then not e1 in [: V, {the_Edges_of G2} :] by FUNCT_3:def 4;
then A13: not e1 in V --> the_Edges_of G2;
then not e1 in dom ((V --> the_Edges_of G2) --> v);
then A14: (the_Source_of G1).e1 = (the_Source_of G2).e1
by A2, FUNCT_4:11;
e1 in the_Edges_of G2 by A2, A10, A13, XBOOLE_0:def 3;
hence contradiction by A14, A10, A1, FUNCT_2:5;
end;
let e2 be object;
assume e1 DJoins v,u,G1 & e2 DJoins v,u,G1;
then A15: e1 in the_Edges_of G1 & e2 in the_Edges_of G1 &
(the_Source_of G1).e1 = v & (the_Source_of G1).e2 = v &
(the_Target_of G1).e1 = u & (the_Target_of G1).e2 = u by GLIB_000:def 14;
not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2
proof
assume e1 in the_Edges_of G2 or e2 in the_Edges_of G2;
then per cases;
suppose A16: e1 in the_Edges_of G2;
reconsider e3=e1 as set by TARSKI:1;
(the_Source_of G2).e3 = v by A15, A16, GLIB_006:def 9;
hence contradiction by A1,A16, FUNCT_2:5;
end;
suppose A17: e2 in the_Edges_of G2;
reconsider e3=e2 as set by TARSKI:1;
(the_Source_of G2).e3 = v by A15, A17, GLIB_006:def 9;
hence contradiction by A1, A17, FUNCT_2:5;
end;
end;
then e1 in V --> the_Edges_of G2 & e2 in V --> the_Edges_of G2
by A2, A15, XBOOLE_0:def 3;
then A18: e1 in [:V,{the_Edges_of G2}:] & e2 in [:V,{the_Edges_of G2}:];
then A19: e1 in dom pr1(V,{the_Edges_of G2}) &
e2 in dom pr1(V,{the_Edges_of G2}) by FUNCT_3:def 4;
consider x1,y1 being object such that
A20: x1 in V & y1 in {the_Edges_of G2} and
A21: e1 = [x1,y1] by A18, ZFMISC_1:def 2;
consider x2,y2 being object such that
A22: x2 in V & y2 in {the_Edges_of G2} and
A23: e2 = [x2,y2] by A18, ZFMISC_1:def 2;
A24: u = pr1(V,{the_Edges_of G2}).e1 by A2, A15, A19, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x1,y1) by A21, BINOP_1:def 1
.= x1 by A20, FUNCT_3:def 4;
A25: u = pr1(V,{the_Edges_of G2}).e2 by A2, A15, A19, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x2,y2) by A23, BINOP_1:def 1
.= x2 by A22, FUNCT_3:def 4;
y1 = the_Edges_of G2 & y2 = the_Edges_of G2 by A20, A22, TARSKI:def 1;
hence thesis by A21, A23, A24, A25;
end;
theorem Th39:
for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
for e1, u being object
holds not e1 DJoins v,u,G1 & (not u in V implies not e1 DJoins u,v,G1) &
for e2 being object
holds e1 DJoins u,v,G1 & e2 DJoins u,v,G1 implies e1 = e2
proof
let G2, v, V;
let G1 be addAdjVertexFromAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} &
the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* pr1(V,{the_Edges_of G2}) &
the_Target_of G1 = the_Target_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def3;
let e1, u be object;
thus not e1 DJoins v,u,G1
proof
assume e1 DJoins v,u,G1;
then A3: e1 in the_Edges_of G1 & (the_Source_of G1).e1 = v &
(the_Target_of G1).e1 = u by GLIB_000:def 14;
not e1 in the_Edges_of G2
proof
reconsider e3=e1 as set by TARSKI:1;
assume A4: e1 in the_Edges_of G2;
then (the_Source_of G2).e3 = v by A3, GLIB_006:def 9;
hence contradiction by A1, A4, FUNCT_2:5;
end;
then e1 in V --> the_Edges_of G2 by A2, A3, XBOOLE_0:def 3;
then A5: e1 in [:V,{the_Edges_of G2}:];
then A6: e1 in dom pr1(V,{the_Edges_of G2}) by FUNCT_3:def 4;
consider x1,y1 being object such that
A7: x1 in V & y1 in {the_Edges_of G2} and
A8: e1 = [x1,y1] by A5, ZFMISC_1:def 2;
v = pr1(V,{the_Edges_of G2}).e1 by A2, A3, A6, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x1,y1) by A8, BINOP_1:def 1
.= x1 by A7, FUNCT_3:def 4;
hence contradiction by A1,A7;
end;
thus not u in V implies not e1 DJoins u,v,G1
proof
assume A9: not u in V;
assume e1 DJoins u,v,G1;
then A10: e1 in the_Edges_of G1 &
(the_Source_of G1).e1 = u & (the_Target_of G1).e1 = v by GLIB_000:def 14;
not e1 in dom pr1(V, {the_Edges_of G2})
proof
assume A11: e1 in dom pr1(V, {the_Edges_of G2});
then consider x,y being object such that
A12: x in V & y in {the_Edges_of G2} & e1=[x,y] by ZFMISC_1:def 2;
u = pr1(V, {the_Edges_of G2}).e1 by A2, A10, A11, FUNCT_4:13
.= pr1(V, {the_Edges_of G2}).(x,y) by A12, BINOP_1:def 1
.= x by A12, FUNCT_3:def 4;
hence contradiction by A9, A12;
end;
then not e1 in [: V, {the_Edges_of G2} :] by FUNCT_3:def 4;
then A13: not e1 in V --> the_Edges_of G2;
then not e1 in dom ((V --> the_Edges_of G2) --> v);
then A14: (the_Target_of G1).e1 = (the_Target_of G2).e1
by A2, FUNCT_4:11;
e1 in the_Edges_of G2 by A2, A10, A13, XBOOLE_0:def 3;
hence contradiction by A14, A10, A1, FUNCT_2:5;
end;
let e2 be object;
assume e1 DJoins u,v,G1 & e2 DJoins u,v,G1;
then A15: e1 in the_Edges_of G1 & e2 in the_Edges_of G1 &
(the_Source_of G1).e1 = u & (the_Source_of G1).e2 = u &
(the_Target_of G1).e1 = v & (the_Target_of G1).e2 = v by GLIB_000:def 14;
not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2
proof
assume e1 in the_Edges_of G2 or e2 in the_Edges_of G2;
then per cases;
suppose A16: e1 in the_Edges_of G2;
reconsider e3=e1 as set by TARSKI:1;
(the_Target_of G2).e3 = v by A15, A16, GLIB_006:def 9;
hence contradiction by A1, A16, FUNCT_2:5;
end;
suppose A17: e2 in the_Edges_of G2;
reconsider e3=e2 as set by TARSKI:1;
(the_Target_of G2).e3 = v by A15, A17, GLIB_006:def 9;
hence contradiction by A1, A17, FUNCT_2:5;
end;
end;
then e1 in V --> the_Edges_of G2 & e2 in V --> the_Edges_of G2
by A2, A15, XBOOLE_0:def 3;
then A18: e1 in [:V,{the_Edges_of G2}:] & e2 in [:V,{the_Edges_of G2}:];
then A19: e1 in dom pr1(V,{the_Edges_of G2}) &
e2 in dom pr1(V,{the_Edges_of G2}) by FUNCT_3:def 4;
consider x1,y1 being object such that
A20: x1 in V & y1 in {the_Edges_of G2} and
A21: e1 = [x1,y1] by A18, ZFMISC_1:def 2;
consider x2,y2 being object such that
A22: x2 in V & y2 in {the_Edges_of G2} and
A23: e2 = [x2,y2] by A18, ZFMISC_1:def 2;
A24: u = pr1(V,{the_Edges_of G2}).e1 by A2, A15, A19, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x1,y1) by A21, BINOP_1:def 1
.= x1 by A20, FUNCT_3:def 4;
A25: u = pr1(V,{the_Edges_of G2}).e2 by A2, A15, A19, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(x2,y2) by A23, BINOP_1:def 1
.= x2 by A22, FUNCT_3:def 4;
y1 = the_Edges_of G2 & y2 = the_Edges_of G2 by A20, A22, TARSKI:def 1;
hence thesis by A21, A23, A24,A25;
end;
theorem Th40:
for G2, v, V for G1 being addAdjVertexToAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
for e, v1, v2 being object st v1 <> v
holds e DJoins v1,v2,G1 implies e DJoins v1,v2,G2
proof
let G2, v, V;
let G1 be addAdjVertexToAll of G2,v,V;
assume V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} &
the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def2;
let e,v1,v2 be object;
assume A2: v1 <> v;
assume A3: e DJoins v1,v2,G1;
then A4: e in the_Edges_of G1 by GLIB_000:def 14;
A5: e in the_Edges_of G2
proof
assume not e in the_Edges_of G2;
then A6: e in (V --> the_Edges_of G2) by A1, A4, XBOOLE_0:def 3;
then e in dom ((V --> the_Edges_of G2) --> v);
then (the_Source_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A1, FUNCT_4:13
.= v by A6, FUNCOP_1:7;
hence contradiction by A2, A3, GLIB_000:def 14;
end;
reconsider e1=e as set by TARSKI:1;
(the_Source_of G1).e1 = (the_Source_of G2).e1 &
(the_Target_of G1).e1 = (the_Target_of G2).e1 by A5, GLIB_006:def 9;
then v1 = (the_Source_of G2).e1 & v2 = (the_Target_of G2).e1
by A3, GLIB_000:def 14;
hence thesis by A5, GLIB_000:def 14;
end;
theorem Th41:
for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
for e, v1, v2 being object st v2 <> v
holds e DJoins v1,v2,G1 implies e DJoins v1,v2,G2
proof
let G2, v, V;
let G1 be addAdjVertexFromAll of G2,v,V;
assume V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} &
the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Target_of G1 = the_Target_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def3;
let e,v1,v2 be object;
assume A2: v2 <> v;
assume A3: e DJoins v1,v2,G1;
then A4: e in the_Edges_of G1 by GLIB_000:def 14;
A5: e in the_Edges_of G2
proof
assume not e in the_Edges_of G2;
then A6: e in (V --> the_Edges_of G2) by A1, A4, XBOOLE_0:def 3;
then e in dom ((V --> the_Edges_of G2) --> v);
then (the_Target_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A1, FUNCT_4:13
.= v by A6, FUNCOP_1:7;
hence contradiction by A2, A3, GLIB_000:def 14;
end;
reconsider e1=e as set by TARSKI:1;
(the_Source_of G1).e1 = (the_Source_of G2).e1 &
(the_Target_of G1).e1 = (the_Target_of G2).e1 by A5, GLIB_006:def 9;
then v1 = (the_Source_of G2).e1 & v2 = (the_Target_of G2).e1
by A3, GLIB_000:def 14;
hence thesis by A5, GLIB_000:def 14;
end;
theorem Th42:
for G2, v, V for G1 being addAdjVertexToAll of G2,v,V, v1 being object
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V
holds [v1,the_Edges_of G2] DJoins v,v1,G1
proof
let G2, v, V;
let G1 be addAdjVertexToAll of G2,v,V, v1 be object;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V;
then A2: the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* ((V --> the_Edges_of G2) --> v) &
the_Target_of G1 = the_Target_of G2 +* pr1(V,{the_Edges_of G2})
by Def2;
set e = [v1,the_Edges_of G2];
A3: the_Edges_of G2 in {the_Edges_of G2} by TARSKI:def 1;
then A4: e in [: V, {the_Edges_of G2} :] by A1, ZFMISC_1:def 2;
then A5: e in V --> the_Edges_of G2 by FUNCOP_1:def 2;
then A6: e in dom ((V --> the_Edges_of G2) --> v);
A7: e in dom pr1(V, {the_Edges_of G2}) by A4, FUNCT_3:def 4;
A8: e in the_Edges_of G1 by A2, A5, XBOOLE_0:def 3;
A9: (the_Source_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A2, A6, FUNCT_4:13
.= v by A5, FUNCOP_1:7;
(the_Target_of G1).e
= pr1(V,{the_Edges_of G2}).e by A2, A7, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(v1, the_Edges_of G2) by BINOP_1:def 1
.= v1 by A1, A3, FUNCT_3:def 4;
hence thesis by A8, A9, GLIB_000:def 14;
end;
theorem Th43:
for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V, v1 being object
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V
holds [v1,the_Edges_of G2] DJoins v1,v,G1
proof
let G2, v, V;
let G1 be addAdjVertexFromAll of G2,v,V, v1 be object;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V;
then A2: the_Edges_of G1 = the_Edges_of G2 \/ (V --> the_Edges_of G2) &
the_Source_of G1 = the_Source_of G2 +* pr1(V,{the_Edges_of G2}) &
the_Target_of G1 = the_Target_of G2 +* ((V --> the_Edges_of G2) --> v)
by Def3;
set e = [v1,the_Edges_of G2];
A3: the_Edges_of G2 in {the_Edges_of G2} by TARSKI:def 1;
then A4: e in [: V, {the_Edges_of G2} :] by A1, ZFMISC_1:def 2;
then A5: e in V --> the_Edges_of G2 by FUNCOP_1:def 2;
then A6: e in dom ((V --> the_Edges_of G2) --> v);
A7: e in dom pr1(V, {the_Edges_of G2}) by A4, FUNCT_3:def 4;
A8: e in the_Edges_of G1 by A2, A5, XBOOLE_0:def 3;
A9: (the_Target_of G1).e
= ((V --> the_Edges_of G2) --> v).e by A2, A6, FUNCT_4:13
.= v by A5, FUNCOP_1:7;
(the_Source_of G1).e
= pr1(V,{the_Edges_of G2}).e by A2, A7, FUNCT_4:13
.= pr1(V,{the_Edges_of G2}).(v1, the_Edges_of G2) by BINOP_1:def 1
.= v1 by A1, A3, FUNCT_3:def 4;
hence thesis by A8, A9, GLIB_000:def 14;
end;
theorem
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W1 being Walk of G1 holds W1 is Walk of G2
proof
let G,v,V;
let G1 be addAdjVertexToAll of G,v,V;
let G2 be addAdjVertexFromAll of G,v,V;
let W1 be Walk of G1;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then G2 is reverseEdgeDirections of G1, G1.edgesOutOf({v}) by Th35;
hence thesis by Th14;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G & G2 == G by Def2, Def3;
hence thesis by GLIB_000:85, GLIB_001:179;
end;
end;
theorem
for G, v, V for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1
proof
let G,v,V;
let G1 be addAdjVertexToAll of G,v,V;
let G2 be addAdjVertexFromAll of G,v,V;
let W2 be Walk of G2;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then G1 is reverseEdgeDirections of G2, G2.edgesInto({v}) by Th35;
hence thesis by Th14;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G & G2 == G by Def2, Def3;
hence thesis by GLIB_000:85, GLIB_001:179;
end;
end;
Lm8:
for V, E holds card V = card (V --> E)
proof
let V, E;
thus card V = card [: V, {E} :] by CARD_1:69
.= card (V --> E) by FUNCOP_1:def 2;
end;
Lm9:
for G2, v, V for G1 being addAdjVertexToAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
(for e being object holds not e Joins v,v,G1 &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,G1) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,G1
holds e DJoins v1,v2,G2) &
ex E being set st card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
proof
let G2, v, V;
let G1 be addAdjVertexToAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
hereby
let e be object;
not e DJoins v,v,G1 by A1, Th38;
hence not e Joins v,v,G1 by GLIB_000:16;
let v1 be object;
thus not v1 in V implies not e Joins v1,v,G1
proof
assume A2: not v1 in V;
assume e Joins v1,v,G1;
then e DJoins v1,v,G1 or e DJoins v,v1,G1 by GLIB_000:16;
hence contradiction by A1, A2, Th38;
end;
let v2 be object;
assume A3: v1 <> v & v2 <> v & e DJoins v1,v2,G1;
thus e DJoins v1,v2,G2 by A1, A3, Th40;
end;
set E = V --> the_Edges_of G2;
take E;
thus card V = card E by Lm8;
the_Edges_of G2 /\ E = {} by Lm6;
hence E misses the_Edges_of G2 by XBOOLE_0:def 7;
thus the_Edges_of G1 = the_Edges_of G2 \/ E by A1, Def2;
let v1 be object;
assume A4: v1 in V;
set e1 = [v1,the_Edges_of G2];
take e1;
the_Edges_of G2 in {the_Edges_of G2} by TARSKI:def 1;
then e1 in [: V, {the_Edges_of G2} :] by A4, ZFMISC_1:def 2;
hence e1 in E by FUNCOP_1:def 2;
A5: e1 DJoins v,v1,G1 by A1, A4, Th42;
hence e1 Joins v1,v,G1 by GLIB_000:16;
let e2 be object;
assume A6: e2 Joins v1,v,G1;
not e2 DJoins v1,v,G1 by A1, Th38;
then e2 DJoins v,v1,G1 by A6, GLIB_000:16;
hence e1 = e2 by A1, A5, Th38;
end;
Lm10:
for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
(for e being object holds not e Joins v,v,G1 &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,G1) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,G1
holds e DJoins v1,v2,G2) &
ex E being set st card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
proof
let G2, v, V;
let G1 be addAdjVertexFromAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
hereby
let e be object;
not e DJoins v,v,G1 by A1, Th39;
hence not e Joins v,v,G1 by GLIB_000:16;
let v1 be object;
thus not v1 in V implies not e Joins v1,v,G1
proof
assume A2: not v1 in V;
assume e Joins v1,v,G1;
then e DJoins v1,v,G1 or e DJoins v,v1,G1 by GLIB_000:16;
hence contradiction by A1, A2, Th39;
end;
let v2 be object;
assume A3: v1 <> v & v2 <> v & e DJoins v1,v2,G1;
thus e DJoins v1,v2,G2 by A1, A3, Th41;
end;
set E = V --> the_Edges_of G2;
take E;
thus card V = card E by Lm8;
the_Edges_of G2 /\ E = {} by Lm6;
hence E misses the_Edges_of G2 by XBOOLE_0:def 7;
thus the_Edges_of G1 = the_Edges_of G2 \/ E by A1, Def3;
let v1 be object;
assume A4: v1 in V;
set e1 = [v1,the_Edges_of G2];
take e1;
the_Edges_of G2 in {the_Edges_of G2} by TARSKI:def 1;
then e1 in [: V, {the_Edges_of G2} :] by A4, ZFMISC_1:def 2;
hence e1 in E by FUNCOP_1:def 2;
A5: e1 DJoins v1,v,G1 by A1, A4, Th43;
hence e1 Joins v1,v,G1 by GLIB_000:16;
let e2 be object;
assume A6: e2 Joins v1,v,G1;
not e2 DJoins v,v1,G1 by A1, Th39;
then e2 DJoins v1,v,G1 by A6, GLIB_000:16;
hence e1 = e2 by A1, A5, Th39;
end;
:: If someone could come up with an easier redefinition
:: without using isomorphisms, it would be appreciated.
:: Note that each property of the definition is used within
:: the next three theorems.
:: Also note that about half the definition is implied when V is finite
:: because of the card-property. However, this will not be proved here.
:: We need this general form (as opposed to addAdjVertexTo/FromAll)
:: to give a constructive characterization of star and wheel graphs
:: without having to use isomorphisms.
definition
let G, v, V;
mode addAdjVertexAll of G,v,V -> Supergraph of G means
:Def4:
the_Vertices_of it = the_Vertices_of G \/ {v} &
(for e being object holds not e Joins v,v,it &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,it) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,it
holds e DJoins v1,v2,G) &
ex E being set st
card V = card E & E misses the_Edges_of G &
the_Edges_of it = the_Edges_of G \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,it &
for e2 being object st e2 Joins v1,v,it holds e1 = e2
if V c= the_Vertices_of G & not v in the_Vertices_of G
otherwise it == G;
existence
proof
hereby
assume A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
reconsider G1 = the addAdjVertexToAll of G,v,V as Supergraph of G;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G \/ {v} by A1, Def2;
thus (for e being object holds not e Joins v,v,G1 &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,G1) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,G1
holds e DJoins v1,v2,G) &
ex E being set st card V = card E & E misses the_Edges_of G &
the_Edges_of G1 = the_Edges_of G \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A1, Lm9;
end;
assume not (V c= the_Vertices_of G & not v in the_Vertices_of G);
reconsider G1 = G as Supergraph of G by GLIB_006:61;
take G1;
thus thesis;
end;
consistency;
end;
definition
let G, v;
mode addAdjVertexAll of G,v is addAdjVertexAll of G,v,the_Vertices_of G;
correctness;
let V;
redefine mode addAdjVertexToAll of G,v,V -> addAdjVertexAll of G,v,V; :: redefines addAdjVertexToAll (GLIB_007, definition)
coherence
proof
let G1 be addAdjVertexToAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
then A2: the_Vertices_of G1 = the_Vertices_of G \/ {v} by Def2;
(for e being object holds not e Joins v,v,G1 &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,G1) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,G1
holds e DJoins v1,v2,G) &
ex E being set st card V = card E & E misses the_Edges_of G &
the_Edges_of G1 = the_Edges_of G \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A1, Lm9;
hence thesis by A1, A2, Def4;
end;
suppose A3: not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def2;
hence thesis by A3, Def4;
end;
end;
redefine mode addAdjVertexFromAll of G,v,V -> addAdjVertexAll of G,v,V; :: redefines addAdjVertexFromAll (GLIB_007, definition)
coherence
proof
let G1 be addAdjVertexFromAll of G,v,V;
per cases;
suppose A4: V c= the_Vertices_of G & not v in the_Vertices_of G;
then A5: the_Vertices_of G1 = the_Vertices_of G \/ {v} by Def3;
(for e being object holds not e Joins v,v,G1 &
for v1 being object
holds (not v1 in V implies not e Joins v1,v,G1) &
for v2 being object st (v1 <> v & v2 <> v) & e DJoins v1,v2,G1
holds e DJoins v1,v2,G) &
ex E being set st card V = card E & E misses the_Edges_of G &
the_Edges_of G1 = the_Edges_of G \/ E &
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A4, Lm10;
hence thesis by A4, A5, Def4;
end;
suppose A6: not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def3;
hence thesis by A6, Def4;
end;
end;
end;
theorem Th46:
for G2, v for G1 being addAdjVertexAll of G2,v,{}
holds the_Edges_of G2 = the_Edges_of G1
proof
let G2, v;
let G1 be addAdjVertexAll of G2,v,{};
per cases;
suppose {} c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then consider E being set such that
A1: card {} = card E & E misses the_Edges_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2 \/ E and
for v1 being object st v1 in {} ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by Def4;
E = {} by A1;
hence thesis by A2;
end;
suppose not ({} c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then G2 == G1 by Def4;
hence the_Edges_of G2 = the_Edges_of G1 by GLIB_000:def 34;
end;
end;
Lm11:
for G2, v for G1 being addAdjVertexAll of G2,v,{}
st the_Edges_of G2 = {} holds the_Edges_of G1 = {} by Th46;
theorem Th47:
for G2, v for V being non empty set, G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds the_Edges_of G1 <> {}
proof
let G2, v;
let V be non empty set, G1 be addAdjVertexAll of G2,v,V;
assume V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then consider E being set such that
A1: card V = card E & E misses the_Edges_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2 \/ E and
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by Def4;
E is non empty by A1;
then consider e being object such that
A3: e in E by XBOOLE_0:def 1;
thus thesis by A2, A3;
end;
theorem
for G, G2, v, V for G1 being addAdjVertexAll of G,v,V
st G1 == G2 holds G2 is addAdjVertexAll of G,v,V
proof
let G, G2, v, V;
let G1 be addAdjVertexAll of G,v,V;
assume A1: G1 == G2;
per cases;
suppose A2: V c= the_Vertices_of G & not v in the_Vertices_of G;
then consider E being set such that
A3: card V = card E & E misses the_Edges_of G and
A4: the_Edges_of G1 = the_Edges_of G \/ E and
A5: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by Def4;
:: show all properties of Definition
A6: now
the_Vertices_of G1 = the_Vertices_of G \/ {v} by A2, Def4;
hence the_Vertices_of G2 = the_Vertices_of G \/ {v}
by A1, GLIB_000:def 34;
hereby
let e be object;
not e Joins v,v,G1 by A2, Def4;
hence not e Joins v,v,G2 by A1, GLIB_000:88;
let v1 be object;
hereby
assume not v1 in V;
then not e Joins v1,v,G1 by A2, Def4;
hence not e Joins v1,v,G2 by A1, GLIB_000:88;
end;
let v2 be object;
assume that
A7: v1 <> v & v2 <> v and
A8: e DJoins v1,v2,G2;
e DJoins v1,v2,G1 by A8, A1, GLIB_000:88;
hence e DJoins v1,v2,G by A2, A7, Def4;
end;
take E;
thus card V = card E & E misses the_Edges_of G by A3;
thus the_Edges_of G2 = the_Edges_of G \/ E by A4, A1, GLIB_000:def 34;
let v1 be object;
assume v1 in V;
then consider e1 being object such that
A9: e1 in E & e1 Joins v1,v,G1 and
A10: for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A5;
take e1;
thus e1 in E & e1 Joins v1,v,G2 by A1, A9, GLIB_000:88;
let e2 be object;
assume e2 Joins v1,v,G2;
then e2 Joins v1,v,G1 by A1, GLIB_000:88;
hence e1 = e2 by A10;
end;
G2 is Supergraph of G1 by A1, GLIB_006:59;
then G2 is Supergraph of G by GLIB_006:62;
hence thesis by A2, A6, Def4;
end;
suppose A11: not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 by Def4;
then A12: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by GLIB_006:59;
hence thesis by A11, A12, Def4;
end;
end;
theorem Th49:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V, v1,e,v2 being object
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
v1 <> v & v2 <> v & e Joins v1,v2,G1
holds e Joins v1,v2,G2
proof
let G2, v, V;
let G1 being addAdjVertexAll of G2,v,V;
let v1,e,v2 being object;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: v1 <> v & v2 <> v and
A3: e Joins v1,v2,G1;
per cases by A3, GLIB_000:16;
suppose e DJoins v1,v2,G1;
then e DJoins v1,v2,G2 by A1, A2, Def4;
hence thesis by GLIB_000:16;
end;
suppose e DJoins v2,v1,G1;
then e DJoins v2,v1,G2 by A1, A2, Def4;
hence thesis by GLIB_000:16;
end;
end;
theorem Th50:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds v is Vertex of G1
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2,v,V;
assume V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by Def4;
v in {v} by TARSKI:def 1;
hence thesis by A1, XBOOLE_0:def 3;
end;
theorem Th51:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V
for E being set, v1,e,v2 being object
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E & E misses the_Edges_of G2 &
e Joins v1,v2,G1 & not e in the_Edges_of G2
holds e in E & ((v1 = v & v2 in V) or (v2 = v & v1 in V))
proof
let G2, v, V;
let G1 being addAdjVertexAll of G2,v,V;
let E being set, v1,e,v2 being object;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2 \/ E & E misses the_Edges_of G2
and A3: e Joins v1,v2,G1 & not e in the_Edges_of G2;
consider E2 being set such that
card V = card E2 and
A4: E2 misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E2 and
A5: for w being object st w in V ex e1 being object st e1 in E2 &
e1 Joins w,v,G1 &
for e2 being object st e2 Joins w,v,G1 holds e1 = e2
by A1, Def4;
A6: E = E2 by A2, A4, XBOOLE_1:71;
:: to show the thesis, we show that all other cases
:: (implicitly) lead to a contradiction
per cases;
:: not possible, no loops on v allowed
suppose v1 = v & v2 = v;
hence thesis by A1, A3, Def4;
end;
:: one possibility
suppose A7: v1 = v & v2 <> v;
per cases;
suppose A8: v2 in V;
then consider e1 being object such that
A9: e1 in E2 & e1 Joins v2,v,G1 and
A10: for e2 being object st e2 Joins v2,v,G1 holds e1 = e2
by A5;
thus e in E by A9, A6, A3, A7, A10, GLIB_000:14;
thus thesis by A7, A8;
end;
:: not possible, only vertices in V are adjacent with v
suppose not v2 in V;
then not e Joins v2,v,G1 by A1, Def4;
hence thesis by A3, A7, GLIB_000:14;
end;
end;
:: symmetric case
suppose A11: v1 <> v & v2 = v;
per cases;
suppose A12: v1 in V;
then consider e1 being object such that
A13: e1 in E2 & e1 Joins v1,v,G1 and
A14: for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A5;
thus e in E by A13, A6, A3, A11, A14;
thus thesis by A11, A12;
end;
:: not possible
suppose not v1 in V;
hence thesis by A3, A11, A1, Def4;
end;
end;
:: not possible since e is a new edge and therefore incident with v
suppose A15: v1 <> v & v2 <> v;
e DJoins v1,v2,G1 or e DJoins v2,v1,G1 by A3, GLIB_000:16;
then e DJoins v1,v2,G2 or e DJoins v2,v1,G2 by A1, A15, Def4;
hence thesis by A3, GLIB_000:def 14;
end;
end;
theorem Th52:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V, E being set
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E & E misses the_Edges_of G2
holds ex f, g being Function of E, V \/ {v} st
the_Source_of G1 = the_Source_of G2 +* f &
the_Target_of G1 = the_Target_of G2 +* g &
for e being object st e in E holds e DJoins f.e,g.e,G1 &
(f.e = v iff g.e <> v)
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2,v,V;
let E be set;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2 \/ E & E misses the_Edges_of G2;
consider E1 being set such that
A3: card V = card E1 & E1 misses the_Edges_of G2 and
A4: the_Edges_of G1 = the_Edges_of G2 \/ E1 and
for v1 being object st v1 in V ex e1 being object st e1 in E1 &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
A5: E1 /\ the_Edges_of G2 = {} by A3, XBOOLE_0:def 7;
A6: E = E1 by A2, A3, A4, XBOOLE_1:71;
:: define f and g
defpred P[object,object] means ex v2 being object st $1 DJoins $2,v2,G1;
A7: for e being object st e in E holds
ex v1 being object st v1 in V \/ {v} & P[e,v1]
proof
let e be object;
set x = (the_Source_of G1).e, y = (the_Target_of G1).e;
assume A8: e in E;
then A9: not e in the_Edges_of G2 by A5, A6, Lm7;
take x;
A10: e in the_Edges_of G1 by A8, A4, A6, XBOOLE_0:def 3;
then e Joins x,y,G1 by GLIB_000:def 13;
then x = v or x in V by A1, A3, A4, A9, Th51;
then x in {v} or x in V by TARSKI:def 1;
hence x in V \/ {v} by XBOOLE_0:def 3;
take y;
thus e DJoins x,y,G1 by A10, GLIB_000:def 14;
end;
consider f being Function of E, V \/ {v} such that
A11: for e being object st e in E holds P[e,f.e] from FUNCT_2:sch 1(A7);
defpred Q[object,object] means $1 DJoins f.$1,$2,G1;
A12: for e being object st e in E holds
ex v2 being object st v2 in V \/ {v} & Q[e,v2]
proof
let e be object;
assume A13: e in E;
then consider v2 being object such that
A14: e DJoins f.e,v2,G1 by A11;
take v2;
A15: not e in the_Edges_of G2 by A5, A6, A13, Lm7;
e Joins f.e,v2,G1 by A14, GLIB_000:16;
then v2 = v or v2 in V by A1, A3, A4, A15, Th51;
then v2 in {v} or v2 in V by TARSKI:def 1;
hence v2 in V \/ {v} by XBOOLE_0:def 3;
thus thesis by A14;
end;
consider g being Function of E, V \/ {v} such that
A16: for e being object st e in E holds Q[e,g.e] from FUNCT_2:sch 1(A12);
take f,g;
:: show S1 = S2 +* f
A17: dom (the_Source_of G2 +* f)
= dom the_Source_of G2 \/ dom f by FUNCT_4:def 1
.= the_Edges_of G2 \/ dom f by GLIB_000:4
.= the_Edges_of G2 \/ E by FUNCT_2:def 1
.= dom the_Source_of G1 by A2, GLIB_000:4;
for e being object st e in dom the_Source_of G1 holds
(the_Source_of G1).e = (the_Source_of G2 +* f).e
proof
let e be object;
assume e in dom the_Source_of G1;
then per cases by A2, XBOOLE_0:def 3;
suppose A18: e in the_Edges_of G2;
then not e in dom f by A5, A6, Lm7;
then (the_Source_of G2 +* f).e = (the_Source_of G2).e by FUNCT_4:11
.= (the_Source_of G1).e by A18, GLIB_006:def 9;
hence thesis;
end;
suppose A19: e in E;
then e in dom f by FUNCT_2:def 1;
then A20: (the_Source_of G2 +* f).e = f.e by FUNCT_4:13;
e DJoins f.e,g.e,G1 by A16, A19;
hence thesis by A20,GLIB_000:def 14;
end;
end;
hence the_Source_of G1 = the_Source_of G2 +* f by A17, FUNCT_1:2;
:: show T1 = T2 +* g (symmetric case)
A21: dom (the_Target_of G2 +* g)
= dom the_Target_of G2 \/ dom g by FUNCT_4:def 1
.= the_Edges_of G2 \/ dom g by GLIB_000:4
.= the_Edges_of G2 \/ E by FUNCT_2:def 1
.= dom the_Target_of G1 by A2, GLIB_000:4;
for e being object st e in dom the_Target_of G1 holds
(the_Target_of G1).e = (the_Target_of G2 +* g).e
proof
let e be object;
assume e in dom the_Target_of G1;
then per cases by A2, XBOOLE_0:def 3;
suppose A22: e in the_Edges_of G2;
then not e in dom g by A5, A6, Lm7;
then (the_Target_of G2 +* g).e = (the_Target_of G2).e by FUNCT_4:11
.= (the_Target_of G1).e by A22, GLIB_006:def 9;
hence thesis;
end;
suppose A23: e in E;
then e in dom g by FUNCT_2:def 1;
then A24: (the_Target_of G2 +* g).e = g.e by FUNCT_4:13;
e DJoins f.e,g.e,G1 by A16, A23;
hence thesis by A24,GLIB_000:def 14;
end;
end;
hence the_Target_of G1 = the_Target_of G2 +* g by A21, FUNCT_1:2;
:: show the rest
let e be object;
assume A25: e in E;
hence A26: e DJoins f.e,g.e,G1 by A16;
then A27: e Joins f.e,g.e,G1 by GLIB_000:16;
thus f.e = v implies g.e <> v by A1, A27, Def4;
assume A28: g.e <> v;
assume f.e <> v;
then e DJoins f.e,g.e,G2 by A1, A26, A28, Def4;
then e in the_Edges_of G2 by GLIB_000:def 14;
hence contradiction by A25, A5, A6, Lm7;
end;
theorem Th53:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G2)
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
set B = G1.edgesBetween(the_Vertices_of G2);
for e being object holds e in the_Edges_of G2 iff e in B
proof
let e be object;
hereby
assume A2: e in the_Edges_of G2;
then (the_Source_of G2).e in the_Vertices_of G2 &
(the_Target_of G2).e in the_Vertices_of G2 by FUNCT_2:5;
then A3: (the_Source_of G1).e in the_Vertices_of G2 &
(the_Target_of G1).e in the_Vertices_of G2 by A2, GLIB_006:def 9;
the_Edges_of G2 c= the_Edges_of G1 by GLIB_006:def 9;
hence e in B by A3, GLIB_000:31, A2;
end;
set x = (the_Source_of G1).e, y = (the_Target_of G1).e;
assume e in B;
then A4: e in the_Edges_of G1 &
x in the_Vertices_of G2 & y in the_Vertices_of G2 by GLIB_000:31; then
e Joins x,y,G1 by GLIB_000:def 13;
then e Joins x,y,G2 by A1, A4, Th49;
hence thesis by GLIB_000:def 13;
end;
hence thesis by TARSKI:2;
end;
theorem
for G2 being _Graph, v, V being set, G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G2 is removeVertex of G1, v
proof
let G2 be _Graph, v, V be set;
let G1 be addAdjVertexAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
A2: G2 is Subgraph of G1 by GLIB_006:57;
set V1 = the_Vertices_of G1 \ {v};
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
then A3: the_Vertices_of G2 = V1 by A1, ZFMISC_1:117;
then reconsider V1 as non empty Subset of the_Vertices_of G1;
the_Edges_of G2 = G1.edgesBetween(V1) by A1, A3, Th53;
hence thesis by A2, A3, GLIB_000:def 37;
end;
theorem Th55:
for G2, v for G1 being addAdjVertexAll of G2,v,{}
holds G1 is addVertex of G2, v
proof
let G2, v;
let G1 be addAdjVertexAll of G2,v,{};
per cases;
suppose {} c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by Def4;
A2: the_Edges_of G1 = the_Edges_of G2 by Th46;
then A3: dom the_Source_of G1 = the_Edges_of G2 &
dom the_Target_of G1 = the_Edges_of G2 by GLIB_000:4;
A4: the_Source_of G1 = (the_Source_of G1) | the_Edges_of G2 by A3
.= the_Source_of G2 by GLIB_006:69;
the_Target_of G1 = (the_Target_of G1) | the_Edges_of G2 by A3
.= the_Target_of G2 by GLIB_006:69;
hence thesis by A1, A2, A4, GLIB_006:def 10;
end;
suppose A5: not ({} c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then A6: {v} c= the_Vertices_of G2 by XBOOLE_1:2, ZFMISC_1:31;
G1 == G2 by A5, Def4;
hence thesis by A6, GLIB_006:79;
end;
end;
:: TODO other direction
theorem
for G2, v for v1 being object, G1 being addAdjVertexAll of G2,v,{v1}
st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2
ex e being object st not e in the_Edges_of G2 &
(G1 is addAdjVertex of G2,v,e,v1 or G1 is addAdjVertex of G2,v1,e,v)
proof
let G2, v;
let v1 be object, G1 be addAdjVertexAll of G2,v,{v1};
assume A1: v1 in the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: {v1} c= the_Vertices_of G2 by ZFMISC_1:31;
then A3: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
consider E being set such that
A4: card {v1} = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A5: for v2 being object st v2 in {v1} ex e1 being object st e1 in E &
e1 Joins v2,v,G1 &
for e2 being object st e2 Joins v2,v,G1 holds e1 = e2 by A1, A2, Def4;
v1 in {v1} by TARSKI:def 1;
then consider e1 being object such that
A6: e1 in E & e1 Joins v1,v,G1 and
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A5;
take e1;
E /\ the_Edges_of G2 = {} by A4, XBOOLE_0:def 7;
hence A7: not e1 in the_Edges_of G2 by A6, Lm7;
consider e being object such that
A8: E = {e} by A4, CARD_1:29;
A9: E = {e1} by A6, A8, TARSKI:def 1;
then A10: the_Edges_of G1 = the_Edges_of G2 \/ {e1} by A4;
consider f,g being Function of E, {v1} \/ {v} such that
A11: the_Source_of G1 = the_Source_of G2 +* f and
A12: the_Target_of G1 = the_Target_of G2 +* g and
A13: for e being object st e in E holds e DJoins f.e,g.e,G1 &
(f.e = v iff g.e <> v) by A1, A2, A4, Th52;
reconsider f,g as Function of {e1}, {v1, v} by A9, ENUMSET1:1;
A14: e1 DJoins f.e1,g.e1,G1 by A6, A13;
per cases by A6, GLIB_000:16;
suppose e1 DJoins v1,v,G1;
then (the_Source_of G1).e1 = v1 & (the_Target_of G1).e1 = v
by GLIB_000:def 14;
then A15: v1 = f.e1 & v = g.e1 by A14, GLIB_000:def 14;
for z being object st z in dom f holds f.z = v1 by A15, TARSKI:def 1;
then f = dom f --> v1 by FUNCOP_1:11;
then f = {e1} --> v1 by FUNCT_2:def 1;
then A16: the_Source_of G1 = the_Source_of G2 +* (e1 .--> v1)
by A11,FUNCOP_1:def 9;
for z being object st z in dom g holds g.z = v by A15, TARSKI:def 1;
then g = dom g --> v by FUNCOP_1:11;
then g = {e1} --> v by FUNCT_2:def 1;
then g = e1 .--> v by FUNCOP_1:def 9;
hence thesis by A1, A7, A3, A10, A16, GLIB_006:def 12, A12;
end;
suppose e1 DJoins v,v1,G1;
then (the_Source_of G1).e1 = v & (the_Target_of G1).e1 = v1
by GLIB_000:def 14;
then A17: v = f.e1 & v1 = g.e1 by A14, GLIB_000:def 14;
for z being object st z in dom f holds f.z = v by A17, TARSKI:def 1;
then f = dom f --> v by FUNCOP_1:11;
then f = {e1} --> v by FUNCT_2:def 1;
then A18: the_Source_of G1 = the_Source_of G2 +* (e1 .--> v) by A11,
FUNCOP_1:def 9;
for z being object st z in dom g holds g.z = v1 by A17, TARSKI:def 1;
then g = dom g --> v1 by FUNCOP_1:11;
then g = {e1} --> v1 by FUNCT_2:def 1;
then g = e1 .--> v1 by FUNCOP_1:def 9;
hence thesis by A1, A7, A3, A10, A18, GLIB_006:def 12, A12;
end;
end;
:: TODO other direction
Lm12:
for G2, v, V for W being Subset of V, G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.edgesBetween(W,{v}) = {} implies W = {}
proof
let G2, v, V;
let W be Subset of V, G1 be addAdjVertexAll of G2,v,V;
assume V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then consider E being set such that
card V = card E and
E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E and
A1: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by Def4;
assume A2: G1.edgesBetween(W,{v}) = {};
assume A3: W <> {};
set w = the Element of W;
w in W by A3;
then consider e being object such that
A4: e in E & e Joins w,v,G1 and
for e2 being object st e2 Joins w,v,G1 holds e = e2 by A1;
v in {v} by TARSKI:def 1;
then e SJoins W,{v},G1 by A3, A4, GLIB_000:17;
hence contradiction by A2,GLIB_000:def 30;
end;
theorem Th57:
for G2, v, V for W being Subset of V, G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
ex f being Function of W, G1.edgesBetween(W,{v}) st
f is one-to-one onto & for w being object st w in W holds f.w Joins w,v,G1
proof
let G2, v, V;
let W be Subset of V, G1 be addAdjVertexAll of G2,v,V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then consider E being set such that
card V = card E and
E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E and
A2: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by Def4;
defpred P[object,object] means $2 Joins $1,v,G1;
A3: for w being object st w in W ex e being object
st e in G1.edgesBetween(W,{v}) & P[w,e]
proof
let w be object;
assume A4: w in W;
then consider e being object such that
A5: e in E & e Joins w,v,G1 and
for e2 being object st e2 Joins w,v,G1 holds e = e2 by A2;
take e;
v in {v} by TARSKI:def 1;
then e SJoins W,{v},G1 by A4, A5, GLIB_000:17;
hence e in G1.edgesBetween(W,{v}) by GLIB_000:def 30;
thus thesis by A5;
end;
consider f being Function of W, G1.edgesBetween(W,{v}) such that
A6: for w being object st w in W holds P[w,f.w] from FUNCT_2:sch 1(A3);
take f;
A7: G1.edgesBetween(W,{v}) = {} implies W = {} by A1, Lm12;
for w1,w2 being object st w1 in W & w2 in W & f.w1 = f.w2 holds w1 = w2
proof
let w1, w2 be object;
assume that
A8: w1 in W & w2 in W and
A9: f.w1 = f.w2;
f.w1 Joins w1,v,G1 & f.w2 Joins w2,v,G1 by A6, A8;
then per cases by A9, GLIB_000:15;
suppose w1 = w2 & v = v;
hence thesis;
end;
suppose w1 = v & v = w2;
hence thesis;
end;
end;
hence f is one-to-one by A7, FUNCT_2:19;
for e being object holds e in G1.edgesBetween(W,{v}) implies e in rng f
proof
let e be object;
assume A11: e in G1.edgesBetween(W,{v});
then A12: e SJoins W,{v},G1 by GLIB_000:def 30;
consider w being object such that
A13: w in W & e Joins w,v,G1 by A12, GLIB_000:102;
consider e1 being object such that
e1 in E & e1 Joins w,v,G1 and
A14: for e2 being object st e2 Joins w,v,G1 holds e1 = e2 by A2,A13;
e1 = e & e1 = f.w by A13, A14,A6;
hence e in rng f by A13, FUNCT_2:4, A11;
end;
then G1.edgesBetween(W,{v}) c= rng f by TARSKI:def 3;
hence f is onto by XBOOLE_0:def 10, FUNCT_2:def 3;
thus thesis by A6;
end;
theorem Th58:
for G2, v, V, E for G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E
holds E = G1.edgesBetween(V,{v})
proof
let G2,v,V,E;
let G1 be addAdjVertexAll of G2,v,V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E;
consider E1 being set such that
A3: card V = card E1 & E1 misses the_Edges_of G2 and
A4: the_Edges_of G1 = the_Edges_of G2 \/ E1 and
A5: for v1 being object st v1 in V ex e1 being object st
e1 in E1 & e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
A6: E = E1 by A2, A3, A4, XBOOLE_1:71;
A7: E /\ the_Edges_of G2 = {} by A2, XBOOLE_0:def 7;
for e being object holds e in E iff e in G1.edgesBetween(V,{v})
proof
let e be object;
set x = (the_Source_of G1).e, y = (the_Target_of G1).e;
hereby
assume A8: e in E;
then e in the_Edges_of G1 by A2, XBOOLE_0:def 3;
then A9: e Joins x,y,G1 by GLIB_000:def 13;
not e in the_Edges_of G2 by A7, A8, Lm7;
then per cases by A1, A2, A9, Th51;
suppose x = v & y in V;
then x in {v} & y in V by TARSKI:def 1;
then e SJoins V,{v},G1 by A9, GLIB_000:17;
hence e in G1.edgesBetween(V,{v}) by GLIB_000:def 30;
end;
suppose y = v & x in V;
then y in {v} & x in V by TARSKI:def 1;
then e SJoins V,{v},G1 by A9, GLIB_000:17;
hence e in G1.edgesBetween(V,{v}) by GLIB_000:def 30;
end;
end;
assume e in G1.edgesBetween(V,{v});
then A10: e SJoins V,{v},G1 by GLIB_000:def 30;
then A11: e in the_Edges_of G1 by GLIB_000:def 15;
per cases by A10, GLIB_000:def 15;
suppose A12: x in V & y in {v};
then consider e1 being object such that
A13: e1 in E1 & e1 Joins x,v,G1 and
A14: for e2 being object st e2 Joins x,v,G1 holds e1 = e2 by A5;
y = v by A12, TARSKI:def 1;
then e Joins x,v,G1 by A11, GLIB_000:def 13;
hence e in E by A6, A13, A14;
end;
suppose A15: x in {v} & y in V;
then consider e1 being object such that
A16: e1 in E1 & e1 Joins y,v,G1 and
A17: for e2 being object st e2 Joins y,v,G1 holds e1 = e2 by A5;
x = v by A15, TARSKI:def 1;
then e Joins y,v,G1 by A11, GLIB_000:def 13;
hence e in E by A6, A16, A17;
end;
end;
hence thesis by TARSKI:2;
end;
theorem
for G2, v, V for G1 being addAdjVertexAll of G2,v,V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.edgesBetween(V,{v}) misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ G1.edgesBetween(V,{v})
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
G1.edgesBetween(V,{v}) /\ the_Edges_of G2 = {}
proof
assume A2: G1.edgesBetween(V,{v}) /\ the_Edges_of G2 <> {};
set e = the Element of G1.edgesBetween(V,{v}) /\ the_Edges_of G2;
A3: e in G1.edgesBetween(V,{v}) /\ the_Edges_of G2 by A2;
e in G1.edgesBetween(V,{v}) by XBOOLE_0:def 4,A2;
then e SJoins V,{v},G1 by GLIB_000:def 30;
then consider w being object such that
A4: w in V & e Joins w,v,G1 by GLIB_000:102;
e in the_Edges_of G2 by A3, XBOOLE_0:def 4;
then e Joins w,v,G2 by A4, GLIB_006:72;
hence contradiction by A1, GLIB_000:13;
end;
hence G1.edgesBetween(V,{v}) misses the_Edges_of G2 by XBOOLE_0:def 7;
A5: the_Edges_of G2 c= the_Edges_of G1 by GLIB_006:def 9;
A6: the_Edges_of G2 \/ G1.edgesBetween(V,{v}) c= the_Edges_of G1
by A5, XBOOLE_1:8;
for e being object holds e in the_Edges_of G1 implies
e in the_Edges_of G2 \/ G1.edgesBetween(V,{v})
proof
let e be object;
set v1 = (the_Source_of G1).e, v2 = (the_Target_of G1).e;
assume e in the_Edges_of G1;
then A7: e Joins v1,v2,G1 by GLIB_000:def 13;
e in the_Edges_of G2 or e in G1.edgesBetween(V,{v})
proof
assume A8: not e in the_Edges_of G2;
consider E being set such that
A9: card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
per cases by A1, A9, A7, A8, Th51;
suppose v1 = v & v2 in V;
then v1 in {v} & v2 in V by TARSKI:def 1;
then e SJoins V,{v},G1 by A7, GLIB_000:17;
hence thesis by GLIB_000:def 30;
end;
suppose v2 = v & v1 in V;
then v2 in {v} & v1 in V by TARSKI:def 1;
then e SJoins V,{v},G1 by A7, GLIB_000:17;
hence thesis by GLIB_000:def 30;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
then the_Edges_of G1 c= the_Edges_of G2 \/ G1.edgesBetween(V,{v})
by TARSKI:def 3;
hence thesis by A6, XBOOLE_0:def 10;
end;
theorem Th60:
for G3 being _Graph, v being object, V1, V2 being set
for G1 being addAdjVertexAll of G3, v, V1 \/ V2
for G2 being removeEdges of G1, G1.edgesBetween(V2,{v})
st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3
& V1 misses V2
holds G2 is addAdjVertexAll of G3, v, V1
proof
let G3 be _Graph, v be object, V1, V2 be set;
let G1 be addAdjVertexAll of G3, v, V1 \/ V2;
let G2 be removeEdges of G1, G1.edgesBetween(V2,{v});
assume that
A1: V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 and
A2: V1 misses V2;
A3: G1 is Supergraph of G2 by GLIB_006:57;
:: for condition in definition
V1 c= V1 \/ V2 by XBOOLE_1:7;
then A4: V1 c= the_Vertices_of G3 & not v in the_Vertices_of G3 by A1,
XBOOLE_1:1;
:: prepare new edge set
consider E being set such that
A5: card (V1 \/ V2) = card E & E misses the_Edges_of G3 and
A6: the_Edges_of G1 = the_Edges_of G3 \/ E and
A7: for v1 being object st v1 in V1 \/ V2 ex e1 being object st
e1 in E & e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
reconsider F = E \ G1.edgesBetween(V2,{v}) as set;
E = G1.edgesBetween(V1 \/ V2,{v}) by A1, A5, A6, Th58;
then E = G1.edgesBetween(V1,{v}) \/ G1.edgesBetween(V2,{v})
by GLIB_000:105;
then A9: F = G1.edgesBetween(V1,{v}) by XBOOLE_1:88, A2, GLIB_000:104;
for e being object st e in the_Edges_of G3
holds e in the_Edges_of G3 \ G1.edgesBetween(V2,{v})
proof
let e be object;
assume A10: e in the_Edges_of G3;
not e in G1.edgesBetween(V2,{v})
proof
assume e in G1.edgesBetween(V2,{v});
then e SJoins V2,{v},G1 by GLIB_000:def 30;
then consider w being object such that
A11: w in V2 & e Joins w,v,G1 by GLIB_000:102;
w in V1 \/ V2 by A11, XBOOLE_1:7, TARSKI:def 3;
then consider e1 being object such that
A12: e1 in E & e1 Joins w,v,G1 and
A13: for e2 being object st e2 Joins w,v,G1 holds e1 = e2 by A7;
A14: E /\ the_Edges_of G3 = {} by A5, XBOOLE_0:def 7;
e1 = e by A11, A13;
hence contradiction by A10,A12, A14, Lm7;
end;
hence thesis by A10, XBOOLE_0:def 5;
end;
then the_Edges_of G3 c= the_Edges_of G3 \ G1.edgesBetween(V2,{v})
by TARSKI:def 3;
then A15: the_Edges_of G3 \ G1.edgesBetween(V2,{v}) = the_Edges_of G3
by XBOOLE_0:def 10;
A16: the_Edges_of G2
= the_Edges_of G1 \ G1.edgesBetween(V2,{v}) by GLIB_000:53
.= the_Edges_of G3 \/ F by A6, A15, XBOOLE_1:42;
:: show all properties of Definition
A17: now
the_Vertices_of G1 = the_Vertices_of G3 \/ {v} by A1, Def4;
hence the_Vertices_of G2 = the_Vertices_of G3 \/ {v} by GLIB_000:53;
hereby
let e be object;
A18: v is set by TARSKI:1;
thus not e Joins v,v,G2
proof
assume e Joins v,v,G2;
then e Joins v,v,G1 by A3, A18, GLIB_006:70;
hence contradiction by A1, Def4;
end;
let v1 be object;
A19: v1 is set by TARSKI:1;
thus not v1 in V1 implies not e Joins v1,v,G2
proof
assume A20: not v1 in V1;
assume A21: e Joins v1,v,G2;
then A22: e Joins v1,v,G1 by A3, A18, A19, GLIB_006:70;
then v1 in V1 \/ V2 by A1, Def4;
then A23: v1 in V2 by A20, XBOOLE_0:def 3;
v in {v} by TARSKI:def 1;
then e SJoins V2,{v},G1 by A22, A23, GLIB_000:17;
then A24: e in G1.edgesBetween(V2,{v}) by GLIB_000:def 30;
the_Edges_of G2 = the_Edges_of G1 \ G1.edgesBetween(V2,{v})
by GLIB_000:53;
then not e in the_Edges_of G2 by A24, XBOOLE_0:def 5;
hence contradiction by A21, GLIB_000:def 13;
end;
let v2 be object;
A25: v2 is set by TARSKI:1;
assume A26: v1 <> v & v2 <> v;
assume e DJoins v1,v2,G2;
then e DJoins v1,v2,G1 by A3, A19, A25, GLIB_006:70;
hence e DJoins v1,v2,G3 by A1, A26, Def4;
end;
take F;
reconsider W = V1 as Subset of V1 \/ V2 by XBOOLE_1:7;
consider f being Function of W, G1.edgesBetween(W,{v}) such that
A27: f is one-to-one onto and
for w being object st w in W holds f.w Joins w,v,G1 by A1, Th57;
A28: dom f = W
proof
per cases;
suppose G1.edgesBetween(W,{v}) <> {};
hence thesis by FUNCT_2:def 1;
end;
suppose A29: G1.edgesBetween(W,{v}) = {};
then dom f = {};
hence thesis by A29, A1, Lm12;
end;
end;
rng f = G1.edgesBetween(W,{v}) by A27, FUNCT_2:def 3;
hence card V1 = card F by A9, CARD_1:5,A27, A28, WELLORD2:def 4;
thus F misses the_Edges_of G3 by A5, XBOOLE_1:63;
thus the_Edges_of G2 = the_Edges_of G3 \/ F by A16;
let v1 be object;
assume A30: v1 in V1;
then v1 in V1 \/ V2 by XBOOLE_0:def 3;
then consider e1 being object such that
A31: e1 in E & e1 Joins v1,v,G1 and
A32: for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A7;
take e1;
v in {v} by TARSKI:def 1;
then e1 SJoins V1,{v},G1 by A30, A31, GLIB_000:17;
hence e1 in F by A9, GLIB_000:def 30;
then A33: e1 in the_Edges_of G2 by A16, XBOOLE_0:def 3;
thus e1 Joins v1,v,G2
proof
reconsider e3 = e1 as set by TARSKI:1;
A34: ((the_Source_of G1).e1 = v1 & (the_Target_of G1).e1 = v) or
((the_Source_of G1).e1 = v & (the_Target_of G1).e1 = v1)
by A31, GLIB_000:def 13;
(the_Source_of G1).e3 = (the_Source_of G2).e3 &
(the_Target_of G1).e3 = (the_Target_of G2).e3
by A33, GLIB_000:def 32;
hence e1 Joins v1,v,G2 by A33, GLIB_000:def 13, A34;
end;
let e2 be object;
assume A35: e2 Joins v1,v,G2;
v1 is set & v is set by TARSKI:1;
hence e1 = e2 by A32,A35, GLIB_000:72;
end;
:: show supergraph property
G2 is Supergraph of G3
proof
A36: the_Vertices_of G3 c= the_Vertices_of G2 by A17, XBOOLE_1:7;
A37: the_Edges_of G3 c= the_Edges_of G2 by A16, XBOOLE_1:7;
now
let e be set;
assume A38: e in the_Edges_of G3;
then A39: e in the_Edges_of G2 by A37;
thus (the_Source_of G3).e = (the_Source_of G1).e by A38, GLIB_006:def 9
.= (the_Source_of G2).e by A39, GLIB_000:def 32;
thus (the_Target_of G3).e = (the_Target_of G1).e by A38, GLIB_006:def 9
.= (the_Target_of G2).e by A39, GLIB_000:def 32;
end;
hence thesis by A36, A37, GLIB_006:def 9;
end;
hence thesis by A4, A17, Def4;
end;
theorem
for G3 being _Graph, v being object, V being set, v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1}
st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V
ex G2 being addAdjVertexAll of G3,v,V, e being object
st not e in the_Edges_of G2 &
(G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v)
proof
let G3 be _Graph, v be object, V be set, v1 be Vertex of G3;
let G1 be addAdjVertexAll of G3,v,V \/ {v1};
assume that
A1: V c= the_Vertices_of G3 & not v in the_Vertices_of G3 and
A2: not v1 in V;
set G2 = the removeEdges of G1,G1.edgesBetween({v1},{v});
A3: V \/ {v1} c= the_Vertices_of G3 by A1, XBOOLE_1:8;
V misses {v1} by A2, ZFMISC_1:50;
then reconsider G2 as addAdjVertexAll of G3,v,V by A1, A3, Th60;
take G2;
reconsider W = {v1} as Subset of V \/ {v1} by XBOOLE_1:7;
consider f being Function of W,G1.edgesBetween(W,{v}) such that
A4: f is one-to-one onto and
A5: for w being object st w in W holds f.w Joins w,v,G1
by A1, A3, Th57;
take f.v1;
v1 in {v1} by TARSKI:def 1;
then A6: f.v1 Joins v1,v,G1 by A5;
thus not f.v1 in the_Edges_of G2
proof
v1 in {v1} & v in {v} by TARSKI:def 1;
then f.v1 SJoins {v1},{v},G1 by A6, GLIB_000:17;
then f.v1 in G1.edgesBetween({v1},{v}) by GLIB_000:def 30;
then not f.v1 in the_Edges_of G1 \ G1.edgesBetween({v1},{v})
by XBOOLE_0:def 5;
hence thesis by GLIB_000:53;
end;
A7: G1 is Supergraph of G2 by GLIB_006:57;
:: vertices stay the same
A8: the_Vertices_of G2 = the_Vertices_of G3 \/ {v} by A1, Def4;
A9: the_Vertices_of G1 = the_Vertices_of G3 \/ {v} by A1, A3, Def4;
then A10: the_Vertices_of G1 = the_Vertices_of G2 by A8;
for w being object st w in dom f holds f.w = f.v1 by TARSKI:def 1;
then f = dom f --> f.v1 by FUNCOP_1:11;
then rng f c= {f.v1} by FUNCOP_1:13;
then A11: G1.edgesBetween(W,{v}) c= {f.v1} by A4, FUNCT_2:def 3;
v1 in {v1} & v in {v} by TARSKI:def 1;
then f.v1 SJoins W,{v},G1 by A6, GLIB_000:17;
then f.v1 in G1.edgesBetween(W,{v}) by GLIB_000:def 30;
then {f.v1} c= G1.edgesBetween(W,{v}) by ZFMISC_1:31;
then A12: G1.edgesBetween(W,{v}) = {f.v1} by A11, XBOOLE_0:def 10;
:: one edge added
A13: f.v1 in the_Edges_of G1 by A6, GLIB_000:def 13;
A14: the_Edges_of G2 = the_Edges_of G1 \ {f.v1} by A12, GLIB_000:53;
then A15: the_Edges_of G1 = the_Edges_of G2 \/ {f.v1} by A13, ZFMISC_1:116;
f.v1 in {f.v1} by TARSKI:def 1;
then A16: not f.v1 in the_Edges_of G2 by A14, XBOOLE_0:def 5;
A17: v1 in the_Vertices_of G1 by A9, XBOOLE_0:def 3;
v is Vertex of G1 by A1, A3, Th50;
then A18: v1 in the_Vertices_of G2 & v in the_Vertices_of G2
by A17, A10;
A19: G1 is Supergraph of G2 & the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {f.v1} by A7, A10, A15;
:: Now we just need to show that adding the edge
:: "repairs" what we removed
per cases by A6, GLIB_000:16;
suppose A20: f.v1 DJoins v1,v,G1;
A21: dom the_Source_of G1 = the_Edges_of G1 by GLIB_000:4
.= the_Edges_of G2 \/ dom ({f.v1} --> v1) by A15
.= (dom the_Source_of G2) \/ dom ({f.v1} --> v1) by GLIB_000:4
.= (dom the_Source_of G2) \/ dom (f.v1 .--> v1) by FUNCOP_1:def 9
.= dom (the_Source_of G2 +* (f.v1 .--> v1)) by FUNCT_4:def 1;
for e being object st e in dom the_Source_of G1 holds
(the_Source_of G1).e = (the_Source_of G2 +* (f.v1 .--> v1)).e
proof
let e be object;
assume e in dom the_Source_of G1;
then per cases by A15, XBOOLE_0:def 3;
suppose A22: e in the_Edges_of G2;
then not e in {f.v1} by A14, XBOOLE_0:def 5;
then A23: e <> f.v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Source_of G1).e
= (the_Source_of G2).e1 by A22, GLIB_000:def 32
.= (the_Source_of G2 +* (f.v1 .--> v1)).e by A23, FUNCT_4:83;
end;
suppose e in {f.v1};
then A24: e = f.v1 by TARSKI:def 1;
hence (the_Source_of G1).e
= v1 by A20, GLIB_000:def 14
.= (the_Source_of G2 +* (f.v1 .--> v1)).e by A24, FUNCT_4:113;
end;
end;
then A25: the_Source_of G1 = the_Source_of G2 +* (f.v1 .--> v1)
by A21, FUNCT_1:2;
A26: dom the_Target_of G1 = the_Edges_of G1 by GLIB_000:4
.= the_Edges_of G2 \/ dom ({f.v1} --> v) by A15
.= (dom the_Target_of G2) \/ dom ({f.v1} --> v) by GLIB_000:4
.= (dom the_Target_of G2) \/ dom (f.v1 .--> v) by FUNCOP_1:def 9
.= dom (the_Target_of G2 +* (f.v1 .--> v)) by FUNCT_4:def 1;
for e being object st e in dom the_Target_of G1 holds
(the_Target_of G1).e = (the_Target_of G2 +* (f.v1 .--> v)).e
proof
let e be object;
assume e in dom the_Target_of G1;
then per cases by A15, XBOOLE_0:def 3;
suppose A27: e in the_Edges_of G2;
then not e in {f.v1} by A14, XBOOLE_0:def 5;
then A28: e <> f.v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Target_of G1).e
= (the_Target_of G2).e1 by A27, GLIB_000:def 32
.= (the_Target_of G2 +* (f.v1 .--> v)).e by A28, FUNCT_4:83;
end;
suppose e in {f.v1};
then A29: e = f.v1 by TARSKI:def 1;
hence (the_Target_of G1).e
= v by A20, GLIB_000:def 14
.= (the_Target_of G2 +* (f.v1 .--> v)).e by A29, FUNCT_4:113;
end;
end;
then the_Target_of G1 = the_Target_of G2 +* (f.v1 .--> v)
by A26, FUNCT_1:2;
hence thesis by A16, A25, A19, A18, GLIB_006:def 11;
end;
suppose A30: f.v1 DJoins v,v1,G1;
A31: dom the_Target_of G1 = the_Edges_of G1 by GLIB_000:4
.= the_Edges_of G2 \/ dom ({f.v1} --> v1) by A15
.= (dom the_Target_of G2) \/ dom ({f.v1} --> v1) by GLIB_000:4
.= (dom the_Target_of G2) \/ dom (f.v1 .--> v1) by FUNCOP_1:def 9
.= dom (the_Target_of G2 +* (f.v1 .--> v1)) by FUNCT_4:def 1;
for e being object st e in dom the_Target_of G1 holds
(the_Target_of G1).e = (the_Target_of G2 +* (f.v1 .--> v1)).e
proof
let e be object;
assume e in dom the_Target_of G1;
then per cases by A15, XBOOLE_0:def 3;
suppose A32: e in the_Edges_of G2;
then not e in {f.v1} by A14, XBOOLE_0:def 5;
then A33: e <> f.v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Target_of G1).e
= (the_Target_of G2).e1 by A32, GLIB_000:def 32
.= (the_Target_of G2 +* (f.v1 .--> v1)).e by A33, FUNCT_4:83;
end;
suppose e in {f.v1};
then A34: e = f.v1 by TARSKI:def 1;
hence (the_Target_of G1).e
= v1 by A30, GLIB_000:def 14
.= (the_Target_of G2 +* (f.v1 .--> v1)).e by A34, FUNCT_4:113;
end;
end;
then A35: the_Target_of G1 = the_Target_of G2 +* (f.v1 .--> v1)
by A31, FUNCT_1:2;
A36: dom the_Source_of G1 = the_Edges_of G1 by GLIB_000:4
.= the_Edges_of G2 \/ dom ({f.v1} --> v) by A15
.= (dom the_Source_of G2) \/ dom ({f.v1} --> v) by GLIB_000:4
.= (dom the_Source_of G2) \/ dom (f.v1 .--> v) by FUNCOP_1:def 9
.= dom (the_Source_of G2 +* (f.v1 .--> v)) by FUNCT_4:def 1;
for e being object st e in dom the_Source_of G1 holds
(the_Source_of G1).e = (the_Source_of G2 +* (f.v1 .--> v)).e
proof
let e be object;
assume e in dom the_Source_of G1;
then per cases by A15, XBOOLE_0:def 3;
suppose A37: e in the_Edges_of G2;
then not e in {f.v1} by A14, XBOOLE_0:def 5;
then A38: e <> f.v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Source_of G1).e
= (the_Source_of G2).e1 by A37, GLIB_000:def 32
.= (the_Source_of G2 +* (f.v1 .--> v)).e by A38, FUNCT_4:83;
end;
suppose e in {f.v1};
then A39: e = f.v1 by TARSKI:def 1;
hence (the_Source_of G1).e
= v by A30, GLIB_000:def 14
.= (the_Source_of G2 +* (f.v1 .--> v)).e by A39, FUNCT_4:113;
end;
end;
then the_Source_of G1 = the_Source_of G2 +* (f.v1 .--> v)
by A36, FUNCT_1:2;
hence thesis by A16, A35, A19, A18, GLIB_006:def 11;
end;
end;
theorem
for G3 being _Graph, v being object, V being set, v1 being Vertex of G3
for e being object, G2 being addAdjVertexAll of G3,v,V
st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V &
not e in the_Edges_of G2
for G1 being _Graph
st G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1
holds G1 is addAdjVertexAll of G3,v,V \/ {v1}
proof
let G3 be _Graph, v be object, V be set, v1 be Vertex of G3, e be object;
let G2 be addAdjVertexAll of G3,v,V;
assume that
A1: V c= the_Vertices_of G3 & not v in the_Vertices_of G3 and
A2: not v1 in V & not e in the_Edges_of G2;
:: show the cardinality property
consider E being set such that
A3: card V = card E & E misses the_Edges_of G3 &
the_Edges_of G2 = the_Edges_of G3 \/ E and
A4: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G2 &
for e2 being object st e2 Joins v1,v,G2 holds e1 = e2 by A1, Def4;
consider f being Function such that
A5: f is one-to-one & dom f = E & rng f = V
by WELLORD2:def 4,A3,CARD_1:5;
set f1 = f +* (e .--> v1);
reconsider E1 = E \/ {e}, V1 = V \/ {v1} as set;
A6: dom f1 = dom f \/ dom (e .--> v1) by FUNCT_4:def 1
.= dom f \/ dom ({e} --> v1) by FUNCOP_1:def 9
.= E1 by A5;
e is set & v1 is set by TARSKI:1;
then A7: rng (e .--> v1) = {v1} by FUNCOP_1:88;
then A8: rng f \/ rng (e .--> v1) = V \/ {v1} by A5;
rng f /\ rng (e .--> v1) = {}
proof
assume A9: rng f /\ rng (e .--> v1) <> {};
set x = the Element of rng f /\ rng (e .--> v1);
x in V & x in {v1} by XBOOLE_0:def 4,A5,A7,A9;
hence contradiction by A2, TARSKI:def 1;
end;
then A10: f1 is one-to-one by A5, XBOOLE_0:def 7, FUNCT_4:92;
for w being object holds w in rng f \/ rng (e .--> v1) implies w in rng f1
proof
let w be object;
assume w in rng f \/ rng (e .--> v1);
then per cases by XBOOLE_0:def 3;
suppose w in rng f;
then consider x being object such that
A11: x in dom f & w = f.x by FUNCT_1:def 3;
x in E by A5, A11;
then x <> e by A2, A3, XBOOLE_0:def 3;
then A13: f1.x = w by A11, FUNCT_4:83;
x in E1 by A5,A11,XBOOLE_0:def 3;
hence w in rng f1 by A6, A13, FUNCT_1:def 3;
end;
suppose w in rng (e .--> v1);
hence thesis by FUNCT_4:18, TARSKI:def 3;
end;
end;
then A14: rng f \/ rng (e .--> v1) c= rng f1 by TARSKI:def 3;
rng f1 c= rng f \/ rng (e .--> v1) by FUNCT_4:17;
then rng f1 = rng f \/ rng (e .--> v1) by A14, XBOOLE_0:def 10;
then A15: card E1 = card V1 by A8, A10, A6, WELLORD2:def 4, CARD_1:5;
:: show other E properties
A16: the_Edges_of G2 /\ {e} = {} by A2, ZFMISC_1:50, XBOOLE_0:def 7;
the_Edges_of G3 c= the_Edges_of G2 by GLIB_006:def 9;
then the_Edges_of G3 /\ {e} c= the_Edges_of G2 /\ {e} by XBOOLE_1:26;
then A17: the_Edges_of G3 /\ {e} = {} by A16;
the_Edges_of G3 /\ E1 = the_Edges_of G3 /\ {e} by XBOOLE_1:78,A3;
then A18: E1 misses the_Edges_of G3 by A17, XBOOLE_0:def 7;
A19: the_Edges_of G3 \/ E1 = the_Edges_of G2 \/ {e} by A3, XBOOLE_1:4;
v is Vertex of G2 & v1 is Vertex of G3 by A1, Th50;
then A20: v in the_Vertices_of G2 & v1 is Vertex of G2 by GLIB_006:68;
A21: V1 c= the_Vertices_of G3 by A1, XBOOLE_1:8;
let G1 be _Graph;
:: the rest of the properties has to be shown step by step
assume G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1;
then per cases;
suppose A22: G1 is addEdge of G2,v1,e,v;
then A23: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v)
by A20, A2, GLIB_006:def 11;
A24: G1 is Supergraph of G3 by A22, GLIB_006:62;
now
thus the_Vertices_of G1 = the_Vertices_of G3 \/ {v} by A23,A1, Def4;
hereby
let e3 be object;
thus not e3 Joins v,v,G1
proof
assume A25: e3 Joins v,v,G1;
then per cases by A22, GLIB_006:72;
suppose e3 Joins v,v,G2;
hence contradiction by A1, Def4;
end;
suppose not e3 in the_Edges_of G2;
then v1 = v by A2, A20, A22, A25, GLIB_006:107;
hence contradiction by A1;
end;
end;
let v3 be object;
thus not v3 in V1 implies not e3 Joins v3,v,G1
proof
assume not v3 in V1;
then A26: not v3 in V & not v3 in {v1} by XBOOLE_0:def 3;
assume A27: e3 Joins v3,v,G1;
then per cases by A22, GLIB_006:72;
suppose e3 Joins v3,v,G2;
hence contradiction by A1, A26, Def4;
end;
suppose not e3 in the_Edges_of G2;
then per cases by A2, A20, A22, A27, GLIB_006:107;
suppose v3 = v1 & v = v;
hence contradiction by A26, TARSKI:def 1;
end;
suppose v3 = v & v = v1;
hence contradiction by A1;
end;
end;
end;
let v2 be object;
assume A28: v3 <> v & v2 <> v & e3 DJoins v3,v2,G1;
then per cases by A24, GLIB_006:71;
suppose e3 DJoins v3,v2,G3;
hence e3 DJoins v3,v2,G3;
end;
suppose not e3 in the_Edges_of G3;
per cases by A22, A28, GLIB_006:71;
suppose e3 DJoins v3,v2,G2;
hence e3 DJoins v3,v2,G3 by A28, A1, Def4;
end;
suppose A29: not e3 in the_Edges_of G2;
e3 Joins v3,v2,G1 by A28, GLIB_000:16;
then (v3 = v1 & v2 = v) or (v3 = v & v2 = v1)
by A2, A20, A22, A29, GLIB_006:107;
hence e3 DJoins v3,v2,G3 by A28; :: by contradiction
end;
end;
end;
take E1;
thus card V1 = card E1 by A15;
thus E1 misses the_Edges_of G3 by A18;
thus the_Edges_of G1 = the_Edges_of G3 \/ E1 by A19, A23;
let v3 be object;
assume A30: v3 in V1;
thus ex e1 being object st e1 in E1 & e1 Joins v3,v,G1 &
for e2 being object st e2 Joins v3,v,G1 holds e1 = e2
proof
per cases by A30, XBOOLE_0:def 3;
suppose A31: v3 in V;
then consider e1 being object such that
A32: e1 in E & e1 Joins v3,v,G2 and
A33: for e2 being object st e2 Joins v3,v,G2 holds e1 = e2 by A4;
take e1;
thus e1 in E1 by A32, XBOOLE_0:def 3;
v3 is set & v is set by TARSKI:1;
hence e1 Joins v3,v,G1 by A22, A32, GLIB_006:70;
let e2 be object;
assume A34: e2 Joins v3,v,G1;
then per cases by A22, GLIB_006:72;
suppose e2 Joins v3,v,G2;
hence e1 = e2 by A33;
end;
suppose not e2 in the_Edges_of G2;
then per cases by A2, A20, A22, A34, GLIB_006:107;
suppose v3 = v1 & v = v;
hence thesis by A2, A31; :: by contradiction
end;
suppose v3 = v & v = v1;
hence thesis by A1; :: by contradiction
end;
end;
end;
suppose v3 in {v1};
then A35: v3 = v1 by TARSKI:def 1;
take e;
e in {e} by TARSKI:def 1;
hence e in E1 by XBOOLE_0:def 3;
e DJoins v1,v,G1 by A2, A20, A22, GLIB_006:105;
hence e Joins v3,v,G1 by A35, GLIB_000:16;
let e2 be object;
assume A36: e2 Joins v3,v,G1;
then per cases by A22, GLIB_006:72, A35;
suppose e2 Joins v1,v,G2;
hence thesis by A2, A1, Def4; :: by contradiction (not v1 in V)
end;
suppose not e2 in the_Edges_of G2;
hence e = e2 by A2, A20, A22, A36, GLIB_006:106;
end;
end;
end;
end;
hence thesis by A24, A21, A1, Def4;
end;
suppose A37: G1 is addEdge of G2,v,e,v1;
then A38: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v1)
by A20, A2, GLIB_006:def 11;
A39: G1 is Supergraph of G3 by A37, GLIB_006:62;
now
thus the_Vertices_of G1 = the_Vertices_of G3 \/ {v} by A1, A38, Def4;
hereby
let e3 be object;
thus not e3 Joins v,v,G1
proof
assume A40: e3 Joins v,v,G1;
then per cases by A37, GLIB_006:72;
suppose e3 Joins v,v,G2;
hence contradiction by A1, Def4;
end;
suppose not e3 in the_Edges_of G2;
then v1 = v by A2, A20, A37, A40, GLIB_006:107;
hence contradiction by A1;
end;
end;
let v3 be object;
thus not v3 in V1 implies not e3 Joins v3,v,G1
proof
assume not v3 in V1;
then A41: not v3 in V & not v3 in {v1} by XBOOLE_0:def 3;
assume A42: e3 Joins v3,v,G1;
then per cases by A37, GLIB_006:72;
suppose e3 Joins v3,v,G2;
hence contradiction by A1, A41, Def4;
end;
suppose not e3 in the_Edges_of G2;
then per cases by A2, A20, A37, A42, GLIB_006:107;
suppose v3 = v & v = v1;
hence contradiction by A1;
end;
suppose v3 = v1 & v = v;
hence contradiction by A41, TARSKI:def 1;
end;
end;
end;
let v2 be object;
assume A43: v3 <> v & v2 <> v & e3 DJoins v3,v2,G1;
then per cases by A39, GLIB_006:71;
suppose e3 DJoins v3,v2,G3;
hence e3 DJoins v3,v2,G3;
end;
suppose not e3 in the_Edges_of G3;
per cases by A37, A43, GLIB_006:71;
suppose e3 DJoins v3,v2,G2;
hence e3 DJoins v3,v2,G3 by A43, A1, Def4;
end;
suppose A44: not e3 in the_Edges_of G2;
e3 Joins v3,v2,G1 by A43, GLIB_000:16;
then (v3 = v & v2 = v1) or (v3 = v1 & v2 = v)
by A2, A20, A37, A44, GLIB_006:107;
hence e3 DJoins v3,v2,G3 by A43; :: by contradiction
end;
end;
end;
take E1;
thus card V1 = card E1 by A15;
thus E1 misses the_Edges_of G3 by A18;
thus the_Edges_of G1 = the_Edges_of G3 \/ E1 by A19, A38;
let v3 be object;
assume A45: v3 in V1;
thus ex e1 being object st e1 in E1 & e1 Joins v3,v,G1 &
for e2 being object st e2 Joins v3,v,G1 holds e1 = e2
proof
per cases by A45, XBOOLE_0:def 3;
suppose A46: v3 in V;
then consider e1 being object such that
A47: e1 in E & e1 Joins v3,v,G2 and
A48: for e2 being object st e2 Joins v3,v,G2 holds e1 = e2 by A4;
take e1;
thus e1 in E1 by A47, XBOOLE_0:def 3;
v3 is set & v is set by TARSKI:1;
hence e1 Joins v3,v,G1 by A37, A47, GLIB_006:70;
let e2 be object;
assume A49: e2 Joins v3,v,G1;
then per cases by A37, GLIB_006:72;
suppose e2 Joins v3,v,G2;
hence e1 = e2 by A48;
end;
suppose not e2 in the_Edges_of G2;
then per cases by A2, A20, A37, A49, GLIB_006:107;
suppose v3 = v & v = v1;
hence thesis by A1; :: by contradiction
end;
suppose v3 = v1 & v = v;
hence thesis by A2, A46; :: by contradiction
end;
end;
end;
suppose v3 in {v1};
then A50: v3 = v1 by TARSKI:def 1;
take e;
e in {e} by TARSKI:def 1;
hence e in E1 by XBOOLE_0:def 3;
e DJoins v,v1,G1 by A2, A20, A37, GLIB_006:105;
hence e Joins v3,v,G1 by A50, GLIB_000:16;
let e2 be object;
assume A51: e2 Joins v3,v,G1;
then per cases by A50, A37, GLIB_006:72;
suppose e2 Joins v1,v,G2;
hence thesis by A2, A1, Def4; :: by contradiction (not v1 in V)
end;
suppose not e2 in the_Edges_of G2;
hence e = e2 by A2, A20, A37, A51, GLIB_006:106;
end;
end;
end;
end;
hence thesis by A39, A21, A1, Def4;
end;
end;
Lm13: for k being odd Element of NAT st 1 < k holds k-2 is odd Element of NAT
proof
let k be odd Element of NAT;
assume A1: 1 < k;
consider i being Nat such that
A2: k = 2*i+1 by ABIAN:9;
0 <> i by A1, A2;
then reconsider j = i-1 as Nat by CHORD:1;
k-2 = 2*j+1 by A2;
hence thesis;
end;
theorem Th63:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V, W being Walk of G1
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds
(W.edges() c= the_Edges_of G2 & W is non trivial implies
not v in W.vertices())
& (not v in W.vertices() implies W.edges() c= the_Edges_of G2)
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2,v,V;
let W be Walk of G1;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
consider E being set such that
A2: card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A3: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
A4: E /\ the_Edges_of G2 = {} by A2, XBOOLE_0:def 7;
hereby
assume A5: W.edges() c= the_Edges_of G2 & W is non trivial;
thus not v in W.vertices()
proof
assume v in W.vertices();
then consider n being odd Element of NAT such that
A6: n <= len W & W.n = v by GLIB_001:87;
per cases by A6, XXREAL_0:1;
suppose A7: n = len W;
A8: 1 <> len W by A5, GLIB_001:126;
1 <= len W by ABIAN:12;
then 1 < len W by A8, XXREAL_0:1;
then reconsider m = len W - 2 as odd Element of NAT by Lm13;
A9: m < len W - 0 by XREAL_1:15;
then W.(m+1) Joins W.m,W.(m+2),G1 by GLIB_001:def 3;
then A10: W.(m+1) Joins W.m,v,G1 by A6, A7;
then W.m in V by A1, Def4;
then consider e1 being object such that
A11: e1 in E & e1 Joins W.m,v,G1 and
A12: for e2 being object st e2 Joins W.m,v,G1 holds e1 = e2 by A3;
W.(m+1) in E by A10, A11, A12;
then not W.(m+1) in W.edges() by A5,A4,Lm7;
hence contradiction by A9, GLIB_001:100;
end;
suppose A13: n < len W;
then A14: W.(n+1) Joins W.(n+2),v,G1 by A6,GLIB_000:14,GLIB_001:def 3;
then W.(n+2) in V by A1, Def4;
then consider e1 being object such that
A15: e1 in E & e1 Joins W.(n+2),v,G1 and
A16: for e2 being object st e2 Joins W.(n+2),v,G1 holds e1 = e2 by A3
;
W.(n+1) in E by A14, A15, A16;
then not W.(n+1) in W.edges() by A5,A4,Lm7;
hence contradiction by A13, GLIB_001:100;
end;
end;
end;
assume A17: not v in W.vertices();
for e being object holds e in W.edges() implies e in the_Edges_of G2
proof
let e be object;
assume e in W.edges();
then consider n being odd Element of NAT such that
A18: n < len W & W.(n+1) = e by GLIB_001:100;
A19: e Joins W.n,W.(n+2),G1 by A18, GLIB_001:def 3;
W.n <> v & W.(n+2) <> v
proof
thus W.n <> v by A17, A18, GLIB_001:87;
A20: n+2 <= len W by A18, GLIB_001:1;
assume W.(n+2) = v;
hence contradiction by A17,A20, GLIB_001:87;
end;
then e Joins W.n,W.(n+2),G2 by A19, A1, Th49;
hence thesis by GLIB_000:def 13;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th64:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V, W being Walk of G1
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
((W.edges() c= the_Edges_of G2 & W is non trivial)
or not v in W.vertices())
holds W is Walk of G2
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2,v,V;
let W be Walk of G1;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: (W.edges() c= the_Edges_of G2 & W is non trivial)
or not v in W.vertices();
A3: W.edges() c= the_Edges_of G2 & not v in W.vertices() by A1, A2, Th63;
for w being object holds w in W.vertices() implies w in the_Vertices_of G2
proof
let w be object;
assume A4: w in W.vertices();
then A5: w in the_Vertices_of G1;
assume A6: not w in the_Vertices_of G2;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
then w in {v} by A5, A6, XBOOLE_0:def 3;
hence contradiction by A4, A3, TARSKI:def 1;
end;
then A7: W.vertices() c= the_Vertices_of G2 by TARSKI:def 3;
rng W = W.vertices() \/ W.edges() by GLIB_001:101;
then A8: W is FinSequence of the_Vertices_of G2 \/ the_Edges_of G2
by FINSEQ_1:def 4,A7, A3, XBOOLE_1:13;
now
thus len W is odd;
W.first() in W.vertices() by GLIB_001:88;
then W.1 in W.vertices() by GLIB_001:def 6;
hence W.1 in the_Vertices_of G2 by A7;
let n be odd Element of NAT;
assume A9: n < len W;
then A10: W.(n+1) Joins W.n,W.(n+2),G1 by GLIB_001:def 3;
W.(n+1) in W.edges() by A9, GLIB_001:100;
hence W.(n+1) Joins W.n,W.(n+2),G2 by A10, GLIB_006:72, A3;
end;
hence thesis by A8, GLIB_001:def 3;
end;
theorem Th65:
for G2, v, V for G1 being addAdjVertexAll of G2,v,V, W being Walk of G1
st W.vertices() c= the_Vertices_of G2
holds W.edges() c= the_Edges_of G2
proof
let G2,v,V;
let G1 be addAdjVertexAll of G2,v,V;
let W be Walk of G1;
assume A1: W.vertices() c= the_Vertices_of G2;
per cases;
suppose A2: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then not v in W.vertices() by A1;
hence thesis by A2, Th63;
end;
suppose not (V c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then G1 == G2 by Def4;
then the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
hence thesis;
end;
end;
theorem
for G, v, V for G1, G2 being addAdjVertexAll of G,v,V
holds the_Vertices_of G1 = the_Vertices_of G2 &
for v1 being Vertex of G1 holds v1 is Vertex of G2
proof
let G,v,V;
let G1,G2 be addAdjVertexAll of G,v,V;
thus the_Vertices_of G1 = the_Vertices_of G2
proof
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v} &
the_Vertices_of G2 = the_Vertices_of G \/ {v} by Def4;
hence thesis;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G & G2 == G by Def4;
then G1 == G2 by GLIB_000:85;
hence thesis by GLIB_000:def 34;
end;
end;
hence thesis;
end;
theorem Th67:
for G, v, V for G1, G2 being addAdjVertexAll of G,v,V
for v1,e1,v2 being object st e1 Joins v1,v2,G1
ex e2 being object st e2 Joins v1,v2,G2
proof
let G,v,V;
let G1,G2 be addAdjVertexAll of G,v,V;
let v1,e1,v2 be object;
assume A1: e1 Joins v1,v2,G1;
per cases;
suppose A2: V c= the_Vertices_of G & not v in the_Vertices_of G;
then consider E2 being set such that
card V = card E2 & E2 misses the_Edges_of G &
the_Edges_of G2 = the_Edges_of G \/ E2 and
A3: for w1 being object st w1 in V ex e3 being object st e3 in E2 &
e3 Joins w1,v,G2 &
for e2 being object st e2 Joins w1,v,G2 holds e3 = e2
by Def4;
per cases;
suppose v1 = v & v2 = v;
hence thesis by A2, Def4, A1;
end;
suppose A4: v1 = v & v2 <> v;
per cases;
suppose not v2 in V;
then not e1 Joins v2,v,G1 by A2, Def4;
hence thesis by A1,A4, GLIB_000:14;
end;
suppose v2 in V;
then consider e3 being object such that
A5: e3 in E2 & e3 Joins v2,v,G2 and
for e2 being object st e2 Joins v2,v,G2 holds e3 = e2 by A3;
take e3;
thus e3 Joins v1,v2,G2 by A5, A4, GLIB_000:14;
end;
end;
suppose A6: v1 <> v & v2 = v;
per cases;
suppose not v1 in V;
hence thesis by A1,A2, A6, Def4;
end;
suppose v1 in V;
then consider e3 being object such that
A7: e3 in E2 & e3 Joins v1,v,G2 and
for e2 being object st e2 Joins v1,v,G2 holds e3 = e2 by A3;
take e3;
thus e3 Joins v1,v2,G2 by A7, A6;
end;
end;
suppose A8: v1 <> v & v2 <> v;
A9: e1 Joins v1,v2,G
proof
e1 DJoins v1,v2,G1 or e1 DJoins v2,v1,G1 by A1, GLIB_000:16;
then e1 DJoins v1,v2,G or e1 DJoins v2,v1,G by A2, A8, Def4;
hence thesis by GLIB_000:16;
end;
take e1;
reconsider w1=v1, w2=v2 as set by TARSKI:1;
e1 Joins w1,w2,G2 by A9, GLIB_006:70;
hence thesis;
end;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G & G2 == G by Def4;
then A10: G1 == G2 by GLIB_000:85;
take e1;
thus thesis by A1, A10, GLIB_000:88;
end;
end;
:: The closest analogon we can get for
:: theorem for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V
:: holds G1 == G2
:: but also preparation for
:: registration let G, v, V; let G1 being addAdjVertexAll of G,v,V;
:: cluster -> G1-isomorphic for addAdjVertexAll of G,v,V;
:: coming soon
theorem
for G, v, V for G1, G2 being addAdjVertexAll of G,v,V
ex f being Function of the_Edges_of G1, the_Edges_of G2
st f|the_Edges_of G = id the_Edges_of G & f is one-to-one onto &
for v1,e,v2 being object st e Joins v1,v2,G1 holds f.e Joins v1,v2,G2
proof
let G,v,V;
let G1,G2 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
:: define an appropiate function using the theorem before
defpred P[object,object] means
for v1,v2 being object st $1 Joins v1,v2,G1 holds $2 Joins v1,v2,G2;
A2: for e1 being object st e1 in the_Edges_of G1
ex e2 being object st e2 in the_Edges_of G2 & P[e1,e2]
proof
let e1 be object;
assume e1 in the_Edges_of G1;
then e1 Joins (the_Source_of G1).e1, (the_Target_of G1).e1,G1
by GLIB_000:def 13;
then consider e2 being object such that
A3: e2 Joins (the_Source_of G1).e1, (the_Target_of G1).e1,G2 by Th67;
take e2;
thus e2 in the_Edges_of G2 by A3, GLIB_000:def 13;
let v1, v2 be object;
assume e1 Joins v1, v2,G1;
then per cases by GLIB_000:def 13;
suppose (the_Source_of G1).e1 = v1 & (the_Target_of G1).e1 = v2;
hence e2 Joins v1,v2,G2 by A3;
end;
suppose (the_Source_of G1).e1 = v2 & (the_Target_of G1).e1 = v1;
hence e2 Joins v1,v2,G2 by A3, GLIB_000:14;
end;
end;
consider f1 being Function of the_Edges_of G1, the_Edges_of G2 such that
A4: for e1 being object st e1 in the_Edges_of G1 holds P[e1,f1.e1]
from FUNCT_2:sch 1(A2);
:: On the old graph the function doesn't have to be the identity
:: but could be some other automorphism that leaves the vertices in V
:: unchanged, so we need to correct that.
set f = f1 +* id the_Edges_of G;
:: show that the function has the correct domain and range
:: (I tried using the clustering from FUNCT_4 but it didn't work out.)
A5: the_Edges_of G c= the_Edges_of G1 by GLIB_006:def 9;
A6: dom f1 = the_Edges_of G1
proof
per cases;
suppose V <> {};
then the_Edges_of G2 <> {} by A1, Th47;
hence thesis by FUNCT_2:def 1;
end;
suppose A7: the_Edges_of G <> {};
the_Edges_of G2 <> {}
proof
assume A8: the_Edges_of G2 = {};
the_Edges_of G c= the_Edges_of G2 by GLIB_006:def 9;
hence contradiction by A7, A8;
end;
hence thesis by FUNCT_2:def 1;
end;
suppose V = {} & the_Edges_of G = {};
then the_Edges_of G1 = {} & the_Edges_of G2 = {} by Lm11;
hence thesis;
end;
end;
A9: dom f = dom f1 \/ dom id the_Edges_of G by FUNCT_4:def 1
.= the_Edges_of G1 by A5, A6, XBOOLE_1:12;
A10: rng id the_Edges_of G c= the_Edges_of G2
by GLIB_006:def 9;
A11: rng f1 \/ rng id the_Edges_of G c= the_Edges_of G2
by A10, XBOOLE_1:8;
rng f c= rng f1 \/ rng id the_Edges_of G by FUNCT_4:17;
then reconsider f as Function of the_Edges_of G1, the_Edges_of G2
by A9, FUNCT_2:2,A11, XBOOLE_1:1;
take f;
:: from definition of f, identity on old graph is trivial
thus f|the_Edges_of G = f|dom id the_Edges_of G
.= id the_Edges_of G;
:: time to bring up the edge sets (E1 for both, E2 only for onto)
consider E1 being set such that
card V = card E1 and
A12: E1 misses the_Edges_of G & the_Edges_of G1 = the_Edges_of G \/ E1
and A13: for v1 being object st v1 in V ex e1 being object st e1 in E1 &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A1, Def4;
consider E2 being set such that
card V = card E2 and
A14: E2 misses the_Edges_of G & the_Edges_of G2 = the_Edges_of G \/ E2
and A15: for v1 being object st v1 in V ex e1 being object st e1 in E2 &
e1 Joins v1,v,G2 &
for e2 being object st e2 Joins v1,v,G2 holds e1 = e2
by A1, Def4;
:: show the one-to-one property
for e1,e2 being object st e1 in dom f & e2 in dom f & f.e1 = f.e2
holds e1 = e2
proof
let e1,e2 be object;
assume that
A16: e1 in dom f & e2 in dom f and
A17: f.e1 = f.e2;
set x1 = (the_Source_of G1).e1, y1 = (the_Target_of G1).e1;
set x2 = (the_Source_of G1).e2, y2 = (the_Target_of G1).e2;
A18: e1 in the_Edges_of G1 & e2 in the_Edges_of G1 by A16;
per cases;
:: one-to-one on old graph / identity is trivial
suppose A19: e1 in the_Edges_of G & e2 in the_Edges_of G;
then e1 in dom id the_Edges_of G & e2 in dom id the_Edges_of G;
then f.e1 = (id the_Edges_of G).e1 & f.e2 = (id the_Edges_of G).e2
by FUNCT_4:13;
then f.e1 = e1 & f.e2 = e2 by A19, FUNCT_1:18;
hence thesis by A17;
end;
:: If e2 is an old edge, it cannot be incident to v.
:: On the other hand, e1 must be incident to v. This leads
:: to a contradiction.
suppose A20: not e1 in the_Edges_of G & e2 in the_Edges_of G;
then not e1 in dom id the_Edges_of G & e2 in dom id the_Edges_of G;
then A21: f.e1 = f1.e1 & f.e2 = (id the_Edges_of G).e2
by FUNCT_4:11, FUNCT_4:13;
A22: e1 Joins x1,y1,G1 by A18, GLIB_000:def 13;
then A23: not x1 in the_Vertices_of G or not y1 in the_Vertices_of G
by A1, A12, A20, Th51;
e2 Joins x2,y2,G1 by A18, GLIB_000:def 13;
then A24: e2 Joins x2,y2,G by A20, GLIB_006:72;
then A25: x2 in the_Vertices_of G & y2 in the_Vertices_of G
by GLIB_000:13;
A26: f.e1 Joins x1,y1,G2 by A21,A18, A22, A4;
A27: e2 Joins x2,y2,G2 by A24, GLIB_006:70;
f.e2 = e2 by A20, A21, FUNCT_1:18;
hence thesis by A23, A25, A26, GLIB_000:15,A17,A27;
end;
:: symmetric case
suppose A28: not e2 in the_Edges_of G & e1 in the_Edges_of G;
then not e2 in dom id the_Edges_of G & e1 in dom id the_Edges_of G;
then A29: f.e2 = f1.e2 & f.e1 = (id the_Edges_of G).e1
by FUNCT_4:11, FUNCT_4:13;
A30: e2 Joins x2,y2,G1 by A18, GLIB_000:def 13;
then e2 in E1 & ((x2 = v & y2 in V) or (y2 = v & x2 in V))
by A1, A12, A28, Th51;
then A31: not x2 in the_Vertices_of G or not y2 in the_Vertices_of G
by A1;
e1 Joins x1,y1,G1 by A18, GLIB_000:def 13;
then A32: e1 Joins x1,y1,G by A28, GLIB_006:72;
then A33: x1 in the_Vertices_of G & y1 in the_Vertices_of G
by GLIB_000:13;
A34: f.e2 Joins x2,y2,G2 by A29,A18, A30, A4;
A35: e1 Joins x1,y1,G2 by A32, GLIB_006:70;
f.e1 = e1 by A28, A29, FUNCT_1:18;
then f.e2 Joins x1,y1,G2 by A17, A35;
hence thesis by A31, A33,A34, GLIB_000:15;
end;
:: interesting case on the new edges
suppose A36: not e1 in the_Edges_of G & not e2 in the_Edges_of G;
then not e1 in dom id the_Edges_of G & not e2 in dom id the_Edges_of G;
then A37: f.e1 = f1.e1 & f.e2 = f1.e2 by FUNCT_4:11;
A38: e1 Joins x1,y1,G1 by A18, GLIB_000:def 13;
then A39: e1 in E1 & ((x1 = v & y1 in V) or (y1 = v & x1 in V))
by A1, A12, A36, Th51;
A40: e2 Joins x2,y2,G1 by A18, GLIB_000:def 13;
A41: f.e1 Joins x1,y1,G2 by A18, A38, A37, A4;
f.e2 Joins x2,y2,G2 by A18, A40, A37, A4;
:: Now essentially we use the one-to-one property of the new
:: edges of addAdjVertexAll to show e1 = e2, but because of
:: the many or's we have to make several further case distinctions
:: to cover symmetric cases.
then per cases by A17, A41, GLIB_000:15;
suppose A42: x1 = x2 & y1 = y2;
per cases by A39;
suppose A43: x1 = v & y1 in V;
then consider e being object such that
e in E1 & e Joins y1,v,G1 and
A44: for e3 being object st e3 Joins y1,v,G1 holds e = e3 by A13;
e1 = e by A44,A38, A43, GLIB_000:14;
hence thesis by A44, A40, A42, A43, GLIB_000:14;
end;
suppose A46: y1 = v & x1 in V;
then consider e being object such that
e in E1 & e Joins x1,v,G1 and
A47: for e3 being object st e3 Joins x1,v,G1 holds e = e3 by A13;
e1 Joins x1,v,G1 by A38, A46;
then e1 = e by A47;
hence thesis by A47, A40, A42, A46;
end;
end;
suppose A49: x1 = y2 & y1 = x2;
per cases by A39;
suppose A50: x1 = v & y1 in V;
then consider e being object such that
e in E1 & e Joins y1,v,G1 and
A51: for e3 being object st e3 Joins y1,v,G1 holds e = e3 by A13;
e1 = e by A51,A38, A50, GLIB_000:14;
hence thesis by A51, A40, A49, A50;
end;
suppose A53: y1 = v & x1 in V;
then consider e being object such that
e in E1 & e Joins x1,v,G1 and
A54: for e3 being object st e3 Joins x1,v,G1 holds e = e3 by A13;
e1 Joins x1,v,G1 by A38, A53;
then A55: e1 = e by A54;
e2 Joins x1,v,G1 by A40, A49, A53, GLIB_000:14;
hence thesis by A54, A55;
end;
end;
end;
end;
hence f is one-to-one by FUNCT_1:def 4;
:: show the onto property
for e being object holds e in the_Edges_of G2 implies e in rng f
proof
let e be object;
assume A56: e in the_Edges_of G2;
per cases;
:: trivial if e is old edge
suppose A57: e in the_Edges_of G;
then e in dom id the_Edges_of G;
then A58: f.e = (id the_Edges_of G).e by FUNCT_4:13
.= e by A57, FUNCT_1:18;
the_Edges_of G c= the_Edges_of G1 by GLIB_006:def 9;
hence thesis by A58, FUNCT_1:def 3, A9, A57;
end;
:: e being a new edge means it is incident to v and a vertex in V,
:: which in turn must be adjacent by some e1 in G1, also by f.e1
:: in G2, and the one-to-one property of the edges returns e = f.e1.
suppose A59: not e in the_Edges_of G;
set v1 = (the_Source_of G2).e, v2 = (the_Target_of G2).e;
A60: e Joins v1,v2,G2 by A56, GLIB_000:def 13;
then per cases by A1, A14, A59, Th51; :: symmetry
suppose A61: v1 = v & v2 in V;
then consider e1 being object such that
A62: e1 in E1 & e1 Joins v2,v,G1 and
for e2 being object st e2 Joins v2,v,G1 holds e1 = e2 by A13;
A63: e1 in the_Edges_of G1 by A62, GLIB_000:def 13;
then A64: f1.e1 Joins v2,v,G2 by A62, A4;
E1 /\ the_Edges_of G = {} by A12, XBOOLE_0:def 7;
then not e1 in dom id the_Edges_of G by A62, Lm7;
then A65: f.e1 Joins v2,v,G2 by A64, FUNCT_4:11;
consider e3 being object such that
e3 in E2 & e3 Joins v2,v,G2 and
A66: for e2 being object st e2 Joins v2,v,G2 holds e3 = e2 by A15,
A61;
f.e1 = e3 by A65, A66;
then f.e1 = e by A66,A61, A60, GLIB_000:14;
hence e in rng f by A63, A9, FUNCT_1:def 3;
end;
suppose A68: v2 = v & v1 in V;
then consider e1 being object such that
A69: e1 in E1 & e1 Joins v1,v,G1 and
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A13;
A70: e1 in the_Edges_of G1 by A69, GLIB_000:def 13;
then A71: f1.e1 Joins v1,v,G2 by A69, A4;
E1 /\ the_Edges_of G = {} by A12, XBOOLE_0:def 7;
then not e1 in dom id the_Edges_of G by A69, Lm7;
then A72: f.e1 Joins v1,v,G2 by A71, FUNCT_4:11;
consider e3 being object such that
e3 in E2 & e3 Joins v1,v,G2 and
A73: for e2 being object st e2 Joins v1,v,G2 holds e3 = e2 by A15,
A68;
f.e1 = e3 by A72, A73;
then f.e1 = e by A73,A68, A60;
hence e in rng f by A70, A9, FUNCT_1:def 3;
end;
end;
end;
then the_Edges_of G2 c= rng f by TARSKI:def 3;
hence f is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
:: rest is trivial from definition of f1 / using the identity on old graph
let v1,e,v2 be object;
assume A75: e Joins v1,v2,G1;
per cases;
suppose A76: e in the_Edges_of G;
then e in dom id the_Edges_of G;
then A77: f.e = (id the_Edges_of G).e by FUNCT_4:13
.= e by A76, FUNCT_1:18;
reconsider w1=v1,w2=v2 as set by TARSKI:1;
e Joins w1,w2,G by A75, A76, GLIB_006:72;
hence thesis by A77,GLIB_006:70;
end;
suppose not e in the_Edges_of G;
then not e in dom id the_Edges_of G;
then A78: f.e = f1.e by FUNCT_4:11;
e in the_Edges_of G1 by A75, GLIB_000:def 13;
hence thesis by A78,A75, A4;
end;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
:: In case we have G == G1 == G2, the identity on the edges obviously
:: satisfies the requirements.
then A79: G1 == G & G2 == G by Def4;
then A80: the_Edges_of G1 = the_Edges_of G &
the_Edges_of G2 = the_Edges_of G by GLIB_000:def 34;
set f = id the_Edges_of G;
reconsider f as Function of the_Edges_of G1, the_Edges_of G2 by A80;
take f;
thus f|the_Edges_of G = id the_Edges_of G;
thus f is one-to-one onto by A80;
let v1,e,v2 be object;
assume A81: e Joins v1,v2,G1;
G1 == G2 by A79, GLIB_000:85;
then A82: e Joins v1,v2,G2 by A81, GLIB_000:88;
e in the_Edges_of G1 by A81, GLIB_000:def 13;
hence thesis by A80, A82, FUNCT_1:18;
end;
end;
registration
let G be loopless _Graph;
let v,V;
cluster -> loopless for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
not ex e being object st e in the_Edges_of G1 &
(the_Source_of G1).e = (the_Target_of G1).e
proof
given e being object such that
A2: e in the_Edges_of G1 and
A3: (the_Source_of G1).e = (the_Target_of G1).e;
per cases;
suppose (the_Source_of G1).e = v;
then e Joins v,v,G1 by A2, A3, GLIB_000:def 13;
hence contradiction by A1, Def4;
end;
suppose A4: (the_Source_of G1).e <> v;
e DJoins (the_Source_of G1).e,(the_Target_of G1).e,G1
by A2, GLIB_000:def 14;
then e DJoins (the_Source_of G1).e,(the_Source_of G1).e,G
by A3, A1, A4, Def4;
then e Joins (the_Source_of G1).e,(the_Source_of G1).e,G
by GLIB_000:16;
hence contradiction by GLIB_000:18;
end;
end;
hence G1 is loopless by GLIB_000:def 18;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def4;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be non-Dmulti _Graph;
let v,V;
cluster -> non-Dmulti for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
for e1,e2,v1,v2 being object holds
e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume A2: e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1;
then A3: e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 by GLIB_000:16;
consider E being set such that
card V = card E & E misses the_Edges_of G &
the_Edges_of G1 = the_Edges_of G \/ E and
A4: for v1 being object st v1 in V ex e being object st e in E &
e Joins v1,v,G1 &
for e3 being object st e3 Joins v1,v,G1 holds e = e3 by A1, Def4;
per cases;
suppose v1 = v & v2 = v; :: no loops on v
hence thesis by A1, A3, Def4;
end;
suppose A5: v1 = v & v2 <> v;
per cases;
suppose v2 in V;
then consider e being object such that
e in E & e Joins v2,v,G1 and
A6: for e3 being object st e3 Joins v2,v,G1 holds e = e3 by A4;
e1 = e & e2 = e by A6,A5, A3, GLIB_000:14;
hence thesis;
end;
suppose not v2 in V;
then not e1 Joins v2,v,G1 by A1, Def4;
hence thesis by A5, A3, GLIB_000:14;
end;
end;
suppose A7: v1 <> v & v2 = v;
per cases;
suppose v1 in V;
then consider e being object such that
e in E & e Joins v1,v,G1 and
A8: for e3 being object st e3 Joins v1,v,G1 holds e = e3 by A4;
e1 Joins v1,v,G1 & e2 Joins v1,v,G1 by A7, A3;
then e1 = e & e2 = e by A8;
hence thesis;
end;
suppose not v1 in V;
hence thesis by A7, A3,A1, Def4;
end;
end;
suppose v1 <> v & v2 <> v;
then e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by A1, A2, Def4;
hence thesis by GLIB_000:def 21;
end;
end;
hence G1 is non-Dmulti by GLIB_000:def 21;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def4;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be non-multi _Graph;
let v,V;
cluster -> non-multi for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
for e1,e2,v1,v2 being object holds
e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume A2: e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1;
consider E being set such that
card V = card E & E misses the_Edges_of G &
the_Edges_of G1 = the_Edges_of G \/ E and
A3: for v1 being object st v1 in V ex e being object st e in E &
e Joins v1,v,G1 &
for e3 being object st e3 Joins v1,v,G1 holds e = e3 by A1, Def4;
per cases;
suppose v1 = v & v2 = v; :: no loops allowed
hence thesis by A1, A2, Def4;
end;
suppose A4: v1 = v & v2 <> v;
per cases;
suppose v2 in V;
then consider e being object such that
e in E & e Joins v2,v,G1 and
A5: for e3 being object st e3 Joins v2,v,G1 holds e = e3 by A3;
e1 = e & e2 = e by A5,A2, A4, GLIB_000:14;
hence thesis;
end;
suppose not v2 in V;
then not e1 Joins v2,v,G1 by A1, Def4;
hence thesis by A2, A4, GLIB_000:14;
end;
end;
suppose A6: v1 <> v & v2 = v;
per cases;
suppose v1 in V;
then consider e being object such that
e in E & e Joins v1,v,G1 and
A7: for e3 being object st e3 Joins v1,v,G1 holds e = e3 by A3;
e1 = e & e2 = e by A7,A2,A6;
hence thesis;
end;
suppose not v1 in V;
hence thesis by A2, A6,A1,Def4;
end;
end;
suppose v1 <> v & v2 <> v; :: old graph is non-multi
then e1 Joins v1,v2,G & e2 Joins v1,v2,G by A1, A2, Th49;
hence thesis by GLIB_000:def 20;
end;
end;
hence G1 is non-multi by GLIB_000:def 20;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def4;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be Dsimple _Graph;
let v,V;
cluster -> Dsimple for addAdjVertexAll of G,v,V;
coherence;
end;
registration
let G be simple _Graph;
let v,V;
cluster -> simple for addAdjVertexAll of G,v,V;
coherence;
end;
theorem Th69:
for G2, v, V for G1 being addAdjVertexAll of G2, v, V, W being Walk of G1
for v1, v2 being Vertex of G2
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
W.first() = v1 & W.last() = v2 & not v2 in G2.reachableFrom(v1)
holds v in W.vertices()
proof
let G2,v,V;
let G1 be addAdjVertexAll of G2,v,V;
let W be Walk of G1, v1,v2 be Vertex of G2;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: W.first() = v1 & W.last() = v2 & not v2 in G2.reachableFrom(v1);
assume not v in W.vertices();
then reconsider W2 = W as Walk of G2 by A1, Th64;
W2.first() = v1 & W2.last() = v2 by A2, GLIB_001:16;
then W2 is_Walk_from v1,v2 by GLIB_001:def 23;
hence contradiction by A2, GLIB_002:def 5;
end;
Lm14: for k being odd Element of NAT holds
k-'1+1 = k & for n being Element of NAT holds k <= n implies k-'1 < n
proof
let k be odd Element of NAT;
thus k-'1+1 = k by ABIAN:12, XREAL_1:235;
let n be Element of NAT;
A1: k-'1 < k by ABIAN:12, XREAL_1:237;
assume k <= n;
hence thesis by A1, XXREAL_0:2;
end;
Lm15: for k,n being odd Element of NAT holds
n+(k-'1) is odd Element of NAT
proof
let k, n be odd Element of NAT;
consider i being Nat such that
A1: k = 2*i+1 by ABIAN:9;
consider j being Nat such that
A2: n = 2*j+1 by ABIAN:9;
n+(k-'1) = 2*j+1+(2*i) by A1, A2, NAT_D:34
.= 2*(j+i)+1;
hence thesis;
end;
Lm16: 1 is odd Element of NAT & 3 is odd Element of NAT
by POLYFORM:4, POLYFORM:6;
:: this means that in each component there is at most one
:: vertex connecting to the new one
theorem
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic &
for G3 being Component of G2, w1, w2 being Vertex of G3
st w1 in V & w2 in V holds w1 = w2
holds G1 is acyclic
proof
let G2, v, V;
let G1 being addAdjVertexAll of G2, v, V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: G2 is acyclic and
A3: for G3 being Component of G2, w1, w2 being Vertex of G3
st w1 in V & w2 in V holds w1 = w2;
consider E being set such that
card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A4: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
not ex W being Walk of G1 st W is Cycle-like
proof
given C being Walk of G1 such that
A5: C is Cycle-like;
A6: C is closed & C is Path-like by A5;
set v1 = C.first();
A7: v1 = C.last() by A6, GLIB_001:def 24;
per cases;
:: If the cycle doesn't start at v, it can at most contain it once
suppose A8: v1 <> v;
then A9: not v1 in {v} by TARSKI:def 1;
A10: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
then reconsider v1 as Vertex of G2 by A9, XBOOLE_0:def 3;
set G3 = the inducedSubgraph of G2, G2.reachableFrom(v1);
per cases;
:: If the cycle lies within the component of v1 in G2,
:: it is a cycle in G2, leading to a contradiction.
suppose C.vertices() c= G2.reachableFrom(v1);
then A11: C.vertices() c= the_Vertices_of G2 by XBOOLE_1:1;
then A12: C.edges() c= the_Edges_of G2 by Th65;
G2 is Subgraph of G1 by GLIB_006:57;
then reconsider C2=C as Walk of G2 by A11, A12, GLIB_001:170;
C2 is Cycle-like by A5, GLIB_006:24;
hence contradiction by A2, GLIB_002:def 2;
end;
:: If the cycle has a vertex out of the component of G2,
:: it is in another component of G2 or equals v2
suppose not C.vertices() c= G2.reachableFrom(v1);
then consider v2 being object such that
A13: v2 in C.vertices() & not v2 in G2.reachableFrom(v1)
by TARSKI:def 3;
reconsider v2 as Vertex of G1 by A13;
consider n being odd Element of NAT such that
A14: n <= len C and
A15: C.n = v2 by A13, GLIB_001:87;
:: v2 cannot be v1 (=C.1=C.len C) because it is not reachable from v1
A16: 1 < n & n < len C
proof
thus 1 < n
proof
assume A17: 1 >= n;
1 <= n by ABIAN:12;
then n = 1 by A17, XXREAL_0:1;
then v2 = v1 by A15, GLIB_001:def 6;
hence contradiction by A13, GLIB_002:9;
end;
assume n >= len C;
then n = len C by A14, XXREAL_0:1;
then v2 = v1 by A7, A15, GLIB_001:def 7;
hence contradiction by A13, GLIB_002:9;
end;
per cases;
:: If v2 <> v, we can split the cycle at v2.
:: One of the two resulting paths cannot contain v,
:: hence connects v1 and v2 in G2, leading to a contradiction
suppose A18: v2 <> v;
then not v2 in {v} by TARSKI:def 1;
then reconsider v2 as Vertex of G2 by A10, XBOOLE_0:def 3;
set P1 = C.cut(1, n);
set P2 = C.cut(n, len C);
A19: 1 is odd Element of NAT by Lm16;
A20: 1 <= n & n <= len C by ABIAN:12, A14;
A21: n <= len C & len C <= len C by A14;
A22: len P1 + 1 = n + 1 by A20, A19, GLIB_001:36;
A23: len P2 + n = len C + 1 by A21, GLIB_001:36;
not v in P1.vertices() or not v in P2.vertices()
proof
assume v in P1.vertices();
then consider m being odd Element of NAT such that
A24: m <= len P1 & P1.m = v by GLIB_001:87;
reconsider m1 = m-'1 as Element of NAT;
A25: m1 + 1 = m by Lm14;
m1 < len P1 by A24, Lm14;
then A26: C.(1+m1) = v by A19, A20, A24, A25, GLIB_001:36;
assume v in P2.vertices();
then consider k being odd Element of NAT such that
A27: k <= len P2 & P2.k = v by GLIB_001:87;
A28: k < len P2
proof
assume k >= len P2;
then A29: k = len P2 by A27, XXREAL_0:1;
v1 = C.len C by A7, GLIB_001:def 7
.= C.cut(n, len C).last() by A21, GLIB_001:37
.= v by A27, A29, GLIB_001:def 7;
hence contradiction by A8;
end;
reconsider k1 = k-'1 as Element of NAT;
A30: k1+1 = k by Lm14;
k1 < len P2 by A27, Lm14;
then C.(n+k1) = v by A21, A27, A30, GLIB_001:36;
then A31: C.m = C.(n+k1) by A25, A26;
reconsider nk = n+k1 as odd Element of NAT by Lm15;
A32: 1 <= k1
proof
A33: 1 <= k by ABIAN:12;
1 < k
proof
assume 1 >= k;
then k = 1 by A33, XXREAL_0:1;
then A34: P2.first() = v by A27, GLIB_001:def 6;
P2.first() = v2 by A15, A21, GLIB_001:37;
hence contradiction by A34, A18;
end;
hence thesis by NAT_D:49;
end;
m < len P1 + 1 by A24, NAT_1:13;
then A35: m < n + 1 by A22;
n + 1 <= n + k1 by A32, XREAL_1:6;
then A36: m < nk by A35, XXREAL_0:2;
A37: 1 <= k by ABIAN:12;
k + n <= len C + 1 by A27, A23, XREAL_1:6;
then k + n - 1 <= len C + 1 - 1 by XREAL_1:9;
then n + (k-1) <= len C;
then n+k1 <= len C by A37, XREAL_1:233;
then m = 1 & nk = len C by A6, A31, GLIB_001:def 28,A36;
hence contradiction by A28, A30, A23;
end;
then per cases;
suppose not v in P1.vertices();
then reconsider P3=P1 as Walk of G2 by A1, Th64;
P1 is_Walk_from C.1, C.n by A20, A19, GLIB_001:37;
then P1 is_Walk_from v1, v2 by A15, GLIB_001:def 6;
then P3 is_Walk_from v1, v2 by GLIB_001:19;
then v2 in G2.reachableFrom(v1) by GLIB_002:def 5;
hence contradiction by A13;
end;
suppose not v in P2.vertices();
then reconsider P3=P2 as Walk of G2 by A1, Th64;
P2 is_Walk_from C.n, C.len C by A21, GLIB_001:37;
then P2 is_Walk_from v2, v1 by A15, A7, GLIB_001:def 7;
then P3 is_Walk_from v2, v1 by GLIB_001:19;
then P3.reverse() is_Walk_from v1,v2 by GLIB_001:23;
hence contradiction by A13,GLIB_002:def 5;
end;
end;
:: If v2 = v, we can split the cycle before and after v2,
:: so the cycle looks like v1,...,w1,v,w2,...,v1.
suppose A38: v2 = v;
reconsider m = n-2 as odd Element of NAT by A16, Lm13;
set P1 = C.cut(1, m);
set P2 = C.cut(n+2, len C);
n-2 <= len C - 0 by A14, XREAL_1:13;
then A39: 1 <= m & m <= len C by ABIAN:12;
A40: n+2 <= len C & len C <= len C by A16, GLIB_001:1;
A41: len P1 + 1 = m + 1 by A39, Lm16, GLIB_001:36;
A42: len P2 + (n+2) = len C + 1 by A40, GLIB_001:36;
:: Neither of these two paths can contain v and are therefore in G2.
A43: not v in P1.vertices() & not v in P2.vertices()
proof
assume v in P1.vertices() or v in P2.vertices();
then per cases;
suppose v in P1.vertices();
then consider k being odd Element of NAT such that
A44: k <= len P1 & P1.k = v by GLIB_001:87;
reconsider k1 = k-'1 as Element of NAT;
k1 < len P1 by A44, Lm14;
then P1.(k1+1) = C.(1+k1) by A39, Lm16, GLIB_001:36;
then P1.k = C.(k1+1) by Lm14;
then P1.k = C.k by Lm14;
then A45: C.k = C.n by A38, A15,A44;
n - 2 < n - 0 by XREAL_1:15;
then A46: m < n;
k <= m by A44, A41;
then k < n & n <= len C by A14, A46, XXREAL_0:2;
then n = len C by A5, A45, GLIB_001:def 28;
hence contradiction by A16;
end;
suppose v in P2.vertices();
then consider k being odd Element of NAT such that
A47: k <= len P2 & P2.k = v by GLIB_001:87;
reconsider k1 = k-'1 as Element of NAT;
k1 < len P2 by A47, Lm14;
then P2.(k1+1) = C.((n+2)+k1) by A40, GLIB_001:36;
then P2.k = C.(n+(k1+1)+1) by Lm14;
then A48: P2.k = C.(n+k+1) by Lm14;
reconsider nk = n+k+1 as odd Element of NAT;
A49: C.nk = C.n by A38, A15,A47,A48;
n < nk & nk <= len C
proof
n < n + 1 by NAT_1:13;
then n + 0 < n + 1 + k by XREAL_1:8;
hence n < nk;
len P2 + (n+1) = len C by A42;
then k + (n+1) <= len C by A47, XREAL_1:6;
hence thesis;
end;
then n = 1 by A49, A5, GLIB_001:def 28;
hence contradiction by A16;
end;
end;
then reconsider P1, P2 as Walk of G2 by A1, Th64;
set w1 = C.m, w2 = C.(n+2);
set e1 = C.(m+1), e2 = C.(n+1);
n-2 < len C - 0 by A14, XREAL_1:15;
then e1 Joins w1,C.(m+2),G1 &
e2 Joins C.n,w2, G1 by GLIB_001:def 3,A16;
:: Since w1 and w2 are adjacent with v, they are in V.
then A50: e1 Joins w1,v,G1 & e2 Joins w2,v,G1
by A38, GLIB_000:14, A15;
then A51: w1 in V & w2 in V by A1, Def4;
then reconsider w1, w2 as Vertex of G2 by A1;
C.cut(1, m).first() = C.1 & C.cut(1, m).last() = C.m
by A39, Lm16, GLIB_001:37;
then A52: C.cut(1, m).first() = v1 & C.cut(1, m).last() = w1
by GLIB_001:def 6;
C.cut(n+2, len C).first() = w2 & C.cut(n+2, len C).last() = C.len C
by A40, GLIB_001:37;
then C.cut(n+2, len C).first() = w2 & C.cut(n+2, len C).last() = v1
by A7, GLIB_001:def 7;
then A53: C.cut(n+2, len C).reverse().first() = v1 &
C.cut(n+2, len C).reverse().last() = w2 by GLIB_001:22;
:: Both paths are connected to v1, so w1 and w2 are in v1s component.
w1 in G2.reachableFrom(v1) by A1, A43, A52, Th69;
then reconsider w1 as Vertex of G3 by GLIB_000:def 37;
w2 in G2.reachableFrom(v1)
proof
assume not w2 in G2.reachableFrom(v1);
then v in C.cut(n+2, len C).reverse().vertices() by A1, A53,Th69;
then v in C.cut(n+2, len C).vertices() by GLIB_001:92;
hence contradiction by A43;
end;
then reconsider w2 as Vertex of G3 by GLIB_000:def 37;
:: Then by assumption, w1 = w2.
A54: w1 = w2 by A51, A3;
:: But then the edges connecting w1 and w2 with v1 must be equal,
:: leading to a contradiction because C is a trail.
consider e3 being object such that
e3 in E & e3 Joins w1,v,G1 and
A55: for e5 being object st e5 Joins w1,v,G1 holds e5 = e3
by A4, A51;
e1 = e3 & e2 = e3 by A54, A50, A55;
then A56: C.(n-1) = C.(n+1);
reconsider n2=m+1 as even Element of NAT;
n + (-1) < n + 1 by XREAL_1:8;
then A57: n2 < n+1;
A58: 1+0 <= m+1 by XREAL_1:7;
n+2 - 1 <= len C - 0 by A40, XREAL_1:13;
then 1 <= n2 & n2 < n+1 & n+1 <= len C by A57, A58;
then C.n2 <> C.(n+1) by A6, GLIB_001:138;
hence contradiction by A56;
end;
end;
end;
:: If the cycle starts at v, since it is not trivial,
:: we can take the inner path C.3,...,C.(len C-2) which cannot contain v
suppose A59: v1 = v;
A60: len C >= 5
proof
assume len C < 5;
then len C < 4+1;
then len C <= 4 by NAT_1:13;
then A61: len C = 3 by A5, GLIB_001:126, CHORD:7;
then 1 < len C;
then C.(1+1) Joins C.1, C.(1+2), G1 by Lm16, GLIB_001:def 3;
then C.2 Joins C.first(), C.len C, G1 by A61, GLIB_001:def 6;
then C.2 Joins C.first(), C.last(), G1 by GLIB_001:def 7;
then C.2 Joins v,v,G1 by A59, A7;
hence contradiction by A1, Def4;
end;
A62: 1 < len C
proof
assume A63: 1 >= len C;
1 <= len C by ABIAN:12;
then len C = 1 by A63, XXREAL_0:1;
hence contradiction by A60;
end;
then reconsider m = len C - 2 as odd Element of NAT by Lm13;
len C - 2 < len C - 0 by XREAL_1:15;
then A64: m < len C;
set w1 = C.3, w2 = C.m;
set e1 = C.2, e2 = C.(m+1);
set P = C.cut(3,m);
A65: 3 is odd Element of NAT by Lm16;
A66: len C - 2 <= len C - 0 by XREAL_1:13;
5-2 <= len C - 2 by A60, XREAL_1:9;
then A67: 3 <= m & m <= len C by A66;
then len P + 3 = len C - 2 + 1 by A65, GLIB_001:36;
then A68: len P + 4 = len C;
not v in P.vertices()
proof
assume v in P.vertices();
then consider k being odd Element of NAT such that
A69: k <= len P & P.k = v by GLIB_001:87;
reconsider k1=k-'1 as Element of NAT;
A70: k1+1 = k by Lm14;
k1 < len P by A69, Lm14;
then P.(k1+1) = C.(3+k1) by A67, A65, GLIB_001:36;
then A71: C.(3+k1) = C.len C by A7, A59, A69, A70, GLIB_001:def 7;
reconsider k3=3+k1 as odd Element of NAT by Lm15, Lm16;
len P + 2 = len C - 2 by A68;
then A72: len P + 2 < len C - 0 by XREAL_1:15;
k3 = k1+1+2;
then k3 = k+2 by Lm14;
then k3 <= len P + 2 by A69, XREAL_1:6;
then k3 < len C by A72, XXREAL_0:2;
then A73: k3 = 1 by A71, A6, GLIB_001:def 28;
3 <= k3 by NAT_1:11;
hence contradiction by A73;
end;
then reconsider P as Walk of G2 by A1, Th64;
:: since w1=C.3 and w2=C.(len C-2) are adjacent to v, they are in V
C.(1+1) Joins C.1,C.(1+2),G1 & C.(m+1) Joins C.m,C.(m+2),G1
by A62, A64, Lm16, GLIB_001:def 3;
then e1 Joins v1,w1,G1 & e2 Joins w2,C.len C,G1 by GLIB_001:def 6;
then e1 Joins w1,v,G1 & e2 Joins w2,C.last(),G1
by A59, GLIB_000:14, GLIB_001:def 7;
then A74: e1 Joins w1,v,G1 & e2 Joins w2,v,G1 by A59, A7;
then A75: w1 in V & w2 in V by A1, Def4;
then reconsider w1,w2 as Vertex of G2 by A1;
set G3 = the inducedSubgraph of G2, G2.reachableFrom(w1);
:: since v is not in the inner path, w1 and w2 share a component
:: and are therefore equal by assumption
C.cut(3,m) is_Walk_from w1,w2 by A67, Lm16, GLIB_001:37;
then P is_Walk_from w1,w2 by GLIB_001:19;
then w2 in G2.reachableFrom(w1) by GLIB_002:def 5;
then reconsider w2 as Vertex of G3 by GLIB_000:def 37;
w1 in G2.reachableFrom(w1) by GLIB_002:9;
then reconsider w1 as Vertex of G3 by GLIB_000:def 37;
A76: w1 = w2 by A3, A75;
:: so w1 and w2 must share the same edge to v,
:: which contradicts the trail property of C
consider e3 being object such that
e3 in E & e3 Joins w1,v,G1 and
A77: for e5 being object st e5 Joins w1,v,G1 holds e3 = e5
by A4, A75;
A78: e1 = e3 & e2 = e3 by A74, A76, A77;
reconsider n2=1+1 as even Element of NAT by Lm16;
len C - 1 <= len C - 0 by XREAL_1:13;
then A79: m+1 <= len C;
2 < 3 & 3 + 0 <= m + 1 by A67, XREAL_1:7;
then 1 <= n2 & n2 < m+1 & m+1 <= len C by A79, XXREAL_0:2;
then C.n2 <> C.(m+1) by A5, GLIB_001:138;
hence contradiction by A78;
end;
end;
hence thesis by GLIB_002:def 2;
end;
theorem
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
(G2 is non acyclic or
ex G3 being Component of G2, w1, w2 being Vertex of G3
st w1 in V & w2 in V & w1 <> w2)
holds G1 is non acyclic
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: G2 is non acyclic or
ex G3 being Component of G2, w1, w2 being Vertex of G3
st w1 in V & w2 in V & w1 <> w2;
per cases by A2;
suppose G2 is non acyclic;
hence thesis;
end;
suppose ex G3 being Component of G2, w1, w2 being Vertex of G3
st w1 in V & w2 in V & w1 <> w2;
then consider G3 being Component of G2, w1, w2 being Vertex of G3 such that
A3: w1 in V & w2 in V & w1 <> w2;
reconsider w1, w2 as Vertex of G2 by A3, A1;
the_Vertices_of G3 = G2.reachableFrom(w1) by GLIB_002:33;
then w2 in G2.reachableFrom(w1);
then consider W being Walk of G2 such that
A4: W is_Walk_from w1, w2 by GLIB_002:def 5;
reconsider W1=W as Walk of G1 by GLIB_006:75;
set P = the Path of W1;
W1 is_Walk_from w1,w2 by A4, GLIB_001:19;
then A5: P is_Walk_from w1,w2 by GLIB_001:160;
consider E being set such that
A6: card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A7: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e3 being object st e3 Joins v1,v,G1 holds e1 = e3 by A1, Def4;
consider e1 being object such that
A8: e1 in E & e1 Joins w1,v,G1 and
for e3 being object st e3 Joins w1,v,G1 holds e1 = e3 by A3, A7;
A9: e1 Joins v,w1,G1 by A8, GLIB_000:14;
consider e2 being object such that
A10: e2 in E & e2 Joins w2,v,G1 and
for e3 being object st e3 Joins w2,v,G1 holds e2 = e3 by A3, A7;
set P2 = P.addEdge(e2);
set P3 = P2.addEdge(e1);
A11: P.first() = w1 & P.last() = w2 by A5, GLIB_001:def 23;
then A12: P2.first() = w1 & P2.last() = v by A10, GLIB_001:63;
then A13: P3 is_Walk_from w1,w1 by A9, GLIB_001:63;
A14: not v in P.vertices()
proof
assume v in P.vertices();
then v in W1.vertices() by GLIB_001:163, TARSKI:def 3;
then v in W.vertices() by GLIB_001:98;
then v in the_Vertices_of G2;
hence contradiction by A1;
end;
P is open by A3, A11, GLIB_001:def 24;
then A15: P2 is Path-like by A10, A11, A14, GLIB_001:151;
w1 <> v by A1;
then A16: P2 is open by A12, GLIB_001:def 24;
A17: not e1 in P2.edges()
proof
assume A18: e1 in P2.edges();
P2.edges() = P.edges() \/ {e2} by A10, A11, GLIB_001:111;
then e1 in P.edges() \/ {e2} by A18;
then per cases by XBOOLE_0:def 3;
suppose e1 in P.edges();
then e1 in W1.edges() by GLIB_001:163, TARSKI:def 3;
then e1 in W.edges() by GLIB_001:110;
then A19: e1 in the_Edges_of G2;
E /\ the_Edges_of G2 = {} by A6, XBOOLE_0:def 7;
hence contradiction by A8, A19, Lm7;
end;
suppose e1 in {e2};
then e1 = e2 by TARSKI:def 1;
then e2 Joins v,w1,G1 by A9;
then per cases by A10, GLIB_000:15;
suppose w1 = w2 & v = v;
hence contradiction by A3;
end;
suppose w1 = v & v = w2;
hence contradiction by A3;
end;
end;
end;
for n being odd Element of NAT st 1 < n & n <= len P2 holds P2.n <> w1
proof
given n being odd Element of NAT such that
A20: 1 < n & n <= len P2 & P2.n = w1;
P2.1 = w1 by A12, GLIB_001:def 6;
then n = len P2 by A20, A15, Lm16, GLIB_001:def 28;
then P2.last() = w1 by A20, GLIB_001:def 7;
then w1 = v by A12;
then v in V by A3;
hence contradiction by A1;
end;
then A21: P3 is Path-like by A9, A12, A15, A16, A17, GLIB_001:150;
A22: P3 is closed by A13, GLIB_001:119;
P3 is non trivial by A9, A12, GLIB_001:132;
then P3 is Cycle-like by A21, A22;
hence thesis by GLIB_002:def 2;
end;
end;
:: this means that in each component there is at least one
:: vertex connecting to the new one
theorem Th72:
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
for G3 being Component of G2 ex w being Vertex of G3 st w in V
holds G1 is connected
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: for G3 being Component of G2 ex w being Vertex of G3 st w in V;
A3: for u being Vertex of G1 st u <> v
holds ex W1 being Walk of G1 st W1 is_Walk_from u,v
proof
let u be Vertex of G1;
assume u <> v;
then A4: not u in {v} by TARSKI:def 1;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
then u in the_Vertices_of G2 by A4, XBOOLE_0:def 3;
then reconsider u1=u as Vertex of G2;
reconsider G3 = the inducedSubgraph of G2,G2.reachableFrom(u1)
as Component of G2;
consider w being Vertex of G3 such that
A5: w in V by A2;
the_Vertices_of G3 = G2.reachableFrom(u1) by GLIB_000:def 37;
then w in G2.reachableFrom(u1);
then consider W2 being Walk of G2 such that
A6: W2 is_Walk_from u1,w by GLIB_002:def 5;
reconsider W3=W2 as Walk of G1 by GLIB_006:75;
A7: W3 is_Walk_from u,w by A6, GLIB_001:19;
consider E being set such that
card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A8: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
consider e1 being object such that
A9: e1 in E & e1 Joins w,v,G1 and
for e2 being object st e2 Joins w,v,G1 holds e1 = e2 by A8, A5;
take W3.addEdge(e1);
W3.first() = u & W3.last() = w by A7, GLIB_001:def 23;
hence W3.addEdge(e1) is_Walk_from u,v by A9, GLIB_001:63;
end;
for u,w being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,w
proof
let u,w be Vertex of G1;
per cases;
suppose A10: u = v & w = v;
take G1.walkOf(u);
thus G1.walkOf(u) is_Walk_from u,w by A10, GLIB_001:13;
end;
suppose u = v & w <> v;
then consider W3 being Walk of G1 such that
A11: W3 is_Walk_from w,u by A3;
take W3.reverse();
thus W3.reverse() is_Walk_from u,w by A11, GLIB_001:23;
end;
suppose u <> v & w = v;
hence thesis by A3;
end;
suppose A12: u <> v & w <> v;
consider W2 being Walk of G1 such that
A13: W2 is_Walk_from u,v by A12, A3;
consider W3 being Walk of G1 such that
A14: W3 is_Walk_from w,v by A12, A3;
A15: W3.reverse() is_Walk_from v,w by A14, GLIB_001:23;
take W2.append(W3.reverse());
thus W2.append(W3.reverse()) is_Walk_from u,w by A13, A15, GLIB_001:31;
end;
end;
hence thesis by GLIB_002:def 1;
end;
registration
let G be connected _Graph, v be object, V be non empty set;
cluster -> connected for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
for G3 being Component of G ex w being Vertex of G3 st w in V
proof
let G3 be Component of G;
set w = the Element of V;
A2: G == G3 by GLIB_006:55;
w in the_Vertices_of G by A1, TARSKI:def 3;
then reconsider w as Vertex of G3 by A2, GLIB_000:def 34;
take w;
thus thesis;
end;
hence thesis by A1, Th72;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def4;
hence thesis by GLIB_002:8;
end;
end;
end;
theorem Th73:
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
ex G3 being Component of G2 st for w being Vertex of G3 holds not w in V
holds G1 is non connected
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V;
consider G3 being Component of G2 such that
A3: for w being Vertex of G3 holds not w in V by A2;
set v1 = the Vertex of G3;
A4: the_Vertices_of G3 c= the_Vertices_of G2;
then A5: v1 in the_Vertices_of G2 by TARSKI:def 3;
then A6: v1 <> v by A1;
A7: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
v in {v} by TARSKI:def 1;
then A8: v in the_Vertices_of G1 by A7, XBOOLE_0:def 3;
A9: v1 in the_Vertices_of G1 by A5, A7, XBOOLE_0:def 3;
not ex W being Walk of G1 st W is_Walk_from v1,v
proof
given W being Walk of G1 such that
A10: W is_Walk_from v1,v;
set P = the Path of W;
reconsider u1=v1, u2=v as set by TARSKI:1;
P is_Walk_from u1,u2 by A10, GLIB_001:160;
then A11: P.first() = v1 & P.last() = v by GLIB_001:def 23;
then P.first() <> P.last() by A6;
then P is non trivial by GLIB_001:127;
then 3 <= len P by GLIB_001:125;
then 1 < len P by XXREAL_0:2;
then reconsider m=len P-2 as odd Element of NAT by Lm13;
A12: m < len P - 0 & m <= len P - 0 by XREAL_1:15;
set P2 = P.cut(1,m);
A13: len P2 = m by A12, GLIB_001:45;
not v in P2.vertices()
proof
assume v in P2.vertices();
then consider k being odd Element of NAT such that
A14: k <= len P2 & P2.k = v by GLIB_001:87;
1 <= k by ABIAN:12;
then k in dom P2 by A14, FINSEQ_3:25;
then P.k = P2.k by A12, GLIB_001:46;
then A15: P.k = v by A14;
A16: P.len P = v by A11, GLIB_001:def 7;
k < len P by A14, A13, A12, XXREAL_0:2;
then k = 1 by A15, A16, GLIB_001:def 28;
then P.1 = v by A15;
hence contradiction by A11, A6, GLIB_001:def 6;
end;
then reconsider P3=P2 as Walk of G2 by A1, Th64;
A17: 1 <= m by ABIAN:12;
set v2 = P3.last();
v2 in the_Vertices_of G3
proof
A18: 1 in dom P2 by A13, A17, FINSEQ_3:25;
P3.first() = P2.1 by GLIB_001:def 6
.= P.1 by A18, A12, GLIB_001:46
.= v1 by A11, GLIB_001:def 6;
then A19: P3 is_Walk_from v1, v2 by GLIB_001:def 23;
reconsider v3=v1 as Vertex of G2 by A4, TARSKI:def 3;
v2 in G2.reachableFrom(v3) by A19, GLIB_002:def 5;
hence thesis by GLIB_002:33;
end;
then A20: not v2 in V by A3;
v2 = P2.last() by GLIB_001:16
.= P.m by A12, A17, Lm16, GLIB_001:37;
then P.(m+1) Joins v2,P.(m+2),G1 by A12, GLIB_001:def 3;
then P.(m+1) Joins v2,P.len P,G1;
then P.(m+1) Joins v2,v,G1 by GLIB_001:def 7, A11;
hence contradiction by A20, A1, Def4;
end;
hence thesis by A8, A9, GLIB_002:def 1;
end;
theorem
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
ex G3 being Component of G2 st the_Vertices_of G3 misses V
holds G1 is non connected
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume that
A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: ex G3 being Component of G2 st the_Vertices_of G3 misses V;
ex G3 being Component of G2 st for w being Vertex of G3 holds not w in V
proof
consider G3 being Component of G2 such that
A3: the_Vertices_of G3 misses V by A2;
take G3;
let w be Vertex of G3;
the_Vertices_of G3 /\ V = {} by A3, XBOOLE_0:def 7;
hence thesis by Lm7;
end;
hence thesis by A1, Th73;
end;
registration
let G be non connected _Graph, v be object;
cluster -> non connected for addAdjVertexAll of G,v,{};
coherence
proof
let G1 be addAdjVertexAll of G, v, {};
G1 is addVertex of G, v by Th55;
hence thesis;
end;
end;
theorem Th75:
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1 is complete iff G2 is complete & V = the_Vertices_of G2
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
hereby
assume A2: G1 is complete;
for u,v being Vertex of G2 st u <> v holds u, v are_adjacent
proof
let u2,v2 be Vertex of G2;
reconsider u1 = u2, v1 = v2 as Vertex of G1 by GLIB_006:68;
assume u2 <> v2;
then u1 <> v1;
then u1, v1 are_adjacent by A2, CHORD:def 6;
then consider e being object such that
A3: e Joins u1,v1,G1 by CHORD:def 3;
u2 <> v & v2 <> v by A1;
then e Joins u2,v2,G2 by A1, A3, Th49;
hence u2, v2 are_adjacent by CHORD:def 3;
end;
hence G2 is complete by CHORD:def 6;
for x being object holds x in the_Vertices_of G2 implies x in V
proof
let x be object;
assume x in the_Vertices_of G2;
then reconsider v2 = x as Vertex of G2;
reconsider v1 = v2 as Vertex of G1 by GLIB_006:68;
reconsider v0 = v as Vertex of G1 by A1, Th50;
v1 <> v by A1;
then v1, v0 are_adjacent by A2, CHORD:def 6;
then consider e being object such that
A4: e Joins v1,v,G1 by CHORD:def 3;
thus thesis by A1, A4, Def4;
end;
then the_Vertices_of G2 c= V by TARSKI:def 3;
hence V = the_Vertices_of G2 by A1, XBOOLE_0:def 10;
end;
assume that
A5: G2 is complete and
A6: V = the_Vertices_of G2;
for u,v being Vertex of G1 st u <> v holds u, v are_adjacent
proof
let u1,v1 be Vertex of G1;
assume A7: u1 <> v1;
consider E being set such that
card V = card E & E misses the_Edges_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ E and
A8: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
A9: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, Def4;
per cases;
suppose A10: u1 = v;
then v1 <> v by A7;
then not v1 in {v} by TARSKI:def 1;
then v1 in the_Vertices_of G2 by A9, XBOOLE_0:def 3;
then consider e1 being object such that
A11: e1 in E & e1 Joins v1,v,G1 and
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A6, A8;
e1 Joins u1,v1,G1 by A10, A11, GLIB_000:14;
hence u1, v1 are_adjacent by CHORD:def 3;
end;
suppose A12: v1 = v;
then u1 <> v by A7;
then not u1 in {v} by TARSKI:def 1;
then u1 in the_Vertices_of G2 by A9, XBOOLE_0:def 3;
then consider e1 being object such that
A13: e1 in E & e1 Joins u1,v,G1 and
for e2 being object st e2 Joins u1,v,G1 holds e1 = e2 by A6, A8;
e1 Joins u1,v1,G1 by A12, A13;
hence u1, v1 are_adjacent by CHORD:def 3;
end;
suppose u1 <> v & v1 <> v;
then not u1 in {v} & not v1 in {v} by TARSKI:def 1;
then reconsider u2 = u1, v2 = v1 as Vertex of G2 by A9, XBOOLE_0:def 3;
u2, v2 are_adjacent by A5, A7, CHORD:def 6;
then consider e being object such that
A14: e Joins u2,v2,G2 by CHORD:def 3;
e Joins u1,v1,G1 by A14, GLIB_006:70;
hence u1, v1 are_adjacent by CHORD:def 3;
end;
end;
hence thesis by CHORD:def 6;
end;
registration
let G be complete _Graph;
cluster -> complete for addAdjVertexAll of G, the_Vertices_of G;
coherence
proof
let G1 be addAdjVertexAll of G, the_Vertices_of G;
the_Vertices_of G c= the_Vertices_of G &
not the_Vertices_of G in the_Vertices_of G;
hence thesis by Th75;
end;
end;
theorem
for G2, v, V for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.order() = G2.order() +` 1 & G1.size() = G2.size() +` card V
proof
let G2, v, V;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by Def4;
consider E being set such that
A3: card V = card E and
A4: E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E and
for w being object st w in V ex e1 being object st e1 in E &
e1 Joins w,v,G1 &
for e2 being object st e2 Joins w,v,G1 holds e1 = e2
by A1, Def4;
A5: {v} misses the_Vertices_of G2 by A1, ZFMISC_1:50;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 +` card {v} by A2, A5, CARD_2:35
.= G2.order() +` card {v} by GLIB_000:def 24
.= G2.order() +` 1 by CARD_1:30;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 +` card E by A4, CARD_2:35
.= G2.size() +` card V by A3, GLIB_000:def 25;
end;
theorem
for G2 being _finite _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.order() = G2.order() + 1
proof
let G2 be _finite _Graph, v be object, V be set;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by Def4;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 + 1 by A1, A2, CARD_2:41
.= G2.order() + 1 by GLIB_000:def 24;
end;
theorem
for G2 being _finite _Graph, v being object, V being finite set
for G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
holds G1.size() = G2.size() + card V
proof
let G2 be _finite _Graph, v be object, V be finite set;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
consider E being set such that
A2: card V = card E and
A3: E misses the_Edges_of G2 & the_Edges_of G1 = the_Edges_of G2 \/ E and
for w being object st w in V ex e1 being object st e1 in E &
e1 Joins w,v,G1 &
for e2 being object st e2 Joins w,v,G1 holds e1 = e2
by A1, Def4;
V,E are_equipotent by A2, CARD_1:5;
then reconsider E as finite set by CARD_1:38;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 + card E by A3, CARD_2:40
.= G2.size() + card V by A2, GLIB_000:def 25;
end;
registration
let G be _finite _Graph, v be object, V be set;
cluster -> _finite for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose A1: V c= the_Vertices_of G & not v in the_Vertices_of G;
then A2: the_Vertices_of G1 = the_Vertices_of G \/ {v} by Def4;
consider E being set such that
A3: card V = card E & E misses the_Edges_of G and
A4: the_Edges_of G1 = the_Edges_of G \/ E and
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by A1, Def4;
A5: V, E are_equipotent by A3, CARD_1:5;
V is finite by A1;
then E is finite by A5, CARD_1:38;
then the_Vertices_of G1 is finite & the_Edges_of G1 is finite by A2, A4;
hence thesis by GLIB_000:def 17;
end;
suppose not (V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by Def4;
hence thesis by GLIB_000:89;
end;
end;
end;