:: Recognizing Chordal Graphs: Lex BFS and MCS
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received November 17, 2006
:: Copyright (c) 2006-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, FUNCT_1, CARD_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1,
XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, FINSET_1, ORDINAL1, ARYTM_1,
NAT_1, ZFMISC_1, FINSEQ_1, UPROOTS, VALUED_0, RELAT_2, BAGORDER,
PRE_POLY, WELLORD1, GLIB_000, GLIB_001, ORDINAL4, PBOOLE, PARTFUN1,
MCART_1, FUNCT_2, FINSUB_1, CHORD, TOPGEN_1, RCOMP_1, FINSEQ_4, GRAPH_1,
MEMBERED, ABIAN, LEXBFS, MATROID0, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, CARD_1, ORDINAL1,
NUMBERS, SUBSET_1, XXREAL_0, VALUED_0, XREAL_0, RELAT_1, RELAT_2,
WELLORD1, MEMBERED, XXREAL_2, PARTFUN1, FUNCT_1, FUNCT_2, PBOOLE,
FINSET_1, XCMPLX_0, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001,
BAGORDER, TERMORD, UPROOTS, CHORD, FINSEQ_1, DOMAIN_1, ABIAN, RELSET_1,
RECDEF_1, FINSUB_1, RFUNCT_3, PRE_POLY;
constructors DOMAIN_1, FUNCT_4, XXREAL_2, BAGORDER, TERMORD, UPROOTS, CHORD,
RECDEF_1, RFUNCT_3, RELSET_1, PBOOLE, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XXREAL_0, XREAL_0, XXREAL_2, NAT_1, INT_1, MEMBERED, FINSEQ_1,
CARD_1, GLIB_000, ABIAN, BAGORDER, TERMORD, GLIB_001, CHORD, VALUED_0,
FINSUB_1, PARTFUN1, RELSET_1, PRE_POLY, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI;
equalities GLIB_000, GLIB_001, FUNCOP_1;
expansions GLIB_000, GLIB_001, TARSKI;
theorems AXIOMS, CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, INT_1, NAT_1,
BAGORDER, TERMORD, ORDINAL1, PARTFUN1, PBOOLE, NAT_D, XREAL_0, RELAT_1,
RELSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, ENUMSET1, CHORD,
NECKLACE, FINSEQ_4, WELLORD1, UPROOTS, TREES_1, NAT_2, XXREAL_0,
XXREAL_2, VALUED_0, MCART_1, FINSUB_1, SYSREL, GRFUNC_1;
schemes NAT_1, FUNCT_1, RECDEF_1, FRAENKEL, PBOOLE, FUNCT_2, CLASSES1;
begin :: Preliminaries
:: What should be the order of RELSET_1, FUNCT_1, FUNCT_2 such that the
:: qua Function and qua Relation are not needed.
Lm1: for F being Function, x,y being set holds dom(F+*(x.-->y)) = dom F \/ {x}
proof
let F be Function, x,y be set;
thus dom(F+*(x.-->y)) = dom F \/ dom(x.-->y) by FUNCT_4:def 1
.= dom F \/ {x};
end;
Lm2: for f being one-to-one Function, X, Y being set st X c= Y for x being set
st x in dom ((f|X)") holds (f|X)".x = (f|Y)".x
proof
let f be one-to-one Function, X, Y be set;
assume X c= Y;
then f|X c= f|Y by RELAT_1:75;
then
A1: ((f|X) qua Relation)~ c= ((f|Y) qua Relation)~ by SYSREL:11;
(f|X) is one-to-one by FUNCT_1:52;
then
A2: ((f|X) qua Relation)~ = (f|X)" by FUNCT_1:def 5;
(f|Y) is one-to-one by FUNCT_1:52;
then
A3: ((f|Y) qua Relation)~ = (f|Y)" by FUNCT_1:def 5;
let x be set;
assume x in dom ((f|X)");
hence thesis by A1,A2,A3,GRFUNC_1:2;
end;
:: More general than GRAPH_2:4
theorem
for A,B being Element of NAT, X being non empty set for F being
sequence of X st F is one-to-one holds card {F.w where w is Element of NAT
: A <= w & w <= A + B} = B+1
proof
let A,B be Element of NAT, X be non empty set;
let F be sequence of X such that
A1: F is one-to-one;
defpred P[Nat] means card { F.w where w is Element of NAT: A<= w
& w<=A+$1 } = $1+1;
A2: dom F = NAT by FUNCT_2:def 1;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
set Fwk = {F.w where w is Element of NAT: A<=w & w<=A+k};
reconsider Fwk as finite set by A4;
set Fwk1 = {F.w where w is Element of NAT: A<=w & w<=A+k+1};
A5: now
let x be object;
hereby
assume x in Fwk1;
then consider w being Element of NAT such that
A6: x = F.w and
A7: A <= w and
A8: w<=A+k+1;
A9: w = A+k+1 or w < A+k+1 by A8,XXREAL_0:1;
per cases by A9,NAT_1:13;
suppose
w = A+k+1;
then x in {F.(A+k+1)} by A6,TARSKI:def 1;
hence x in Fwk \/ {F.(A+k+1)} by XBOOLE_0:def 3;
end;
suppose
w <= A + k;
then x in Fwk by A6,A7;
hence x in Fwk \/ {F.(A+k+1)} by XBOOLE_0:def 3;
end;
end;
assume
A10: x in Fwk \/ {F.(A+k+1)};
per cases by A10,XBOOLE_0:def 3;
suppose
x in Fwk;
then consider w being Element of NAT such that
A11: x = F.w and
A12: A <= w and
A13: w<=A+k;
w <= A+k+1 by A13,NAT_1:13;
hence x in Fwk1 by A11,A12;
end;
suppose
A14: x in {F.(A+k+1)};
A15: A <= A+(k+1) by NAT_1:11;
x = F.(A+k+1) by A14,TARSKI:def 1;
hence x in Fwk1 by A15;
end;
end;
now
assume F.(A+k+1) in Fwk;
then consider w being Element of NAT such that
A16: F.(A+k+1) = F.w and
A <= w and
A17: w <= A+k;
A+k+1 = w by A1,A2,A16,FUNCT_1:def 4;
hence contradiction by A17,NAT_1:13;
end;
then card (Fwk \/ {F.(A+k+1)}) = (k+1)+1 by A4,CARD_2:41;
hence thesis by A5,TARSKI:2;
end;
now
let x be object;
hereby
assume x in { F.w where w is Element of NAT: A <= w & w <= A+0};
then consider w being Element of NAT such that
A18: F.w = x and
A19: A<=w and
A20: w<=A+0;
w = A by A19,A20,XXREAL_0:1;
hence x in {F.A} by A18,TARSKI:def 1;
end;
assume x in {F.A};
then x = F.A by TARSKI:def 1;
hence x in {F.w where w is Element of NAT: A<=w & w<=A+0};
end;
then {F.w where w is Element of NAT: A<=w & w<=A+0} = {F.A} by TARSKI:2;
then
A21: P[ 0 ] by CARD_1:30;
for k being Nat holds P[k] from NAT_1:sch 2(A21,A3);
hence thesis;
end;
Lm3: for a,b,c being Real st a < b holds c-b+1 < c-a+1
proof
let a,b,c be Real;
assume a < b;
then c-b < c-a by XREAL_1:10;
hence thesis by XREAL_1:6;
end;
theorem Th2:
for n,m,k being Nat st m <= k & n < m holds k -' m < k -' n
proof
let n,m,k be Nat such that
A1: m <= k and
A2: n < m;
A3: k - m < k - n by A2,XREAL_1:15;
k -' n = k - n by A1,A2,XREAL_1:233,XXREAL_0:2;
hence thesis by A1,A3,XREAL_1:233;
end;
notation
let S be set;
synonym S is with_finite-elements for S is finite-membered;
end;
registration
cluster non empty finite with_finite-elements for Subset of bool NAT;
existence
proof
set x = {{1}};
reconsider x as Subset of bool NAT;
take x;
thus x is non empty;
thus x is finite;
thus thesis;
end;
end;
definition
::$CD
let f,g be Function;
func f .\/ g -> Function means
:Def1:
dom it = dom f \/ dom g & for x being
object st x in dom f \/ dom g holds it.x = f.x \/ g.x;
existence
proof
defpred P[object,object] means f.$1 \/ g.$1 = $2;
set A = dom f \/ dom g;
A1: for x being object st x in A ex y being object st P[x,y];
ex f being Function st dom f = A &
for x being object st x in A holds P[x,f.x] from CLASSES1:sch 1(A1);
then consider IT being Function such that
A2: dom IT = A and
A3: for x being object st x in A holds P[x,IT.x];
take IT;
thus dom IT = dom f \/ dom g by A2;
thus thesis by A3;
end;
uniqueness
proof
let IT1,IT2 be Function such that
A4: dom IT1 = dom f \/ dom g and
A5: for x being object st x in dom f \/ dom g holds IT1.x = f.x \/ g.x and
A6: dom IT2 = dom f \/ dom g and
A7: for x being object st x in dom f \/ dom g holds IT2.x = f.x \/ g.x;
now
let x be object such that
A8: x in dom IT1;
IT1.x = f.x \/ g.x by A4,A5,A8;
hence IT1.x = IT2.x by A4,A7,A8;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
end;
theorem Th3:
for m,n,k being Nat holds m in ((Seg k) \ Seg (k -' n)) iff k -'
n < m & m <= k
proof
let m,n,k be Nat;
hereby
assume
A1: m in ((Seg k) \ Seg (k -' n));
then
A2: not m in Seg (k -' n) by XBOOLE_0:def 5;
A3: m in Seg k by A1,XBOOLE_0:def 5;
then 1 <= m by FINSEQ_1:1;
hence k -' n < m & m <= k by A3,A2,FINSEQ_1:1;
end;
assume that
A4: k -' n < m and
A5: m <= k;
0+1 <= m by A4,NAT_1:13;
then
A6: m in Seg k by A5,FINSEQ_1:1;
not m in Seg (k -' n) by A4,FINSEQ_1:1;
hence thesis by A6,XBOOLE_0:def 5;
end;
theorem Th4:
for n,k,m being Nat st n <= m holds ((Seg k) \ Seg (k -' n)) c= (
(Seg k) \ Seg (k -' m))
proof
let n,k,m be Nat such that
A1: n <= m;
per cases;
suppose
A2: k < m;
A3: for x be object st x in ((Seg k)\Seg(k-'n))holds x in Seg k
by XBOOLE_0:def 5;
k -' m = 0 by A2,NAT_2:8;
then Seg (k -' m) = {};
hence thesis by A3;
end;
suppose
A4: m <= k;
now
let x be object such that
A5: x in ((Seg k) \ Seg (k -' n));
reconsider y = x as Element of NAT by A5;
A6: k -' n < y by A5,Th3;
per cases by A1,XXREAL_0:1;
suppose
m = n;
hence x in ((Seg k) \ Seg (k -' m)) by A5;
end;
suppose
n < m;
then k -' m < k -' n by A4,Th2;
then
A7: k -' m < y by A6,XXREAL_0:2;
y <= k by A5,Th3;
hence x in ((Seg k) \ Seg (k -' m)) by A7,Th3;
end;
end;
hence thesis;
end;
end;
theorem Th5:
for n,k being Nat st n < k holds ((Seg k) \ Seg (k -' n)) \/ {k
-' n} = (Seg k) \ Seg (k -' (n+1))
proof
let n, k be Nat such that
A1: n < k;
set Sn1 = (Seg k) \ Seg (k -' (n+1));
set Sn = (Seg k) \ Seg (k -' n);
now
let x be object such that
A2: x in Sn \/ {k -' n};
per cases by A2,XBOOLE_0:def 3;
suppose
A3: x in Sn;
n <= n+1 by NAT_1:13;
then Sn c= Sn1 by Th4;
hence x in Sn1 by A3;
end;
suppose
A4: x in {k -' n};
then reconsider y = x as Nat;
A5: n < n + 1 by NAT_1:13;
n+1 <= k by A1,NAT_1:13;
then
A6: k -' (n+1) < k -' n by A5,Th2;
A7: x = k -' n by A4,TARSKI:def 1;
then y <= k by NAT_D:35;
hence x in Sn1 by A7,A6,Th3;
end;
end;
then
A8: Sn \/ {k -' n} c= Sn1;
now
let x be object such that
A9: x in Sn1;
reconsider y = x as Element of NAT by A9;
A10: y <= k by A9,Th3;
A11: k -' (n+1) + 1 = k -' n by A1,NAT_D:59;
k -' (n+1) < y by A9,Th3;
then
A12: k -' n <= y by A11,NAT_1:13;
per cases by A12,XXREAL_0:1;
suppose
k -' n = y;
then y in {k -' n} by TARSKI:def 1;
hence x in Sn \/ {k -' n} by XBOOLE_0:def 3;
end;
suppose
k -' n < y;
then y in Sn by A10,Th3;
hence x in Sn \/ {k -' n} by XBOOLE_0:def 3;
end;
end;
then Sn1 c= Sn \/ {k -' n};
hence thesis by A8,XBOOLE_0:def 10;
end;
definition
let f be Relation;
attr f is natsubset-yielding means
:Def2:
rng f c= bool NAT;
end;
registration
cluster finite-yielding natsubset-yielding for Function;
existence
proof
set F = NAT --> {};
take F;
for x be set st x in rng F holds x is finite;
hence F is finite-yielding by FINSET_1:def 2;
now
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng F;
then x = {} by TARSKI:def 1;
then xx c= NAT;
hence x in bool NAT;
end;
then rng F c= bool NAT;
hence thesis;
end;
end;
definition
let f be finite-yielding natsubset-yielding Function, x be set;
redefine func f.x -> finite Subset of NAT; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
A1: x in dom f;
A2: rng f c= bool NAT by Def2;
f.x in rng f by A1,FUNCT_1:3;
hence thesis by A2;
end;
suppose
not x in dom f;
then f.x = {} by FUNCT_1:def 2;
hence thesis by XBOOLE_1:2;
end;
end;
end;
theorem Th6:
for X being Ordinal, a, b be finite Subset of X st a <> b holds (
a,1)-bag <> (b,1)-bag
proof
let X be Ordinal, a,b be finite Subset of X such that
A1: a <> b;
assume
A2: (a,1)-bag = (b,1)-bag;
now
let x be object;
x in a iff (b,1)-bag.x = 1 by A2,UPROOTS:6,7;
hence x in a iff x in b by UPROOTS:6,7;
end;
hence contradiction by A1,TARSKI:2;
end;
definition
let F be natural-valued Function, S be set, k be Nat;
func F.incSubset(S,k) -> natural-valued Function means
:Def3:
dom it = dom F
& for y being object holds (y in S & y in dom F implies it.y = F.y + k) &
(not y in S implies it.y = F.y);
existence
proof
deffunc G(object) = F.$1 + k;
consider H being Function such that
A1: dom H = S /\ dom F and
A2: for x being object st x in (S /\ dom F) holds H.x = G(x) from FUNCT_1
:sch 3;
now
let x be object;
assume x in rng H;
then consider y being object such that
A3: y in dom H and
A4: H.y = x by FUNCT_1:def 3;
H.y = F.y + k by A1,A2,A3;
hence x in NAT by A4,ORDINAL1:def 12;
end;
then
A5: rng H c= NAT;
A6: rng (F+*H) c= rng F \/ rng H by FUNCT_4:17;
rng F \/ rng H c= NAT by A5,XBOOLE_1:8;
then rng (F+*H) c= NAT by A6;
then reconsider IT = F+*H as natural-valued Function by VALUED_0:def 6;
take IT;
dom IT = dom F \/ (S /\ dom F) by A1,FUNCT_4:def 1;
hence dom IT = dom F by XBOOLE_1:22;
now
let y be object;
A7: now
assume that
A8: y in S and
A9: y in dom F;
y in dom H by A1,A8,A9,XBOOLE_0:def 4;
then
A10: IT.y = H.y by FUNCT_4:13;
y in S /\ dom F by A8,A9,XBOOLE_0:def 4;
hence IT.y = F.y + k by A2,A10;
end;
now
assume not y in S;
then not y in dom H by A1,XBOOLE_0:def 4;
hence IT.y = F.y by FUNCT_4:11;
end;
hence (y in S & y in dom F implies IT.y = F.y + k) & (not y in S implies
IT.y = F.y) by A7;
end;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be natural-valued Function such that
A11: dom IT1 = dom F and
A12: for y being object holds (y in S & y in dom F implies IT1.y = F.y +
k) & (not y in S implies IT1.y = F.y) and
A13: dom IT2 = dom F and
A14: for y being object holds (y in S & y in dom F implies IT2.y = F.y +
k) & (not y in S implies IT2.y = F.y);
now
let x be object such that
A15: x in dom IT1;
per cases by A11,A15;
suppose
A16: x in S & x in dom F;
then IT1.x = F.x + k by A12;
hence IT1.x = IT2.x by A14,A16;
end;
suppose
A17: not x in S;
then IT1.x = F.x by A12;
hence IT1.x = IT2.x by A14,A17;
end;
end;
hence thesis by A11,A13,FUNCT_1:2;
end;
end;
definition
let n be Ordinal, T be connected TermOrder of n, B be non empty finite
Subset of Bags n;
func max(B,T) -> bag of n means
:Def4:
it in B & for x being bag of n st x in B holds x <= it,T;
existence
proof
consider p being FinSequence such that
A1: rng p = B by FINSEQ_1:52;
defpred P[Nat] means $1 <= len p implies (ex a being Nat, A being bag of n
st a in dom p & a <= $1 & p.a = A & (for c being Nat, C being bag of n st c in
dom p & c <= $1 & p.c = C holds C <= A, T));
A2: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat such that
A3: P[k];
per cases;
suppose
A4: k < len p;
A5: 1 <= k+1 by CHORD:1;
k+1 <= len p by A4,NAT_1:13;
then
A6: k+1 in dom p by A5,FINSEQ_3:25;
then p.(k+1) in B by A1,FUNCT_1:def 3;
then reconsider Ck = p.(k+1) as bag of n;
consider a being Nat, A being bag of n such that
A7: a in dom p and
A8: a <= k and
A9: p.a = A and
A10: for c being Nat, C being bag of n st c in dom p & c <= k & p.
c = C holds C <= A,T by A3,A4;
set m = max(A,Ck,T);
A11: A <= m,T by TERMORD:14;
per cases by TERMORD:12;
suppose
A12: m = A;
A13: now
let c be Nat,C be bag of n such that
A14: c in dom p and
A15: c <= k+1 and
A16: p.c = C;
per cases by A15,XXREAL_0:1;
suppose
c = k+1;
hence C <= m,T by A16,TERMORD:14;
end;
suppose
c < k+1;
then c <= k by NAT_1:13;
then C <= A,T by A10,A14,A16;
hence C <= m,T by A11,TERMORD:8;
end;
end;
a <= k+1 by A8,NAT_1:13;
hence thesis by A7,A9,A12,A13;
end;
suppose
A17: m = Ck;
now
let c be Nat, C be bag of n such that
A18: c in dom p and
A19: c <= k+1 and
A20: p.c = C;
per cases by A19,XXREAL_0:1;
suppose
c = k+1;
hence C <= m,T by A20,TERMORD:14;
end;
suppose
c < k+1;
then c <= k by NAT_1:13;
then C <= A,T by A10,A18,A20;
hence C <= m,T by A11,TERMORD:8;
end;
end;
hence thesis by A6,A17;
end;
end;
suppose
k >= len p;
hence thesis by NAT_1:13;
end;
end;
A21: p <> {} by A1;
A22: P[1]
proof
A23: 1 in dom p by A1,FINSEQ_3:32;
then p.1 in B by A1,FUNCT_1:def 3;
then reconsider A = p.1 as bag of n;
now
let c be Nat, C be bag of n such that
A24: c in dom p and
A25: c <= 1 and
A26: p.c = C;
1 <= c by A24,FINSEQ_3:25;
then C = A by A25,A26,XXREAL_0:1;
hence C <= A,T by TERMORD:6;
end;
hence thesis by A23;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A22,A2);
then consider a being Nat, A being bag of n such that
A27: a in dom p and
a <= len p and
A28: p.a = A and
A29: for c being Nat, C being bag of n st c in dom p & c <= len p & p.
c = C holds C <= A, T by A21;
take A;
thus A in B by A1,A27,A28,FUNCT_1:def 3;
now
let x be bag of n;
assume x in B;
then consider y being Nat such that
A30: y in dom p and
A31: p.y = x by A1,FINSEQ_2:10;
y <= len p by A30,FINSEQ_3:25;
hence x <= A,T by A29,A30,A31;
end;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be bag of n such that
A32: IT1 in B and
A33: for x being bag of n st x in B holds x <= IT1,T and
A34: IT2 in B and
A35: for x being bag of n st x in B holds x <= IT2,T;
A36: IT1 <= IT2,T by A32,A35;
IT2 <= IT1,T by A33,A34;
hence IT1 = IT2 by A36,TERMORD:7;
end;
end;
registration
let O be Ordinal;
cluster InvLexOrder O -> connected;
coherence
proof
InvLexOrder O is well-ordering by BAGORDER:25;
hence thesis by WELLORD1:def 4;
end;
end;
Lm4: for G being _Graph, W being Walk of G,
e,v being object st e Joins W.last(),
v,G holds W.addEdge(e).length() = W.length() + 1
proof
let G be _Graph, W be Walk of G, e,v be object;
assume e Joins W.last(),v,G;
then
A1: W.addEdge(e).edgeSeq() = W.edgeSeq()^<*e*> by GLIB_001:82;
len <*e*> = 1 by FINSEQ_1:39;
hence thesis by A1,FINSEQ_1:22;
end;
Lm5: for G being _Graph, W being Walk of G holds W.length() = W.reverse()
.length()
proof
let G be _Graph, W be Walk of G;
A1: len W = 2*W.length() + 1 by GLIB_001:112;
len W = len W.reverse() by GLIB_001:21;
then 2*W.length()+1-1 = 2*W.reverse().length()+1-1 by A1,GLIB_001:112;
hence thesis;
end;
Lm6: for G being _Graph, W being Walk of G
for e,x being object st e Joins W
.last(),x,G for n being Nat st n in dom W holds W.addEdge(e).n = W.n & n in dom
W.addEdge(e)
proof
let G be _Graph, W be Walk of G;
let e,x be object such that
A1: e Joins W.last(),x,G;
let n be Nat such that
A2: n in dom W;
thus W.addEdge(e).n = W.n by A1,A2,GLIB_001:65;
A3: 1 <= n by A2,FINSEQ_3:25;
A4: len W < len W + 2 by XREAL_1:29;
n <= len W by A2,FINSEQ_3:25;
then
A5: n <= len W + 2 by A4,XXREAL_0:2;
len W.addEdge(e) = len W + 2 by A1,GLIB_001:64;
hence thesis by A3,A5,FINSEQ_3:25;
end;
begin :: More on Sequences
definition
let s be ManySortedSet of NAT;
attr s is iterative means
:Def5:
for k, n being Nat st s.k = s.n holds s.(k+ 1) = s.(n+1);
end;
definition
let S be ManySortedSet of NAT;
attr S is eventually-constant means
:Def6:
ex n being Nat st for m being Nat st n <= m holds S.n = S.m;
end;
registration
cluster halting iterative eventually-constant for ManySortedSet of NAT;
existence
proof
set Fa = NAT --> 1;
reconsider F=Fa as ManySortedSet of NAT;
take F;
F.0 = F.(0+1);
hence F is halting;
thus F is iterative;
for n be Nat st 0 <= n holds F.0 = F.n by FUNCOP_1:7,ORDINAL1:def 12;
hence thesis;
end;
end;
theorem Th7:
for Gs being ManySortedSet of NAT st Gs is halting & Gs is
iterative holds Gs is eventually-constant
proof
let Gs be ManySortedSet of NAT such that
A1: Gs is halting and
A2: Gs is iterative;
set GL = Gs.Lifespan();
defpred P[Nat] means Gs.GL = Gs.(GL+$1);
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Gs.(GL+1) = Gs.(GL+k+1) by A2;
hence thesis by A1,GLIB_000:def 56;
end;
A4: P[ 0 ];
A5: for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
now
let n be Nat;
assume GL <= n;
then ex i being Nat st GL + i = n by NAT_1:10;
hence Gs.GL = Gs.n by A5;
end;
hence thesis;
end;
registration
cluster halting iterative -> eventually-constant for ManySortedSet of NAT;
coherence by Th7;
end;
theorem Th8:
for Gs being ManySortedSet of NAT st Gs is eventually-constant
holds Gs is halting
proof
let Gs be ManySortedSet of NAT;
assume Gs is eventually-constant;
then consider n being Nat such that
A1: for m being Nat st n <= m holds Gs.n = Gs.m;
n <= n+1 by NAT_1:13;
then Gs.n = Gs.(n+1) by A1;
hence thesis;
end;
registration
cluster eventually-constant -> halting for ManySortedSet of NAT;
coherence by Th8;
end;
theorem Th9:
for Gs being iterative eventually-constant ManySortedSet of NAT
for n being Nat st Gs.Lifespan() <= n holds Gs.(Gs.Lifespan()) = Gs.n
proof
let Gs be iterative eventually-constant ManySortedSet of NAT;
set GL = Gs.Lifespan();
defpred P[Nat] means Gs.GL = Gs.(GL+$1);
let n be Nat;
assume GL <= n;
then
A1: ex i being Nat st GL + i = n by NAT_1:10;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Gs.(GL+1) = Gs.(GL+k+1) by Def5;
hence thesis by GLIB_000:def 56;
end;
A3: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
hence thesis by A1;
end;
theorem Th10:
for Gs being iterative eventually-constant ManySortedSet of NAT
for n,m being Nat st Gs.Lifespan() <= n & n <= m holds Gs.m = Gs.n
proof
let Gs be iterative eventually-constant ManySortedSet of NAT;
let n,m be Nat such that
A1: Gs.Lifespan() <= n and
A2: n <= m;
Gs.(Gs.Lifespan()) = Gs.m by A1,A2,Th9,XXREAL_0:2;
hence thesis by A1,Th9;
end;
begin :: Vertex numbering sequences
definition
let G be _finite _Graph;
mode preVNumberingSeq of G -> ManySortedSet of NAT means
:Def7:
for i being Nat holds it.i is PartFunc of the_Vertices_of G, NAT;
existence
proof
deffunc F(object) = {};
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
take f;
let i be Nat;
i in NAT by ORDINAL1:def 12;
then f.i = {} by A1;
hence thesis by RELSET_1:12;
end;
end;
definition
let G be _finite _Graph, S be preVNumberingSeq of G, n be Nat;
redefine func S.n -> PartFunc of the_Vertices_of G, NAT; :: redefines . (FUNCT_1, definition)
coherence by Def7;
end;
definition
let G be _finite _Graph, S be preVNumberingSeq of G;
attr S is vertex-numbering means
:Def8:
S.0 = {} & S is iterative & S is
halting & S.Lifespan() = G.order() & for n being Nat st n < S.Lifespan() ex w
being Vertex of G st not w in dom (S.n) & (S.(n+1)) = (S.n) +* (w .--> (S
.Lifespan()-'n));
end;
registration
let G be _finite _Graph;
cluster vertex-numbering for preVNumberingSeq of G;
existence
proof
set N = card the_Vertices_of G;
set vs = canFS the_Vertices_of G;
deffunc F(Element of NAT) = N -' $1 +1;
consider s being sequence of NAT such that
A1: for n being Element of NAT holds s.n = F(n) from FUNCT_2:sch 4;
defpred P[object,object] means
ex n being Nat st $1 = n & $2 = s*((vs | Seg n)");
A2: for n being object st n in NAT ex j being object st P[n,j]
proof
let n be object;
assume n in NAT;
then reconsider n9 = n as Nat;
take s*((vs | Seg n9)");
thus thesis;
end;
consider S being ManySortedSet of NAT such that
A3: for n being object st n in NAT holds P[n,S.n] from PBOOLE:sch 3(A2);
A4: for n being Nat holds S.n = s*((vs | Seg n)")
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then ex i9 being Nat st n = i9 & S.n = s*((vs | Seg i9)") by A3;
hence thesis;
end;
A5: for n being Nat st n >= len vs holds S.n = s*(vs")
proof
A6: dom vs = Seg len vs by FINSEQ_1:def 3;
let n be Nat;
assume n >= len vs;
then dom vs c= Seg n by A6,FINSEQ_1:5;
then vs | Seg n = vs by RELAT_1:68;
hence thesis by A4;
end;
A7: now
let i be Nat;
set Si = s*((vs | Seg i)");
A8: rng (Si) c= NAT;
vs | Seg i is one-to-one by FUNCT_1:52;
then
A9: (vs | Seg i)~ = (vs | Seg i)" by FUNCT_1:def 5;
now
let x be object;
assume x in dom Si;
then x in dom ((vs | Seg i)") by FUNCT_1:11;
then x in rng (vs | Seg i) by A9,RELAT_1:20;
hence x in the_Vertices_of G;
end;
then
A10: dom (Si) c= the_Vertices_of G;
S.i = s*((vs | Seg i)") by A4;
hence S.i is PartFunc of the_Vertices_of G, NAT by A10,A8,RELSET_1:4;
end;
A11: dom s = NAT by FUNCT_2:def 1;
A12: for n being Nat st n <= len vs holds card (S.n) = n
proof
let n be Nat;
assume n <= len vs;
then
A13: Seg n c= Seg len vs by FINSEQ_1:5;
A14: vs | Seg n is one-to-one by FUNCT_1:52;
A15: S.n = s*((vs | Seg n)") by A4;
A16: card Seg n = n by FINSEQ_1:57;
dom vs = Seg len vs by FINSEQ_1:def 3;
then
A17: dom (vs | Seg n) = Seg n by A13,RELAT_1:62;
then rng ((vs | Seg n)") = Seg n by A14,FUNCT_1:33;
then dom (s*((vs | Seg n)")) = dom ((vs | Seg n)") by A11,RELAT_1:27
.= rng (vs | Seg n) by A14,FUNCT_1:33;
then card dom (s*((vs | Seg n)")) = n by A14,A17,A16,CARD_1:70;
hence thesis by A15,CARD_1:62;
end;
reconsider S as preVNumberingSeq of G by A7,Def7;
A18: len vs = N by FINSEQ_1:93;
A19: S is iterative
proof
A20: for k, n being Nat st k < n & S.k = S.n holds S.(k+1) = S.(n+1)
proof
let k, n be Nat such that
A21: k < n and
A22: S.k = S.n;
per cases;
suppose
A23: n < N;
then card (S.n) = n by A18,A12;
hence thesis by A18,A12,A21,A22,A23,XXREAL_0:2;
end;
suppose
A24: N <= n;
per cases;
suppose
A25: k < N;
A26: rng (vs") c= dom s
proof
let x be object;
assume x in rng (vs");
then x in rng ((vs qua Relation)~) by FUNCT_1:def 5;
then x in dom vs by RELAT_1:20;
then x in NAT;
hence thesis by FUNCT_2:def 1;
end;
A27: S.n = (vs" qua Relation)*s by A18,A5,A24;
card (S.n) = card dom (S.n) by CARD_1:62
.= card dom (vs") by A27,A26,RELAT_1:27
.= card rng vs by FUNCT_1:33
.= card dom vs by CARD_1:70
.= len vs by CARD_1:62;
hence thesis by A18,A12,A22,A25;
end;
suppose
A28: k >= N;
A29: n+1 >= N by A24,NAT_1:13;
k+1 >= N by A28,NAT_1:13;
hence S.(k+1) = s*(vs") by A18,A5
.= S.(n+1) by A18,A5,A29;
end;
end;
end;
let k, n be Nat such that
A30: S.k = S.n;
per cases by XXREAL_0:1;
suppose
k < n;
hence S.(k+1) = S.(n+1) by A20,A30;
end;
suppose
k > n;
hence S.(k+1) = S.(n+1) by A20,A30;
end;
suppose
k = n;
hence thesis;
end;
end;
reconsider N as Element of NAT;
A31: N <= N+1 by NAT_1:11;
A32: N >= len vs by FINSEQ_1:93;
then
A33: S.N = s*(vs") by A5
.= S.(N+1) by A5,A32,A31,XXREAL_0:2;
then
A34: S is halting;
A35: for n being Nat st S.n = S.(n+1) holds N <= n
proof
let n be Nat such that
A36: S.n = S.(n+1) and
A37: N > n;
A38: n+1 <= N by A37,NAT_1:13;
n = card (S.(n+1)) by A18,A12,A36,A37
.= n+1 by A18,A12,A38;
hence thesis;
end;
then
A39: S.Lifespan() = G.order() by A33,A34,GLIB_000:def 56;
A40: now
let n be Nat such that
A41: n < S.Lifespan();
n < N by A33,A34,A35,A41,GLIB_000:def 56;
then
A42: n+1 <= N by NAT_1:13;
set w = vs.(n+1);
A43: 0+1 <= n+1 by NAT_1:13;
n+1 <= len vs by A42,FINSEQ_1:93;
then
A44: n+1 in dom vs by A43,FINSEQ_3:25;
then w in rng vs by FUNCT_1:3;
then reconsider w as Vertex of G;
take w;
A45: vs | Seg n is one-to-one by FUNCT_1:52;
hereby
assume w in dom (S.n);
then w in dom (s*((vs | Seg n)")) by A4;
then w in dom ((vs | Seg n)") by FUNCT_1:11;
then w in rng (vs | Seg n) by A45,FUNCT_1:33;
then consider x being object such that
A46: x in dom (vs | Seg n) and
A47: w = (vs | Seg n).x by FUNCT_1:def 3;
A48: w = vs.x by A46,A47,FUNCT_1:47;
A49: x in Seg n by A46,RELAT_1:57;
A50: x in dom vs by A46,RELAT_1:57;
reconsider x as Nat by A46;
x <= n by A49,FINSEQ_1:1;
then x <> n+1 by NAT_1:13;
hence contradiction by A44,A48,A50,FUNCT_1:def 4;
end;
A51: vs | Seg (n+1) is one-to-one by FUNCT_1:52;
n <= n+1 by NAT_1:11;
then
A52: Seg n c= Seg (n+1) by FINSEQ_1:5;
now
now
let x be object;
hereby
assume x in dom (S.(n+1));
then x in dom (s*((vs | Seg (n+1))")) by A4;
then x in dom ((vs | Seg (n+1))") by FUNCT_1:11;
then x in rng (vs | Seg (n+1)) by A51,FUNCT_1:33;
then consider a being object such that
A53: a in dom (vs | Seg (n+1)) and
A54: x = (vs | Seg (n+1)).a by FUNCT_1:def 3;
A55: a in Seg (n+1) by A53,RELAT_1:57;
A56: dom ((S.n) +* (w .--> (S.Lifespan()-'n))) = dom (S.n) \/ dom
(w .--> (S.Lifespan()-'n)) by FUNCT_4:def 1;
reconsider a as Nat by A53;
A57: a in dom vs by A53,RELAT_1:57;
A58: a <= n+1 by A55,FINSEQ_1:1;
A59: 1 <= a by A55,FINSEQ_1:1;
per cases by A58,NAT_1:8;
suppose
a <= n;
then
A60: a in Seg n by A59,FINSEQ_1:1;
then
A61: a in dom (vs | Seg n) by A57,RELAT_1:57;
A62: (vs | Seg n).a = vs.a by A60,FUNCT_1:49
.= x by A54,A55,FUNCT_1:49;
then x in rng (vs | Seg n) by A61,FUNCT_1:3;
then
A63: x in dom ((vs | Seg n)") by A45,FUNCT_1:33;
((vs | Seg n)").x = a by A45,A61,A62,FUNCT_1:32;
then ((vs | Seg n)").x in dom s by A11,ORDINAL1:def 12;
then x in dom (s*((vs | Seg n)")) by A63,FUNCT_1:11;
then x in dom (S.n) by A4;
hence x in dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by A56,
XBOOLE_0:def 3;
end;
suppose
a = n+1;
then x = w by A53,A54,FUNCT_1:47;
then x in dom (w .--> (S.Lifespan()-'n)) by FUNCOP_1:74;
hence x in dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by A56,
XBOOLE_0:def 3;
end;
end;
assume x in dom ((S.n) +* (w .--> (S.Lifespan()-'n)));
then
A64: x in dom (S.n) \/ dom (w .--> (S.Lifespan()-'n)) by FUNCT_4:def 1;
per cases by A64,XBOOLE_0:def 3;
suppose
A65: x in dom (S.n);
vs | Seg n c= vs | Seg (n+1) by A52,RELAT_1:75;
then
A66: rng (vs | Seg n) c= rng (vs | Seg (n+1)) by RELAT_1:11;
A67: x in dom (s*((vs | Seg n)")) by A4,A65;
then
A68: x in dom ((vs | Seg n)") by FUNCT_1:11;
then x in rng (vs | Seg n) by A45,FUNCT_1:33;
then x in rng (vs | Seg (n+1)) by A66;
then
A69: x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
A70: ((vs | Seg n)").x in dom s by A67,FUNCT_1:11;
((vs | Seg n)").x = ((vs | Seg (n+1))").x by A52,A68,Lm2;
then x in dom (s*((vs | Seg (n+1))")) by A70,A69,FUNCT_1:11;
hence x in dom (S.(n+1)) by A4;
end;
suppose
A71: x in dom (w .--> (S.Lifespan()-'n));
A72: rng ((vs | Seg (n+1))") = dom (vs | Seg (n+1)) by A51,FUNCT_1:33;
x = w by A71,FUNCOP_1:75;
then x in rng (vs | Seg (n+1)) by A44,FINSEQ_1:4,FUNCT_1:50;
then
A73: x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
then ((vs | Seg (n+1))").x in rng ((vs | Seg (n+1))") by FUNCT_1:3;
then x in dom (s*((vs | Seg (n+1))")) by A11,A73,A72,FUNCT_1:11;
hence x in dom (S.(n+1)) by A4;
end;
end;
hence
A74: dom (S.(n+1)) = dom ((S.n) +* (w .--> (S.Lifespan()-'n))) by TARSKI:2;
let x be object such that
A75: x in dom (S.(n+1));
A76: x in dom (S.n) \/ dom (w .--> (S.Lifespan()-'n)) by A74,A75,
FUNCT_4:def 1;
A77: S.(n+1) = s*((vs | Seg (n+1))") by A4;
A78: S.n = s*((vs | Seg n)") by A4;
per cases by A76,XBOOLE_0:def 3;
suppose
A79: x in dom (S.n);
then
A80: x in dom ((vs | Seg n)") by A78,FUNCT_1:11;
then x in rng (vs | Seg n) by A45,FUNCT_1:33;
then consider m being object such that
A81: m in dom (vs | Seg n) and
A82: (vs | Seg n).m = x by FUNCT_1:def 3;
A83: m in Seg n by A81,RELAT_1:57;
reconsider m as Nat by A81;
A84: m in dom vs by A81,RELAT_1:57;
m <= n by A83,FINSEQ_1:1;
then
A85: m < n+1 by NAT_1:13;
vs.m = x by A81,A82,FUNCT_1:47;
then
A86: x <> w by A44,A84,A85,FUNCT_1:def 4;
thus (S.(n+1)).x = s.(((vs | Seg (n+1))").x) by A75,A77,FUNCT_1:12
.= s.(((vs | Seg n)").x) by A52,A80,Lm2
.= (S.n).x by A78,A79,FUNCT_1:12
.= ((S.n) +* (w .--> (S.Lifespan()-'n))).x by A86,FUNCT_4:83;
end;
suppose
A87: x in dom (w .--> (S.Lifespan()-'n));
n+1 in Seg (n+1) by FINSEQ_1:4;
then
A88: n+1 in dom (vs | Seg (n+1)) by A44,RELAT_1:57;
then
A89: (vs | Seg (n+1)).(n+1) = w by FUNCT_1:47;
A90: x = w by A87,FUNCOP_1:75;
then x in rng (vs | Seg (n+1)) by A44,FINSEQ_1:4,FUNCT_1:50;
then
A91: x in dom ((vs | Seg (n+1))") by A51,FUNCT_1:33;
A92: ((S.n) +* (w .--> (S.Lifespan()-'n))).x = (w .--> (S
.Lifespan()-'n)).x by A87,FUNCT_4:13
.= (S.Lifespan()-'n) by A90,FUNCOP_1:72;
(S.(n+1)).x = (s*((vs | Seg (n+1))")).x by A4
.= s.(((vs | Seg (n+1))").x) by A91,FUNCT_1:13
.= s.(n+1) by A51,A90,A88,A89,FUNCT_1:32
.= N-'(n+1)+1 by A1
.= N-(n+1)+1 by A42,XREAL_1:233
.= N-n
.= S.Lifespan() -' n by A39,A41,XREAL_1:233;
hence (S.(n+1)).x = ((S.n) +* (w .--> (S.Lifespan()-'n))).x by A92;
end;
end;
hence S.(n+1) = (S.n) +* (w .--> (S.Lifespan()-'n)) by FUNCT_1:2;
end;
take S;
card (S.0) = 0 by A12;
then S.0 = {};
hence thesis by A19,A34,A39,A40;
end;
end;
:: Facts hidden in the existence proof?
registration
let G be _finite _Graph;
cluster vertex-numbering -> halting iterative for preVNumberingSeq of G;
correctness;
end;
definition
let G be _finite _Graph;
mode VNumberingSeq of G is vertex-numbering preVNumberingSeq of G;
end;
definition
let G be _finite _Graph, S be VNumberingSeq of G, n be Nat;
func S.PickedAt(n) -> set means
:Def9:
it = the Element of the_Vertices_of G if n
>= S.Lifespan() otherwise not it in dom (S.n) & S.(n+1) = S.n +* (it .--> (S
.Lifespan()-'n));
existence
proof
per cases;
suppose
n >= S.Lifespan();
hence thesis;
end;
suppose
n < S.Lifespan();
then
ex w being Vertex of G st ( not w in dom (S.n))& S.(n+1) = (S.n) +*
(w .--> (S.Lifespan()-'n)) by Def8;
hence thesis;
end;
end;
uniqueness
proof
set VL1 = S.(n+1);
set VLN = S.n;
let IT1,IT2 be set;
thus n >= S.Lifespan() & IT1 = the Element of the_Vertices_of G &
IT2 = the Element of the_Vertices_of G implies IT1 = IT2;
assume n < S.Lifespan();
assume that
A1: not IT1 in dom VLN and
A2: VL1 = VLN +* (IT1 .--> (S.Lifespan()-'n));
set f2 = IT2 .--> (S.Lifespan()-'n);
set f1 = IT1 .--> (S.Lifespan()-'n);
assume that
not IT2 in dom VLN and
A3: VL1 = VLN +* (IT2 .--> (S.Lifespan()-'n));
dom f2 = {IT2};
then
A4: dom VL1 = dom VLN \/ {IT2} by A3,FUNCT_4:def 1;
dom f1 = {IT1};
then
A5: dom VL1 = dom VLN \/ {IT1} by A2,FUNCT_4:def 1;
now
assume IT1 <> IT2;
then not IT1 in {IT2} by TARSKI:def 1;
then
A6: not IT1 in dom VL1 by A1,A4,XBOOLE_0:def 3;
IT1 in {IT1} by TARSKI:def 1;
hence contradiction by A5,A6,XBOOLE_0:def 3;
end;
hence thesis;
end;
consistency;
end;
theorem Th11:
for G being _finite _Graph, S being VNumberingSeq of G, n being
Nat st n < S.Lifespan() holds S.PickedAt(n) in dom (S.(n+1)) & dom (S.(n+1)) =
dom (S.n) \/ {S.PickedAt(n)}
proof
let G being _finite _Graph, GS be VNumberingSeq of G, n be Nat such that
A1: n < GS.Lifespan();
set f = (GS.PickedAt(n)) .--> (GS.Lifespan() -' n);
set CN1 = GS.(n+1);
set CSN = GS.n;
set VLN = CSN;
set VN1 = CN1;
A2: dom f = {GS.PickedAt(n)};
A3: GS.PickedAt(n) in {GS.PickedAt(n)} by TARSKI:def 1;
A4: VN1 = VLN +* (GS.PickedAt(n) .--> (GS.Lifespan() -' n)) by A1,Def9;
then dom VN1 = dom VLN \/ {GS.PickedAt(n)} by A2,FUNCT_4:def 1;
hence GS.PickedAt(n) in dom CN1 by A3,XBOOLE_0:def 3;
thus thesis by A4,A2,FUNCT_4:def 1;
end;
theorem Th12:
for G being _finite _Graph, S being VNumberingSeq of G, n being
Nat st n < S.Lifespan() holds (S.(n+1)).(S.PickedAt(n)) = S.Lifespan()-'n
proof
let G being _finite _Graph, GS be VNumberingSeq of G, n be Nat such that
A1: n < GS.Lifespan();
set w = GS.PickedAt(n);
set CN1 = GS.(n+1);
set CSN = GS.n;
set VLN = CSN;
set VN1 = CN1;
set f = w .--> (GS.Lifespan() -' n);
A2: f.w = GS.Lifespan() -' n by FUNCOP_1:72;
A3: w in dom f by TARSKI:def 1;
VN1 = VLN +* (w .--> (GS.Lifespan() -' n)) by A1,Def9;
hence thesis by A3,A2,FUNCT_4:13;
end;
theorem
for G being _finite _Graph, S being VNumberingSeq of G, n being Nat st
n <= S.Lifespan() holds card dom (S.n) = n
proof
let G be _finite _Graph, S be VNumberingSeq of G, n be Nat such that
A1: n <= S.Lifespan();
defpred P[Nat] means $1 <= S.Lifespan() implies card dom (S.$1) = $1;
A2: for k being Nat st k < S.Lifespan() & card dom (S.k) = k holds card dom
(S.(k+1)) = k+1
proof
let k be Nat such that
A3: k < S.Lifespan() and
A4: card dom (S.k) = k;
set w = S.PickedAt(k);
set CK1 = S.(k+1);
set CSK = S.k;
set VLK = CSK;
set VK1 = CK1;
set wf = w .--> (S.Lifespan() -' k);
A5: dom wf = {w};
VK1 = VLK +* (w .--> (S.Lifespan()-'k)) by A3,Def9;
then
A6: dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
not w in dom VLK by A3,Def9;
hence thesis by A4,A6,CARD_2:41;
end;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A8: P[k];
per cases;
suppose
k < S.Lifespan();
hence thesis by A2,A8;
end;
suppose
k >= S.Lifespan();
hence thesis by NAT_1:13;
end;
end;
A9: P[ 0 ] by Def8,CARD_1:27,RELAT_1:38;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A7);
hence thesis by A1;
end;
theorem Th14:
for G being _finite _Graph, S being VNumberingSeq of G, n being
Nat holds rng (S.n) = (Seg S.Lifespan()) \ Seg (S.Lifespan()-'n)
proof
let G be _finite _Graph, S be VNumberingSeq of G, n be Nat;
set CSN = S.n;
set CSO = S.S.Lifespan();
set GN = S.Lifespan();
defpred P[Nat] means $1 <= GN implies rng (S.$1) = (Seg GN) \ Seg (GN-'$1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
set CK1 = S.(k+1);
set CSK = S.k;
set VLK = CSK;
set VK1 = CK1;
per cases;
suppose
A3: k+1 <= GN;
set w = S.PickedAt(k);
set wf = w .--> (GN -' k);
A5: k < GN by A3,NAT_1:13;
then not w in dom VLK by Def9;
then
A6: dom wf misses dom VLK by ZFMISC_1:50;
A7: rng wf = {GN -' k} by FUNCOP_1:8;
VK1 = VLK +* (w .--> (GN -' k)) by A5,Def9;
then rng VK1 = rng VLK \/ {GN -' k} by A7,A6,NECKLACE:6;
hence thesis by A2,A5,Th5;
end;
suppose
GN < k+1;
hence thesis;
end;
end;
A8: P[ 0 ]
proof
set CS0 = S.0;
set VL0 = CS0;
A9: GN -' 0 = GN - 0 by XREAL_1:233;
rng VL0 = {} by Def8,RELAT_1:38;
hence thesis by A9,XBOOLE_1:37;
end;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A8,A1);
per cases;
suppose
n <= GN;
hence thesis by A10;
end;
suppose
A11: GN < n;
then GN - n < n - n by XREAL_1:9;
then GN -' n = 0 by XREAL_0:def 2;
then
A12: GN -' GN = GN -' n by XREAL_1:232;
CSO = CSN by A11,Th9;
hence thesis by A10,A12;
end;
end;
theorem Th15:
for G being _finite _Graph, S being VNumberingSeq of G, n being
Nat, x being set holds (S.n).x <= S.Lifespan() & (x in dom (S.n) implies 1 <= (
S.n).x)
proof
let G be _finite _Graph, S be VNumberingSeq of G, n be Nat, x be set;
set CSN = S.n;
set VLN = CSN;
A1: now
per cases;
suppose
not x in dom VLN;
hence VLN.x <= S.Lifespan() by FUNCT_1:def 2;
end;
suppose
x in dom VLN;
then VLN.x in rng VLN by FUNCT_1:def 3;
then VLN.x in (Seg S.Lifespan()) \ Seg (S.Lifespan() -'n ) by Th14;
hence VLN.x <= S.Lifespan() by Th3;
end;
end;
now
assume x in dom (S.n);
then VLN.x in rng VLN by FUNCT_1:def 3;
then VLN.x in (Seg S.Lifespan()) \ Seg (S.Lifespan() -'n ) by Th14;
then S.Lifespan() -' n < VLN.x by Th3;
then 0+1 <= VLN.x by NAT_1:13;
hence 1 <= VLN.x;
end;
hence thesis by A1;
end;
theorem Th16:
for G being _finite _Graph, S being VNumberingSeq of G, n,m being
Nat st S.Lifespan() -' n < m & m <= S.Lifespan() ex v being Vertex of G st v in
dom (S.n) & (S.n).v = m
proof
let G being _finite _Graph, S be VNumberingSeq of G, n,m be Nat such that
A1: S.Lifespan() -' n < m and
A2: m <= S.Lifespan();
set CSN = S.n;
set VLN = CSN;
m in (Seg S.Lifespan()) \ Seg (S.Lifespan()-'n) by A1,A2,Th3;
then m in rng VLN by Th14;
then consider v being object such that
A3: v in dom VLN and
A4: m = VLN.v by FUNCT_1:def 3;
reconsider v as set by TARSKI:1;
take v;
thus v is Vertex of G by A3;
thus v in dom CSN by A3;
thus thesis by A4;
end;
theorem Th17:
for G being _finite _Graph, S being VNumberingSeq of G, m, n
being Nat st m <= n holds S.m c= S.n
proof
let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat;
assume m <= n;
then
A1: ex j being Nat st n = m + j by NAT_1:10;
set CSM = S.m;
set VLM = CSM;
defpred P[Nat] means VLM c= S.(m+$1);
A2: now
let k be Nat;
set CSK = S.k;
set VLK = CSK;
set CK1 = S.(k+1);
set VK1 = CK1;
per cases;
suppose
A3: k < S.Lifespan();
set w = S.PickedAt(k);
set wf = w .--> (S.Lifespan() -' k);
not w in dom VLK by A3,Def9;
then
A5: dom wf misses dom VLK by ZFMISC_1:50;
VK1 = VLK +* (w .--> (S.Lifespan()-'k)) by A3,Def9;
hence VLK c= VK1 by A5,FUNCT_4:32;
end;
suppose
A6: S.Lifespan() <= k;
k <= k+1 by NAT_1:13;
hence VLK c= VK1 by A6,Th10;
end;
end;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A8: P[k];
S.(m+k) c= S.(m+k+1) by A2;
hence thesis by A8,XBOOLE_1:1;
end;
A9: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A9,A7);
hence thesis by A1;
end;
theorem Th18:
for G being _finite _Graph, S being VNumberingSeq of G, n being
Nat holds S.n is one-to-one
proof
let G being _finite _Graph, S be VNumberingSeq of G, n be Nat;
defpred P[Nat] means S.$1 is one-to-one;
A1: for k being Nat st P[k] holds P[k+1]
proof
set GN = S.Lifespan();
let k be Nat such that
A2: P[k];
set w = S.PickedAt(k);
set CK1 = S.(k+1);
set CSK = S.k;
set VLK = CSK;
set VL1 = CK1;
per cases;
suppose
A3: k < GN;
set wf = w .--> (GN -' k);
A4: now
assume
A5: GN -' k in rng VLK;
rng VLK = (Seg GN) \ Seg (GN -' k) by Th14;
hence contradiction by A5,Th3;
end;
rng wf = {GN -' k} by FUNCOP_1:8;
then
A6: rng wf misses rng VLK by A4,ZFMISC_1:50;
VL1 = VLK +* (w .--> (GN -' k)) by A3,Def9;
hence thesis by A2,A6,FUNCT_4:92;
end;
suppose
A7: k >= GN;
k <= k+1 by NAT_1:13;
hence thesis by A2,A7,Th10;
end;
end;
A8: P[ 0 ] by Def8;
for k being Nat holds P[k] from NAT_1:sch 2(A8,A1);
hence thesis;
end;
theorem Th19:
for G being _finite _Graph, S being VNumberingSeq of G, m,n being
Nat, v being set st v in dom (S.m) & v in dom (S.n) holds (S.m).v = (S.n).v
proof
let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat;
let v be set such that
A1: v in dom (S.m) and
A2: v in dom (S.n);
set VLM = S.m;
A3: [v,VLM.v] in VLM by A1,FUNCT_1:def 2;
set VLN = S.n;
A4: [v,VLN.v] in VLN by A2,FUNCT_1:def 2;
per cases;
suppose
m <= n;
then VLM c= VLN by Th17;
hence thesis by A2,A3,FUNCT_1:def 2;
end;
suppose
m > n;
then VLN c= VLM by Th17;
hence thesis by A1,A4,FUNCT_1:def 2;
end;
end;
theorem Th20:
for G being _finite _Graph, S being VNumberingSeq of G, m,n being
Nat, v being set st v in dom (S.m) & (S.m).v = n holds S.PickedAt(S.Lifespan()
-'n) = v
proof
let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat, v be set;
set CSM = S.m;
set VLM = CSM;
set j = S.Lifespan() -' n;
set CJ1 = S.(j+1);
set VJ1 = CJ1;
assume that
A1: v in dom CSM and
A2: VLM.v = n;
set w = S.PickedAt(j);
n <= S.Lifespan() by A2,Th15;
then
A3: S.Lifespan() -' n = S.Lifespan() - n by XREAL_1:233;
A4: 0 < n by A1,A2,Th15;
then
A5: j < S.Lifespan() by A3,XREAL_1:44;
then S.Lifespan() -' j = S.Lifespan() - (S.Lifespan() - n) by A3,XREAL_1:233;
then
A6: VJ1.w = n by A4,A3,Th12,XREAL_1:44;
A7: VLM is one-to-one by Th18;
A8: w in dom CJ1 by A5,Th11;
per cases;
suppose
A9: m <= j;
then m + n <= S.Lifespan() - n + n by A3,XREAL_1:6;
then
A10: n + m - m <= S.Lifespan() - m by XREAL_1:9;
A11: rng VLM = (Seg S.Lifespan()) \ Seg (S.Lifespan() -' m) by Th14;
A12: n in rng VLM by A1,A2,FUNCT_1:def 3;
S.Lifespan() - m = S.Lifespan() -' m by A5,A9,XREAL_1:233,XXREAL_0:2;
hence thesis by A10,A12,A11,Th3;
end;
suppose
j < m;
then j+1 <= m by NAT_1:13;
then
A13: VJ1 c= VLM by Th17;
then
A14: dom VJ1 c= dom VLM by RELAT_1:11;
[w,n] in VJ1 by A8,A6,FUNCT_1:def 2;
then VLM.w = n by A8,A13,A14,FUNCT_1:def 2;
hence thesis by A1,A2,A8,A7,A14,FUNCT_1:def 4;
end;
end;
theorem Th21:
for G being _finite _Graph, S being VNumberingSeq of G, m, n
being Nat st n < S.Lifespan() & n < m holds S.PickedAt(n) in dom (S.m) & (S.m).
(S.PickedAt(n)) = S.Lifespan() -' n
proof
let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat such that
A1: n < S.Lifespan() and
A2: n < m;
set CN1 = S.(n+1);
set VN1 = CN1;
set v = S.PickedAt(n);
A3: VN1.v = S.Lifespan() -' n by A1,Th12;
set CSM = S.m;
set VLM = CSM;
n+1 <= m by A2,NAT_1:13;
then VN1 c= VLM by Th17;
then
A4: dom VN1 c= dom VLM by RELAT_1:11;
v in dom CN1 by A1,Th11;
hence thesis by A3,A4,Th19;
end;
:: Inequalities relating the vlabel and the current iteration
theorem Th22:
for G being _finite _Graph, S being VNumberingSeq of G, m being
Nat, v being set st v in dom (S.m) holds S.Lifespan() -' (S.m).v < m & S
.Lifespan() -' m < (S.m).v
proof
let G be _finite _Graph, S be VNumberingSeq of G, m be Nat, v be set;
set VLM = S.m;
set j = S.Lifespan() -' VLM.v;
set VLJ = S.j;
assume
A1: v in dom VLM;
then
A2: S.PickedAt(j) = v by Th20;
A3: 0 < VLM.v by A1,Th15;
A4: VLM.v <= S.Lifespan() by Th15;
then j = S.Lifespan() - VLM.v by XREAL_1:233;
then
A5: j < S.Lifespan() by A3,XREAL_1:44;
A6: now
per cases;
suppose
m <= j;
then VLM c= VLJ by Th17;
then dom VLM c= dom VLJ by RELAT_1:11;
hence S.Lifespan() -' VLM.v < m by A1,A2,A5,Def9;
end;
suppose
m > j;
hence S.Lifespan() -' VLM.v < m;
end;
end;
now
per cases;
suppose
A7: S.Lifespan() - m >= 0;
S.Lifespan() - VLM.v < m by A4,A6,XREAL_1:233;
then S.Lifespan() - VLM.v + VLM.v < m + VLM.v by XREAL_1:6;
then S.Lifespan() - m < VLM.v + m - m by XREAL_1:9;
hence S.Lifespan() -'m < VLM.v by A7,XREAL_0:def 2;
end;
suppose
S.Lifespan() - m < 0;
hence S.Lifespan() -'m < VLM.v by A3,XREAL_0:def 2;
end;
end;
hence thesis by A6;
end;
:: If a vertex has a larger vlabel than we do at some point in the
:: algorithm, then it must have been in the vlabel when we were picked
theorem Th23:
for G being _finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & b in dom (S.i) & (S.i).a < (S.i).b holds
b in dom (S.(S.Lifespan() -' (S.i).a))
proof
let G be _finite _Graph, S be VNumberingSeq of G;
let i be Nat, a,b be set such that
A1: a in dom (S.i) and
A2: b in dom (S.i) and
A3: (S.i).a < (S.i).b;
set GN = S.Lifespan();
set CSI = S.i;
set VLI = CSI;
set j = S.Lifespan() -' VLI.a;
set CSJ = S.j;
set VLJ = CSJ;
VLI.a <= GN by Th15;
then
A4: GN -' VLI.a = GN - VLI.a by XREAL_1:233;
then GN -' j = GN - (GN - VLI.a) by NAT_D:35,XREAL_1:233;
then consider w being Vertex of G such that
A5: w in dom CSJ and
A6: VLJ.w = VLI.b by A3,Th15,Th16;
now
assume j >= i;
then VLI c= VLJ by Th17;
then
A7: dom VLI c= dom VLJ by RELAT_1:11;
0 < VLI.a by A1,Th15;
then
A8: j < GN by A4,XREAL_1:44;
a = S.PickedAt(j) by A1,Th20;
hence contradiction by A1,A7,A8,Def9;
end;
then
A9: VLJ c= VLI by Th17;
A10: [w,VLI.b] in VLJ by A5,A6,FUNCT_1:1;
then
A11: VLI.w = VLI.b by A9,FUNCT_1:1;
A12: VLI is one-to-one by Th18;
w in dom VLI by A9,A10,FUNCT_1:1;
hence thesis by A2,A5,A11,A12,FUNCT_1:def 4;
end;
theorem Th24:
for G being _finite _Graph, S being VNumberingSeq of G, i being
Nat, a,b being set st a in dom (S.i) & (S.i).a < (S.i).b holds not a in dom (S.
(S.Lifespan() -' (S.i).b))
proof
let G be _finite _Graph, S be VNumberingSeq of G, i be Nat, a,b being set
such that
A1: a in dom (S.i) and
A2: (S.i).a < (S.i).b;
set GN = S.Lifespan();
set CSI = S.i;
set VLI = CSI;
set k = GN -' VLI.a;
VLI.a <= GN by Th15;
then
A3: k = GN - VLI.a by XREAL_1:233;
set CSK = S.k;
set j = GN -' VLI.b;
set CSJ = S.j;
set VLJ = CSJ;
set VLK = CSK;
VLI.b <= GN by Th15;
then j = GN - VLI.b by XREAL_1:233;
then j < k by A2,A3,XREAL_1:15;
then VLJ c= VLK by Th17;
then
A4: dom VLJ c= dom VLK by RELAT_1:11;
assume
A5: a in dom CSJ;
1 <= VLI.a by A1,Th15;
then
A6: k < GN by A3,XREAL_1:44;
S.PickedAt(k) = a by A1,Th20;
hence contradiction by A6,A5,A4,Def9;
end;
begin :: Lexicographic Breadth-First Search
definition
let X1,X3 be set, X2 be non empty set;
let x be Element of [: PFuncs(X1,X3),X2 :];
redefine func x`1 -> Element of PFuncs(X1,X3); :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
definition
let X1, X3 be non empty set, X2 be set;
let x be Element of [: X1, Funcs(X2,X3) :];
redefine func x`2 -> Element of Funcs(X2,X3); :: redefines `2 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
definition
let G be _Graph;
mode LexBFS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
Funcs(the_Vertices_of G, Fin NAT) :];
end;
registration
let G be _finite _Graph, L be LexBFS:Labeling of G;
cluster L`1 -> finite for set;
coherence
proof
dom L`1 c= the_Vertices_of G;
hence thesis by FINSET_1:10;
end;
cluster L`2 -> finite for set;
coherence;
end;
definition
let G be _Graph;
func LexBFS:Init(G) -> LexBFS:Labeling of G equals
[ {}, the_Vertices_of G
--> {} ];
coherence
proof
set f = the_Vertices_of G --> {};
A1: rng {} c= NAT;
{} c= NAT;
then {} in Fin NAT by FINSUB_1:def 5;
then {{}} c= Fin NAT by ZFMISC_1:31;
then
A2: rng f c= Fin NAT;
dom f = the_Vertices_of G;
then
A3: f in Funcs(the_Vertices_of G, Fin NAT) by A2,FUNCT_2:def 2;
dom {} c= the_Vertices_of G;
then {} in PFuncs(the_Vertices_of G,NAT) by A1,PARTFUN1:def 3;
hence thesis by A3,ZFMISC_1:def 2;
end;
end;
definition
let G be _finite _Graph, L be LexBFS:Labeling of G;
func LexBFS:PickUnnumbered(L) -> Vertex of G means
:Def11:
it = the Element of
the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being non empty
finite Subset of bool NAT, B being non empty finite Subset of Bags NAT, F being
Function st S = rng F & F = L`2 | (the_Vertices_of G \ dom L`1) & (for x being
finite Subset of NAT holds x in S implies ((x,1)-bag in B)) & (for x being set
holds x in B implies ex y being finite Subset of NAT st y in S & x = (y,1)-bag)
& it = the Element of F " {support max(B,InvLexOrder NAT)};
existence
proof
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set F = V2G | (VG \ dom VLG);
set S = rng F;
A1: ex f being Function st L`2 = f & dom f = VG & rng f c= Fin NAT by
FUNCT_2:def 2;
per cases;
suppose
dom VLG = VG;
hence thesis;
end;
suppose
A2: dom VLG <> VG;
dom F = dom V2G /\ (VG \ dom VLG) by RELAT_1:61;
then
A3: dom F = (VG /\ VG) \ dom VLG by A1,XBOOLE_1:49;
A4: now
assume dom F = {};
then VG c= dom VLG by A3,XBOOLE_1:37;
hence contradiction by A2,XBOOLE_0:def 10;
end;
A5: for x being set st x in S holds x is finite;
A6: rng F c= rng V2G by RELAT_1:70;
now
A7: rng V2G c= bool NAT
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng V2G;
then xx c= NAT by FINSUB_1:def 5;
hence thesis;
end;
let x be set such that
A8: x in S;
x in rng V2G by A6,A8;
hence x in bool NAT by A7;
thus x is finite by A8;
end;
then for x being object holds x in S implies x in bool NAT;
then reconsider
S as non empty finite with_finite-elements Subset of bool NAT
by A4,A5,FINSET_1:def 6,RELAT_1:42,TARSKI:def 3;
deffunc F(finite Subset of NAT) = ($1,1)-bag;
set B = {F(x) where x is Element of S: x in S};
consider z being object such that
A9: z in S by XBOOLE_0:def 1;
reconsider z as finite Subset of NAT by A9;
A10: (z,1)-bag in B by A9;
A11: S is finite;
A12: B is finite from FRAENKEL:sch 21(A11);
now
let x be object;
assume x in B;
then ex y being Element of S st x = (y,1)-bag & y in S;
hence x in Bags NAT;
end;
then reconsider B as non empty finite Subset of Bags NAT by A12,A10,
TARSKI:def 3;
A13: for x being set holds x in B implies ex y being finite Subset of
NAT st y in S & x = (y,1)-bag
proof
let x be set;
assume x in B;
then ex y being Element of S st x = (y,1)-bag & y in S;
hence thesis;
end;
set mw = max(B,InvLexOrder NAT);
mw in B by Def4;
then consider y being finite Subset of NAT such that
A14: y in S and
A15: mw = (y,1)-bag by A13;
set IT = the Element of F " {support mw};
y = support mw by A15,UPROOTS:8;
then F " {support mw} is non empty by A14,FUNCT_1:72;
then IT in dom F by FUNCT_1:def 7;
then IT in dom V2G by RELAT_1:57;
then reconsider IT as Vertex of G;
for x being finite Subset of NAT holds x in S implies (x,1)-bag in B;
then ex S being non empty finite Subset of bool NAT, B being non empty
finite Subset of Bags NAT, F being Function st S = rng F & F = (V2G | (VG \ dom
VLG)) & (for x being finite Subset of NAT holds x in S implies ((x,1)-bag in B)
) & (for x being set holds x in B implies ex y being finite Subset of NAT st y
in S & x = (y,1)-bag) &
IT = the Element of F " {support max(B,InvLexOrder NAT)} & IT
is Vertex of G by A13;
hence thesis;
end;
end;
uniqueness
proof
let IT1, IT2 be Vertex of G;
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
thus dom VLG = VG & IT1 = the Element of VG &
IT2 = the Element of VG implies IT1=IT2;
assume dom VLG <> VG;
given
S1 being non empty finite Subset of bool NAT, B1 being non empty
finite Subset of Bags NAT, F1 being Function such that
A16: S1 = rng F1 and
A17: F1 = (V2G | (VG \ dom VLG)) and
A18: for x being finite Subset of NAT holds x in S1 implies (x,1)-bag in B1 and
A19: for x being set holds x in B1 implies ex y being finite Subset of
NAT st y in S1 & x = (y,1)-bag and
A20: IT1 = the Element of F1 " {support max(B1,InvLexOrder NAT)};
given
S2 being non empty finite Subset of bool NAT, B2 being non empty
finite Subset of Bags NAT, F2 being Function such that
A21: S2 = rng F2 and
A22: F2 = (V2G | (VG \ dom VLG)) and
A23: for x being finite Subset of NAT holds x in S2 implies (x,1)-bag in B2 and
A24: for x being set holds x in B2 implies ex y being finite Subset of
NAT st y in S2 & x = (y,1)-bag and
A25: IT2 = the Element of F2 " {support max(B2,InvLexOrder NAT)};
now
let x be object;
assume x in B2;
then
ex y being finite Subset of NAT st y in S2 & x = (y,1)-bag by A24;
hence x in B1 by A16,A17,A18,A21,A22;
end;
then
A26: B2 c= B1;
now
let x be object;
assume x in B1;
then
ex y being finite Subset of NAT st y in S1 & x = (y,1)-bag by A19;
hence x in B2 by A16,A17,A21,A22,A23;
end;
then B1 c= B2;
then B1 = B2 by A26,XBOOLE_0:def 10;
hence IT1 = IT2 by A17,A20,A22,A25;
end;
consistency;
end;
definition
let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, n be
Nat;
func LexBFS:Update(L, v, n) -> LexBFS:Labeling of G equals
[ L`1 +* (v .-->
(G.order()-'n)), L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n}) ];
coherence
proof
set F = ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n});
reconsider nn = G.order()-'n as Element of NAT;
set L2 = L`2 .\/ ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'n});
set f = (v .--> (G.order()-'n));
set L1 = L`1 +* f;
A1: dom f = {v};
A2: rng L1 c= NAT;
dom L1 = dom L`1 \/ dom f by FUNCT_4:def 1;
then dom L1 c= the_Vertices_of G by A1,XBOOLE_1:8;
then
A3: L1 in PFuncs(the_Vertices_of G, NAT) by A2,PARTFUN1:def 3;
{nn} in Fin NAT by FINSUB_1:def 5;
then
A4: {{nn}} c= Fin NAT by ZFMISC_1:31;
consider f being Function such that
A5: L`2 = f and
A6: dom f = the_Vertices_of G and
A7: rng f c= Fin NAT by FUNCT_2:def 2;
rng F c= {{nn}} by FUNCOP_1:13;
then
A8: rng F c= Fin NAT by A4;
A9: dom L2 = dom f \/ dom F by A5,Def1;
A10: rng L2 c= Fin NAT
proof
let y be object;
assume y in rng L2;
then consider x being object such that
A11: x in dom L2 and
A12: y = L2.x by FUNCT_1:def 3;
A13: y = f.x \/ F.x by A5,A11,A12,Def1,A9;
per cases by A11,A9,XBOOLE_0:def 3;
suppose that
A14: x in dom f and
A15: not x in dom F;
A16: F.x = {} by A15,FUNCT_1:def 2;
f.x in rng f by A14,FUNCT_1:3;
hence thesis by A7,A13,A16;
end;
suppose that
A17: not x in dom f and
A18: x in dom F;
A19: f.x = {} by A17,FUNCT_1:def 2;
F.x in rng F by A18,FUNCT_1:3;
hence thesis by A8,A13,A19;
end;
suppose that
A20: x in dom f and
A21: x in dom F;
A22: F.x in rng F by A21,FUNCT_1:3;
f.x in rng f by A20,FUNCT_1:3;
hence thesis by A7,A8,A13,A22,FINSUB_1:def 1;
end;
end;
dom L2 = dom f \/ dom F by A9;
then dom L2 = the_Vertices_of G by A6,XBOOLE_1:12;
then L2 in Funcs(the_Vertices_of G, Fin NAT) by A10,FUNCT_2:def 2;
hence thesis by A3,ZFMISC_1:def 2;
end;
end;
theorem Th25:
for G being _finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st not x in G.AdjacentSet({v}) holds L`2.
x = (LexBFS:Update(L,v,k))`2.x
proof
let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
set, k be Nat such that
A1: not x in G.AdjacentSet({v});
set F = (G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k};
A2: not x in dom F by A1,XBOOLE_0:def 5;
then
A3: F.x = {} by FUNCT_1:def 2;
set L2 = LexBFS:Update(L,v,k)`2;
per cases;
suppose
x in dom L`2;
then x in dom L`2 \/ dom F by XBOOLE_0:def 3;
hence L2.x = L`2.x \/ F.x by Def1
.= L`2.x by A3;
end;
suppose
A4: not x in dom L`2;
then not x in dom L`2 \/ dom F by A2,XBOOLE_0:def 3;
then not x in dom L2 by Def1;
hence L2.x = {} by FUNCT_1:def 2
.= L`2.x by A4,FUNCT_1:def 2;
end;
end;
theorem Th26:
for G being _finite _Graph, L being LexBFS:Labeling of G, v being
Vertex of G, x being set, k being Nat st x in dom L`1 holds LexBFS:Update(L,v,k
)`2.x = L`2.x
proof
let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
set, k be Nat such that
A1: x in dom L`1;
set F = (G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k};
A2: not x in dom F by A1,XBOOLE_0:def 5;
then
A3: F.x = {} by FUNCT_1:def 2;
set L2 = LexBFS:Update(L,v,k)`2;
per cases;
suppose
x in dom L`2;
then x in dom L`2 \/ dom F by XBOOLE_0:def 3;
hence L2.x = L`2.x \/ F.x by Def1
.= L`2.x by A3;
end;
suppose
A4: not x in dom L`2;
then not x in dom L`2 \/ dom F by A2,XBOOLE_0:def 3;
then not x in dom L2 by Def1;
hence L2.x = {} by FUNCT_1:def 2
.= L`2.x by A4,FUNCT_1:def 2;
end;
end;
theorem Th27:
for G being _finite _Graph, L being LexBFS:Labeling of G, v be
Vertex of G, x being set, k being Nat st x in G.AdjacentSet({v}) & not x in dom
L`1 holds LexBFS:Update(L,v,k)`2.x = L`2.x \/ {G.order() -' k}
proof
let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be
set, k be Nat such that
A1: x in G.AdjacentSet({v}) and
A2: not x in dom L`1;
A3: x in (G.AdjacentSet({v}) \ dom L`1) by A1,A2,XBOOLE_0:def 5;
then x in dom ((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k});
then
A4: x in dom (L`2) \/ dom ((G.AdjacentSet({v})\dom L`1)-->{G.order()-'k}) by
XBOOLE_0:def 3;
set L2 = LexBFS:Update(L,v,k)`2;
((G.AdjacentSet({v}) \ dom L`1) --> {G.order()-'k}).x = {G.order()-'k}
by A3,FUNCOP_1:7;
hence thesis by A4,Def1;
end;
definition
let G be _finite _Graph, L be LexBFS:Labeling of G;
func LexBFS:Step(L) -> LexBFS:Labeling of G equals
:Def13:
L if G.order() <=
card (dom L`1) otherwise LexBFS:Update(L, LexBFS:PickUnnumbered(L), card dom L
`1);
coherence;
consistency;
end;
definition
let G be _Graph;
mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means
:Def14:
for n being Nat holds it.n is LexBFS:Labeling of G;
existence
proof
set L = the LexBFS:Labeling of G;
deffunc F(object) = L;
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
end;
definition
let G be _Graph, S be LexBFS:LabelingSeq of G, n be Nat;
redefine func S.n -> LexBFS:Labeling of G; :: redefines . (FUNCT_1, definition)
coherence by Def14;
end;
definition
let G be _Graph, S be LexBFS:LabelingSeq of G;
redefine func S.Result() -> LexBFS:Labeling of G; :: redefines .Result() (GLIB_000, definition)
coherence by Def14;
end;
definition
let G be _finite _Graph, S be LexBFS:LabelingSeq of G;
func S``1 -> preVNumberingSeq of G means
:Def15:
for n being Nat holds it.n = (S.n)`1;
existence
proof
deffunc F(object) = (S.$1)`1;
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then f.i = (S.i)`1 by A1;
hence f.i is PartFunc of the_Vertices_of G, NAT;
end;
then reconsider f as preVNumberingSeq of G by Def7;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let it1, it2 be preVNumberingSeq of G such that
A2: for n being Nat holds it1.n = (S.n)`1 and
A3: for n being Nat holds it2.n = (S.n)`1;
now
let i be object;
assume i in NAT;
then reconsider i9 = i as Nat;
thus it1.i = (S.i9)`1 by A2
.= it2.i by A3;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
definition
let G be _finite _Graph;
func LexBFS:CSeq(G) -> LexBFS:LabelingSeq of G means
:Def16:
it.0 = LexBFS:Init(G) & for n being Nat holds it.(n+1) = LexBFS:Step(it.n);
existence
proof
defpred P[Nat,set,set] means ($2 is LexBFS:Labeling of G
implies ex L being LexBFS:Labeling of G st $2 = L & $3 = LexBFS:Step(L)) & (not
$2 is LexBFS:Labeling of G implies $3 = $2);
now
let n be Nat,x be set;
now
per cases;
suppose
x is LexBFS:Labeling of G;
then reconsider L = x as LexBFS:Labeling of G;
LexBFS:Step(L) = LexBFS:Step(L);
hence ex y being set st P[n,x,y];
end;
suppose
not x is LexBFS:Labeling of G;
hence ex y being set st P[n,x,y];
end;
end;
hence ex y being set st P[n,x,y];
end;
then
A1: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A2: dom IT = NAT & IT.0 = LexBFS:Init(G) & for n being Nat
holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
reconsider IT as ManySortedSet of NAT by A2,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means IT.$1 is LexBFS:Labeling of G;
A3: now
let n be Nat;
assume
A4: P2[n];
ex Gn being LexBFS:Labeling of G st IT.n = Gn & IT.(n+1) =
LexBFS:Step(Gn) by A2,A4;
hence P2[n+1];
end;
A5: P2[ 0 ] by A2;
for n being Nat holds P2[n] from NAT_1:sch 2(A5,A3);
then reconsider IT as LexBFS:LabelingSeq of G by Def14;
take IT;
thus IT.0 = LexBFS:Init(G) by A2;
let n be Nat;
ex Gn being LexBFS:Labeling of G st IT.n = Gn & IT.(n+1) =
LexBFS:Step(Gn) by A2;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be LexBFS:LabelingSeq of G such that
A6: IT1.0 = LexBFS:Init(G) and
A7: for n being Nat holds IT1.(n+1) = LexBFS:Step(IT1.n) and
A8: IT2.0 = LexBFS:Init(G) and
A9: for n being Nat holds IT2.(n+1) = LexBFS:Step(IT2.n);
defpred P[Nat] means IT1.$1 = IT2.$1;
now
let n be Nat;
assume P[n];
then IT1.(n+1) = LexBFS:Step(IT2.n) by A7
.= IT2.(n+1) by A9;
hence P[n+1];
end;
then
A10: for n being Nat st P[n] holds P[n+1];
A11: P[ 0 ] by A6,A8;
for n being Nat holds P[n] from NAT_1:sch 2(A11,A10);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
theorem Th28:
for G being _finite _Graph holds LexBFS:CSeq(G) is iterative
proof
let G be _finite _Graph;
set CS = LexBFS:CSeq(G);
let k,n be Nat such that
A1: CS.k = CS.n;
CS.(k+1) = LexBFS:Step(CS.k) by Def16;
hence CS.(k+1) = CS.(n+1) by A1,Def16;
end;
registration
let G be _finite _Graph;
cluster LexBFS:CSeq(G) -> iterative;
coherence by Th28;
end;
definition
let X, Y be set, f be Function of X, Fin Y, x be set;
redefine func f.x -> finite Subset of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: dom f = X by FUNCT_2:def 1;
per cases;
suppose
x in X;
then f.x in Fin Y by FUNCT_2:5;
hence thesis by FINSUB_1:def 5;
end;
suppose
not x in X;
then f.x = {} by A1,FUNCT_1:def 2;
hence thesis by XBOOLE_1:2;
end;
end;
end;
:: the vertex picked has the largest v2label
theorem Th29:
for G being _finite _Graph, L be LexBFS:Labeling of G, x being
set st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds (L`2.x,1)-bag <= (
L`2.(LexBFS:PickUnnumbered(L)),1)-bag, InvLexOrder NAT
proof
let G be _finite _Graph, L be LexBFS:Labeling of G, x be set such that
A1: not x in dom L`1 and
A2: dom L`1 <> the_Vertices_of G;
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set w = LexBFS:PickUnnumbered(L);
consider S being non empty finite Subset of bool NAT, B being non empty
finite Subset of Bags NAT, F being Function such that
A3: S = rng F and
A4: F = V2G | (VG \ dom VLG) and
A5: for x being finite Subset of NAT holds x in S implies (x,1)-bag in B and
A6: for x being set holds x in B implies ex y being finite Subset of NAT
st y in S & x = (y,1)-bag and
A7: w = the Element of F " {support max(B,InvLexOrder NAT)} by A2,Def11;
A8: dom F = dom V2G /\ (VG \ dom VLG) by A4,RELAT_1:61;
set mw = max(B,InvLexOrder NAT);
mw in B by Def4;
then consider y being finite Subset of NAT such that
A9: y in S and
A10: mw = (y,1)-bag by A6;
A11: y = support mw by A10,UPROOTS:8;
then
A12: F " {support mw} is non empty by A3,A9,FUNCT_1:72;
then w in dom F by A7,FUNCT_1:def 7;
then
A13: V2G.w = F.w by A4,FUNCT_1:47;
F.w in {support mw} by A7,A12,FUNCT_1:def 7;
then
A14: (V2G.w,1)-bag = mw by A10,A11,A13,TARSKI:def 1;
A15: dom V2G = the_Vertices_of G by FUNCT_2:def 1;
per cases;
suppose
x in the_Vertices_of G;
then x in VG \ dom VLG by A1,XBOOLE_0:def 5;
then
A16: x in dom F by A15,A8,XBOOLE_0:def 4;
then
A17: F.x in S by A3,FUNCT_1:def 3;
F.x = V2G.x by A4,A16,FUNCT_1:47;
then (V2G.x,1)-bag in B by A5,A17;
hence thesis by A14,Def4;
end;
suppose
not x in the_Vertices_of G;
then V2G.x = {} by A15,FUNCT_1:def 2;
then (V2G.x,1)-bag = EmptyBag NAT by UPROOTS:9;
hence thesis by TERMORD:9;
end;
end;
:: the vertex picked is not currently in the vlabel
theorem Th30:
for G being _finite _Graph, L be LexBFS:Labeling of G st dom L`1
<> the_Vertices_of G holds not LexBFS:PickUnnumbered(L) in dom L`1
proof
let G be _finite _Graph, L be LexBFS:Labeling of G such that
A1: dom L`1 <> the_Vertices_of G;
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set w = LexBFS:PickUnnumbered(L);
consider S being non empty finite Subset of bool NAT, B being non empty
finite Subset of Bags NAT, F being Function such that
A2: S = rng F and
A3: F = V2G | (VG \ dom VLG) and
for x being finite Subset of NAT holds x in S implies (x,1)-bag in B and
A4: for x being set holds x in B implies ex y being finite Subset of NAT
st y in S & x = (y,1)-bag and
A5: w = the Element of F " {support max(B,InvLexOrder NAT)} by A1,Def11;
set mw = max(B,InvLexOrder NAT);
mw in B by Def4;
then consider y being finite Subset of NAT such that
A6: y in S and
A7: mw = (y,1)-bag by A4;
y = support mw by A7,UPROOTS:8;
then F " {support mw} is non empty by A2,A6,FUNCT_1:72;
then
A8: w in dom F by A5,FUNCT_1:def 7;
assume w in dom VLG;
then
A9: not w in VG \ dom VLG by XBOOLE_0:def 5;
dom F = dom V2G /\ (VG \ dom VLG) by A3,RELAT_1:61;
hence contradiction by A8,A9,XBOOLE_0:def 4;
end;
theorem Th31:
for G being _finite _Graph, n being Nat st card dom ((LexBFS:CSeq
(G)).n)`1 < G.order() holds ((LexBFS:CSeq(G)).(n+1))`1 = ((LexBFS:CSeq(G)).n)`1
+* (LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) .--> (G.order()-'(card (dom ((
LexBFS:CSeq(G)).n)`1))))
proof
let G be _finite _Graph, n be Nat;
set CS = LexBFS:CSeq(G);
assume
A1: card dom ((CS.n)`1) < G.order();
set CN1 = CS.(n+1);
set CSN = CS.n;
set VLN = CSN`1;
set w = LexBFS:PickUnnumbered(CSN);
CN1 = LexBFS:Step(CSN) by Def16;
then CN1 = LexBFS:Update(CSN, w, card (dom VLN)) by A1,Def13;
hence thesis;
end;
theorem Th32:
for G being _finite _Graph, n being Nat st n <= G.order() holds
card dom ((LexBFS:CSeq(G)).n)`1 = n
proof
let G be _finite _Graph, n be Nat such that
A1: n <= G.order();
set CS = LexBFS:CSeq(G);
defpred P[Nat] means $1 <= G.order() implies card dom ((CS.$1)`1) = $1;
A2: for k being Nat st k < G.order() & card dom ((CS.k)`1) = k holds card
dom ((CS.(k+1))`1) = k+1
proof
let k be Nat such that
A3: k < G.order() and
A4: card dom ((CS.k)`1) = k;
set CK1 = CS.(k+1);
set CSK = CS.k;
set VLK = CSK`1;
set VK1 = CK1`1;
set w = LexBFS:PickUnnumbered(CSK);
set wf = w .--> (G.order() -' k);
A5: dom wf = {w};
VK1 = VLK +* (w .--> (G.order()-'k)) by A3,A4,Th31;
then dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
hence thesis by A3,A4,Th30,CARD_2:41;
end;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
per cases;
suppose
k < G.order();
hence thesis by A2,A7;
end;
suppose
k >= G.order();
hence thesis by NAT_1:13;
end;
end;
CS.0 = LexBFS:Init(G) by Def16;
then
A8: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A8,A6);
hence thesis by A1;
end;
theorem Th33:
for G being _finite _Graph, n being Nat st G.order() <= n holds (
LexBFS:CSeq(G)).(G.order()) = (LexBFS:CSeq(G)).n
proof
let G be _finite _Graph, n be Nat;
assume G.order() <= n;
then
A1: ex i being Nat st G.order() + i = n by NAT_1:10;
set CS = LexBFS:CSeq(G);
defpred V[Nat] means G.order() = card dom (CS.(G.order()+$1))`1;
defpred P[Nat] means (CS.(G.order())) = (CS.(G.order()+$1));
A2: for k being Nat st V[k] holds V[k+1]
proof
let k be Nat such that
A3: V[k];
set CK1 = CS.(G.order()+k+1);
set CSK = CS.(G.order()+k);
CK1 = LexBFS:Step(CSK) by Def16;
hence thesis by A3,Def13;
end;
A4: V[ 0 ] by Th32;
A5: for k being Nat holds V[k] from NAT_1:sch 2(A4,A2);
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
set CK1 = CS.(G.order()+k+1);
set CSK = CS.(G.order()+k);
set VLK = CSK`1;
A8: CK1 = LexBFS:Step(CSK) by Def16;
card dom VLK = G.order() by A5;
hence thesis by A7,A8,Def13;
end;
A9: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
hence thesis by A1;
end;
theorem Th34:
for G being _finite _Graph, m,n being Nat st G.order() <= m & m
<= n holds (LexBFS:CSeq(G)).m = (LexBFS:CSeq(G)).n
proof
let G be _finite _Graph, m,n be Nat such that
A1: G.order() <= m and
A2: m <= n;
(LexBFS:CSeq(G)).m = (LexBFS:CSeq(G)).(G.order()) by A1,Th33;
hence thesis by A1,A2,Th33,XXREAL_0:2;
end;
theorem Th35:
for G being _finite _Graph holds LexBFS:CSeq(G) is eventually-constant
proof
let G be _finite _Graph;
take G.order();
let m be Nat;
assume G.order() <= m;
hence (LexBFS:CSeq(G)).(G.order()) = (LexBFS:CSeq(G)).m by Th33;
end;
registration
let G be _finite _Graph;
cluster LexBFS:CSeq(G) -> eventually-constant;
coherence by Th35;
end;
theorem Th36:
for G being _finite _Graph, n being Nat holds dom ((LexBFS:CSeq(G
)).n)`1 = the_Vertices_of(G) iff G.order() <= n
proof
let G be _finite _Graph, n be Nat;
set CS = LexBFS:CSeq(G);
set CSN = CS.n;
set VLN = CSN`1;
set CSO = CS.G.order();
set VLO = CSO`1;
thus not dom VLN = the_Vertices_of G or not n < G.order() by Th32;
card dom VLO = card the_Vertices_of G by Th32;
then
A1: dom VLO = the_Vertices_of G by CARD_2:102;
assume G.order() <= n;
hence thesis by A1,Th34;
end;
theorem Th37:
for G being _finite _Graph holds (LexBFS:CSeq(G)).Lifespan() = G .order()
proof
let G be _finite _Graph;
set CS = LexBFS:CSeq(G);
A1: for n being Nat st CS.n = CS.(n+1) holds G.order() <= n
proof
let n be Nat such that
A2: CS.n = CS.(n+1);
set w = LexBFS:PickUnnumbered(CS.n);
set VN1 = (CS.(n+1))`1;
set VLN = (CS.n)`1;
set j = card (dom VLN);
set wf = w .--> (G.order() -' j);
assume
A3: n < G.order();
then dom VLN <> the_Vertices_of G by Th36;
then
A4: not w in dom VLN by Th30;
j < G.order() by A3,Th32;
then
A5: VN1 = VLN +* (w .--> (G.order() -' j)) by Th31;
dom wf = {w};
then
A6: dom VN1 = dom VLN \/ {w} by A5,FUNCT_4:def 1;
w in {w} by TARSKI:def 1;
hence contradiction by A2,A4,A6,XBOOLE_0:def 3;
end;
G.order() <= G.order()+1 by NAT_1:13;
then CS.(G.order()) = CS.(G.order()+1) by Th33;
hence thesis by A1,GLIB_000:def 56;
end;
theorem Th38:
for G being _finite _Graph holds (LexBFS:CSeq(G))``1 is eventually-constant
proof
let G be _finite _Graph;
set CS = (LexBFS:CSeq(G));
set S = (LexBFS:CSeq(G))``1;
now
consider n being Nat such that
A1: for m being Nat st n <= m holds CS.n = CS.m by Def6;
take n;
let m be Nat such that
A2: n <= m;
thus S.n = (CS.n)`1 by Def15
.= (CS.m)`1 by A1,A2
.= S.m by Def15;
end;
hence thesis;
end;
theorem Th39:
for G being _finite _Graph holds (LexBFS:CSeq(G))``1.Lifespan() =
(LexBFS:CSeq(G)).Lifespan()
proof
let G be _finite _Graph;
set S = LexBFS:CSeq(G);
set VN = S``1;
set ls = G.order();
A1: VN is eventually-constant by Th38;
A2: (S.(ls+1))`1 = S``1.(ls+1) by Def15;
A3: now
let n be Nat such that
A4: VN.n = VN.(n+1) and
A5: ls > n;
n+1 <= ls by A5,NAT_1:13;
then
A6: card dom (S.(n+1))`1 = n+1 by Th32;
A7: (S.(n+1))`1 = VN.(n+1) by Def15;
A8: (S.n)`1 = VN.n by Def15;
card dom (S.n)`1 = n by A5,Th32;
hence contradiction by A4,A6,A8,A7;
end;
(S.ls)`1 = S``1.ls by Def15;
then
A9: VN.ls = VN.(ls+1) by A2,Th33,NAT_1:11;
S.Lifespan() = ls by Th37;
hence thesis by A1,A9,A3,GLIB_000:def 56;
end;
registration
let G be _finite _Graph;
cluster (LexBFS:CSeq(G))``1 -> vertex-numbering;
correctness
proof
set S = (LexBFS:CSeq(G))``1;
set CS = (LexBFS:CSeq(G));
A1: S.Lifespan() = CS.Lifespan() by Th39;
thus S.0 = (CS.0)`1 by Def15
.= (LexBFS:Init(G))`1 by Def16
.= {};
now
let k, n be Nat such that
A2: S.k = S.n;
A3: S.(k+1) = (CS.(k+1))`1 by Def15;
A4: S.k = (CS.k)`1 by Def15;
A5: S.(n+1) = (CS.(n+1))`1 by Def15;
A6: S.n = (CS.n)`1 by Def15;
per cases;
suppose
A7: k <= G.order() & n <= G.order();
then card dom ((CS.n)`1) = n by Th32;
hence S.(k+1) = S.(n+1) by A2,A4,A6,A7,Th32;
end;
suppose
A8: k <= G.order() & n >= G.order();
then
A9: CS.n = CS.(G.order()) by Th33;
A10: card dom ((CS.(G.order()))`1) = G.order() by Th32;
A11: n+1 >= G.order() by A8,NAT_1:13;
card dom ((CS.k)`1) = k by A8,Th32;
then k+1 >= G.order() by A2,A4,A6,A9,A10,NAT_1:13;
hence S.(k+1) = (CS.(G.order()))`1 by A3,Th33
.= S.(n+1) by A5,A11,Th33;
end;
suppose
A12: k >= G.order() & n <= G.order();
then
A13: CS.k = CS.(G.order()) by Th33;
A14: card dom ((CS.(G.order()))`1) = G.order() by Th32;
card dom ((CS.n)`1) = n by A12,Th32;
then
A15: n+1 >= G.order() by A2,A4,A6,A13,A14,NAT_1:13;
k+1 >= G.order() by A12,NAT_1:13;
hence S.(k+1) = (CS.(G.order()))`1 by A3,Th33
.= S.(n+1) by A5,A15,Th33;
end;
suppose
A16: k >= G.order() & n >= G.order();
then
A17: n+1 >= G.order() by NAT_1:13;
A18: k+1 >= G.order() by A16,NAT_1:13;
thus S.(k+1) = (CS.(k+1))`1 by Def15
.= (CS.(G.order()))`1 by A18,Th33
.= (CS.(n+1))`1 by A17,Th33
.= S.(n+1) by Def15;
end;
end;
hence S is iterative;
S is eventually-constant by Th38;
hence S is halting;
A19: CS.Lifespan() = G.order() by Th37;
hence S.Lifespan() = G.order() by Th39;
let n be Nat such that
A20: n < S.Lifespan();
A21: n < G.order() by A19,A20,Th39;
take w = LexBFS:PickUnnumbered(CS.n);
A22: S.n = (CS.n)`1 by Def15;
A23: card dom ((CS.n)`1) = n by A21,Th32;
hence not w in dom (S.n) by A21,A22,Th30;
S.(n+1) = (CS.(n+1))`1 by Def15;
hence thesis by A1,A19,A20,A22,A23,Th31;
end;
end;
theorem Th40:
for G being _finite _Graph holds (LexBFS:CSeq(G))``1.Result() = (
LexBFS:CSeq(G)).Result()`1
proof
let G be _finite _Graph;
set S = LexBFS:CSeq(G);
thus S``1.Result() = S``1.(S.Lifespan()) by Th39
.= S.Result()`1 by Def15;
end;
theorem Th41:
for G being _finite _Graph, n being Nat st n < G.order() holds ((
LexBFS:CSeq(G))``1).PickedAt(n) = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n)
proof
let G be _finite _Graph, n be Nat such that
A1: n < G.order();
set CS = LexBFS:CSeq(G);
set CSN = CS.n;
set CS1 = CS.(n+1);
set VLN = CSN`1;
set VL1 = CS1`1;
A2: CS.Lifespan() = G.order() by Th37;
set PU = LexBFS:PickUnnumbered(CSN);
set f2 = PU .--> (CS.Lifespan()-'n);
A3: dom f2 = {PU};
n = card dom VLN by A1,Th32;
then VL1 = VLN +* (PU .--> (CS.Lifespan()-'n)) by A1,A2,Th31;
then
A4: dom VL1 = dom VLN \/ {PU} by A3,FUNCT_4:def 1;
A5: CSN`1 = CS``1.n by Def15;
set PA = CS``1.PickedAt(n);
set f1 = PA .--> (CS.Lifespan()-'n);
A6: dom f1 = {PA};
A7: CS.Lifespan() = CS``1.Lifespan() by Th39;
CS1`1 = CS``1.(n+1) by Def15;
then VL1 = VLN +* (PA .--> (CS.Lifespan()-'n)) by A1,A2,A7,A5,Def9;
then
A8: dom VL1 = dom VLN \/ {PA} by A6,FUNCT_4:def 1;
A9: not PA in dom VLN by A1,A2,A7,A5,Def9;
now
assume PA <> PU;
then not PA in {PU} by TARSKI:def 1;
then
A10: not PA in dom VL1 by A9,A4,XBOOLE_0:def 3;
PA in {PA} by TARSKI:def 1;
hence contradiction by A8,A10,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem Th42:
for G being _finite _Graph, n being Nat st n < G.order() ex w
being Vertex of G st w = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & for v
being set holds (v in G.AdjacentSet({w}) & not v in dom ((LexBFS:CSeq(G)).n)`1
implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v \/ {G
.order() -' n}) & ((not v in G.AdjacentSet({w}) or v in dom (((LexBFS:CSeq(G)).
n))`1) implies ((LexBFS:CSeq(G)).(n+1)) `2.v = (((LexBFS:CSeq(G)).n))`2.v)
proof
let G be _finite _Graph, n be Nat such that
A1: n < G.order();
set CS = (LexBFS:CSeq(G));
set CSN = CS.n;
set VLN = CSN`1;
set V2N = CSN`2;
set CN1 = CS.(n+1);
set V21 = CN1`2;
set w = LexBFS:PickUnnumbered(CSN);
take w;
A2: CN1 = LexBFS:Step(CSN) by Def16;
card dom VLN = n by A1,Th32;
then
A3: CN1 = LexBFS:Update(CSN, w, n) by A1,A2,Def13;
now
let v be set;
assume
A4: not v in G.AdjacentSet({w}) or v in dom VLN;
per cases by A4;
suppose
not v in G.AdjacentSet({w});
hence V21.v = V2N.v by A3,Th25;
end;
suppose
v in dom VLN;
hence V21.v = V2N.v by A3,Th26;
end;
end;
hence thesis by A3,Th27;
end;
theorem Th43:
for G being _finite _Graph, i being Nat, v being set holds ((
LexBFS:CSeq(G)).i)`2.v c= (Seg G.order()) \ Seg (G.order()-'i)
proof
let G be _finite _Graph, i be Nat, v be set;
set CS = (LexBFS:CSeq(G));
set CSI = CS.i;
set V2I = CSI`2;
set CSO = CS.(G.order());
set V2O = CSO`2;
defpred P[Nat] means $1 <= G.order() implies (((LexBFS:CSeq(G)).$1)`2).v c=
(Seg G.order()) \ Seg (G.order() -' $1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
set CK1 = CS.(k+1);
set CSK = CS.k;
set V2K = CSK`2;
set VLK = CSK`1;
set V21 = CK1`2;
per cases;
suppose
k+1 <= G.order();
then
A3: k < G.order() by NAT_1:13;
then consider w being Vertex of G such that
w = LexBFS:PickUnnumbered(CSK) and
A4: for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' k}) & (not v in G.AdjacentSet({w})
or v in dom VLK implies V21.v = V2K.v) by Th42;
per cases;
suppose
A5: v in G.AdjacentSet({w}) & not v in dom VLK;
A6: ((Seg G.order()) \ Seg (G.order() -' k)) \/ {G.order() -' k} = (
Seg G.order()) \ Seg (G.order() -' (k+1)) by A3,Th5;
V21.v = V2K.v \/ {G.order() -' k} by A4,A5;
hence thesis by A2,A6,NAT_1:13,XBOOLE_1:9;
end;
suppose
A7: not v in G.AdjacentSet({w}) or v in dom VLK;
k <= k+1 by NAT_1:13;
then
A8: (Seg G.order()) \ Seg (G.order() -' k) c= (Seg G.order()) \ Seg (
G.order() -' (k+1)) by Th4;
V21.v = V2K.v by A4,A7;
hence thesis by A2,A8,NAT_1:13,XBOOLE_1:1;
end;
end;
suppose
G.order() < k+1;
hence thesis;
end;
end;
CS.0 = LexBFS:Init(G) by Def16;
then (CS.0)`2.v = {};
then
A9: P[ 0 ] by XBOOLE_1:2;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A9,A1);
per cases;
suppose
i <= G.order();
hence thesis by A10;
end;
suppose
A11: i > G.order();
then G.order() - i < i - i by XREAL_1:9;
then G.order() -' i = 0 by XREAL_0:def 2;
then
A12: G.order() -' G.order() = G.order() -' i by XREAL_1:232;
V2O = V2I by A11,Th34;
hence thesis by A10,A12;
end;
end;
theorem Th44:
for G being _finite _Graph, x being set, i,j being Nat st i <= j
holds ((LexBFS:CSeq(G)).i)`2.x c= ((LexBFS:CSeq(G)).j)`2.x
proof
let G be _finite _Graph, x be set, i,j be Nat;
assume i <= j;
then
A1: ex k being Nat st j = i+k by NAT_1:10;
set CS = (LexBFS:CSeq(G));
set CSI = CS.i, V2I = CSI`2;
defpred P[Nat] means V2I.x c= (CS.(i+$1))`2.x;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
set CK1 = CS.(i+k+1);
set CSK = CS.(i+k);
set V2K = CSK`2;
set VLK = CSK`1;
set V21 = CK1`2;
per cases;
suppose
i+k+1 <= G.order();
then i+k < G.order() by NAT_1:13;
then consider w being Vertex of G such that
w = LexBFS:PickUnnumbered(CSK) and
A4: for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' (i+k)}) & (not v in G.AdjacentSet({w
}) or v in dom VLK implies V21.v = V2K.v) by Th42;
per cases;
suppose
x in G.AdjacentSet({w}) & not x in dom VLK;
then V21.x = V2K.x \/ {G.order() -' (i+k)} by A4;
then V2K.x c= V21.x by XBOOLE_1:7;
hence thesis by A3,XBOOLE_1:1;
end;
suppose
not x in G.AdjacentSet({w}) or x in dom VLK;
hence thesis by A3,A4;
end;
end;
suppose
A5: G.order() < i+k+1;
A6: i+k <= i+k+1 by NAT_1:13;
G.order() <= i+k by A5,NAT_1:13;
hence thesis by A3,A6,Th34;
end;
end;
A7: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A7,A2);
hence thesis by A1;
end;
theorem Th45:
for G being _finite _Graph, m,n being Nat, x, y being set st n <
G.order() & n < m & y = LexBFS:PickUnnumbered((LexBFS:CSeq(G)).n) & not x in
dom ((LexBFS:CSeq(G)).n)`1 & x in G.AdjacentSet({y}) holds (G.order() -' n) in
((LexBFS:CSeq(G)).m)`2.x
proof
let G be _finite _Graph;
let m,n be Nat, x, y be set such that
A1: n < G.order() and
A2: n < m;
set CS = (LexBFS:CSeq(G));
set CSM = CS.m, V2M = CSM`2;
set CN1 = CS.(n+1);
set V21 = CN1`2;
n+1 <= m by A2,NAT_1:13;
then
A3: V21.x c= V2M.x by Th44;
A4: G.order() -' n in {G.order() -' n} by TARSKI:def 1;
set CSN = CS.n, VLN = CSN`1, V2N = CSN`2;
assume that
A5: y = LexBFS:PickUnnumbered(CSN) and
A6: not x in dom VLN and
A7: x in G.AdjacentSet({y});
ex w being Vertex of G st w = LexBFS:PickUnnumbered(CSN) & for v
being set holds (v in G.AdjacentSet({w}) & not v in dom VLN implies V21.v = V2N
.v \/ {G.order() -' n}) & (not v in G.AdjacentSet({w}) or v in dom VLN implies
V21.v = V2N.v) by A1,Th42;
then V21.x = V2N.x \/ {G.order() -' n} by A5,A6,A7;
then G.order() -' n in V21.x by A4,XBOOLE_0:def 3;
hence thesis by A3;
end;
theorem Th46:
for G being _finite _Graph, m,n being Nat st m < n for x being
set st not G.order()-'m in ((LexBFS:CSeq(G)).(m+1))`2.x holds not G.order()-'m
in ((LexBFS:CSeq(G)).n)`2.x
proof
let G be _finite _Graph, m,n be Nat;
assume m < n;
then m+1 <= n by NAT_1:13;
then
A1: ex j being Nat st m+1+j = n by NAT_1:10;
set CS = LexBFS:CSeq(G);
set CSM = CS.(m+1);
set V2M = CSM`2;
let x be set such that
A2: not G.order() -' m in V2M.x;
defpred P[Nat] means not G.order() -' m in (((LexBFS:CSeq(G)).(m+1+$1))`2).x;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
set CSK = CS.(m+1+k);
set VLK = CSK`1, V2K = CSK`2, CK1 = CS.(m+1+k+1);
set V21 = CK1`2;
now
per cases;
suppose
A5: m+1+k < G.order();
then consider w being Vertex of G such that
w = LexBFS:PickUnnumbered(CSK) and
A6: for v being set holds ( v in G.AdjacentSet({w}) & not v in dom
VLK implies V21.v = V2K.v \/ {G.order() -' (m+1+k)}) & ((not v in G.AdjacentSet
({w}) or v in dom VLK) implies V21.v = V2K.v) by Th42;
per cases;
suppose
A7: x in G.AdjacentSet({w}) & not x in dom VLK;
m+1 <= m+1+k by NAT_1:11;
then m < m+1+k by XREAL_1:39;
then G.order() -' m > G.order() -' (m+1+k) by A5,Th2;
then
A8: not G.order() -' m in {G.order() -' (m+1+k)} by TARSKI:def 1;
V21.x = V2K.x \/ {G.order() -' (m+1+k)} by A6,A7;
hence not G.order() -' m in V21.x by A4,A8,XBOOLE_0:def 3;
end;
suppose
not x in G.AdjacentSet({w}) or x in dom VLK;
hence not G.order() -' m in V21.x by A4,A6;
end;
end;
suppose
A9: G.order() <= m+1+k;
m+1+k <= m+1+k+1 by NAT_1:13;
hence not G.order() -' m in V21.x by A4,A9,Th34;
end;
end;
hence thesis;
end;
A10: P[ 0 ] by A2;
for k being Nat holds P[k] from NAT_1:sch 2(A10,A3);
hence thesis by A1;
end;
:: More general version of the above:
:: if the value added during step k doesn't appear in a later step (n),
:: then that value cannot appear in an even later step (m)
theorem Th47:
for G being _finite _Graph, m,n,k being Nat st k < n & n <= m for
x being set st not G.order()-'k in ((LexBFS:CSeq(G)).n)`2.x holds not G.order()
-'k in ((LexBFS:CSeq(G)).m)`2.x
proof
let G be _finite _Graph, m,n,k be Nat such that
A1: k < n and
A2: n <= m;
set CS = LexBFS:CSeq(G);
set CSN = CS.n;
set V2N = CSN`2;
let x be set such that
A3: not G.order() -' k in V2N.x;
set CK1 = CS.(k+1), V21 = CK1`2;
k+1 <= n by A1,NAT_1:13;
then V21.x c= V2N.x by Th44;
then
A4: not G.order() -' k in V21.x by A3;
k < m by A1,A2,XXREAL_0:2;
hence thesis by A4,Th46;
end;
:: relates a value in a vertex's v2label to the vertex chosen at that time
theorem Th48:
for G being _finite _Graph, m,n being Nat, x being Vertex of G st
n in ((LexBFS:CSeq(G)).m)`2.x ex y being Vertex of G st (LexBFS:PickUnnumbered(
(LexBFS:CSeq(G)).(G.order()-'n))) = y & not y in dom ((LexBFS:CSeq(G)).(G
.order()-'n))`1 & x in G.AdjacentSet({y})
proof
let G be _finite _Graph, m, n be Nat;
set CS = LexBFS:CSeq(G);
set CSM = CS.m;
set V2M = CSM`2;
set CSN = CS.(G.order() -' n);
set VLN = CSN`1;
set V2N = CSN`2;
set on1 = G.order() -' n + 1;
set CN1 = CS.on1;
set V21 = CN1`2;
let x be Vertex of G such that
A1: n in V2M.x;
A2: V2M.x c= (Seg G.order()) \ Seg (G.order() -' m) by Th43;
then
A3: G.order() -' m < n by A1,Th3;
n <= G.order() by A1,A2,Th3;
then
A4: G.order() -' n = G.order() - n by XREAL_1:233;
then
A5: G.order() -' n < G.order() by A3,XREAL_1:44;
then
A6: G.order() -' (G.order() -' n) = G.order() - (G.order() - n) by A4,
XREAL_1:233;
then consider w being Vertex of G such that
A7: w = LexBFS:PickUnnumbered(CSN) and
A8: for v being set holds (v in G.AdjacentSet({w}) & not v in dom VLN
implies V21.v = V2N.v\/{n}) & (not v in G.AdjacentSet({w}) or v in dom VLN
implies V21.v = V2N.v) by A3,A4,Th42,XREAL_1:44;
V2N.x c= (Seg G.order()) \ Seg (G.order() -' (G.order() -' n)) by Th43;
then
A9: not n in V2N.x by A6,Th3;
A10: now
per cases;
suppose
m <= G.order();
then G.order() -' m = G.order() - m by XREAL_1:233;
then G.order() - m + m < n + m by A3,XREAL_1:6;
then G.order() - n < m + n - n by XREAL_1:9;
hence on1 <= m by A4,NAT_1:13;
end;
suppose
G.order() < m;
then G.order() -' n < m by A5,XXREAL_0:2;
hence on1 <= m by NAT_1:13;
end;
end;
A11: G.order() -' n < on1 by XREAL_1:39;
assume
A12: not ex y being Vertex of G st LexBFS:PickUnnumbered(CSN) = y & not y
in dom VLN & x in G.AdjacentSet({y});
dom VLN <> the_Vertices_of G by A5,Th36;
then not x in G.AdjacentSet({w}) by A12,A7,Th30;
then not n in V21.x by A9,A8;
hence contradiction by A1,A6,A10,A11,Th47;
end;
theorem Th49:
for G being _finite _Graph holds dom ((LexBFS:CSeq(G)).Result())
`1 = the_Vertices_of G
proof
let G be _finite _Graph;
set CS = LexBFS:CSeq(G);
set CSO = CS.(G.order());
CS.Result() = CSO by Th37;
hence thesis by Th36;
end;
::$N Lexicographic_breadth-first_search
theorem Th50:
for G being _finite _Graph holds ((LexBFS:CSeq(G)).Result()`1)"
is VertexScheme of G
proof
let G be _finite _Graph;
set CS = LexBFS:CSeq(G);
set CSO = CS.(G.order());
set VLO = CSO`1;
set VL = CS``1;
A1: CSO = (LexBFS:CSeq(G)).Result() by Th37;
A2: CS.Lifespan() = G.order() by Th37;
A3: VLO = VL.(G.order()) by Def15;
then
A4: VLO is one-to-one by Th18;
dom VLO = the_Vertices_of G by Th36;
then
A5: rng (VLO") = the_Vertices_of G by A4,FUNCT_1:33;
CS.Lifespan() = VL.Lifespan() by Th39;
then
rng (VL.(G.order())) = (Seg G.order()) \ Seg (G.order() -' G.order()) by A2
,Th14
.= (Seg G.order()) \ Seg 0 by XREAL_1:232
.= Seg G.order();
then dom (VLO") = Seg G.order() by A3,A4,FUNCT_1:33;
then VLO" is FinSequence by FINSEQ_1:def 2;
then VLO" is FinSequence of the_Vertices_of G by A5,FINSEQ_1:def 4;
hence thesis by A1,A4,A5,CHORD:def 12;
end;
:: A vertex with a vlabel of k must have had the largest v2label when chosen
theorem Th51:
for G being _finite _Graph, i,j being Nat, a,b being Vertex of G
st a in dom ((LexBFS:CSeq(G)).i)`1 & b in dom ((LexBFS:CSeq(G)).i)`1 & ((
LexBFS:CSeq(G)).i)`1.a < ((LexBFS:CSeq(G)).i)`1.b & j = G.order() -' ((
LexBFS:CSeq(G)).i)`1.b holds (((LexBFS:CSeq(G)).j)`2.a,1)-bag <= ((((
LexBFS:CSeq(G)).j)`2).b,1)-bag, InvLexOrder NAT
proof
let G be _finite _Graph;
let i,j be Nat, a,b be Vertex of G such that
A1: a in dom ((LexBFS:CSeq(G)).i)`1 and
A2: b in dom ((LexBFS:CSeq(G)).i)`1 and
A3: ((LexBFS:CSeq(G)).i)`1.a < ((LexBFS:CSeq(G)).i)`1.b and
A4: j = G.order() -' ((LexBFS:CSeq(G)).i)`1.b;
set VL = (LexBFS:CSeq(G))``1;
set CSJ = (LexBFS:CSeq(G)).j;
set VLI = VL.i, VLJ = VL.j;
A5: ((LexBFS:CSeq(G)).i)`1.b = ((LexBFS:CSeq(G))``1.i).b by Def15;
A6: a in the_Vertices_of G;
A7: ((LexBFS:CSeq(G)).i)`1 = ((LexBFS:CSeq(G))``1.i) by Def15;
A8: (LexBFS:CSeq(G)).Lifespan() = VL.Lifespan() by Th39;
A9: G.order() = (LexBFS:CSeq(G)).Lifespan() by Th37;
then VLI.b <= G.order() by A8,Th15;
then
A10: G.order() -' VLI.b = G.order() - VLI.b by XREAL_1:233;
then
A11: G.order() -' j = G.order() - (G.order() - VLI.b) by A4,A5,NAT_D:35
,XREAL_1:233;
A12: now
assume a in dom (CSJ`1);
then
A13: a in dom VLJ by Def15;
then VLI.b < VLJ.a by A9,A8,A11,Th22;
hence contradiction by A1,A3,A7,A13,Th19;
end;
VL.PickedAt(j) = b by A2,A4,A7,A9,A8,Th20;
then LexBFS:PickUnnumbered(CSJ) = b by A3,A4,A5,A10,Th41,XREAL_1:44;
hence thesis by A6,A12,Th29;
end;
:: Any value in our v2label corresponds to a vertex that we are
:: adjacent to in our in our vlabel
theorem Th52:
for G being _finite _Graph, i,j being Nat,v being Vertex of G st
j in ((LexBFS:CSeq(G)).i)`2.v ex w being Vertex of G st w in dom ((LexBFS:CSeq(
G)).i)`1 & (((LexBFS:CSeq(G)).i)`1).w = j & v in G.AdjacentSet{w}
proof
let G be _finite _Graph, i,j be Nat;
let v be Vertex of G;
set CSI = (LexBFS:CSeq(G)).i;
set VLI = (LexBFS:CSeq(G))``1.i;
set V2I = CSI`2;
set n = G.order() -' j;
set CSN = (LexBFS:CSeq(G)).n;
set VLN = CSN`1;
A1: G.order() = (LexBFS:CSeq(G)).Lifespan() by Th37;
A2: (LexBFS:CSeq(G)).Lifespan() = (LexBFS:CSeq(G)``1).Lifespan() by Th39;
assume
A3: j in V2I.v;
then consider w being Vertex of G such that
A4: LexBFS:PickUnnumbered(CSN) = w and
not w in dom VLN and
A5: v in G.AdjacentSet({w}) by Th48;
A6: V2I.v c= Seg G.order() \ Seg (G.order() -' i) by Th43;
then
A7: G.order() -' i < j by A3,Th3;
A8: j <= G.order() by A3,A6,Th3;
then
A9: G.order() -' j = G.order() - j by XREAL_1:233;
then
A10: n < G.order() by A7,XREAL_1:44;
A11: G.order() - n = G.order() - (G.order() - j) by A8,XREAL_1:233;
then G.order() - i < G.order() - n by A7,XREAL_0:def 2;
then G.order() - i + i < G.order() - n + i by XREAL_1:6;
then G.order() + n < G.order() + i - n + n by XREAL_1:6;
then
A12: n + G.order() - G.order() < i + G.order() - G.order() by XREAL_1:9;
A13: w = ((LexBFS:CSeq(G))``1).PickedAt(n) by A4,A7,A9,Th41,XREAL_1:44;
then
A14: VLI.w = G.order()-'n by A10,A1,A2,A12,Th21;
A15: CSI`1 = VLI by Def15;
then w in dom CSI`1 by A10,A1,A2,A13,A12,Th21;
hence thesis by A15,A5,A10,A11,A14,XREAL_1:233;
end;
definition
let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
attr F is with_property_L3 means
for a,b,c being Vertex of G st a in
dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
not b,c are_adjacent ex d being Vertex of G st d in dom F & F.c < F.d & b,d
are_adjacent & not a,d are_adjacent & for e being Vertex of G st e <> d & e,b
are_adjacent & not e,a are_adjacent holds F.e < F.d;
end;
theorem Th53:
for G being _finite _Graph, n being Nat holds ((LexBFS:CSeq(G)).n
)`1 is with_property_L3
proof
let G be _finite _Graph, i be Nat;
set CSi = (LexBFS:CSeq(G)).i;
set VLi = (LexBFS:CSeq(G))``1.i;
A1: CSi`1 = VLi by Def15;
now
A2: (LexBFS:CSeq(G)).Lifespan() = (LexBFS:CSeq(G))``1.Lifespan() by Th39;
A3: (LexBFS:CSeq(G)).Lifespan() = G.order() by Th37;
let a, b, c be Vertex of G such that
A4: a in dom VLi and
A5: b in dom VLi and
A6: c in dom VLi and
A7: VLi.a < VLi.b and
A8: VLi.b < VLi.c and
A9: a,c are_adjacent and
A10: not b,c are_adjacent;
defpred P[Nat] means ex v being Vertex of G st v in dom VLi & b,v
are_adjacent & not a,v are_adjacent & VLi.c < VLi.v & VLi.v = $1;
A11: VLi.a < VLi.c by A7,A8,XXREAL_0:2;
now
set kc = G.order() -' VLi.c;
set k = G.order() -' VLi.b;
assume
A12: for d being Vertex of G st d in dom VLi & VLi.c < VLi.d & d,b
are_adjacent holds d,a are_adjacent;
set VLc = (LexBFS:CSeq(G))``1.kc;
set CSc = (LexBFS:CSeq(G)).kc;
set VLb = (LexBFS:CSeq(G))``1.k;
set CSb = (LexBFS:CSeq(G)).k;
reconsider sb = CSb`2.b, sa = CSb`2.a as finite Subset of NAT;
A13: (Seg G.order()) \ Seg (G.order() -' k) c= Seg G.order() by XBOOLE_1:36;
sb c= (Seg G.order()) \ Seg (G.order() -' k) by Th43;
then
A14: sb c= Seg G.order() by A13;
A15: CSc`1 = VLc by Def15;
sa c= (Seg G.order()) \ Seg (G.order() -' k) by Th43;
then
A16: sa c= Seg G.order() by A13;
A17: c in dom VLb by A5,A6,A8,A3,A2,Th23;
A18: VLi.c <= G.order() by A3,A2,Th15;
then
A19: G.order() -' VLi.c = G.order() - VLi.c by XREAL_1:233;
then
A20: kc < G.order() by A8,XREAL_1:44;
then
A21: G.order() -' kc = G.order() - (G.order() - VLi.c) by A19,XREAL_1:233;
A22: now
A23: rng VLc=(Seg G.order()) \ Seg (G.order()-'kc) by A3,A2,Th14;
A24: VLi.a < VLi.c by A7,A8,XXREAL_0:2;
assume
A25: a in dom VLc;
then VLc.a in rng VLc by FUNCT_1:def 3;
then VLi.c < VLc.a by A21,A23,Th3;
hence contradiction by A4,A25,A24,Th19;
end;
(LexBFS:CSeq(G))``1.PickedAt(kc) = c by A6,A3,A2,Th20;
then
A26: c = LexBFS:PickUnnumbered(CSc) by A8,A19,Th41,XREAL_1:44;
A27: kc < k by A8,A18,Th2;
set j = VLb.c;
A28: CSb`1 = VLb by Def15;
a in G.AdjacentSet({c}) by A7,A8,A9,CHORD:52;
then VLi.c in sa by A15,A20,A27,A26,A21,A22,Th45;
then
A29: VLb.c in sa by A6,A17,Th19;
A30: not b in G.AdjacentSet({c}) by A10,CHORD:52;
A31: now
assume VLb.c in sb;
then
A32: ex z being Vertex of G st z in dom VLb & VLb.z = VLb.c & b in
G.AdjacentSet({z}) by A28,Th52;
VLb is one-to-one by Th18;
hence contradiction by A30,A17,A32,FUNCT_1:def 4;
end;
then (sb,1)-bag.j = 0 by UPROOTS:6;
then
A33: (sb,1)-bag.j < (sa,1)-bag.j by A29,UPROOTS:7;
[(sb,1)-bag,(sa,1)-bag] in InvLexOrder NAT
proof
per cases;
suppose
for k being Ordinal st j in k & k in NAT holds (sb,1)-bag.k
= (sa,1)-bag.k;
hence thesis by A33,BAGORDER:def 6;
end;
suppose
A34: not for k being Ordinal st j in k & k in NAT holds (sb,1)
-bag.k = (sa,1)-bag.k;
defpred M[Nat] means j in $1 & (sb,1)-bag.$1 <> (sa,1)-bag.$1;
A35: for k being Nat st M[k] holds k <= G.order()
proof
let k be Nat such that
A36: M[k];
A37: (sa,1)-bag.k = 1 or (sa,1)-bag.k = 0 by UPROOTS:6,7;
k in NAT by ORDINAL1:def 12;
then consider ok being Ordinal such that
A38: ok = k and
j in ok and
ok in NAT and
A39: (sb,1)-bag.ok <> (sa,1)-bag.ok by A36;
per cases;
suppose
not ok in sb;
then ok in sa by A38,A39,A37,UPROOTS:6;
hence thesis by A16,A38,FINSEQ_1:1;
end;
suppose
ok in sb;
hence thesis by A14,A38,FINSEQ_1:1;
end;
end;
A40: ex k being Nat st M[k] by A34;
consider mm being Nat such that
A41: M[mm] and
A42: for i being Nat st M[i] holds i <= mm from NAT_1:sch 6(A35,
A40 );
reconsider mm as Element of NAT by ORDINAL1:def 12;
A43: now
let k be Ordinal such that
A44: mm in k and
A45: k in NAT;
reconsider kk = k as Element of NAT by A45;
mm in {y where y is Nat : y < kk} by A44,AXIOMS:4;
then
A46: ex mmy being Nat st mmy = mm & mmy < kk;
assume (sb,1)-bag.k <> (sa,1)-bag.k;
hence contradiction by A41,A42,A44,A46,ORDINAL1:10;
end;
j in {y where y is Nat : y < mm} by A41,AXIOMS:4;
then
A47: ex jy being Nat st jy = j & jy < mm;
A48: now
assume
A49: (sb,1)-bag.mm = 1;
then mm in sb by UPROOTS:6;
then consider z being Vertex of G such that
A50: z in dom (CSb`1) and
A51: (CSb`1).z = mm and
A52: b in G.AdjacentSet({z}) by Th52;
set kc = G.order() -' VLi.z;
A53: VLi.z <= G.order() by A3,A2,Th15;
then
A54: G.order() -' VLi.z = G.order() - VLi.z by XREAL_1:233;
k < i by A5,A3,A2,Th22;
then
A55: CSb`1 c= CSi`1 by A1,A28,Th17;
then
A56: dom (CSb`1) c= dom (CSi`1) by RELAT_1:11;
then
A57: 0 < VLi.z by A1,A50,Th15;
then
A58: kc < G.order() by A54,XREAL_1:44;
then
A59: G.order() -' kc = G.order() - (G.order() - VLi.z) by A54,
XREAL_1:233;
set VLc = (LexBFS:CSeq(G))``1.kc;
set CSc = (LexBFS:CSeq(G)).kc;
z = (LexBFS:CSeq(G))``1.PickedAt(kc) by A1,A3,A2,A50,A56,Th20;
then
A60: z = LexBFS:PickUnnumbered(CSc) by A57,A54,Th41,XREAL_1:44;
A61: [z,mm] in CSb`1 by A50,A51,FUNCT_1:def 2;
then
A62: VLi.z = mm by A1,A50,A55,A56,FUNCT_1:def 2;
A63: [c,j] in CSb`1 by A28,A17,FUNCT_1:def 2;
then
A64: VLi.c = j by A1,A6,A55,FUNCT_1:def 2;
then VLi.b < VLi.z by A8,A47,A62,XXREAL_0:2;
then
A65: kc < k by A53,Th2;
A66: VLi.c < VLi.z by A1,A47,A50,A55,A56,A61,A64,FUNCT_1:def 2;
A67: now
VLi.a < VLi.c by A7,A8,XXREAL_0:2;
then
A68: VLi.a < VLi.z by A66,XXREAL_0:2;
A69: rng VLc = (Seg G.order())\ Seg (G.order()-'kc) by A3,A2,Th14;
assume
A70: a in dom VLc;
then VLc.a in rng VLc by FUNCT_1:def 3;
then VLi.z < VLc.a by A59,A69,Th3;
hence contradiction by A4,A70,A68,Th19;
end;
A71: VLi.c < VLi.z by A1,A6,A47,A55,A62,A63,FUNCT_1:def 2;
b,z are_adjacent by A52,CHORD:52;
then z,a are_adjacent by A1,A12,A47,A50,A56,A62,A64;
then
A72: a in G.AdjacentSet({z}) by A11,A71,CHORD:52;
CSc`1 = VLc by Def15;
then (G.order() -' kc) in (CSb`2).a by A72,A58,A65,A60,A67,Th45;
hence contradiction by A41,A49,A62,A59,UPROOTS:7;
end;
(sb,1)-bag.mm = 0 or (sb,1)-bag.mm = 1 by UPROOTS:6,7;
hence thesis by A41,A48,A43,BAGORDER:def 6;
end;
end;
then
A73: (sb,1)-bag <= (sa,1)-bag, InvLexOrder NAT by TERMORD:def 2;
(sb,1)-bag <> (sa,1)-bag by A29,A31,Th6;
then
A74: (sb,1)-bag < (sa,1)-bag, InvLexOrder NAT by A73,TERMORD:def 3;
(sa,1)-bag <= (sb,1)-bag, InvLexOrder NAT by A1,A4,A5,A7,Th51;
hence contradiction by A74,TERMORD:5;
end;
then
A75: ex k being Nat st P[k];
A76: for k being Nat st P[k] holds k <= G.order()
proof
let k be Nat;
assume P[k];
then k in rng VLi by FUNCT_1:def 3;
then
A77: k in (Seg G.order()) \ Seg (G.order()-'i) by A3,A2,Th14;
(Seg G.order()) \ Seg (G.order()-'i) c= Seg G.order() by XBOOLE_1:36;
hence thesis by A77,FINSEQ_1:1;
end;
ex k being Nat st P[k] & for n being Nat st P[n] holds n <= k from
NAT_1:sch 6(A76,A75);
then consider k being Nat such that
A78: P[k] and
A79: for n being Nat st P[n] holds n <= k;
consider v being Vertex of G such that
A80: v in dom VLi and
A81: b,v are_adjacent and
A82: not a,v are_adjacent and
A83: VLi.c < VLi.v and
A84: VLi.v = k by A78;
for d being Vertex of G st d <> v & d,b are_adjacent & not d,a
are_adjacent holds VLi.d < VLi.v
proof
let d be Vertex of G such that
A85: d <> v and
A86: d,b are_adjacent and
A87: not d,a are_adjacent;
per cases;
suppose
VLi.d <= VLi.c;
hence thesis by A83,XXREAL_0:2;
end;
suppose
A88: VLi.c < VLi.d;
then
A89: d in dom VLi by FUNCT_1:def 2;
VLi is one-to-one by Th18;
then
A90: VLi.d <> VLi.v by A80,A85,A89,FUNCT_1:def 4;
VLi.d <= k by A79,A86,A87,A88,A89;
hence thesis by A84,A90,XXREAL_0:1;
end;
end;
hence ex d being Vertex of G st d in dom VLi & VLi.c < VLi.d & b,d
are_adjacent & not a,d are_adjacent & for e being Vertex of G st e <> d & e,b
are_adjacent & not e,a are_adjacent holds VLi.e < VLi.d by A80,A81,A82,A83;
end;
hence thesis by A1;
end;
theorem Th54: :: Theorem 4.3, Golumbic p. 86
for G being _finite chordal _Graph, L be PartFunc of
the_Vertices_of G, NAT st L is with_property_L3 & dom L = the_Vertices_of G for
V being VertexScheme of G st V" = L holds V is perfect
proof
let G be _finite chordal _Graph, L be PartFunc of the_Vertices_of G, NAT such
that
A1: L is with_property_L3 and
A2: dom L = the_Vertices_of G;
let V be VertexScheme of G such that
A3: V" = L;
A4: V is one-to-one by CHORD:def 12;
A5: for x,y being Vertex of G, i,j being Nat st i in dom V & j in dom V & V
/.i = x & V/.j = y holds i < j iff L.x < L.y
proof
let x,y being Vertex of G;
let i,j be Nat such that
A6: i in dom V and
A7: j in dom V and
A8: V/.i = x and
A9: V/.j = y;
V.j = y by A7,A9,PARTFUN1:def 6;
then
A10: L.y = j by A3,A4,A7,FUNCT_1:34;
A11: V.i = x by A6,A8,PARTFUN1:def 6;
hence i<j implies L.x < L.y by A3,A4,A6,A10,FUNCT_1:34;
thus thesis by A3,A4,A6,A11,A10,FUNCT_1:34;
end;
defpred R[Nat] means ex P being Walk of G, v1,v2,v3,v4 being Vertex of G st
P is Path-like & P is open & P is chordless & P.length() = $1-1 & v1 = P.(len P
-2) & v2 = P.3 & v3 = P.last() & v4 = P.first() & L.v4 > L.v3 & L.v3 > L.v2 & L
.v2 > L.v1 & (for x being set st x in P.vertices() holds L.x <= L.v4) & for x
being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1 are_adjacent holds
L.x < L.v4;
A12: for k being Nat st 4 <= k & R[k] holds R[k+1]
proof
A13: 2*0+1 < 2*1+1;
let kk be Nat such that
A14: 4 <= kk and
A15: R[kk];
reconsider k=kk as non zero Nat by A14;
consider P being Walk of G, v1,v2,v3,v4 being Vertex of G such that
A16: P is Path-like and
A17: P is open and
A18: P is chordless and
A19: P.length() = k-1 and
A20: v1 = P.(len P-2) and
A21: v2 = P.3 and
A22: v3 = P.last() and
A23: v4 = P.first() and
A24: L.v4 > L.v3 and
A25: L.v3 > L.v2 and
A26: L.v2 > L.v1 and
A27: for x being set st x in P.vertices() holds L.x <= L.v4 and
A28: for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,
v1 are_adjacent holds L.x < L.v4 by A15;
A29: len P = 2*(k-1) + 1 by A19,GLIB_001:112;
2*k >= 2*4 by A14,XREAL_1:64;
then
A30: 2*k-1 >= 8-1 by XREAL_1:9;
then 1 <= len P by A29,XXREAL_0:2;
then
A31: len P in dom P by FINSEQ_3:25;
now
A32: 2*0+1 < len P by A29,A30,XXREAL_0:2;
let e be object;
assume e Joins v4,v3,G;
then 1+2 = len P by A16,A17,A18,A22,A23,A32,CHORD:92;
hence contradiction by A14,A29;
end;
then
A33: not v4,v3 are_adjacent by CHORD:def 3;
3 < len P by A29,A30,XXREAL_0:2;
then ex ez being object st ez Joins P.1,P.3,G by A16,A17,A18,A13,CHORD:92;
then v4,v2 are_adjacent by A21,A23,CHORD:def 3;
then consider v5 being Vertex of G such that
v5 in dom L and
A34: L.v4 < L.v5 and
A35: v5,v3 are_adjacent and
A36: not v5,v2 are_adjacent and
A37: for x being Vertex of G st x <> v5 & x,v3 are_adjacent & not x,
v2 are_adjacent holds L.x < L.v5 by A1,A2,A24,A25,A33;
consider e being object such that
A38: e Joins P.last(),v5,G by A22,A35,CHORD:def 3;
now
L.v2 < L.v4 by A24,A25,XXREAL_0:2;
then
A39: L.v2 < L.v5 by A34,XXREAL_0:2;
assume v5,v1 are_adjacent;
then consider v6 being Vertex of G such that
v6 in dom L and
A40: L.v5 < L.v6 and
A41: v6,v2 are_adjacent and
A42: not v6,v1 are_adjacent and
for x being Vertex of G st x <> v6 & x,v2 are_adjacent & not x,v1
are_adjacent holds L.x < L.v6 by A1,A2,A26,A36,A39;
thus contradiction by A28,A34,A40,A41,A42,XXREAL_0:2;
end;
then
A43: not ex e being object st e Joins P.(len P-2),v5,G by A20,CHORD:def 3;
set Qr = P.addEdge(e);
set Q = Qr.reverse();
A44: len Q = len Qr by GLIB_001:21;
A45: not v5 in P.vertices() by A27,A34;
then Qr is open by A16,A17,A18,A38,A43,CHORD:97;
then
A46: Q is open by GLIB_001:120;
3 <= len P by A29,A30,XXREAL_0:2;
then
A47: 3 in dom P by FINSEQ_3:25;
then
A48: 3 in dom Qr by A38,Lm6;
v2 = Qr.3 by A21,A38,A47,Lm6;
then
A49: v2 = Q.(len Q-3+1) by A48,A44,GLIB_001:24;
v4 = Qr.first() by A23,A38,GLIB_001:63;
then
A50: v4 = Q.last() by GLIB_001:22;
A51: len Qr = len P + 2 by A38,GLIB_001:64;
then
A52: len Qr-2 in dom Qr by A38,A31,Lm6;
v3 = Qr.(len Qr - 2) by A22,A38,A51,A31,Lm6;
then
A53: v3 = Q.(len Q-(len Qr-2)+1) by A52,A44,GLIB_001:24;
v5 = Qr.last() by A38,GLIB_001:63;
then
A54: v5 = Q.first() by GLIB_001:22;
Qr is chordless by A16,A17,A18,A38,A45,A43,CHORD:97;
then
A55: Q is chordless by CHORD:91;
Qr.length() = k-1+1 by A19,A38,Lm4;
then
A56: Q.length() = (k+1)-1 by Lm5;
A57: now
let x be set;
assume x in Q.vertices();
then x in Qr.vertices() by GLIB_001:92;
then
A58: x in P.vertices() \/ {v5} by A38,GLIB_001:95;
per cases by A58,XBOOLE_0:def 3;
suppose
x in P.vertices();
then L.x <= L.v4 by A27;
hence L.x <= L.v5 by A34,XXREAL_0:2;
end;
suppose
x in {v5};
hence L.x <= L.v5 by TARSKI:def 1;
end;
end;
Qr is Path-like by A16,A17,A18,A38,A45,A43,CHORD:97;
hence thesis by A24,A25,A34,A37,A46,A55,A56,A44,A49,A53,A50,A54,A57;
end;
A59: 11 <= 11+G.order() by NAT_1:11;
assume not V is perfect;
then consider k being non zero Nat such that
A60: k <= len V and
A61: not for H being inducedSubgraph of G, V.followSet(k) for v being
Vertex of H st v = V.k holds v is simplicial by CHORD:def 13;
consider HH being (inducedSubgraph of G,V.followSet(k)), hv being Vertex of
HH such that
A62: hv = V.k and
A63: not hv is simplicial by A61;
consider ha,hb being Vertex of HH such that
A64: ha<>hb and
hv<>ha and
hv<>hb and
A65: hv,ha are_adjacent and
A66: hv,hb are_adjacent and
A67: not ha,hb are_adjacent by A63,CHORD:69;
A68: hv in the_Vertices_of HH;
A69: hb in the_Vertices_of HH;
ha in the_Vertices_of HH;
then reconsider v=hv,aa=ha,bb=hb as Vertex of G by A68,A69;
A70: V.followSet(k) is non empty Subset of the_Vertices_of G by A60,CHORD:107;
then
A71: the_Vertices_of HH = V.followSet(k) by GLIB_000:def 37;
now
A72: L.aa <> L.bb by A2,A3,A4,A64,FUNCT_1:def 4;
per cases by A72,XXREAL_0:1;
suppose
A73: L.aa < L.bb;
take aa, bb;
thus aa in V.followSet(k) by A71;
thus L.aa < L.bb by A73;
thus v,aa are_adjacent by A65,A70,CHORD:45;
thus v,bb are_adjacent by A66,A70,CHORD:45;
thus not aa,bb are_adjacent by A67,A70,CHORD:45;
end;
suppose
A74: L.aa > L.bb;
take bb, aa;
thus bb in V.followSet(k) by A71;
thus L.aa > L.bb by A74;
thus v,bb are_adjacent by A66,A70,CHORD:45;
thus v,aa are_adjacent by A65,A70,CHORD:45;
thus not bb,aa are_adjacent by A67,A70,CHORD:45;
end;
end;
then consider a,bb being Vertex of G such that
A75: a in V.followSet(k) and
A76: L.a < L.bb and
A77: v,a are_adjacent and
A78: v,bb are_adjacent and
A79: not a,bb are_adjacent;
defpred Q[Nat] means $1 in dom V & L.a < L.(V/.$1) & a <> V/.$1 & v,V/.$1
are_adjacent & not a,V/.$1 are_adjacent;
A80: rng V = the_Vertices_of G by CHORD:def 12;
A81: ex k being Nat st Q[k]
proof
consider mbb being object such that
A82: mbb in dom V and
A83: bb = V.mbb by A80,FUNCT_1:def 3;
reconsider mbb as Element of NAT by A82;
take mbb;
thus mbb in dom V by A82;
thus L.a < L.(V/.mbb) by A76,A82,A83,PARTFUN1:def 6;
thus a <> V/.mbb by A76,A82,A83,PARTFUN1:def 6;
thus v,V/.mbb are_adjacent by A78,A82,A83,PARTFUN1:def 6;
thus thesis by A79,A82,A83,PARTFUN1:def 6;
end;
A84: for k being Nat st Q[k] holds k <= len V by FINSEQ_3:25;
consider mb being Nat such that
A85: Q[mb] and
for n being Nat st Q[n] holds n <= mb from NAT_1:sch 6(A84,A81);
reconsider v,a,b = V/.mb as Vertex of G;
consider ma being object such that
A86: ma in dom V and
A87: a = V.ma by A80,FUNCT_1:def 3;
reconsider ma as Element of NAT by A86;
A88: a = V/.ma by A86,A87,PARTFUN1:def 6;
0+1 <= k by NAT_1:13;
then
A89: k in dom V by A60,FINSEQ_3:25;
A90: now
assume ma <= k;
then
A91: ma < k by A62,A78,A79,A87,XXREAL_0:1;
a in the_Vertices_of G;
then
A92: a in rng V by CHORD:def 12;
V is one-to-one by CHORD:def 12;
then a..V >= k by A75,A89,A92,CHORD:16;
then a..V > ma by A91,XXREAL_0:2;
hence contradiction by A86,A87,FINSEQ_4:24;
end;
A93: v = V/.k by A62,A89,PARTFUN1:def 6;
then
A94: L.v < L.a by A5,A89,A86,A88,A90;
A95: v <> b by A77,A85;
A96: R[4]
proof
A97: L.a > L.v by A5,A89,A93,A86,A88,A90;
consider c being Vertex of G such that
c in dom L and
A98: L.b < L.c and
A99: c,a are_adjacent and
A100: not c,v are_adjacent and
A101: for x being Vertex of G st x <> c & x,a are_adjacent & not x,v
are_adjacent holds L.x < L.c by A1,A2,A85,A94;
consider P being Path of G,e1,e2 being object such that
A102: P is open and
A103: len P = 5 and
A104: P.length() = 2 and
e1 Joins b,v,G and
e2 Joins v,a,G and
P.edges() = {e1,e2} and
A105: P.vertices() = {b,v,a} and
A106: P.1 = b and
A107: P.3 = v and
A108: P.5 = a by A77,A85,A95,CHORD:47;
consider e being object such that
A109: e Joins P.last(),c,G by A99,A103,A108,CHORD:def 3;
set Qr = P.addEdge(e);
set Q = Qr.reverse();
A110: Qr.last() = c by A109,GLIB_001:63;
A111: len Qr = 5+2 by A103,A109,GLIB_001:64;
then
A112: 1 in dom Qr by FINSEQ_3:25;
5 in dom P by A103,FINSEQ_3:25;
then
A113: Qr.5 = a by A108,A109,GLIB_001:65;
5 in dom Qr by A111,FINSEQ_3:25;
then
A114: a = Q.(7-5+1) by A111,A113,GLIB_001:24;
7 in dom Qr by A111,FINSEQ_3:25;
then c = Q.(7-7+1) by A111,A110,GLIB_001:24;
then
A115: c = Q.first();
3 in dom P by A103,FINSEQ_3:25;
then
A116: Qr.3 = v by A107,A109,GLIB_001:65;
Qr.length() = 2+1 by A104,A109,Lm4;
then
A117: Q.length() = (3+1)-1 by Lm5;
1 in dom P by A103,FINSEQ_3:25;
then Qr.1 = b by A106,A109,GLIB_001:65;
then b = Q.(len Qr-1+1) by A112,GLIB_001:24;
then
A118: b = Q.last() by GLIB_001:21;
A119: len Q = len Qr by GLIB_001:21;
A120: P.first() = b by A106;
P.last() = a by A103,A108;
then
A121: P is chordless by A85,A103,A120,CHORD:90;
A122: now
let x be set such that
A123: x in P.vertices();
per cases by A105,A123,ENUMSET1:def 1;
suppose
x = b;
hence L.x <= L.b;
end;
suppose
x = v;
hence L.x <= L.b by A85,A94,XXREAL_0:2;
end;
suppose
x = a;
hence L.x <= L.b by A85;
end;
end;
then
A124: not c in P.vertices() by A98;
A125: not ex e being object st e Joins P.(len P-2),c,G by A100,A103,A107,
CHORD:def 3;
then Qr is open by A102,A121,A109,A124,CHORD:97;
then
A126: Q is open by GLIB_001:120;
A127: now
let x be set;
assume x in Q.vertices();
then x in Qr.vertices() by GLIB_001:92;
then
A128: x in P.vertices() \/ {c} by A109,GLIB_001:95;
per cases by A128,XBOOLE_0:def 3;
suppose
x in P.vertices();
then L.x <= L.b by A122;
hence L.x <= L.c by A98,XXREAL_0:2;
end;
suppose
x in {c};
hence L.x <= L.c by TARSKI:def 1;
end;
end;
3 in dom Qr by A111,FINSEQ_3:25;
then v = Q.(7-3+1) by A111,A116,GLIB_001:24;
then
A129: v = Q.(len Q-2) by A111,A119;
Qr is chordless by A102,A121,A109,A124,A125,CHORD:97;
then
A130: Q is chordless by CHORD:91;
Qr is Path-like by A102,A121,A109,A124,A125,CHORD:97;
hence thesis by A85,A98,A101,A126,A130,A117,A114,A129,A118,A115,A97,A127;
end;
for i being Nat st 4 <= i holds R[i] from NAT_1:sch 8(A96,A12);
then R[G.order()+11] by A59,XXREAL_0:2;
then consider P being Walk of G, v1,v2,v3,v4 being Vertex of G such that
A131: P is Path-like and
P is open and
P is chordless and
A132: P.length() = (G.order()+11)-1 and
v1 = P.(len P-2) and
v2 = P.3 and
v3 = P.last() and
v4 = P.first() and
L.v4 > L.v3 and
L.v3 > L.v2 and
L.v2 > L.v1 and
for x being Vertex of G st x <> v4 & x,v2 are_adjacent & not x,v1
are_adjacent holds L.x < L.v4;
len P = 2*(G.order()+10)+1 by A132,GLIB_001:112;
then 2*G.order()+21 + 1 = 2*len P.vertexSeq() by GLIB_001:def 14;
then G.order() + 11 <= G.order() + 1 by A131,GLIB_001:154;
hence contradiction by XREAL_1:8;
end;
theorem :: Theorem 4.3, Golumbic p. 86
for G being _finite chordal _Graph holds (((LexBFS:CSeq(G)).Result())`1
)" is perfect VertexScheme of G
proof
let G be _finite chordal _Graph;
set Hh = ((LexBFS:CSeq(G)).Result())`1;
reconsider V = Hh" as VertexScheme of G by Th50;
A1: dom Hh = the_Vertices_of G by Th49;
Hh = (LexBFS:CSeq(G))``1.Result() by Th40;
then Hh is one-to-one by Th18;
then
A2: V" = Hh by FUNCT_1:43;
Hh is with_property_L3 by Th53;
hence thesis by A1,A2,Th54;
end;
begin :: The Maximum Cardinality Search algorithm
definition
let G be _Graph;
mode MCS:Labeling of G is Element of [: PFuncs(the_Vertices_of G, NAT),
Funcs(the_Vertices_of G, NAT) :];
end;
definition
let G be _finite _Graph;
func MCS:Init(G) -> MCS:Labeling of G equals
[ {}, the_Vertices_of G --> 0 ];
coherence
proof
set f = the_Vertices_of G --> 0;
A1: rng {} c= NAT;
A2: rng f c= NAT;
dom f = the_Vertices_of G;
then
A3: f in Funcs(the_Vertices_of G, NAT) by A2,FUNCT_2:def 2;
dom {} c= the_Vertices_of G;
then {} in PFuncs(the_Vertices_of G,NAT) by A1,PARTFUN1:def 3;
hence thesis by A3,ZFMISC_1:def 2;
end;
end;
definition
let G be _finite _Graph, L be MCS:Labeling of G;
func MCS:PickUnnumbered(L) -> Vertex of G means
:Def19:
it = the Element of
the_Vertices_of G if dom L`1 = the_Vertices_of G otherwise ex S being finite
non empty natural-membered set, F being Function st S = rng F & F = L`2 | (
the_Vertices_of G \ dom (L`1)) & it = the Element of F " {max S};
existence
proof
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set F = V2G | (VG \ dom VLG);
set S = rng F;
per cases;
suppose
dom VLG = VG;
hence thesis;
end;
suppose
A1: dom VLG <> VG;
A2: dom F = dom V2G /\ (VG \ dom VLG) by RELAT_1:61;
dom V2G = VG by FUNCT_2:def 1;
then
A3: dom F = (VG /\ VG) \ dom VLG by A2,XBOOLE_1:49;
now
assume dom F = {};
then VG c= dom VLG by A3,XBOOLE_1:37;
hence contradiction by A1,XBOOLE_0:def 10;
end;
then reconsider S as non empty finite natural-membered set by RELAT_1:42;
set y = max S;
set IT = the Element of F " {max S};
y in S by XXREAL_2:def 8;
then F " {max S} is non empty by FUNCT_1:72;
then IT in dom F by FUNCT_1:def 7;
then IT in dom V2G by RELAT_1:57;
then reconsider IT as Vertex of G;
ex S being finite non empty natural-membered set, F being Function
st S = rng F & F = (L`2) | (the_Vertices_of G \ dom L`1) &
IT = the Element of F " {
max S} & IT is Vertex of G;
hence thesis;
end;
end;
uniqueness;
consistency;
end;
definition
let G be _finite _Graph, L be MCS:Labeling of G, v be set;
func MCS:LabelAdjacent(L, v) -> MCS:Labeling of G equals
[ L`1, (L`2).incSubset(G.AdjacentSet({v}) \ dom L`1, 1) ];
coherence
proof
set V2G = L`2;
set VLG = L`1;
set f = V2G.incSubset(G.AdjacentSet({v})\ dom VLG,1);
A1: rng f c= NAT;
dom f = dom V2G by Def3;
then dom f = the_Vertices_of G by FUNCT_2:def 1;
then f is Function of the_Vertices_of G, NAT by A1,FUNCT_2:2;
then f in Funcs(the_Vertices_of G, NAT) by FUNCT_2:8;
hence thesis by ZFMISC_1:87;
end;
end;
definition
let G be _finite _Graph, L be MCS:Labeling of G, v be Vertex of G, n be Nat;
func MCS:Update(L, v, n) -> MCS:Labeling of G means
:Def21:
ex M being
MCS:Labeling of G st M = [L`1 +* (v .--> (G.order()-'n)), L`2] & it =
MCS:LabelAdjacent(M, v);
existence
proof
set k = G.order()-'n;
set L1 = L`1 +* (v .--> k);
A1: dom L1 = dom L`1 \/ {v} by Lm1;
rng L1 c= NAT;
then L1 in PFuncs(the_Vertices_of G, NAT) by A1,PARTFUN1:def 3;
then reconsider M = [L1, L`2] as MCS:Labeling of G by ZFMISC_1:87;
MCS:LabelAdjacent(M, v) is MCS:Labeling of G;
hence thesis;
end;
uniqueness;
end;
definition
let G be _finite _Graph, L be MCS:Labeling of G;
func MCS:Step(L) -> MCS:Labeling of G equals
:Def22:
L if G.order() <= card
dom (L`1) otherwise MCS:Update(L, MCS:PickUnnumbered(L), card dom (L`1));
coherence;
consistency;
end;
definition
let G be _Graph;
mode MCS:LabelingSeq of G -> ManySortedSet of NAT means
:Def23:
for n being Nat holds it.n is MCS:Labeling of G;
existence
proof
set L = the MCS:Labeling of G;
deffunc F(object) = L;
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
end;
definition
let G be _Graph, S be MCS:LabelingSeq of G, n be Nat;
redefine func S.n -> MCS:Labeling of G; :: redefines . (FUNCT_1, definition)
coherence by Def23;
end;
definition
let G be _Graph, S be MCS:LabelingSeq of G;
redefine func S.Result() -> MCS:Labeling of G; :: redefines .Result() (GLIB_000, definition)
coherence by Def23;
end;
definition
let G be _finite _Graph, S be MCS:LabelingSeq of G;
func S``1 -> preVNumberingSeq of G means
:Def24:
for n being Nat holds it.n = (S.n)`1;
existence
proof
deffunc F(object) = (S.$1)`1;
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds f.i = F(i) from PBOOLE:sch 4;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then f.i = (S.i)`1 by A1;
hence f.i is PartFunc of the_Vertices_of G, NAT;
end;
then reconsider f as preVNumberingSeq of G by Def7;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let it1, it2 be preVNumberingSeq of G such that
A2: for n being Nat holds it1.n = (S.n)`1 and
A3: for n being Nat holds it2.n = (S.n)`1;
now
let i be object;
assume i in NAT;
then reconsider i9 = i as Nat;
thus it1.i = (S.i9)`1 by A2
.= it2.i by A3;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
definition
let G be _finite _Graph;
func MCS:CSeq(G) -> MCS:LabelingSeq of G means
:Def25:
it.0 = MCS:Init(G) & for n being Nat holds it.(n+1) = MCS:Step(it.n);
existence
proof
defpred P[set,set,set] means ($2 is MCS:Labeling of G & $1 is Nat & ex nn
being Nat,Gn,Gn1 being MCS:Labeling of G st $1 = nn & $2 = Gn & $3 = Gn1 & Gn1
= MCS:Step(Gn)) or ((not $2 is MCS:Labeling of G or not $1 is Nat) & $2 = $3);
now
let n,x be set;
now
per cases;
suppose
A1: x is MCS:Labeling of G & n is Nat;
then reconsider Gn=x as MCS:Labeling of G;
ex SGn being MCS:Labeling of G st SGn = MCS:Step(Gn);
hence ex y being set st P[n,x,y] by A1;
end;
suppose
not x is MCS:Labeling of G or not n is Nat;
hence ex y being set st P[n,x,y];
end;
end;
hence ex y being set st P[n,x,y];
end;
then
A2: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A3: dom IT = NAT & IT.0 = MCS:Init(G) & for n being Nat
holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2);
reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means IT.$1 is MCS:Labeling of G;
A4: now
let n be Nat;
assume
A5: P2[n];
ex nn being Nat, Gn,Gn1 being MCS:Labeling of G st n = nn & IT.n =
Gn & IT.(n+1) = Gn1 & Gn1 = MCS:Step(Gn) by A3,A5;
hence P2[n+1];
end;
A6: P2[ 0 ] by A3;
for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4);
then reconsider IT as MCS:LabelingSeq of G by Def23;
take IT;
thus IT.0 = MCS:Init(G) by A3;
let n be Nat;
ex nn being Nat, Gn,Gn1 being MCS:Labeling of G st n = nn & IT.n =
Gn & IT.(n+1) = Gn1 & Gn1 = MCS:Step(Gn) by A3;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be MCS:LabelingSeq of G such that
A7: IT1.0 = MCS:Init(G) and
A8: for n being Nat holds IT1.(n+1) = MCS:Step(IT1.n) and
A9: IT2.0 = MCS:Init(G) and
A10: for n being Nat holds IT2.(n+1) = MCS:Step(IT2.n);
defpred P[Nat] means IT1.$1 = IT2.$1;
now
let n be Nat;
assume P[n];
then IT1.(n+1) = MCS:Step(IT2.n) by A8
.= IT2.(n+1) by A10;
hence P[n+1];
end;
then
A11: for n being Nat st P[n] holds P[n+1];
A12: P[ 0 ] by A7,A9;
for n being Nat holds P[n] from NAT_1:sch 2(A12,A11);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
theorem Th56:
for G being _finite _Graph holds MCS:CSeq(G) is iterative
proof
let G be _finite _Graph;
set CS = MCS:CSeq(G);
let k,n be Nat;
CS.(k+1) = MCS:Step(CS.k) by Def25;
hence thesis by Def25;
end;
registration
let G be _finite _Graph;
cluster MCS:CSeq(G) -> iterative;
coherence by Th56;
end;
theorem
for G being _finite _Graph, v being set holds ((MCS:Init(G))`2).v = 0;
theorem Th58:
for G being _finite _Graph, L be MCS:Labeling of G, x being set
st not x in dom L`1 & dom L`1 <> the_Vertices_of G holds
(L`2).x <= (L`2).(MCS:PickUnnumbered(L))
proof
let G be _finite _Graph, L be MCS:Labeling of G, x be set such that
A1: not x in dom L`1 and
A2: dom L`1 <> the_Vertices_of G;
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set w = MCS:PickUnnumbered(L);
consider S being finite non empty natural-membered set, F being Function
such that
A3: S = rng F and
A4: F = V2G | (VG \ dom VLG) and
A5: w = the Element of F " {max S} by A2,Def19;
A6: dom F = dom V2G /\ (VG \ dom VLG) by A4,RELAT_1:61;
set y = max S;
y in rng F by A3,XXREAL_2:def 8;
then
A7: F " {max S} is non empty by FUNCT_1:72;
then w in dom F by A5,FUNCT_1:def 7;
then
A8: V2G.w = F.w by A4,FUNCT_1:47;
F.w in {max S} by A5,A7,FUNCT_1:def 7;
then
A9: V2G.w = y by A8,TARSKI:def 1;
A10: dom L`2 = the_Vertices_of G by FUNCT_2:def 1;
per cases;
suppose
x in the_Vertices_of G;
then x in VG \ dom VLG by A1,XBOOLE_0:def 5;
then
A11: x in dom F by A10,A6,XBOOLE_0:def 4;
then
A12: F.x in S by A3,FUNCT_1:def 3;
F.x = V2G.x by A4,A11,FUNCT_1:47;
hence thesis by A9,A12,XXREAL_2:def 8;
end;
suppose
not x in the_Vertices_of G;
hence thesis by A10,FUNCT_1:def 2;
end;
end;
theorem Th59:
for G being _finite _Graph, L be MCS:Labeling of G st dom L`1 <>
the_Vertices_of G holds not MCS:PickUnnumbered(L) in dom L`1
proof
let G be _finite _Graph, L be MCS:Labeling of G such that
A1: dom L`1 <> the_Vertices_of G;
set VG = the_Vertices_of G;
set V2G = L`2;
set VLG = L`1;
set w = MCS:PickUnnumbered(L);
consider S being finite non empty natural-membered set, F being Function
such that
A2: S = rng F and
A3: F = V2G | (VG \ dom VLG) and
A4: w = the Element of F " {max S} by A1,Def19;
set y = max S;
y in rng F by A2,XXREAL_2:def 8;
then F " {max S} is non empty by FUNCT_1:72;
then
A5: w in dom F by A4,FUNCT_1:def 7;
assume w in dom VLG;
then
A6: not w in VG \ dom VLG by XBOOLE_0:def 5;
dom F = dom V2G /\ (VG \ dom VLG) by A3,RELAT_1:61;
hence contradiction by A5,A6,XBOOLE_0:def 4;
end;
theorem Th60:
for G being _finite _Graph, L be MCS:Labeling of G, v,x being set
st not x in G.AdjacentSet({v}) holds (L`2).x = (MCS:LabelAdjacent(L,v))`2.x
proof
let G be _finite _Graph, L be MCS:Labeling of G, v,x be set such that
A1: not x in G.AdjacentSet({v});
set V2G = L`2;
set VLG = L`1;
set GL = MCS:LabelAdjacent(L,v);
set V2 = GL`2;
not x in G.AdjacentSet({v}) \ dom VLG by A1,XBOOLE_0:def 5;
hence thesis by Def3;
end;
theorem Th61:
for G being _finite _Graph, L be MCS:Labeling of G, v,x being set
st x in dom L`1 holds L`2.x = (MCS:LabelAdjacent(L,v))`2.x
proof
let G be _finite _Graph, L be MCS:Labeling of G, v,x be set such that
A1: x in dom L`1;
set V2G = L`2;
set VLG = L`1;
set GL = MCS:LabelAdjacent(L,v);
set V2 = GL`2;
not x in G.AdjacentSet({v}) \ dom VLG by A1,XBOOLE_0:def 5;
hence thesis by Def3;
end;
theorem Th62:
for G being _finite _Graph, L being MCS:Labeling of G, v,x being
set st x in dom L`2 & x in G.AdjacentSet{v} & not x in dom L`1 holds (
MCS:LabelAdjacent(L,v))`2.x = (L`2).x + 1
proof
let G be _finite _Graph, L being MCS:Labeling of G, v,x be set such that
A1: x in dom L`2 and
A2: x in G.AdjacentSet({v}) and
A3: not x in dom L`1;
set V2G = L`2;
set VLG = L`1;
set GL = MCS:LabelAdjacent(L,v);
set V2 = GL`2;
x in G.AdjacentSet({v}) \ dom VLG by A2,A3,XBOOLE_0:def 5;
hence thesis by A1,Def3;
end;
theorem
for G being _finite _Graph, L being MCS:Labeling of G, v being set st
dom L`2 = the_Vertices_of G holds dom (MCS:LabelAdjacent(L,v))`2 =
the_Vertices_of G
by Def3;
theorem Th64:
for G being _finite _Graph, n being Nat st card dom (((MCS:CSeq(G
)).n))`1 < G.order() holds ((MCS:CSeq(G)).(n+1))`1 = ((MCS:CSeq(G)).n)`1 +* (
MCS:PickUnnumbered((MCS:CSeq(G)).n) .--> (G.order()-'(card (dom ((MCS:CSeq(G)).
n)`1))))
proof
let G be _finite _Graph, n be Nat such that
A1: card (dom ((MCS:CSeq(G)).n)`1) < G.order();
set CN1 = (MCS:CSeq(G)).(n+1);
set CSN = (MCS:CSeq(G)).n;
set VLN = CSN`1;
set w = MCS:PickUnnumbered(CSN);
set k = G.order() -' card (dom VLN);
CN1 = MCS:Step(CSN) by Def25;
then CN1 = MCS:Update(CSN, w, card (dom VLN)) by A1,Def22;
then consider L being MCS:Labeling of G such that
A2: L = [CSN`1 +* (w .--> k), CSN`2] and
A3: CN1 = MCS:LabelAdjacent(L, w) by Def21;
CN1`1 = [CSN`1 +* (w .--> k), CSN`2]`1 by A3,A2;
hence thesis;
end;
theorem Th65:
for G being _finite _Graph, n being Nat st n <= G.order() holds
card dom ((MCS:CSeq(G)).n)`1 = n
proof
let G be _finite _Graph, n be Nat such that
A1: n <= G.order();
defpred P[Nat] means $1 <= G.order() implies card dom ((MCS:CSeq(G)).$1)`1 =
$1;
A2: for k being Element of NAT st k < G.order() & card dom ((MCS:CSeq(G)).k)
`1 = k holds card dom ((MCS:CSeq(G)).(k+1))`1 = k+1
proof
let k be Element of NAT such that
A3: k < G.order() and
A4: card dom ((MCS:CSeq(G)).k)`1 = k;
set CK1 = (MCS:CSeq(G)).(k+1);
set CSK = (MCS:CSeq(G)).k;
set VLK = CSK`1;
set VK1 = CK1`1;
set w = MCS:PickUnnumbered(CSK);
set wf = w .--> (G.order() -' k);
A5: dom wf = {w};
VK1 = VLK +* (w .--> (G.order()-'k)) by A3,A4,Th64;
then dom VK1 = dom VLK \/ {w} by A5,FUNCT_4:def 1;
hence thesis by A3,A4,Th59,CARD_2:41;
end;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
per cases;
suppose
k < G.order();
hence thesis by A2,A7;
end;
suppose
k >= G.order();
hence thesis by NAT_1:13;
end;
end;
(MCS:CSeq(G)).0 = MCS:Init(G) by Def25;
then
A8: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A8,A6);
hence thesis by A1;
end;
theorem Th66:
for G being _finite _Graph, n being Nat st G.order() <= n holds (
MCS:CSeq(G)).(G.order()) = (MCS:CSeq(G)).n
proof
let G be _finite _Graph, n be Nat;
assume G.order() <= n;
then
A1: ex i being Nat st G.order() + i = n by NAT_1:10;
set CS = MCS:CSeq(G);
defpred V[Nat] means G.order() = card (dom (CS.(G.order()+$1))`1);
defpred P[Nat] means (CS.(G.order())) = (CS.(G.order()+$1));
A2: for k being Nat st V[k] holds V[k+1]
proof
let k be Nat such that
A3: V[k];
set CK1 = (MCS:CSeq(G)).(G.order()+k+1);
set CSK = (MCS:CSeq(G)).(G.order()+k);
CK1 = MCS:Step(CSK) by Def25;
hence thesis by A3,Def22;
end;
A4: V[ 0 ] by Th65;
A5: for k being Nat holds V[k] from NAT_1:sch 2(A4,A2);
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
set CK1 = (MCS:CSeq(G)).(G.order()+k+1);
set CSK = (MCS:CSeq(G)).(G.order()+k);
set VLK = CSK`1;
A8: CK1 = MCS:Step(CSK) by Def25;
card dom VLK = G.order() by A5;
hence thesis by A7,A8,Def22;
end;
A9: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
hence thesis by A1;
end;
theorem Th67:
for G being _finite _Graph, m,n being Nat st G.order() <= m & m
<= n holds (MCS:CSeq(G)).m = (MCS:CSeq(G)).n
proof
let G be _finite _Graph, m,n be Nat such that
A1: G.order() <= m and
A2: m <= n;
(MCS:CSeq(G)).m = (MCS:CSeq(G)).(G.order()) by A1,Th66;
hence thesis by A1,A2,Th66,XXREAL_0:2;
end;
theorem Th68:
for G being _finite _Graph holds MCS:CSeq(G) is eventually-constant
proof
let G be _finite _Graph;
take G.order();
let m be Nat;
assume G.order() <= m;
hence (MCS:CSeq(G)).(G.order()) = (MCS:CSeq(G)).m by Th66;
end;
registration
let G be _finite _Graph;
cluster MCS:CSeq(G) -> eventually-constant;
coherence by Th68;
end;
theorem Th69:
for G being _finite _Graph, n being Nat holds dom ((MCS:CSeq(G)).
n)`1 = the_Vertices_of G iff G.order() <= n
proof
let G be _finite _Graph, n be Nat;
set VLN = ((MCS:CSeq(G)).n)`1;
set CSO = (MCS:CSeq(G)).G.order();
set VLO = CSO`1;
thus dom VLN = the_Vertices_of G implies not n < G.order() by Th65;
card dom VLO = card the_Vertices_of G by Th65;
then
A1: dom VLO = the_Vertices_of G by CARD_2:102;
assume G.order() <= n;
hence thesis by A1,Th67;
end;
theorem Th70:
for G being _finite _Graph holds (MCS:CSeq(G)).Lifespan() = G .order()
proof
let G be _finite _Graph;
set CS = MCS:CSeq(G);
A1: for n being Nat st CS.n = CS.(n+1) holds G.order() <= n
proof
let n be Nat such that
A2: CS.n = CS.(n+1);
set w = MCS:PickUnnumbered(CS.n);
set VN1 = (CS.(n+1))`1;
set VLN = (CS.n)`1;
set j = card (dom VLN);
set wf = w .--> (G.order() -' j);
assume
A3: n < G.order();
then dom VLN <> the_Vertices_of G by Th69;
then
A4: not w in dom VLN by Th59;
j < G.order() by A3,Th65;
then
A5: VN1 = VLN +* (w .--> (G.order() -' j)) by Th64;
dom wf = {w};
then
A6: dom VN1 = dom VLN \/ {w} by A5,FUNCT_4:def 1;
w in {w} by TARSKI:def 1;
hence contradiction by A2,A4,A6,XBOOLE_0:def 3;
end;
G.order() <= G.order()+1 by NAT_1:13;
then CS.(G.order()) = CS.(G.order()+1) by Th66;
hence thesis by A1,GLIB_000:def 56;
end;
theorem Th71:
for G being _finite _Graph holds (MCS:CSeq(G))``1 is eventually-constant
proof
let G be _finite _Graph;
set CS = (MCS:CSeq(G));
set S = CS``1;
now
consider n being Nat such that
A1: for m being Nat st n <= m holds CS.n = CS.m by Def6;
take n;
let m be Nat such that
A2: n <= m;
thus S.n = (CS.n)`1 by Def24
.= (CS.m)`1 by A1,A2
.= S.m by Def24;
end;
hence thesis;
end;
theorem Th72:
for G being _finite _Graph holds (MCS:CSeq(G))``1.Lifespan() = (
MCS:CSeq(G)).Lifespan()
proof
let G be _finite _Graph;
set S = MCS:CSeq(G);
set VN = S``1;
set ls = G.order();
A1: VN is eventually-constant by Th71;
A2: (S.(ls+1))`1 = S``1.(ls+1) by Def24;
A3: now
let n be Nat such that
A4: VN.n = VN.(n+1) and
A5: ls > n;
n+1 <= ls by A5,NAT_1:13;
then
A6: card dom (S.(n+1))`1 = n+1 by Th65;
A7: (S.(n+1))`1 = VN.(n+1) by Def24;
A8: (S.n)`1 = VN.n by Def24;
card dom (S.n)`1 = n by A5,Th65;
hence contradiction by A4,A6,A8,A7;
end;
(S.ls)`1 = S``1.ls by Def24;
then
A9: VN.ls = VN.(ls+1) by A2,Th66,NAT_1:11;
S.Lifespan() = ls by Th70;
hence thesis by A1,A9,A3,GLIB_000:def 56;
end;
theorem Th73:
for G being _finite _Graph holds MCS:CSeq(G)``1 is vertex-numbering
proof
let G be _finite _Graph;
set GS = MCS:CSeq(G);
set S = GS``1;
A1: GS.0 = MCS:Init(G) by Def25;
S.0 = (GS.0)`1 by Def24;
hence S.0 = {} by A1;
now
let k, n be Nat such that
A2: S.k = S.n;
A3: S.(k+1) = (GS.(k+1))`1 by Def24;
A4: S.k = (GS.k)`1 by Def24;
A5: S.(n+1) = (GS.(n+1))`1 by Def24;
A6: S.n = (GS.n)`1 by Def24;
per cases;
suppose
A7: k <= G.order() & n <= G.order();
then card dom ((GS.n)`1) = n by Th65;
hence S.(k+1) = S.(n+1) by A2,A4,A6,A7,Th65;
end;
suppose
A8: k <= G.order() & n >= G.order();
then
A9: GS.n = GS.(G.order()) by Th66;
A10: card dom ((GS.(G.order()))`1) = G.order() by Th65;
A11: n+1 >= G.order() by A8,NAT_1:13;
card dom ((GS.k)`1) = k by A8,Th65;
then k+1 >= G.order() by A2,A4,A6,A9,A10,NAT_1:13;
hence S.(k+1) = (GS.(G.order()))`1 by A3,Th66
.= S.(n+1) by A5,A11,Th66;
end;
suppose
A12: k >= G.order() & n <= G.order();
then
A13: GS.k = GS.(G.order()) by Th66;
A14: card dom ((GS.(G.order()))`1) = G.order() by Th65;
card dom ((GS.n)`1) = n by A12,Th65;
then
A15: n+1 >= G.order() by A2,A4,A6,A13,A14,NAT_1:13;
k+1 >= G.order() by A12,NAT_1:13;
hence S.(k+1) = (GS.(G.order()))`1 by A3,Th66
.= S.(n+1) by A5,A15,Th66;
end;
suppose
A16: k >= G.order() & n >= G.order();
then
A17: n+1 >= G.order() by NAT_1:13;
A18: k+1 >= G.order() by A16,NAT_1:13;
thus S.(k+1) = (GS.(k+1))`1 by Def24
.= (GS.(G.order()))`1 by A18,Th66
.= (GS.(n+1))`1 by A17,Th66
.= S.(n+1) by Def24;
end;
end;
hence S is iterative;
S is eventually-constant by Th71;
hence S is halting;
GS.Lifespan() = S.Lifespan() by Th72;
hence
A19: S.Lifespan() = G.order() by Th70;
let n be Nat such that
A20: n < S.Lifespan();
take w = MCS:PickUnnumbered(GS.n);
A21: (GS.n)`1 = S.n by Def24;
then dom (S.n) <> the_Vertices_of G by A19,A20,Th69;
hence not w in dom (S.n) by A21,Th59;
A22: (GS.(n+1))`1 = S.(n+1) by Def24;
n = card dom (S.n) by A19,A20,A21,Th65;
hence thesis by A19,A20,A21,A22,Th64;
end;
registration
let G be _finite _Graph;
cluster (MCS:CSeq(G))``1 -> vertex-numbering;
coherence by Th73;
end;
theorem Th74:
for G being _finite _Graph, n being Nat st n < G.order() holds ((
MCS:CSeq(G))``1).PickedAt(n) = MCS:PickUnnumbered((MCS:CSeq(G)).n)
proof
let G be _finite _Graph, n be Nat such that
A1: n < G.order();
set GS = MCS:CSeq(G);
set CSN = GS.n;
set CS1 = GS.(n+1);
set VLN = CSN`1;
set VL1 = CS1`1;
A2: GS.Lifespan() = G.order() by Th70;
set PU = MCS:PickUnnumbered(CSN);
set f2 = PU .--> (GS.Lifespan()-'n);
A3: dom f2 = {PU};
n = card dom VLN by A1,Th65;
then VL1 = VLN +* (PU .--> (GS.Lifespan()-'n)) by A1,A2,Th64;
then
A4: dom VL1 = dom VLN \/ {PU} by A3,FUNCT_4:def 1;
A5: (GS``1).Lifespan() = GS.Lifespan() by Th72;
set PA = (GS``1).PickedAt(n);
set f1 = PA .--> (GS.Lifespan()-'n);
A6: dom f1 = {PA};
A7: VLN = (GS``1).n by Def24;
VL1 = (GS``1).(n+1) by Def24;
then VL1 = VLN +* (PA .--> (GS.Lifespan()-'n)) by A1,A2,A7,A5,Def9;
then
A8: dom VL1 = dom VLN \/ {PA} by A6,FUNCT_4:def 1;
A9: not PA in dom VLN by A1,A2,A7,A5,Def9;
now
assume PA <> PU;
then not PA in {PU} by TARSKI:def 1;
then
A10: not PA in dom VL1 by A9,A4,XBOOLE_0:def 3;
PA in {PA} by TARSKI:def 1;
hence contradiction by A8,A10,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem Th75:
for G being _finite _Graph, n being Nat st n < G.order() ex w
being Vertex of G st w = MCS:PickUnnumbered((MCS:CSeq(G)).n) & for v being set
holds (v in G.AdjacentSet({w}) & not v in dom (((MCS:CSeq(G)).n)`1) implies (((
MCS:CSeq(G)).(n+1))`2).v = (((MCS:CSeq(G)).n)`2).v + 1) & (not v in G
.AdjacentSet({w}) or v in dom (((MCS:CSeq(G)).n)`1) implies (((MCS:CSeq(G)).(n+
1))`2).v = (((MCS:CSeq(G)).n)`2).v)
proof
let G be _finite _Graph, n be Nat such that
A1: n < G.order();
set CSN = (MCS:CSeq(G)).n;
set VLN = CSN`1;
A2: n = card dom VLN by A1,Th65;
set k = G.order() -' n;
set w = MCS:PickUnnumbered(CSN);
set CN1 = (MCS:CSeq(G)).(n+1);
set CSlv = [ CSN`1 +* (w .--> k), CSN`2 ];
set CSlv1 = CSN`1 +* (w .--> k);
A3: dom CSlv1 = dom (CSN`1) \/ {w} by Lm1;
rng CSlv1 c= NAT;
then CSlv1 in PFuncs(the_Vertices_of G, NAT) by A3,PARTFUN1:def 3;
then reconsider CSlv as MCS:Labeling of G by ZFMISC_1:def 2;
A4: CN1 = MCS:Step(CSN) by Def25
.= MCS:Update(CSN, w, n) by A1,A2,Def22
.= MCS:LabelAdjacent(CSlv,w) by Def21;
take w;
set V2v = CSlv`2;
set VLv = CSlv`1;
set V21 = CN1`2;
set V2N = CSN`2;
A5: dom VLv = (dom CSN`1) \/ {w} by Lm1;
then
A6: dom VLN c= dom VLv by XBOOLE_1:7;
A7: now
let v be set;
assume
A8: not v in G.AdjacentSet({w}) or v in dom VLN;
per cases by A8;
suppose
not v in G.AdjacentSet({w});
hence V21.v = V2N.v by A4,Th60;
end;
suppose
v in dom VLN;
hence V21.v = V2N.v by A4,A6,Th61;
end;
end;
A9: dom V2N = the_Vertices_of G by FUNCT_2:def 1;
now
let v be set;
assume that
A10: v in G.AdjacentSet({w}) and
A11: not v in dom VLN;
not v in {w} by A10,CHORD:49;
then not v in dom VLv by A5,A11,XBOOLE_0:def 3;
hence V21.v = V2N.v + 1 by A4,A9,A10,Th62;
end;
hence thesis by A7;
end;
theorem Th76:
for G being _finite _Graph, n being Nat, x being set st not x in
dom ((MCS:CSeq(G)).n)`1 holds (((MCS:CSeq(G)).n)`2).x = card (G.AdjacentSet({x}
) /\ (dom ((MCS:CSeq(G)).n)`1))
proof
let G be _finite _Graph, n be Nat;
set CN = (MCS:CSeq(G)).n;
set VLN = CN`1;
defpred P[Nat] means for x being set st not x in dom ((MCS:CSeq(G)).$1)`1
holds (((MCS:CSeq(G)).$1)`2).x = card (G.AdjacentSet({x}) /\ (dom ((MCS:CSeq(G)
).$1)`1));
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
set CS1 = (MCS:CSeq(G)).(k+1);
set CSK = (MCS:CSeq(G)).k;
set VLK = CSK`1;
set VK2 = CSK`2;
set VL1 = CS1`1;
set V12 = CS1`2;
A3: k <= k+1 by XREAL_1:38;
per cases;
suppose
A4: G.order() <= k;
then
A5: VK2 = V12 by A3,Th67;
VLK = VL1 by A3,A4,Th67;
hence thesis by A2,A5;
end;
suppose
A6: k < G.order();
set VL = (MCS:CSeq(G))``1;
A7: G.order() = (MCS:CSeq(G)).Lifespan() by Th70;
A8: VLK = VL.k by Def24;
A9: (MCS:CSeq(G)).Lifespan() = VL.Lifespan() by Th72;
A10: VL1 = VL.(k+1) by Def24;
consider w being Vertex of G such that
A11: w = MCS:PickUnnumbered(CSK) and
A12: for v being set holds (v in G.AdjacentSet({w}) & not v in dom
VLK implies V12.v = VK2.v + 1) & (not v in G.AdjacentSet({w}) or v in dom VLK
implies V12.v = VK2.v) by A6,Th75;
w = (MCS:CSeq(G)``1).PickedAt(k) by A6,A11,Th74;
then
A13: dom CS1`1 = (dom CSK`1) \/ {w} by A6,A7,A8,A10,A9,Th11;
now
let x be set such that
A14: not x in dom VL1;
A15: not x in dom VLK by A13,A14,XBOOLE_0:def 3;
then
A16: card (G.AdjacentSet({x}) /\ dom VLK) = VK2.x by A2;
per cases;
suppose
A17: x in G.AdjacentSet({w}) & not x in dom VLK;
set GAS = G.AdjacentSet({x});
w in GAS by A17,CHORD:53;
then
A18: {w} c= GAS by ZFMISC_1:31;
A19: GAS /\ dom VL1 = (GAS /\ dom VLK) \/ (GAS /\ {w}) by A13,XBOOLE_1:23
.= (GAS /\ dom VLK) \/ {w} by A18,XBOOLE_1:28;
dom VLK <> the_Vertices_of G by A6,Th69;
then not w in dom VLK by A11,Th59;
then
A20: not w in GAS /\ dom VLK by XBOOLE_0:def 4;
V12.x = VK2.x + 1 by A12,A17;
hence card (G.AdjacentSet({x}) /\ dom VL1) = V12.x by A16,A20,A19,
CARD_2:41;
end;
suppose
A21: not x in G.AdjacentSet({w}) or x in dom VLK;
set GAS = G.AdjacentSet({x});
A22: not w in GAS by A13,A14,A21,CHORD:53,XBOOLE_0:def 3;
A23: now
assume GAS /\ {w} = {w};
then w in GAS /\ {w} by TARSKI:def 1;
hence contradiction by A22,XBOOLE_0:def 4;
end;
GAS /\ {w} c= {w} by XBOOLE_1:17;
then GAS /\ {w} in bool {w};
then
A24: GAS /\ {w} in { {}, {w} } by ZFMISC_1:24;
A25: V12.x = VK2.x by A12,A21;
GAS /\ dom VL1 = (GAS /\ dom VLK) \/ (GAS /\ {w}) by A13,XBOOLE_1:23
.= (GAS /\ dom VLK) \/ {} by A24,A23,TARSKI:def 2
.= GAS /\ dom VLK;
hence card (G.AdjacentSet({x}) /\ dom VL1) = V12.x by A2,A15,A25;
end;
end;
hence thesis;
end;
end;
now
set C0 = (MCS:CSeq(G)).0;
let x be set;
set VL0 = C0`1;
set V20 = C0`2;
assume not x in dom VL0;
A26: C0 = MCS:Init(G) by Def25;
dom VL0 = {} by A26;
hence V20.x = card (G.AdjacentSet({x}) /\ dom VL0) by A26;
end;
then
A27: P[ 0 ];
A28: for k being Nat holds P[k] from NAT_1:sch 2(A27,A1);
let x be set;
assume not x in dom VLN;
hence thesis by A28;
end;
definition
let G be _Graph, F be PartFunc of the_Vertices_of G, NAT;
attr F is with_property_T means
for a,b,c being Vertex of G st a in
dom F & b in dom F & c in dom F & F.a < F.b & F.b < F.c & a,c are_adjacent &
not b,c are_adjacent ex d being Vertex of G st d in dom F & F.b < F.d & b,d
are_adjacent & not a,d are_adjacent;
end;
theorem
for G being _finite _Graph, n being Nat holds ((MCS:CSeq(G)).n)`1 is
with_property_T
proof
let G be _finite _Graph, n be Nat;
set CN = (MCS:CSeq(G)).n;
set VLN = CN`1;
set VL = (MCS:CSeq(G))``1;
now
A1: (MCS:CSeq(G)).Lifespan() = VL.Lifespan() by Th72;
A2: VLN = VL.n by Def24;
let a,b,c be Vertex of G such that
A3: a in dom VLN and
A4: b in dom VLN and
A5: c in dom VLN and
A6: VLN.a < VLN.b and
A7: VLN.b < VLN.c and
A8: a,c are_adjacent and
A9: not b,c are_adjacent;
A10: G.order() = (MCS:CSeq(G)).Lifespan() by Th70;
now
set bn = G.order() -' VLN.b;
set CSB = (MCS:CSeq(G)).bn;
set VLB = CSB`1;
set VL2 = CSB`2;
not c in G.AdjacentSet({b}) by A9,CHORD:52;
then
A11: not c in (G.AdjacentSet({b}) /\ dom VLB) by XBOOLE_0:def 4;
A12: b = (MCS:CSeq(G)``1).PickedAt(bn) by A4,A10,A2,A1,Th20;
A13: c in G.AdjacentSet({a}) by A6,A7,A8,CHORD:52;
A14: VLB = VL.bn by Def24;
then not a in dom VLB by A3,A6,A10,A2,A1,Th24;
then
A15: VL2.a = card (G.AdjacentSet({a}) /\ dom VLB) by Th76;
bn < n by A4,A10,A2,A1,Th22;
then VLB c= VLN by A2,A14,Th17;
then
A16: dom VLB c= dom VLN by RELAT_1:11;
VLN.b <= G.order() by A10,A2,A1,Th15;
then
A17: G.order() -' VLN.b = G.order() - VLN.b by XREAL_1:233;
then VLN.b = G.order() - (G.order() -' VLN.b);
then
A18: VLN.b = G.order() -' (G.order() -' VLN.b) by NAT_D:35,XREAL_1:233;
A19: now
assume
A20: a in dom VLB;
then VLN.b < VLB.a by A10,A1,A14,A18,Th22;
hence contradiction by A3,A6,A2,A14,A20,Th19;
end;
A21: 1 <= VLN.b by A4,A2,Th15;
then
A22: bn < G.order() by A17,XREAL_1:44;
then
A23: dom VLB <> the_Vertices_of G by Th69;
assume
A24: for d being Vertex of G st d in dom VLN & VLN.b < VLN.d & b,d
are_adjacent holds a,d are_adjacent;
now
set CSB1 = (MCS:CSeq(G)).(bn+1);
set VLB1 = CSB1`1;
let x be object such that
A25: x in G.AdjacentSet({b}) /\ dom VLB;
reconsider d = x as Vertex of G by A25;
A26: x in dom VLB by A25,XBOOLE_0:def 4;
x in dom VLB by A25,XBOOLE_0:def 4;
then
A27: VLN.d = VLB.d by A2,A14,A16,Th19;
A28: VLB1 = VL.(bn+1) by Def24;
then b in dom VLB1 by A10,A1,A22,A12,Th11;
then
A29: VLN.b = VLB1.b by A4,A2,A28,Th19;
bn < bn+1 by XREAL_1:39;
then VLB c= VLB1 by A14,A28,Th17;
then dom VLB c= dom VLB1 by RELAT_1:11;
then
A30: VLB.d = VLB1.d by A14,A26,A28,Th19;
VLB.d in rng VLB by A26,FUNCT_1:def 3;
then VLB.d in (Seg G.order()\Seg (G.order()-'bn)) by A10,A1,A14,Th14;
then G.order() -' bn < VLB1.d by A30,Th3;
then
A31: VLN.b < VLN.d by A10,A1,A17,A21,A12,A28,A29,A27,A30,Th12,XREAL_1:44;
d in G.AdjacentSet({b}) by A25,XBOOLE_0:def 4;
then b,d are_adjacent by CHORD:52;
then a,d are_adjacent by A24,A16,A26,A31;
then d in G.AdjacentSet({a}) by A6,A31,CHORD:52;
hence x in G.AdjacentSet({a}) /\ dom VLB by A26,XBOOLE_0:def 4;
end;
then
A32: (G.AdjacentSet({b}) /\ dom VLB) c= (G.AdjacentSet({a}) /\ dom VLB);
c in dom VLB by A4,A5,A7,A10,A2,A1,A14,Th23;
then c in (G.AdjacentSet({a}) /\ dom VLB) by A13,XBOOLE_0:def 4;
then
A33: (G.AdjacentSet({b}) /\ dom VLB) c< (G.AdjacentSet({a}) /\ dom VLB)
by A11,A32,XBOOLE_0:def 8;
A34: b = MCS:PickUnnumbered(CSB) by A17,A21,A12,Th74,XREAL_1:44;
then VL2.b = card (G.AdjacentSet({b}) /\ dom VLB) by A23,Th59,Th76;
hence contradiction by A23,A34,A19,A15,A33,Th58,TREES_1:6;
end;
hence ex d being Vertex of G st d in dom VLN & VLN.b < VLN.d & b,d
are_adjacent & not a,d are_adjacent;
end;
hence thesis;
end;
theorem
for G being _finite _Graph holds ((LexBFS:CSeq(G)).Result())`1 is
with_property_T
proof
let G be _finite _Graph;
set CS = LexBFS:CSeq(G);
set L = (CS.Result())`1;
A1: L is with_property_L3 by Th53;
now
let a,b,c be Vertex of G such that
A2: a in dom L and
A3: b in dom L and
A4: c in dom L and
A5: L.a < L.b and
A6: L.b < L.c and
A7: a,c are_adjacent and
A8: not b,c are_adjacent;
consider d being Vertex of G such that
A9: d in dom L and
A10: L.c < L.d and
A11: b,d are_adjacent and
A12: not a,d are_adjacent and
for e being Vertex of G st e <> d & e,b are_adjacent & not e,a
are_adjacent holds L.e < L.d by A1,A2,A3,A4,A5,A6,A7,A8;
take d;
thus d in dom L by A9;
thus L.b < L.d by A6,A10,XXREAL_0:2;
thus b,d are_adjacent by A11;
thus not a,d are_adjacent by A12;
end;
hence thesis;
end;
theorem :: Tarjan (SIAM Journal of Computing; 13(3):August 1984)
for G being _finite chordal _Graph, L being PartFunc of the_Vertices_of
G, NAT st L is with_property_T & dom L = the_Vertices_of G for V being
VertexScheme of G st V" = L holds V is perfect
proof
let G be _finite chordal _Graph, L be PartFunc of the_Vertices_of G, NAT such
that
A1: L is with_property_T and
A2: dom L = the_Vertices_of G;
defpred Q[Path of G] means len $1 >= 5 & $1 is open & $1 is chordless & L.(
$1.first()) > L.($1.last()) & L.($1.last()) > L.($1.3) & ex i being odd Element
of NAT st 1 < i & i < len $1 & (for j,k being odd Element of NAT st i <= j & j
< k & k <= len $1 holds L.($1.j) < L.($1.k)) & (for j,k being odd Element of
NAT st 1 <= j & j < k & k <= i holds L.($1.j) > L.($1.k));
let V be VertexScheme of G such that
A3: V" = L;
A4: V is one-to-one by CHORD:def 12;
len V = card the_Vertices_of G by CHORD:104;
then dom V = Seg G.order() by FINSEQ_1:def 3;
then
A5: rng L = Seg G.order() by A3,A4,FUNCT_1:33;
A6: now
defpred M[Nat] means ex P being Path of G st Q[P] & L.(P.last()) = $1;
A7: for k being Nat st M[k] holds k <= G.order()
proof
let k be Nat;
assume M[k];
then consider P being Path of G such that
Q[P] and
A8: L.(P.last()) = k;
L.(P.last()) in Seg G.order() by A2,A5,FUNCT_1:def 3;
hence thesis by A8,FINSEQ_1:1;
end;
let R being Path of G;
assume Q[R];
then
A9: ex k being Nat st M[k];
consider k being Nat such that
A10: M[k] and
A11: for n being Nat st M[n] holds n <= k from NAT_1:sch 6(A7,A9);
consider P being Path of G such that
A12: Q[P] and
A13: L.(P.last()) = k by A10;
3 <= len P by A12,XXREAL_0:2;
then P.3 = P.vertexAt(2*1+1) by GLIB_001:def 8;
then reconsider a = P.3 as Vertex of G;
A14: 3 < len P by A12,XXREAL_0:2;
reconsider b = P.last() as Vertex of G;
reconsider c = P.first() as Vertex of G;
A15: now
2*0+1 < len P by A12,XXREAL_0:2;
then
A16: (ex e being object st e Joins P.1,P.(len P),G) iff 1+2=len P
by A12,CHORD:92;
let e be object;
assume e Joins c,b,G;
hence contradiction by A12,A16;
end;
then
A17: not b,c are_adjacent by CHORD:def 3;
2*0+1 < 2*1+1;
then ex ez being object st ez Joins P.1,P.3,G by A12,A14,CHORD:92;
then c,a are_adjacent by CHORD:def 3;
then consider d being Vertex of G such that
d in dom L and
A18: L.b < L.d and
A19: b,d are_adjacent and
A20: not a,d are_adjacent by A1,A2,A12,A17;
A21: L.d <> L.c by A2,A3,A4,A17,A19,FUNCT_1:def 4;
consider i being odd Element of NAT such that
A22: 1 < i and
i < len P and
A23: for j,k being odd Element of NAT st i <= j & j < k & k <= len P
holds L.(P.j) < L.(P.k) and
A24: for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L.(P.j) > L.(P.k) by A12;
A25: L.a < L.d by A12,A18,XXREAL_0:2;
A26: now
assume d in P.vertices();
then consider dn being odd Element of NAT such that
A27: dn <= len P and
A28: P.dn = d by GLIB_001:87;
A29: 1 <= dn by CHORD:2;
dn <> 1 by A15,A19,A28,CHORD:def 3;
then 2*0+1 < dn by A29,XXREAL_0:1;
then 1+2 <= dn by CHORD:4;
then
A30: 2*1+1 < dn by A12,A18,A28,XXREAL_0:1;
A31: dn < len P by A18,A27,A28,XXREAL_0:1;
per cases;
suppose
i <= dn;
hence contradiction by A23,A18,A28,A31;
end;
suppose
dn < i;
hence contradiction by A24,A25,A28,A30;
end;
end;
defpred Mi[Nat] means $1 is odd & 3 < $1 & $1 <= len P &
ex e being object st e Joins P.$1,d,G;
ex el being object st el Joins P.last(),d,G by A19,CHORD:def 3;
then
A32: ex k being Nat st Mi[k] by A14;
ex j being Nat st Mi[j] & for n being Nat st Mi[n] holds j <= n from
NAT_1:sch 5(A32);
then consider j being Nat such that
A33: j is odd and
A34: 3 < j and
A35: j <= len P and
A36: ex e being object st e Joins P.j,d,G and
A37: for i being Nat st Mi[i] holds j <= i;
reconsider j as odd Element of NAT by A33,ORDINAL1:def 12;
reconsider C = P.cut(1,j) as Path of G;
consider e being object such that
A38: e Joins P.j,d,G by A36;
2*0+1 < j by A34,XXREAL_0:2;
then
A39: C is open chordless by A12,A35,CHORD:93;
A40: 2*0+1 <= j by CHORD:2;
then
A41: len C + 1 = j + 1 by A35,GLIB_001:36;
A42: now
let n be odd Element of NAT such that
A43: n <= j;
1 <= n by CHORD:2;
then n in dom C by A41,A43,FINSEQ_3:25;
then C.n = P.(1 + n - 1) by A35,A40,GLIB_001:47;
hence C.n = P.n;
end;
2*1+1 < j by A34;
then
A44: C.3 = a by A42;
A45: now
len C > 2*1+1 by A34,A41;
then
A46: len C >= 3+2 by CHORD:4;
let f be object such that
A47: f Joins C.(len C-2),d,G;
len C <> 5 by A20,A44,A47,CHORD:def 3;
then len C > 5 by A46,XXREAL_0:1;
then
A48: 3+2-2 < len C-2 by XREAL_1:9;
then 0 < len C-2*1;
then reconsider cc = len C - 2 as odd Element of NAT by INT_1:3;
A49: cc < len C by XREAL_1:44;
then
A50: cc < len P by A35,A41,XXREAL_0:2;
f Joins P.cc,d,G by A41,A42,A47,A49;
hence contradiction by A37,A41,A48,A49,A50;
end;
A51: e Joins C.last(),d,G by A35,A38,A40,GLIB_001:37;
C.vertices() c= P.vertices() by A35,A40,GLIB_001:94;
then
A52: not d in C.vertices() by A26;
then reconsider D = C.addEdge(e) as Path of G by A51,A39,A45,CHORD:97;
reconsider R = D.reverse() as Path of G;
A53: C.last() = P.j by A35,A40,GLIB_001:37;
then
A54: len D = len C + 2 by A38,GLIB_001:64;
A55: now
per cases;
suppose
A56: i < j;
now
per cases by A35,XXREAL_0:1;
suppose
j = len P;
hence L.(P.j) <= L.b;
end;
suppose
j < len P;
hence L.(P.j) <= L.b by A23,A56;
end;
end;
hence L.(P.j) < L.c by A12,XXREAL_0:2;
end;
suppose
A57: i >= j;
1 < 2*1+1;
then L.(P.j) < L.(P.3) by A24,A34,A57;
then L.(P.j) < L.b by A12,XXREAL_0:2;
hence L.(P.j) < L.c by A12,XXREAL_0:2;
end;
end;
C.first() = P.first() by A35,A40,GLIB_001:37;
then
A58: D.first() = c by A38,A53,GLIB_001:63;
then
A59: R.last() = c by GLIB_001:22;
3 in dom C by A34,A41,FINSEQ_3:25;
then
A60: D.3 = a by A38,A53,A44,GLIB_001:65;
A61: D is chordless by A52,A51,A39,A45,CHORD:97;
A62: D.last() = d by A38,A53,GLIB_001:63;
then
A63: R.first() = d by GLIB_001:22;
A64: for n being odd Element of NAT st n <= len R holds R.n = D.(len D -
n + 1) & len D - n + 1 is Element of NAT
proof
let n be odd Element of NAT such that
A65: n <= len R;
1 <= n by CHORD:2;
then
A66: n in dom R by A65,FINSEQ_3:25;
hence R.n = D.(len D - n + 1) by GLIB_001:25;
len D - n + 1 in dom D by A66,GLIB_001:25;
hence thesis;
end;
A67: now
let n be odd Nat such that
A68: n <= j;
1 <= n by CHORD:2;
then n in dom C by A41,A68,FINSEQ_3:25;
hence C.n = D.n by A51,GLIB_001:65;
end;
A69: ex i being odd Element of NAT st 1 < i & i < len D & (for j,k being
odd Element of NAT st i <= j & j < k & k <= len D holds L.(D.j) < L.(D.k)) &
for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds L.(D.j) > L.(
D.k)
proof
per cases;
suppose
A70: j <= i;
A71: now
1 < 2*1+1;
then
A72: L.(P.3) > L.(P.j) by A24,A34,A70;
let e,f be odd Element of NAT such that
A73: j <= e and
A74: e < f and
A75: f <= len D;
e < j + 2*1 by A41,A54,A74,A75,XXREAL_0:2;
then e <= j + 2 - 2 by CHORD:3;
then
A76: e = j by A73,XXREAL_0:1;
then D.e = C.j by A67;
then
A77: D.e = P.j by A42;
len C + 2 <= f by A41,A74,A76,CHORD:4;
then D.f = d by A54,A62,A75,XXREAL_0:1;
hence L.(D.e) < L.(D.f) by A25,A77,A72,XXREAL_0:2;
end;
take j;
now
let e,f be odd Element of NAT such that
A78: 1 <= e and
A79: e < f and
A80: f <= j;
D.e = C.e by A67,A79,A80,XXREAL_0:2;
then
A81: D.e = P.e by A42,A79,A80,XXREAL_0:2;
D.f = C.f by A67,A80;
then
A82: D.f = P.f by A42,A80;
f <= i by A70,A80,XXREAL_0:2;
hence L.(D.e) > L.(D.f) by A24,A78,A79,A81,A82;
end;
hence thesis by A34,A41,A54,A71,XREAL_1:29,XXREAL_0:2;
end;
suppose
A83: i < j;
take i;
A84: now
let e,f be odd Element of NAT such that
A85: i <= e and
A86: e < f and
A87: f <= len D;
e < j + 2*1 by A41,A54,A86,A87,XXREAL_0:2;
then
A88: e <= j + 2 - 2 by CHORD:3;
then
A89: e <= len P by A35,XXREAL_0:2;
A90: D.e = C.e by A67,A88;
then
A91: D.e = P.e by A42,A88;
per cases by A87,XXREAL_0:1;
suppose
A92: f = len D;
now
per cases by A89,XXREAL_0:1;
suppose
e = len P;
hence L.(D.e) <= L.b by A42,A88,A90;
end;
suppose
e < len P;
hence L.(D.e) <= L.b by A23,A85,A91;
end;
end;
hence L.(D.e) < L.(D.f) by A18,A62,A92,XXREAL_0:2;
end;
suppose
f < len D;
then
A93: f <= j + 2 - 2 by A41,A54,CHORD:3;
then D.f = C.f by A67;
then
A94: D.f = P.f by A42,A93;
f <= len P by A35,A93,XXREAL_0:2;
hence L.(D.e) < L.(D.f) by A23,A85,A86,A91,A94;
end;
end;
A95: now
let e,f be odd Element of NAT such that
A96: 1 <= e and
A97: e < f and
A98: f <= i;
D.f = C.f by A67,A83,A98,XXREAL_0:2;
then
A99: D.f = P.f by A42,A83,A98,XXREAL_0:2;
A100: e <= i by A97,A98,XXREAL_0:2;
then D.e = C.e by A67,A83,XXREAL_0:2;
then D.e = P.e by A42,A83,A100,XXREAL_0:2;
hence L.(D.e) > L.(D.f) by A24,A96,A97,A98,A99;
end;
len D > j by A41,A54,XREAL_1:29;
hence thesis by A22,A83,A84,A95,XXREAL_0:2;
end;
end;
A101: ex i being odd Element of NAT st 1 < i & i < len R & (for j,k being
odd Element of NAT st i <= j & j < k & k <= len R holds L.(R.j) < L.(R.k)) &
for j,k being odd Element of NAT st 1 <= j & j < k & k <= i holds L.(R.j) > L.(
R.k)
proof
consider i being odd Element of NAT such that
A102: 1 < i and
A103: i < len D and
A104: for j,k being odd Element of NAT st i <= j & j < k & k <= len
D holds L.(D.j) < L.(D.k) and
A105: for j,k being odd Element of NAT st 1 <= j & j < k & k <= i
holds L.(D.j) > L.(D.k) by A69;
set ir = len D - i + 1;
len D - 1 > len D - i by A102,XREAL_1:15;
then
A106: len D - 1 + 1 > len D - i + 1 by XREAL_1:8;
then
A107: ir < len R by GLIB_001:21;
A108: len D - len D < len D - i by A103,XREAL_1:15;
then reconsider ir as odd Element of NAT by INT_1:3;
A109: now
let ja,k be odd Element of NAT such that
A110: 1 <= ja and
A111: ja < k and
A112: k <= ir;
set jr = len D - ja + 1;
A113: k <= len R by A107,A112,XXREAL_0:2;
then
A114: ja <= len R by A111,XXREAL_0:2;
then
A115: R.ja = D.jr by A64;
i + k <= len D - i + 1 + i by A112,XREAL_1:7;
then
A116: i + k - k <= len D + 1 - k by XREAL_1:9;
set kr = len D - k + 1;
A117: kr < jr by A111,Lm3;
reconsider jr as odd Element of NAT by A64,A114;
reconsider kr as odd Element of NAT by A64,A113;
len D - ja <= len D - 1 by A110,XREAL_1:10;
then jr <= len D - 1 + 1 by XREAL_1:7;
then L.(D.kr) < L.(D.jr) by A104,A116,A117;
hence L.(R.ja) > L.(R.k) by A64,A113,A115;
end;
take ir;
A118: now
let j,k be odd Element of NAT such that
A119: ir <= j and
A120: j < k and
A121: k <= len R;
set kr = len D - k + 1;
A122: R.k = D.kr by A64,A121;
set jr = len D - j + 1;
A123: j <= len R by A120,A121,XXREAL_0:2;
then
A124: R.j = D.jr by A64;
reconsider kr as odd Element of NAT by A64,A121;
i + j >= len D - i + 1 + i by A119,XREAL_1:7;
then
A125: i + j - j >= len D + 1 - j by XREAL_1:9;
reconsider jr as odd Element of NAT by A64,A123;
kr < jr by A120,Lm3;
hence L.(R.j) < L.(R.k) by A105,A124,A122,A125,CHORD:2;
end;
0 + 1 < len D - i + 1 by A108,XREAL_1:8;
hence thesis by A106,A118,A109,GLIB_001:21;
end;
A126: len D >= 3+2 by A34,A41,A54,XREAL_1:7;
then
A127: len R >= 3+2 by GLIB_001:21;
then 3 <= len R by XXREAL_0:2;
then 3 in dom R by FINSEQ_3:25;
then R.3 = D.(len D - 3 + 1) by GLIB_001:25;
then R.3 = C.j by A41,A54,A67;
then
A128: L.(R.last()) > L.(R.3) by A42,A59,A55;
d <> c by A15,A19,CHORD:def 3;
then
A129: R is open by A63,A59;
D is open by A52,A51,A39,A45,CHORD:97;
then L.c <= L.d by A11,A13,A18,A25,A61,A126,A58,A62,A60,A69;
then
A130: L.c < L.d by A21,XXREAL_0:1;
R is chordless by A61,CHORD:91;
hence contradiction by A11,A12,A13,A130,A63,A59,A129,A127,A128,A101;
end;
A131: L" = V by A3,A4,FUNCT_1:43;
now
let a,b,c be Vertex of G such that
A132: b<>c and
A133: a,b are_adjacent and
A134: a,c are_adjacent;
let va,vb,vc be Nat such that
A135: va in dom V and
A136: vb in dom V and
A137: vc in dom V and
A138: V.va = a and
A139: V.vb = b and
A140: V.vc = c and
A141: va < vb and
A142: va < vc;
A143: L.a = va by A3,A4,A135,A138,FUNCT_1:34;
A144: c = V.(L.c) by A2,A3,A4,A131,FUNCT_1:34;
A145: b = V.(L.b) by A2,A3,A4,A131,FUNCT_1:34;
assume
A146: not b,c are_adjacent;
A147: L.b = vb by A3,A4,A136,A139,FUNCT_1:34;
A148: L.c = vc by A3,A4,A137,A140,FUNCT_1:34;
per cases by A132,A145,A144,XXREAL_0:1;
suppose
A149: L.b < L.c;
A150: 2*1+1 is odd;
consider P being Path of G, e1, e2 being object such that
A151: P is open and
A152: len P = 5 and
P.length() = 2 and
e1 Joins c,a,G and
e2 Joins a,b,G and
P.edges() = {e1,e2} and
P.vertices() = {c,a,b} and
A153: P.1 = c and
A154: P.3 = a and
A155: P.5 = b by A132,A133,A134,A141,A142,A143,A147,A148,CHORD:47;
A156: P.first() = c by A153;
A157: now
let j,k be odd Element of NAT such that
1 <= j and
A158: j < k and
A159: k <= 3;
j < 3 by A158,A159,XXREAL_0:2;
then j = 1 by CHORD:7,XXREAL_0:2;
hence L.(P.j) > L.(P.k) by A142,A143,A148,A153,A154,A158,A159,CHORD:7
,XXREAL_0:2;
end;
A160: now
let j,k be odd Element of NAT such that
A161: 3 <= j and
A162: j < k and
A163: k <= len P;
j < 5 by A152,A162,A163,XXREAL_0:2;
then j = 1 or j = 3 or j = 5 by CHORD:8,XXREAL_0:2;
hence
L.(P.j) < L.(P.k) by A141,A142,A143,A147,A148,A152,A153,A154,A155,A161
,A162,A163,CHORD:8,XXREAL_0:2;
end;
P.last() = b by A152,A155;
then Q[P] by A146,A149,A151,A152,A156,A160,A157,A150,CHORD:90;
hence contradiction by A6;
end;
suppose
A164: L.c < L.b;
A165: 2*1+1 is odd;
consider P being Path of G, e1, e2 being object such that
A166: P is open and
A167: len P = 5 and
P.length() = 2 and
e1 Joins b,a,G and
e2 Joins a,c,G and
P.edges() = {e1,e2} and
P.vertices() = {b,a,c} and
A168: P.1 = b and
A169: P.3 = a and
A170: P.5 = c by A132,A133,A134,A141,A142,A143,A147,A148,CHORD:47;
A171: P.first() = b by A168;
A172: now
let j,k be odd Element of NAT such that
1 <= j and
A173: j < k and
A174: k <= 3;
j < 3 by A173,A174,XXREAL_0:2;
then j = 1 by CHORD:7,XXREAL_0:2;
hence L.(P.j) > L.(P.k) by A141,A143,A147,A168,A169,A173,A174,CHORD:7
,XXREAL_0:2;
end;
A175: now
let j,k be odd Element of NAT such that
A176: 3 <= j and
A177: j < k and
A178: k <= len P;
j < 5 by A167,A177,A178,XXREAL_0:2;
then j = 1 or j = 3 or j = 5 by CHORD:8,XXREAL_0:2;
hence
L.(P.j) < L.(P.k) by A141,A142,A143,A147,A148,A167,A168,A169,A170,A176
,A177,A178,CHORD:8,XXREAL_0:2;
end;
P.last() = c by A167,A170;
then Q[P] by A146,A164,A166,A167,A171,A175,A172,A165,CHORD:90;
hence contradiction by A6;
end;
end;
hence thesis by CHORD:109;
end;