:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 13, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, XBOOLE_0, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0,
ARYTM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, ORDINAL4, GRAPH_1,
STRUCT_0, TREES_2, PARTFUN1, GLIB_000, FINSEQ_2, ZFMISC_1, FINSEQ_4,
FUNCT_4, GRAPH_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, RELSET_1, XXREAL_2, FINSEQ_1, FUNCT_1, PARTFUN1,
FUNCT_2, ZFMISC_1, FINSEQ_2, FINSEQ_4, FUNCT_7, FINSET_1, INT_1, NAT_1,
NAT_D, RECDEF_1, STRUCT_0, GRAPH_1, FINSEQ_6;
constructors WELLORD2, RECDEF_1, FINSEQ_4, FINSEQ_6, GRAPH_1, FUNCT_7,
XXREAL_2, NAT_D, RELSET_1, FINSEQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
CARD_1, FINSEQ_1, FINSEQ_6, GRAPH_1, STRUCT_0, RELSET_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, GRAPH_1;
equalities FINSEQ_2, FINSEQ_1, FINSEQ_6;
expansions TARSKI, GRAPH_1;
theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, GRAPH_1, RELAT_1, FUNCT_1,
GRFUNC_1, FUNCT_2, INT_1, CARD_1, CARD_2, FINSEQ_3, FINSEQ_4, XBOOLE_0,
XBOOLE_1, ORDINAL1, XREAL_1, FINSEQ_5, XXREAL_0, MEMBERED, FUNCT_7,
PARTFUN1, XXREAL_2, XREAL_0, NAT_D, FINSEQ_6;
schemes NAT_1, FINSEQ_1, FUNCT_1;
begin :: Vertex sequences induced by chains
Lm2: for p be FinSequence, m, n be Nat st 1<=m & m<=n+1 & n<=len p
holds len (m, n)-cut p +m = n+1 & for i being Nat st i set equals
{ v: ex e being Element of the carrier' of G st
e in X & (v = (the Source of G).e or v = (the Target of G).e) };
correctness;
end;
definition
let G, vs;
let c be FinSequence;
pred vs is_vertex_seq_of c means
len vs = len c + 1 & for n being Nat st 1<=n &
n<=len c holds c.n joins vs/.n, vs/.(n+1);
end;
theorem Th31:
c <>{} & vs is_vertex_seq_of c implies G-VSet rng c = rng vs
proof
assume that
A1: c <>{} and
A2: vs is_vertex_seq_of c;
A3: len vs = len c + 1 by A2;
now
let y be object;
hereby
assume y in G-VSet rng c;
then consider v being Element of G such that
A4: v=y and
A5: ex e being Element of the carrier' of G st e in rng c & (v = (
the Source of G).e or v = (the Target of G).e);
consider e being Element of the carrier' of G such that
A6: e in rng c and
A7: v = (the Source of G).e or v = (the Target of G).e by A5;
consider x being object such that
A8: x in dom c and
A9: e = c.x by A6,FUNCT_1:def 3;
reconsider x as Element of NAT by A8;
A10: 1<=x+1 by NAT_1:12;
set v2 = vs/.(x+1);
set v1 = vs/.x;
A11: x<=len c by A8,FINSEQ_3:25;
then
A12: x+1 in dom vs by A10,FINSEQ_3:25,A3,XREAL_1:7;
A13: 1<=x by A8,FINSEQ_3:25;
then c.x joins v1, v2 by A2,A11;
then
A14: v = v1 or v = v2 by A7,A9;
A15: x<=len vs by A3,A11,NAT_1:12;
then
A16: v1 = vs.x by A13,FINSEQ_4:15;
A17: x in dom vs by A13,A15,FINSEQ_3:25;
v2 = vs.(x+1) by A3,A11,A10,FINSEQ_4:15,XREAL_1:7;
hence y in rng vs by A4,A16,A14,A17,A12,FUNCT_1:def 3;
end;
assume y in rng vs;
then consider x being object such that
A18: x in dom vs and
A19: y = vs.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A18;
A20: 1<=x by A18,FINSEQ_3:25;
A21: x<=len vs by A18,FINSEQ_3:25;
per cases by A3,A21,NAT_1:8;
suppose
A22: x<=len c;
then x in dom c by A20,FINSEQ_3:25;
then
A23: c.x in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = c.x as Element of the carrier' of G by A23;
x in dom c by A20,A22,FINSEQ_3:25;
then
A24: e in rng c by FUNCT_1:def 3;
set v2 = vs/.(x+1);
set v1 = vs/.x;
c.x joins v1, v2 by A2,A20,A22;
then
A25: v1 = (the Source of G).e & v2 = (the Target of G).e or v2 = (the
Source of G).e & v1 = (the Target of G).e;
v1 = vs.x by A20,A21,FINSEQ_4:15;
hence y in G-VSet rng c by A19,A25,A24;
end;
suppose
A26: x=len c+1;
set l = len c;
A27: rng c c= the carrier' of G by FINSEQ_1:def 4;
0+1=1;
then
A28: 1<=l by A1,NAT_1:13;
then l in dom c by FINSEQ_3:25;
then c.l in rng c by FUNCT_1:def 3;
then reconsider e = c.l as Element of the carrier' of G by A27;
set v2 = vs/.(l+1);
set v1 = vs/.l;
l in dom c by A28,FINSEQ_3:25;
then
A29: e in rng c by FUNCT_1:def 3;
c.l joins v1, v2 by A2,A28;
then
A30: v1 = (the Source of G).e & v2 = (the Target of G).e or v2 = (the
Source of G).e & v1 = (the Target of G).e;
v2 = vs.(l+1) by A3,A20,A26,FINSEQ_4:15;
hence y in G-VSet rng c by A19,A26,A30,A29;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th32:
<*v*> is_vertex_seq_of {}
by FINSEQ_1:40;
theorem Th33:
ex vs st vs is_vertex_seq_of c
proof
consider p such that
A1: len p = len c + 1 and
A2: for n st 1<=n & n<=len p holds p.n in the carrier of G and
A3: for n st 1<=n & n<=len c ex v1,v2 st v1=p.n & v2=p.(n+1) & c.n joins
v1,v2 by GRAPH_1:def 14;
rng p c= the carrier of G
proof
let y be object;
assume y in rng p;
then consider x being object such that
A4: x in dom p and
A5: y = p.x by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A4;
A6: n<=len p by A4,FINSEQ_3:25;
1<=n by A4,FINSEQ_3:25;
hence thesis by A2,A5,A6;
end;
then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4;
take p;
thus len p = len c + 1 by A1;
let n be Nat;
assume that
A7: 1<=n and
A8: n<=len c;
A9: n<=len p by A1,A8,NAT_1:12;
1<=n+1 by NAT_1:12;
then
A10: p/.(n+1)=p.(n+1) by A1,A8,FINSEQ_4:15,XREAL_1:7;
ex v1,v2 st v1=p.n & v2=p.(n+1) & c.n joins v1,v2 by A3,A7,A8;
hence thesis by A7,A9,A10,FINSEQ_4:15;
end;
theorem Th34:
c <>{} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1
<> vs2 implies vs1.1<>vs2.1 & for vs st vs is_vertex_seq_of c holds vs = vs1 or
vs = vs2
proof
assume that
A1: c <>{} and
A2: vs1 is_vertex_seq_of c and
A3: vs2 is_vertex_seq_of c;
A4: len vs1 = len c +1 by A2;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs2.$1;
set TG = the Target of G;
set SG = the Source of G;
A5: Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
A6: Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
A7: len vs2 = len c +1 by A3;
assume vs1 <> vs2;
then
A8: ex j being Nat st P[j] by A4,A7,FINSEQ_2:9;
consider k be Nat such that
A9: P[k] and
A10: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A8);
A11: 1<=k by A9,FINSEQ_3:25;
per cases by A11,XXREAL_0:1;
suppose
A12: k=1;
hence vs1.1 <> vs2.1 by A9;
set v21 = vs2/.1;
set v12 = vs1/.(1+1);
set v11 = vs1/.1;
let vs;
set v1 = vs/.1;
set v2 = vs/.(1+1);
assume
A13: vs is_vertex_seq_of c;
then
A14: len vs = len c +1;
0+1=1;
then
A15: 1<=len c by A1,NAT_1:13;
then
A16: c.1 joins vs/.1, vs/.(1+1) by A13;
c.1 joins vs1/.1, vs1/.(1+1) by A2,A15;
then
A17: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A16;
A18: 1<=len vs1 by A4,NAT_1:12;
then
A19: v11=vs1.1 by FINSEQ_4:15;
A20: v21=vs2.1 by A4,A7,A18,FINSEQ_4:15;
A21: c.1 joins vs2/.1, vs2/.(1+1) by A3,A15;
thus vs = vs1 or vs = vs2
proof
per cases by A9,A12,A19,A20,A16,A21,A17;
suppose
A22: v1 = v11;
now
defpred P[Nat] means $1 in dom vs implies vs.$1=vs1.$1;
thus len vs = len vs;
thus len vs1 = len vs by A4,A13;
A23: for i being Nat st P[i] holds P[i+1]
proof
A24: 0+1=1;
let i be Nat;
assume
A25: i in dom vs implies vs.i=vs1.i;
assume
A26: i+1 in dom vs;
reconsider i as Element of NAT by ORDINAL1:def 12;
A27: 1<=i+1 by A26,FINSEQ_3:25;
A28: i+1<=len vs by A26,FINSEQ_3:25;
per cases by A24,NAT_1:13;
suppose
i=0;
hence thesis by A4,A14,A18,A19,A22,FINSEQ_4:15;
end;
suppose
A29: 1<=i;
set v12 = vs1/.(i+1);
set v11 = vs1/.i;
set v2 = vs/.(i+1);
A30: v2=vs.(i+1) by A27,A28,FINSEQ_4:15;
set v1 = vs/.i;
A31: i<=len c by A14,A28,XREAL_1:6;
then
A32: c.i joins vs1/.i, vs1/.(i+1) by A2,A29;
A33: i<=len vs by A14,A31,NAT_1:12;
then
A34: v1 =vs.i by A29,FINSEQ_4:15;
c.i joins vs/.i, vs/.(i+1) by A13,A29,A31;
then
A35: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A32;
v11=vs1.i by A4,A14,A29,A33,FINSEQ_4:15;
hence thesis by A4,A14,A25,A27,A28,A29,A33,A34,A30,A35,
FINSEQ_3:25,FINSEQ_4:15;
end;
end;
A36: P[0] by FINSEQ_3:25;
thus for i being Nat holds P[i] from NAT_1:sch 2(A36, A23);
end;
hence thesis by FINSEQ_2:9;
end;
suppose
A37: v1 = v21;
now
defpred P[Nat] means $1 in dom vs implies vs.$1=vs2.$1;
thus len vs = len vs;
thus len vs2 = len vs by A7,A13;
A38: for i being Nat st P[i] holds P[i+1]
proof
A39: 0+1=1;
let i be Nat;
assume
A40: i in dom vs implies vs.i=vs2.i;
assume
A41: i+1 in dom vs;
then
A42: 1<=i+1 by FINSEQ_3:25;
A43: i+1<=len vs by A41,FINSEQ_3:25;
reconsider i as Element of NAT by ORDINAL1:def 12;
per cases by A39,NAT_1:13;
suppose
i=0;
hence thesis by A4,A14,A18,A20,A37,FINSEQ_4:15;
end;
suppose
A44: 1<=i;
set v12 = vs2/.(i+1);
set v11 = vs2/.i;
set v2 = vs/.(i+1);
A45: v2=vs.(i+1) by A42,A43,FINSEQ_4:15;
set v1 = vs/.i;
A46: i<=len c by A14,A43,XREAL_1:6;
then
A47: c.i joins vs2/.i, vs2/.(i+1) by A3,A44;
A48: i<=len vs by A14,A46,NAT_1:12;
then
A49: v1 =vs.i by A44,FINSEQ_4:15;
c.i joins vs/.i, vs/.(i+1) by A13,A44,A46;
then
A50: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A47;
v11=vs2.i by A7,A14,A44,A48,FINSEQ_4:15;
hence thesis by A7,A14,A40,A42,A43,A44,A48,A49,A45,A50,
FINSEQ_3:25,FINSEQ_4:15;
end;
end;
A51: P[0] by FINSEQ_3:25;
thus for i being Nat holds P[i] from NAT_1:sch 2(A51, A38);
end;
hence thesis by FINSEQ_2:9;
end;
end;
end;
suppose
1=1 & card (G-VSet rng c) = 2 &
for n st n in dom c holds (the Source of G).(c.n) <> (the Target of G).(c
.n);
end;
theorem Th35:
c alternates_vertices_in G & vs is_vertex_seq_of c implies for k
st k in dom c holds vs.k <> vs.(k+1)
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
set TG = (the Target of G);
set SG = (the Source of G);
let k;
set px = vs/.k;
set px1 = vs/.(k+1);
assume
A3: k in dom c;
then
A4: k<=len c by FINSEQ_3:25;
A5: 1<=k by A3,FINSEQ_3:25;
then c.k joins px, px1 by A2,A4;
then
A6: TG.(c.k)=px1 & SG.(c.k)=px or TG.(c.k)=px & SG.(c.k)=px1;
A7: len vs = len c +1 by A2;
then k<=len vs by A4,NAT_1:12;
then
A8: px = vs.k by A5,FINSEQ_4:15;
1<=k+1 by NAT_1:12;
then px1 = vs.(k+1) by A4,A7,FINSEQ_4:15,XREAL_1:7;
hence thesis by A1,A3,A8,A6;
end;
theorem Th36:
c alternates_vertices_in G & vs is_vertex_seq_of c implies rng
vs = {(the Source of G).(c.1), (the Target of G).(c.1)}
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
set px1 = vs/.(1+1);
set TG = (the Target of G);
set SG = (the Source of G);
set px = vs/.1;
A3: len vs = len c +1 by A2;
then
A4: 1<=len vs by NAT_1:12;
then
A5: px = vs.1 by FINSEQ_4:15;
c <>{} by A1;
then card rng vs = 2 by A1,A2,Th31;
then consider x, y being object such that
x<>y and
A6: rng vs={x,y} by CARD_2:60;
1 in dom vs by A4,FINSEQ_3:25;
then vs.1 in rng vs by FUNCT_1:def 3;
then
A7: vs.1 = x or vs.1 = y by A6,TARSKI:def 2;
A8: 1<=len c by A1;
then
A9: 1 in dom c by FINSEQ_3:25;
A10: px1 = vs.(1+1) by A8,A3,FINSEQ_4:15,XREAL_1:7;
c.1 joins px, px1 by A2,A8;
then
A11: TG.(c.1)=px1 & SG.(c.1)=px or TG.(c.1)=px & SG.(c.1)=px1;
1+1 in dom vs by FINSEQ_3:25,A8,A3,XREAL_1:7;
then vs.(1+1) in rng vs by FUNCT_1:def 3;
then vs.(1+1) = x or vs.(1+1) = y by A6,TARSKI:def 2;
hence thesis by A1,A6,A5,A10,A11,A7,A9;
end;
theorem Th37:
c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is
TwoValued Alternating FinSequence
proof
assume that
A1: c alternates_vertices_in G and
A2: vs is_vertex_seq_of c;
A3: c <>{} by A1;
A4: len vs = len c + 1 by A2;
A5: now
let k be Nat;
assume that
A6: 1<=k and
A7: (k+1)<=len vs;
k<=len c by A4,A7,XREAL_1:6;
hence vs.k <> vs.(k+1) by A1,A2,Th35,A6,FINSEQ_3:25;
end;
card rng vs = 2 by A2,A3,Th31,A1;
hence thesis by A5,FINSEQ_6:def 6,FINSEQ_6:def 7;
end;
theorem Th38:
c alternates_vertices_in G implies ex vs1,vs2 st vs1<>vs2 & vs1
is_vertex_seq_of c & vs2 is_vertex_seq_of c & for vs st vs is_vertex_seq_of c
holds vs=vs1 or vs=vs2
proof
set X = (the Source of G).(c.1);
set Y = (the Target of G).(c.1);
consider p1 being FinSequence of the carrier of G such that
A1: p1 is_vertex_seq_of c by Th33;
assume
A2: c alternates_vertices_in G;
then
A3: 1<=len c;
then
A4: 1 in dom c by FINSEQ_3:25;
A5: 1+1=2;
then
A6: p1.1 <> p1.2 by A2,A1,A4,Th35;
A7: rng p1 = {X, Y} by A2,A1,Th36;
A8: len p1 = len c + 1 by A1;
then
A9: len p1 > 1 by A3,NAT_1:13;
then consider p2 being TwoValued Alternating FinSequence such that
A10: rng p2 = {p1.2, p1.1} and
A11: len p2 = len p1 and
A12: p2.1=p1.2 by A6,FINSEQ_6:149;
A13: dom p1 = dom p2 by A11,FINSEQ_3:29;
1+1<=len p1 by A9,NAT_1:13;
then 2 in dom p1 by FINSEQ_3:25;
then p1.2 in rng p1 by FUNCT_1:def 3;
then
A14: p1.2 = X or p1.2 = Y by A7,TARSKI:def 2;
1 in dom p1 by A9,FINSEQ_3:25;
then p1.1 in rng p1 by FUNCT_1:def 3;
then
A15: p1.1 = X or p1.1 = Y by A7,TARSKI:def 2;
then reconsider p2 as FinSequence of the carrier of G by A2,A1,A7,A4,A5,A10
,A14,Th35,FINSEQ_1:def 4;
take p1, p2;
thus p1<>p2 by A2,A1,A4,A5,A12,Th35;
thus p1 is_vertex_seq_of c by A1;
A16: p1 is TwoValued Alternating FinSequence by A2,A1,Th37;
now
thus len p2 = len c + 1 by A1,A11;
let n be Nat such that
A17: 1<=n and
A18: n<=len c;
A19: n<=len p1 by A8,A18,NAT_1:12;
then
A20: p2/.n = p2.n by A11,A17,FINSEQ_4:15;
A21: n in dom p1 by A17,A19,FINSEQ_3:25;
then p2.n in {X, Y} by A2,A1,A4,A5,A10,A13,A15,A14,Th35,FUNCT_1:def 3;
then
A22: p2.n=X or p2.n=Y by TARSKI:def 2;
set x = p1/.n;
set y = p1/.(n+1);
A23: c.n joins x, y by A1,A17,A18;
A24: n+1<=len p1 by A8,A18,XREAL_1:6;
then
A25: p2/.(n+1) = p2.(n+1) by A11,FINSEQ_4:15,NAT_1:12;
A26: 1<=n+1 by NAT_1:12;
then
A27: n+1 in dom p1 by A24,FINSEQ_3:25;
then p2.(n+1) in {X, Y} by A2,A1,A4,A5,A10,A13,A15,A14,Th35,FUNCT_1:def 3;
then
A28: p2.(n+1)=X or p2.(n+1)=Y by TARSKI:def 2;
p1.n in {X, Y} by A7,A21,FUNCT_1:def 3;
then p1.n=X or p1.n=Y by TARSKI:def 2;
then
A29: x = p2.(n+1) by A7,A16,A6,A10,A11,A12,A15,A14,A17,A19,A24,A22,A28,
FINSEQ_6:def 7,FINSEQ_6:147,FINSEQ_4:15;
p1.(n+1) in {X, Y} by A7,A27,FUNCT_1:def 3;
then p1.(n+1)=X or p1.(n+1)=Y by TARSKI:def 2;
then y = p2.n by A7,A16,A6,A10,A11,A12,A15,A14,A17,A26,A24,
A22,A28,FINSEQ_6:def 7,FINSEQ_6:147,FINSEQ_4:15;
hence c.n joins p2/.n,p2/.(n+1) by A23,A29,A20,A25;
end;
hence p2 is_vertex_seq_of c;
let p be FinSequence of the carrier of G;
assume
A30: p is_vertex_seq_of c;
then reconsider p9 = p as TwoValued Alternating FinSequence by A2,Th37;
A31: len p = len c + 1 by A30;
rng p = {X, Y} by A2,A30,Th36;
then p9=p1 or p9=p2 by A8,A7,A16,A6,A10,A11,A12,A15,A14,A31,FINSEQ_6:148;
hence thesis;
end;
Lm7: (for x, y st x in D & y in D holds x=y) implies card D = 1
proof
set x = the Element of D;
assume for x, y st x in D & y in D holds x=y;
then for y be object holds y in D iff y=x;
then D = {x} by TARSKI:def 1;
hence thesis by CARD_2:42;
end;
theorem Th39:
vs is_vertex_seq_of c implies (card the carrier of G = 1 or c <>
{} & not c alternates_vertices_in G iff for vs1 st vs1 is_vertex_seq_of c holds
vs1 = vs)
proof
assume
A1: vs is_vertex_seq_of c;
hereby
assume
A2: card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
per cases by A2;
suppose
A3: card the carrier of G = 1;
then reconsider tVG = the carrier of G as finite set;
consider X being object such that
A4: tVG = {X} by A3,CARD_2:42;
A5: rng vs c= {X} by A4,FINSEQ_1:def 4;
A6: len vs = len c +1 by A1;
let vs1;
A7: Seg len vs = dom vs by FINSEQ_1:def 3;
assume vs1 is_vertex_seq_of c;
then
A8: len vs1 = len c +1;
assume vs1 <> vs;
then consider j being Nat such that
A9: j in dom vs and
A10: vs1.j <> vs.j by A8,A6,FINSEQ_2:9;
vs.j in rng vs by A9,FUNCT_1:def 3;
then
A11: vs.j = X by A5,TARSKI:def 1;
A12: rng vs1 c= {X} by A4,FINSEQ_1:def 4;
Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
then vs1.j in rng vs1 by A8,A6,A7,A9,FUNCT_1:def 3;
hence contradiction by A10,A12,A11,TARSKI:def 1;
end;
suppose
A13: c <>{} & not c alternates_vertices_in G;
thus for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs
proof
set TG = the Target of G;
set SG = the Source of G;
let vs1;
defpred P[Nat] means $1 in dom vs1 & vs1.$1<>vs.$1;
assume
A14: vs1 is_vertex_seq_of c;
then
A15: len vs1 = len c +1;
A16: len vs = len c +1 by A1;
then
A17: dom vs1 = dom vs by A15,FINSEQ_3:29;
assume vs1 <> vs;
then
A18: ex i being Nat st P[i] by A15,A16,FINSEQ_2:9;
consider k be Nat such that
A19: P[k] and
A20: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A18);
A21: 0+1=1 & k=0 or 0+1<=k by NAT_1:13;
per cases by A21,XXREAL_0:1;
suppose
k=0;
hence contradiction by A19,FINSEQ_3:25;
end;
suppose
A22: k=1;
thus contradiction
proof
A23: 0+1=1;
per cases by A23,NAT_1:13;
suppose
len c = 0;
hence contradiction by A13;
end;
suppose
A24: 1<=len c;
defpred P[Nat] means
$1 in dom c implies vs1/.$1<>vs
/.$1 & vs1/.($1+1)<>vs/.($1+1) & (TG.(c.$1)=TG.(c.1) & SG.(c.$1)=SG.(c.1) or TG
.(c.$1)=SG.(c.1) & SG.(c.$1)=TG.(c.1));
A25: vs/.k=vs.k by A17,A19,PARTFUN1:def 6;
A26: vs1/.k=vs1.k by A19,PARTFUN1:def 6;
A27: now
let n be Nat;
assume
A28: P[n];
thus P[n+1]
proof
assume
A29: (n+1) in dom c;
then
A30: 1<=n+1 by FINSEQ_3:25;
A31: n+1<=len c by A29,FINSEQ_3:25;
thus vs1/.(n+1)<>vs/.(n+1) & vs1/.(n+1+1)<>vs/.(n+1+1) & (TG
.(c.(n+1))=TG.(c.1) & SG.(c.(n+1))=SG.(c.1) or TG.(c.(n+1))=SG.(c.1) & SG.(c.(n
+1))=TG.(c.1))
proof
per cases;
suppose
A32: n=0;
hence vs1/.(n+1)<>vs/.(n+1) by A17,A19,A22,A26,
PARTFUN1:def 6;
A33: 1<=len c by A30,A31,XXREAL_0:2;
then c.1 joins vs/.1,vs/.(1+1) by A1;
then
A34: SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(1+1) or SG.(c.1)=vs
/.(1+1) & TG.(c.1)= vs/.1;
c.1 joins vs1/.1,vs1/.(1+1) by A14,A33;
hence vs1/.(n+1+1)<>vs/.(n+1+1) by A17,A19,A22,A26,A32
,A34,PARTFUN1:def 6;
thus thesis by A32;
end;
suppose
A35: 0 vs/.(n+1) by A28,A36,FINSEQ_3:25;
c.n joins vs1/.n, vs1/.(n+1) by A14,A37,A36;
then
A38: SG.(c.n)=vs1/.n & TG.(c.n)= vs1/.(n+1) or SG.(c.n)=
vs1/.(n+1) & TG.(c. n)=vs1/.n;
c.(n+1) joins vs/.(n+1), vs/.(n+1+1) by A1,A30,A31;
then
A39: SG.(c.(n+1))=vs/.(n+1) & TG.(c.(n+1))=vs/.(n+1+1)
or SG.(c.(n+1))=vs/. (n+1+1) & TG.(c.(n+1))=vs/.(n+1);
A40: c.(n+1) joins vs1/.(n+1), vs1/.(n+1+1) by A14,A30,A31;
hence vs1/.(n+1+1)<>vs/.(n+1+1) by A28,A37,A36,A39,
FINSEQ_3:25;
c.n joins vs/.n, vs/.(n+1) by A1,A37,A36;
hence thesis by A28,A37,A36,A38,A40,A39,FINSEQ_3:25;
end;
end;
end;
end;
A41: P[0] by FINSEQ_3:25;
A42: for n being Nat holds P[n] from NAT_1:sch 2(A41,A27);
now
let x be object;
hereby
assume x in G-VSet rng c;
then consider v such that
A43: x=v and
A44: ex e being Element of the carrier' of G st e in rng
c & (v = (the Source of G).e or v = (the Target of G).e);
consider e such that
A45: e in rng c and
A46: v = SG.e or v = TG.e by A44;
consider d being object such that
A47: d in dom c and
A48: e=c.d by A45,FUNCT_1:def 3;
reconsider d as Element of NAT by A47;
TG.(c.d)=TG.(c.1) & SG.(c.d)=SG.(c.1) or TG.(c.d)=SG.(c
.1) & SG.(c.d)=TG.(c.1) by A42,A47;
hence x in {SG.(c.1), TG.(c.1)} by A43,A46,A48,TARSKI:def 2;
end;
0+1<=len c by A13,NAT_1:13;
then
A49: 1 in dom c by FINSEQ_3:25;
then
A50: c.1 in rng c by FUNCT_1:def 3;
A51: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e=c.1 as Element of the carrier' of G by A50;
reconsider t = TG.e as Element of G by A50,A51,FUNCT_2:5;
reconsider s = SG.e as Element of G by A50,A51,FUNCT_2:5;
assume x in {SG.(c.1), TG.(c.1)};
then
A52: x=s or x =t by TARSKI:def 2;
e in rng c by A49,FUNCT_1:def 3;
hence x in G-VSet rng c by A52;
end;
then
A53: G-VSet rng c = {SG.(c.1), TG.(c.1)} by TARSKI:2;
c.k joins vs1/.k, vs1/.(k+1) by A14,A22,A24;
then
A54: SG.(c.1)=vs1/.1 & TG.(c.1)=vs1/.(k+1) or SG.(c.1)=vs1/.(k+1
) & TG.(c.1 )=vs1/.1 by A22;
A55: c.k joins vs/.k, vs/.(k+1) by A1,A22,A24;
A56: now
let n;
n in dom c implies TG.(c.n)=TG.(c.1) & SG.(c.n)=SG.(c.1)
or TG.(c.n)=SG.(c.1) & SG.(c.n)=TG.(c.1) by A42;
hence n in dom c implies SG.(c.n) <> TG.(c.n) by A19,A22,A26
,A25,A55,A54;
end;
SG.(c.1)=vs/.1 & TG.(c.1)=vs/.(k+1) or SG.(c.1)=vs/.(k+1) &
TG.(c.1)= vs/.1 by A22,A55;
then card (G-VSet rng c) = 2 by A19,A22,A26,A25,A54,A53,CARD_2:57
;
hence contradiction by A13,A24,A56;
end;
end;
end;
suppose
1 1;
then consider x, y such that
A70: x in the carrier of G and
A71: y in the carrier of G and
A72: x<>y by Lm7;
reconsider y as Element of G by A71;
reconsider x as Element of G by A70;
assume
A73: c ={} or c alternates_vertices_in G;
thus contradiction
proof
per cases by A73;
suppose
A74: c ={};
then <*x*> = vs by A69,Th32;
then
A75: vs.1 = x by FINSEQ_1:40;
<*y*> = vs by A69,A74,Th32;
hence contradiction by A72,A75,FINSEQ_1:40;
end;
suppose
c alternates_vertices_in G;
then consider vs1,vs2 such that
A76: vs1<>vs2 and
A77: vs1 is_vertex_seq_of c and
A78: vs2 is_vertex_seq_of c and
for vs st vs is_vertex_seq_of c holds vs=vs1 or vs=vs2 by Th38;
vs1 = vs by A69,A77;
hence contradiction by A69,A76,A78;
end;
end;
end;
definition
let G, c;
assume
A1: card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
func vertex-seq c -> FinSequence of the carrier of G means
it is_vertex_seq_of c;
existence by Th33;
uniqueness by A1,Th39;
end;
theorem Th40:
vs is_vertex_seq_of c & c1 = c|Seg n & vs1= vs|Seg (n+1) implies
vs1 is_vertex_seq_of c1
proof
assume
A1: vs is_vertex_seq_of c;
then
A2: len vs = len c + 1;
assume that
A3: c1 = c|Seg n and
A4: vs1= vs|Seg (n+1);
now
per cases;
suppose
A5: n<=len c;
then
A6: n+1<=len vs by A2,XREAL_1:6;
then
A7: len vs1 = n+1 by A4,FINSEQ_1:17;
A8: len c1 = n by A3,A5,FINSEQ_1:17;
hence len vs1 = len c1 + 1 by A4,A6,FINSEQ_1:17;
let k be Nat;
assume that
A9: 1<=k and
A10: k<=len c1;
A11: 1<=k+1 by NAT_1:12;
then
A12: vs1/.(k+1)=vs1.(k+1) by A8,A7,A10,FINSEQ_4:15,XREAL_1:7;
k+1<=len c1 +1 by A10,XREAL_1:7;
then k+1 in Seg (n+1) by A8,A11;
then
A13: vs1.(k+1)=vs.(k+1) by A4,FUNCT_1:49;
A14: k<=len c by A5,A8,A10,XXREAL_0:2;
then k<=len vs by A2,NAT_1:12;
then
A15: vs/.k=vs.k by A9,FINSEQ_4:15;
A16: k<=n+1 by A8,A10,NAT_1:12;
then
A17: vs1/.k=vs1.k by A7,A9,FINSEQ_4:15;
k in Seg n by A8,A9,A10;
then
A18: c1.k = c.k by A3,FUNCT_1:49;
k in Seg (n+1) by A9,A16;
then
A19: vs1.k=vs.k by A4,FUNCT_1:49;
vs/.(k+1)=vs.(k+1) by A2,A14,A11,FINSEQ_4:15,XREAL_1:7;
hence c1.k joins vs1/.k,vs1/.(k+1) by A1,A9,A14,A18,A19,A13,A15,A17,A12;
end;
suppose
A20: len c <=n;
then len vs<=n+1 by A2,XREAL_1:6;
then
A21: vs1 = vs by A4,FINSEQ_2:20;
c1 = c by A3,A20,FINSEQ_2:20;
hence len vs1 = len c1 + 1 & for k being Nat st 1<=k & k<=len
c1 holds c1.k joins vs1/.k,vs1/.(k+1) by A1,A21;
end;
end;
hence thesis;
end;
theorem Th41:
1<=m & m<=n & n<=len c & q = (m,n)-cut c implies q is Chain of G
proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
A4: m<=n+1 by A2,NAT_1:12;
consider vs such that
A5: vs is_vertex_seq_of c by Th33;
set p9 = (m,n+1)-cut vs;
A6: now
let k be Nat;
assume that
A7: 1<=k and
A8: k<=len p9;
k in dom p9 by A7,A8,FINSEQ_3:25;
then
A9: p9.k in rng p9 by FUNCT_1:def 3;
A10: rng vs c= the carrier of G by FINSEQ_1:def 4;
rng p9 c= rng vs by FINSEQ_6:137;
hence p9.k in the carrier of G by A10,A9;
end;
assume
A11: q = (m,n)-cut c;
then
A12: len q +m-m=n+1-m by A1,A3,A4,Lm2;
A13: len vs = len c + 1 by A5;
then
A14: n+1<=len vs by A3,XREAL_1:6;
then
A15: len p9+m-m=(n+1)+1-m by A1,A4,FINSEQ_6:def 4;
then
A16: len p9 = n-m+1+1;
A17: now
1-1<=m-1 by A1,XREAL_1:9;
then m-1 = m-'1 by XREAL_0:def 2;
then reconsider m1= m-1 as Element of NAT;
let k be Nat;
reconsider i = m1+k as Nat;
assume that
A18: 1<=k and
A19: k<=len q;
0+1<=k by A18;
then consider j such that
0<=j and
A20: j {};
then
A5: len p +1 = len vs1 +len vs2 by FINSEQ_6:139;
A6: now
let n be Nat such that
A7: 1<=n and
A8: n<=len p;
per cases;
suppose
A9: n<=len vs1;
then
A10: n in dom vs1 by A7,FINSEQ_3:25;
p.n = vs1.n by A7,A9,FINSEQ_6:140;
hence p.n in the carrier of G by A10,FINSEQ_2:11;
end;
suppose
A11: n > len vs1;
then consider m being Nat such that
A12: n = len vs1 + m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
m <> 0 by A11,A12;
then
A13: 0+1<=m by NAT_1:13;
len vs1 + m<=len vs1 + (len vs2 - 1) by A5,A8,A12;
then m<=len vs2 - 1 by XREAL_1:6;
then
A14: m+1<=len vs2 - 1+1 by XREAL_1:6;
1<=m+1 by NAT_1:12;
then
A15: m+1 in dom vs2 by A14,FINSEQ_3:25;
m {};
then len p +1 = len vs1 +len vs2 by FINSEQ_6:139;
then
A8: len p = len c1 + len c2 + 1 by A6,A7
.= len q + 1 by FINSEQ_1:22;
reconsider p as FinSequence of the carrier of G;
now
let n be Nat;
assume that
A9: 1<=n and
A10: n<=len q;
A11: n in dom q by A9,A10,FINSEQ_3:25;
n<=len p by A8,A10,NAT_1:12;
then
A12: p/.n=p.n by A9,FINSEQ_4:15;
1<=n+1 by NAT_1:12;
then
A13: p/.(n+1)=p.(n+1) by A8,A10,FINSEQ_4:15,XREAL_1:7;
per cases by A11,FINSEQ_1:25;
suppose
A14: n in dom c1;
set v2=vs1/.(n+1);
set v1=vs1/.n;
A15: 1<=n by A14,FINSEQ_3:25;
A16: n<=len c1 by A14,FINSEQ_3:25;
then
A17: n+1<=len vs1 by A1,XREAL_1:6;
then
A18: vs1/.(n+1)=vs1.(n+1) by FINSEQ_4:15,NAT_1:12;
A19: n<=len vs1 by A6,A16,NAT_1:12;
then
A20: vs1/.n=vs1.n by A15,FINSEQ_4:15;
A21: p.(n+1) = vs1.(n+1) by A17,FINSEQ_6:140,NAT_1:12;
A22: p.n = vs1.n by A15,A19,FINSEQ_6:140;
c1.n joins v1, v2 by A1,A15,A16;
hence q.n joins p/.n, p/.(n+1) by A12,A13,A14,A20,A18,A22,A21,
FINSEQ_1:def 7;
end;
suppose
ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Element of NAT such that
A23: k in dom c2 and
A24: n = len c1 + k;
A25: 0+1<=k by A23,FINSEQ_3:25;
set v2 = vs2/.(k+1);
set v1 = vs2/.k;
A26: k<=len c2 by A23,FINSEQ_3:25;
then
A27: k is_vertex_seq_of {}
by FINSEQ_1:39;
definition
let G;
let IT be Chain of G;
attr IT is simple means
:Def9:
ex vs st vs is_vertex_seq_of IT & for n,m st
1<=n & n as FinSequence of the carrier of G;
take p;
thus p is_vertex_seq_of q by Lm8;
let n,m;
assume that
A1: 1<=n and
A2: nvs2.$1;
set TG = the Target of G;
set SG = the Source of G;
A5: Seg len vs1 = dom vs1 by FINSEQ_1:def 3;
A6: Seg len vs2 = dom vs2 by FINSEQ_1:def 3;
A7: len vs2 = len sc +1 by A3;
assume
A8: vs1 <> vs2;
then
A9: ex j being Nat st P[j] by A4,A7,FINSEQ_2:9;
consider k be Nat such that
A10: P[k] and
A11: for n be Nat st P[n] holds k<=n from NAT_1:sch 5 (A9);
A12: 1<=k by A10,FINSEQ_3:25;
per cases by A12,XXREAL_0:1;
suppose
A13: k=1;
set v23=vs2/.(1+1+1);
set v22=vs2/.(1+1);
set v21=vs2/.1;
set v13=vs1/.(1+1+1);
set v12=vs1/.(1+1);
set v11=vs1/.1;
A14: 1+1+1<=len vs1 by A1,A4,XREAL_1:6;
then
A15: v13=vs1.(1+1+1) by FINSEQ_4:15;
A16: 1<=len vs1 by A14,XXREAL_0:2;
then
A17: v11=vs1.1 by FINSEQ_4:15;
A18: 1<=len sc by A1,XXREAL_0:2;
then
A19: sc.1 joins v21,v22 by A3;
sc.1 joins v11,v12 by A2,A18;
then
A20: v11=v21 & v12=v22 or v11=v22 & v12=v21 by A19;
A21: v21=vs2.1 by A4,A7,A16,FINSEQ_4:15;
consider vs such that
A22: vs is_vertex_seq_of sc and
A23: for n,m st 1<=n & n{} by A1;
then
A24: vs = vs1 or vs = vs2 by A2,A3,A8,A22,Th34;
A25: v23=vs2.(1+1+1) by A4,A7,A14,FINSEQ_4:15;
A26: sc.2 joins v22,v23 by A1,A3;
A27: sc.2 joins v12,v13 by A1,A2;
then
A28: v21=v23 by A10,A13,A17,A21,A26,A20;
v11=v13 by A10,A13,A17,A21,A27,A26,A20;
then 1+1+1 = len vs by A4,A7,A14,A17,A15,A21,A25,A28,A23,A24;
hence contradiction by A1,A4,A7,A24;
end;
suppose
1.
:: ^ |
:: | v
:: .--->.<---.--->.
:: | ^
:: v |
:: .--->.
:: is a case in point:
theorem Th48:
not c is simple Chain of G & vs is_vertex_seq_of c implies ex fc
being Subset of c, fvs being Subset of vs, c1, vs1 st len c1 < len c & vs1
is_vertex_seq_of c1 & len vs1 < len vs & vs.1 = vs1.1 & vs.len vs = vs1.len vs1
& Seq fc = c1 & Seq fvs = vs1
proof
assume that
A1: not c is simple Chain of G and
A2: vs is_vertex_seq_of c;
consider n, m being Nat such that
A3: 1<=n and
A4: n1 or m<>len vs by A1,A2,Def9;
A8: m-n>n-n by A4,XREAL_1:9;
A9: len vs = len c + 1 by A2;
reconsider n1 = n-'1 as Element of NAT;
A10: 1-1<=n-1 by A3,XREAL_1:9;
then
A11: n-1 = n-'1 by XREAL_0:def 2;
then
A12: n1+1 = n;
per cases by A7;
suppose
A13: n<>1 & m <> len vs;
set DR = {kk where kk is Nat: m<=kk & kk<= len c};
set DL = {kk where kk is Nat: 1<=kk & kk<=n1};
set domfvs = {k where k is Nat: 1<=k & k<=n or m+1<=k & k<= len vs};
reconsider p2 = (m,len c+1)-cut vs as FinSequence of the carrier of G;
reconsider pp = (1,n)-cut vs as FinSequence of the carrier of G;
set p29 = (m+1, len c +1)-cut vs;
A14: 1<=m+1 by NAT_1:12;
A15: 1<=m by A3,A4,XXREAL_0:2;
then 1-1<=m-1 by XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A16: m < len vs by A5,A13,XXREAL_0:1;
then
A17: m<=len c by A9,NAT_1:13;
then reconsider c2 = (m,len c)-cut c as Chain of G by A15,Th41;
A18: len c2 +m = len c +1 by A15,A17,FINSEQ_6:def 4;
deffunc F(object) = c.$1;
set domfc = {k where k is Nat: 1<=k & k<=n1 or m<=k & k<= len c};
consider fc being Function such that
A19: dom fc = domfc and
A20: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
n < len vs by A4,A5,XXREAL_0:2;
then
A21: n-1 < len c +1-1 by A9,XREAL_1:9;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A22: x = kk and
A23: 1<=kk & kk<=n1 or m<=kk & kk<= len c;
A24: 1<=kk by A15,A23,XXREAL_0:2;
kk<=len c by A11,A21,A23,XXREAL_0:2;
hence thesis by A22,A24;
end;
then reconsider fc as FinSubsequence by A19,FINSEQ_1:def 12;
A25: fc c= c
proof
let p be object;
assume
A26: p in fc;
then consider x, y being object such that
A27: [x,y] = p by RELAT_1:def 1;
A28: x in dom fc by A26,A27,FUNCT_1:1;
then consider kk being Nat such that
A29: x = kk and
A30: 1<=kk & kk<=n1 or m<=kk & kk<= len c by A19;
A31: 1<=kk by A15,A30,XXREAL_0:2;
kk<=len c by A11,A21,A30,XXREAL_0:2;
then
A32: x in dom c by A29,A31,FINSEQ_3:25;
y = fc.x by A26,A27,FUNCT_1:1;
then y = c.kk by A19,A20,A28,A29;
hence thesis by A27,A29,A32,FUNCT_1:1;
end;
1 < n by A3,A13,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A33: 1+1-1<=n-1 by XREAL_1:9;
then reconsider c1 = (1,n1)-cut c as Chain of G by A11,A21,Th41;
reconsider fc as Subset of c by A25;
take fc;
A34: pp is_vertex_seq_of c1 by A2,A12,A33,A21,Th42;
then
A35: len pp = len c1 + 1;
now
let x be object;
hereby
assume x in domfc;
then ex k being Nat st x=k &( 1<=k & k<=n1 or m<=k & k<=
len c);
then x in DL or x in DR;
hence x in DL \/ DR by XBOOLE_0:def 3;
end;
assume
A36: x in DL \/ DR;
per cases by A36,XBOOLE_0:def 3;
suppose
x in DL;
then ex k being Nat st x=k & 1<=k & k<=n1;
hence x in domfc;
end;
suppose
x in DR;
then ex k being Nat st x=k & m<=k & k<=len c;
hence x in domfc;
end;
end;
then
A37: domfc = DL \/ DR by TARSKI:2;
A38: DL c= Seg len c & DR c= Seg len c
proof
hereby
let x be object;
assume x in DL;
then consider k being Nat such that
A39: x=k and
A40: 1<=k and
A41: k<=n1;
k<=len c by A11,A21,A41,XXREAL_0:2;
hence x in Seg len c by A39,A40;
end;
let x be object;
assume x in DR;
then consider k being Nat such that
A42: x=k and
A43: m<=k and
A44: k<=len c;
1<=k by A15,A43,XXREAL_0:2;
hence thesis by A42,A44;
end;
then reconsider DR as finite set;
rng Sgm DR = DR by A38,FINSEQ_1:def 13;
then
A45: rng Sgm DR c= dom fc by A19,A37,XBOOLE_1:7;
reconsider DL as finite set by A38;
set SL = Sgm DL;
A46: 1<=m by A3,A4,XXREAL_0:2;
set SR = Sgm DR;
A47: len Sgm DR = card DR by A38,FINSEQ_3:39;
A48: m<=len c by A9,A16,NAT_1:13;
then
A49: m-m<=len c -m by XREAL_1:9;
then len c2 -'1 = len c2 -1 by A18,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
-(-(m-n)) = m-n;
then
A50: -(m-n) < 0 by A8;
A51: m = m1 +1;
then m1<=m by NAT_1:12;
then
A52: p2 = (m1+1, m)-cut vs ^ (m+1, len c +1)-cut vs by A5,A9,FINSEQ_6:134;
A53: p2 is_vertex_seq_of c2 by A2,A15,A17,Th42;
then
A54: len p2 = len c2 + 1;
then 1<=len p2 by NAT_1:12;
then 1-1<=len p2 -1 by XREAL_1:9;
then len p2 -'1 = len p2 -1 by XREAL_0:def 2;
then reconsider lp21 = len p2 -1 as Element of NAT;
0+1=1;
then
A55: 1<=len p2 by A54,NAT_1:13;
m-m<=len c -m by A48,XREAL_1:9;
then 0+1<=len c -m+1 by XREAL_1:6;
then
A56: 1 by A55,FINSEQ_6:132
.= <*vs.(m+0)*> by A9,A15,A54,A147,Lm2
.= (m,m)-cut vs by A5,A15,FINSEQ_6:132;
then
A209: p1 = pp^p29 by A135,A52,FINSEQ_1:33;
rng Sgm DL = DL by A136,FINSEQ_1:def 13;
then rng Sgm DL c= dom fvs by A88,A144,XBOOLE_1:7;
hence thesis by A88,A209,A144,A208,A145,A175,A202,FINSEQ_6:150;
end;
suppose
A210: n=1 & m <> len vs;
set domfvs = {k where k is Nat: m<=k & k<= len vs};
deffunc F(object) = c.$1;
set domfc = {k where k is Nat: m<=k & k<= len c};
set p2 = (m,len c+1)-cut vs;
consider fc being Function such that
A211: dom fc = domfc and
A212: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
A213: 1 < m by A3,A4,XXREAL_0:2;
then 1-1 < m-1 by XREAL_1:9;
then 0 < -(-(m-1));
then
A214: -(m-1) < 0;
1-1<=m-1 by A213,XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A215: m = m1 +1;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A216: x = kk and
A217: m<=kk and
A218: kk<= len c;
1<=kk by A213,A217,XXREAL_0:2;
hence thesis by A216,A218;
end;
then reconsider fc as FinSubsequence by A211,FINSEQ_1:def 12;
fc c= c
proof
let p be object;
assume
A219: p in fc;
then consider x, y being object such that
A220: [x,y] = p by RELAT_1:def 1;
A221: x in dom fc by A219,A220,FUNCT_1:1;
then consider kk being Nat such that
A222: x = kk and
A223: m<=kk and
A224: kk<= len c by A211;
1<=kk by A213,A223,XXREAL_0:2;
then
A225: x in dom c by A222,A224,FINSEQ_3:25;
y = fc.x by A219,A220,FUNCT_1:1;
then y = c.kk by A211,A212,A221,A222;
hence thesis by A220,A222,A225,FUNCT_1:1;
end;
then reconsider fc as Subset of c;
take fc;
deffunc F(object) = vs.$1;
consider fvs being Function such that
A226: dom fvs = domfvs and
A227: for x being object st x in domfvs holds fvs.x = F(x) from FUNCT_1:sch 3;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider kk being Nat such that
A228: x = kk and
A229: m<=kk and
A230: kk<= len vs;
1<=kk by A213,A229,XXREAL_0:2;
hence thesis by A228,A230;
end;
then reconsider fvs as FinSubsequence by A226,FINSEQ_1:def 12;
A231: fvs c= vs
proof
let p be object;
assume
A232: p in fvs;
then consider x, y being object such that
A233: [x,y] = p by RELAT_1:def 1;
A234: x in dom fvs by A232,A233,FUNCT_1:1;
then consider kk being Nat such that
A235: x = kk and
A236: m<=kk and
A237: kk<= len vs by A226;
1<=kk by A213,A236,XXREAL_0:2;
then
A238: x in dom vs by A235,A237,FINSEQ_3:25;
y = fvs.x by A232,A233,FUNCT_1:1;
then y = vs.kk by A226,A227,A234,A235;
hence thesis by A233,A235,A238,FUNCT_1:1;
end;
A239: m < len vs by A5,A210,XXREAL_0:1;
then
A240: m<=len c by A9,NAT_1:13;
then reconsider c2 = (m,len c)-cut c as Chain of G by A213,Th41;
A241: m<=len c by A9,A239,NAT_1:13;
reconsider fvs as Subset of vs by A231;
take fvs;
take c1 = c2;
take p1 = p2;
A242: len c2 +m = len c +1 by A4,A5,A9,A210,Lm2;
then len c2 = len c +(-m+1);
hence
A243: len c1 < len c by A214,XREAL_1:30;
1<=m by A3,A4,XXREAL_0:2;
hence p1 is_vertex_seq_of c1 by A2,A241,Th42;
p2 is_vertex_seq_of c2 by A2,A240,A213,Th42;
then len p1 = len c1 + 1;
hence len p1 < len vs by A9,A243,XREAL_1:6;
thus vs.1 = p1.1 by A4,A5,A6,A9,A210,FINSEQ_6:138;
thus vs.len vs = p1.len p1 by A4,A5,A9,A210,FINSEQ_6:138;
A244: domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A245: x=k and
A246: m<=k and
A247: k<=len vs;
1<=k by A213,A246,XXREAL_0:2;
hence thesis by A245,A247;
end;
A248: domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A249: x=k and
A250: m<=k and
A251: k<=len c;
1<=k by A213,A250,XXREAL_0:2;
hence thesis by A249,A251;
end;
then reconsider domfc as finite set;
A252: len Sgm domfc = card domfc by A248,FINSEQ_3:39;
reconsider domfvs as finite set by A244;
A253: rng Sgm domfvs c= dom fvs by A226,A244,FINSEQ_1:def 13;
set SR = Sgm domfc;
A254: len c +1<=len vs by A2;
A255: m-m<=len c -m by A240,XREAL_1:9;
then len c2 -'1 = len c2 -1 by A242,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
A256: m+lc21 = m1+len c2;
len c2 -'1 = len c2 -1 by A242,A255,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
m+lc21 = len c by A242;
then
A257: card domfc = len c2 + -1 +1 by FINSEQ_6:130
.= len c2;
A258: rng Sgm domfc c= dom fc by A211,A248,FINSEQ_1:def 13;
now
let p be object;
hereby
assume
A259: p in c2;
then consider x, y being object such that
A260: p=[x,y] by RELAT_1:def 1;
A261: y=c2.x by A259,A260,FUNCT_1:1;
A262: x in dom c2 by A259,A260,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A263: k<=len c2 by A262,FINSEQ_3:25;
1<=k by A262,FINSEQ_3:25;
then
A264: m1+k=SR.k by A242,A215,A256,A263,FINSEQ_6:131;
0+1<=k by A262,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A265: i1 & m = len vs;
set domfvs = {k where k is Nat: 1<=k & k<=n};
set pp = (1,n)-cut vs;
deffunc F(object) = c.$1;
reconsider domfc = {k where k is Nat: 1<=k & k<=n1} as set;
consider fc being Function such that
A309: dom fc = domfc and
A310: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
n < len vs by A4,A5,XXREAL_0:2;
then
A311: n-1 < len c +1-1 by A9,XREAL_1:9;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A312: x = kk and
A313: 1<=kk and
A314: kk<=n1;
kk<=len c by A11,A311,A314,XXREAL_0:2;
hence thesis by A312,A313;
end;
then reconsider fc as FinSubsequence by A309,FINSEQ_1:def 12;
1 < n by A3,A308,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A315: 1+1-1<=n-1 by XREAL_1:9;
then reconsider c1 = (1,n1)-cut c as Chain of G by A11,A311,Th41;
A316: 1<=n1+1 by NAT_1:12;
then
A317: len c1+1=n1+1 by A11,A311,Lm2;
then
A318: len c1 = n - 1 by A10,XREAL_0:def 2;
A319: fc c= c
proof
let p be object;
assume
A320: p in fc;
then consider x, y being object such that
A321: [x,y] = p by RELAT_1:def 1;
A322: x in dom fc by A320,A321,FUNCT_1:1;
then consider kk being Nat such that
A323: x = kk and
A324: 1<=kk and
A325: kk<=n1 by A309;
kk<=len c by A11,A311,A325,XXREAL_0:2;
then
A326: x in dom c by A323,A324,FINSEQ_3:25;
y = fc.x by A320,A321,FUNCT_1:1;
then y = c.kk by A309,A310,A322,A323;
hence thesis by A321,A323,A326,FUNCT_1:1;
end;
A327: domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A328: x=k and
A329: 1<=k and
A330: k<=n1;
k<=len c by A11,A311,A330,XXREAL_0:2;
hence thesis by A328,A329;
end;
reconsider fc as Subset of c by A319;
take fc;
reconsider domfc as finite set by A327;
set SL = Sgm domfc;
deffunc F(object) = vs.$1;
consider fvs being Function such that
A331: dom fvs = domfvs and
A332: for x being object st x in domfvs holds fvs.x = F(x)
from FUNCT_1:sch 3;
A333: n<=len vs by A4,A5,XXREAL_0:2;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider kk being Nat such that
A334: x = kk and
A335: 1<=kk and
A336: kk<=n;
kk<=len vs by A333,A336,XXREAL_0:2;
hence thesis by A334,A335;
end;
then reconsider fvs as FinSubsequence by A331,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A337: p in fvs;
then consider x, y being object such that
A338: [x,y] = p by RELAT_1:def 1;
A339: x in dom fvs by A337,A338,FUNCT_1:1;
then consider kk being Nat such that
A340: x = kk and
A341: 1<=kk and
A342: kk<=n by A331;
kk<=len vs by A333,A342,XXREAL_0:2;
then
A343: x in dom vs by A340,A341,FINSEQ_3:25;
y = fvs.x by A337,A338,FUNCT_1:1;
then y = vs.kk by A331,A332,A339,A340;
hence thesis by A338,A340,A343,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A344: x=k and
A345: 1<=k and
A346: k<=n;
k<=len vs by A333,A346,XXREAL_0:2;
hence thesis by A344,A345;
end;
then reconsider domfvs as finite set;
take fvs;
take c9 = c1;
take p1 = pp;
A347: pp is_vertex_seq_of c1 by A2,A12,A315,A311,Th42;
then
A348: len pp = len c1 + 1;
thus len c9 < len c by A10,A311,A317,XREAL_0:def 2;
thus p1 is_vertex_seq_of c9 by A2,A12,A315,A311,Th42;
len p1 = len c1 + 1 by A347;
hence len p1 < len vs by A4,A5,A318,XXREAL_0:2;
thus vs.1 = p1.1 by A3,A333,FINSEQ_6:138;
thus vs.len vs = p1.len p1 by A3,A4,A6,A308,FINSEQ_6:138;
A349: Sgm domfc = idseq n1 by FINSEQ_3:48;
then
A350: dom Sgm domfc = Seg n1;
now
let p be object;
hereby
assume
A351: p in c1;
then consider x, y being object such that
A352: p=[x,y] by RELAT_1:def 1;
A353: y=c1.x by A351,A352,FUNCT_1:1;
A354: x in dom c1 by A351,A352,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A355: k<=len c1 by A354,FINSEQ_3:25;
A356: 1<=k by A354,FINSEQ_3:25;
then x in dom SL by A317,A350,A355;
then
A357: k=SL.k by A349,FUNCT_1:18;
0+1<=k by A354,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A358: i one-to-one for Chain of G;
correctness;
end;
theorem
p is Path of G implies p|Seg(n) is Path of G
proof
reconsider q=p|(Seg n) as FinSequence;
assume
A1: p is Path of G;
now
let n1,m1 be Nat;
assume that
A2: 1<=n1 and
A3: n1 < m1 and
A4: m1<=len q;
1 q.m1 by A1,A2,A3,A5,A6,GRAPH_1:def 16;
end;
hence thesis by A1,GRAPH_1:4,def 16;
end;
registration
let G;
cluster simple for Path of G;
existence
proof
set x = the Element of G;
set q = the empty Chain of G;
reconsider q as one-to-one Chain of G;
take q;
reconsider p = <*x*> as FinSequence of the carrier of G;
take p;
thus p is_vertex_seq_of q by Lm8;
let n,m;
assume that
A1: 1<=n and
A2: nsc.2
proof
hereby
assume
A1: sc is Path of G;
assume
A2: not len sc = 0;
assume not len sc = 1;
then len sc >1 by A2,NAT_1:25;
then
A3: 1+1<=len sc by NAT_1:13;
assume sc.1 = sc.2;
hence contradiction by A1,A3,GRAPH_1:def 16;
end;
assume
A4: len sc = 0 or len sc = 1 or sc.1<>sc.2;
per cases by A4;
suppose
len sc = 0;
then for n, m st 1<=n & nsc.m;
hence thesis by GRAPH_1:def 16;
end;
suppose
len sc = 1;
then for n,m st 1<=n & nsc.m by XXREAL_0:2;
hence thesis by GRAPH_1:def 16;
end;
suppose
A5: sc.1<>sc.2;
now
let n, m;
assume that
A6: 1<=n and
A7: nsc.m
proof
consider vs such that
A9: vs is_vertex_seq_of sc and
A10: for n,m st 1<=n & n oriented for Chain of G;
correctness;
end;
definition
let G;
let oc be oriented Chain of G;
assume
A1: oc <> {};
func vertex-seq oc -> FinSequence of the carrier of G means
it is_vertex_seq_of oc & it.1 = (the Source of G).(oc.1);
existence
proof
set TG = the Target of G;
set SG = the Source of G;
deffunc F(Nat) = SG.(oc.$1);
consider z being FinSequence such that
A2: len z = len oc & for j be Nat st j in dom z holds z.j = F(j) from
FINSEQ_1:sch 2;
set vs = z^<*TG.(oc.len oc)*>;
A3: len vs = len oc + len <*TG.(oc.len oc)*> by A2,FINSEQ_1:22
.= len oc +1 by FINSEQ_1:39;
A4: Seg len z = dom z by FINSEQ_1:def 3;
A5: Seg len oc = dom oc by FINSEQ_1:def 3;
0+1=1;
then
A6: 1<=len oc by A1,NAT_1:13;
rng vs c= the carrier of G
proof
let y be object;
assume y in rng vs;
then consider x being object such that
A7: x in dom vs and
A8: y = vs.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A7;
A9: 1<=x by A7,FINSEQ_3:25;
A10: x<=len vs by A7,FINSEQ_3:25;
per cases by A3,A10,NAT_1:8;
suppose
A11: x<=len oc;
A12: rng oc c= the carrier' of G by FINSEQ_1:def 4;
A13: x in dom oc by A9,A11,FINSEQ_3:25;
then
A14: oc.x in rng oc by FUNCT_1:def 3;
then reconsider e=oc.x as Element of the carrier' of G by A12;
A15: SG.e in rng the Source of G by A14,A12,FUNCT_2:4;
A16: rng the Source of G c= the carrier of G by RELAT_1:def 19;
vs.x = z.x by A2,A5,A4,A13,FINSEQ_1:def 7
.= SG.e by A2,A5,A4,A13;
hence thesis by A8,A15,A16;
end;
suppose
A17: x=len oc +1;
len oc in dom oc by A6,FINSEQ_3:25;
then
A18: oc.len oc in rng oc by FUNCT_1:def 3;
A19: rng oc c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e=oc.len oc as Element of the carrier' of G by A18;
A20: rng the Target of G c= the carrier of G by RELAT_1:def 19;
TG.e in rng the Target of G by A18,A19,FUNCT_2:4;
then y is Element of G by A2,A8,A17,A20,FINSEQ_1:42;
hence thesis;
end;
end;
then reconsider vs as FinSequence of the carrier of G by FINSEQ_1:def 4;
take vs;
now
thus len vs = len oc + 1 by A3;
let n;
assume that
A21: 1<=n and
A22: n<=len oc;
A23: 1<=n+1 by NAT_1:12;
n+1<=len vs by A3,A22,XREAL_1:7;
then n+1 in dom vs by A23,FINSEQ_3:25;
then reconsider vsn1 = vs.(n+1) as Element of G by FINSEQ_2:11;
A24: vsn1 = vs/.(n+1) by A3,A22,A23,FINSEQ_4:15,XREAL_1:7;
A25: vsn1 = TG.(oc.n)
proof
per cases by A22,XXREAL_0:1;
suppose
A26: n