:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 13, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, 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, NUMBER09;
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<len (m, n)
-cut p holds ((m, n)-cut p).(i+1)=p.(m+i) ::: copied from FINSEQ_6
proof
let p be FinSequence, m, n be Nat such that
A1: 1<=m and
A2: m<=n+1 and
A3: n<=len p;
A4: m = n+1 or m < n+1 by A2,XXREAL_0:1;
per cases by A4,NAT_1:13;
suppose
A5: m = n+1;
then
A6: n < m by XREAL_1:29;
then (m, n)-cut p = {} by FINSEQ_6:def 4;
hence len (m, n)-cut p +m = n+1 by A5;
thus thesis by A6,FINSEQ_6:def 4,CARD_1:27;
end;
suppose
m<=n;
hence thesis by A1,A3,FINSEQ_6:def 4;
end;
end;
::$CT 28
::$CD 4
reserve p, q for FinSequence,
X, Y, x, y, e for set,
D for non empty set,
i, j, k, l, m, n, r for Nat;
reserve G for Graph;
reserve v, v1, v2, v3, v4 for Element of G;
theorem
e joins v1,v2 implies e joins v2,v1;
theorem
e joins v1,v2 & e joins v3,v4 implies v1=v3 & v2=v4 or v1=v4 & v2=v3;
reserve vs, vs1, vs2 for FinSequence of the carrier of G,
c, c1, c2 for Chain of G;
definition
let G, X;
func G-VSet X -> 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<k;
then 1+1<=k by NAT_1:13;
then consider k1 being Nat such that
A52: 1<=k1 and
A53: k1<k and
A54: k=k1+1 by FINSEQ_6:127;
A55: k<=len vs1 by A9,FINSEQ_3:25;
then
A56: k1<=len vs1 by A53,XXREAL_0:2;
then
A57: k1 in dom vs1 by A52,FINSEQ_3:25;
A58: vs1/.k1=vs1.k1 by A52,A56,FINSEQ_4:15;
A59: vs2/.k=vs2.k by A4,A7,A5,A6,A9,PARTFUN1:def 6;
A60: vs1/.k=vs1.k by A9,PARTFUN1:def 6;
A61: k1<=len c by A4,A54,A55,XREAL_1:6;
then c.k1 joins vs1/.k1, vs1/.(k1+1) by A2,A52;
then
A62: SG.(c.k1)=vs1/.k1 & TG.(c.k1)=vs1/.k or SG.(c.k1)=vs1/.k & TG.(c.k1)=
vs1/.k1 by A54;
c.k1 joins vs2/.k1, vs2/.(k1+1) by A3,A52,A61;
then
A63: SG.(c.k1)=vs2/.k1 & TG.(c.k1)=vs2/.k or SG.(c.k1)=vs2/.k & TG.(c.k1)=
vs2/.k1 by A54;
vs2/.k1=vs2.k1 by A4,A7,A52,A56,FINSEQ_4:15;
hence thesis by A9,A10,A53,A57,A58,A60,A59,A62,A63;
end;
end;
definition
let G;
let c be FinSequence;
pred c alternates_vertices_in G means
len c>=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<n;
A36: n<=len c by A31,NAT_1:13;
A37: 0+1<=n by A35,NAT_1:13;
hence vs1/.(n+1)<> 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<k;
then 1+1<=k by NAT_1:13;
then consider k1 being Nat such that
A57: 1<=k1 and
A58: k1<k and
A59: k=k1+1 by FINSEQ_6:127;
A60: k<=len vs1 by A19,FINSEQ_3:25;
then
A61: k1<=len vs1 by A58,XXREAL_0:2;
then
A62: k1 in dom vs1 by A57,FINSEQ_3:25;
A63: k1<=len c by A15,A59,A60,XREAL_1:6;
then c.k1 joins vs1/.k1, vs1/.(k1+1) by A14,A57;
then
A64: SG.(c.k1)=vs1/.k1 & TG.(c.k1)=vs1/.k or SG.(c.k1)=vs1/.k & TG.(
c.k1)= vs1/.k1 by A59;
A65: vs1/.k1=vs1.k1 by A57,A61,FINSEQ_4:15;
A66: vs1/.k=vs1.k by A19,PARTFUN1:def 6;
c.k1 joins vs/.k1, vs/.(k1+1) by A1,A57,A63;
then
A67: SG.(c.k1)=vs/.k1 & TG.(c.k1)=vs/.k or SG.(c.k1)=vs/.k & TG.(c.
k1)=vs/. k1 by A59;
A68: vs/.k=vs.k by A17,A19,PARTFUN1:def 6;
vs/.k1=vs.k1 by A15,A16,A57,A61,FINSEQ_4:15;
hence contradiction by A19,A20,A58,A62,A65,A66,A68,A64,A67;
end;
end;
end;
end;
assume
A69: for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs;
assume card the carrier of G <> 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;
<*y*> = vs by A69,A74,Th32;
hence contradiction by A72,A75;
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<len q and
A21: k=j+1 by A19,FINSEQ_6:127;
A22: j+1<len p9 by A12,A16,A20,XREAL_1:6;
i+1 = m+(j+1) by A21;
then
A23: p9.(k+1) = vs.(i+1) by A1,A4,A14,A22,FINSEQ_6:def 4;
set v2 = vs/.(i+1);
set v1 = vs/.i;
A24: 1<=i+1 by NAT_1:12;
A25: i= m+j by A21;
j<len p9 by A12,A16,A20,NAT_1:13;
then
A26: p9.k = vs.i by A1,A4,A14,A25,A22,FINSEQ_6:def 4;
i<=(m-1)+(n-(m-1)) by A12,A19,XREAL_1:6;
then
A27: i<=len c by A3,XXREAL_0:2;
then
A28: i<=len vs by A13,NAT_1:12;
take v1, v2;
A29: i+1<=len vs by A13,A27,XREAL_1:7;
1-1<=m-1 by A1,XREAL_1:9;
then
A30: 0+1<=m-1+k by A18,XREAL_1:7;
then c.i joins v1, v2 by A5,A27;
hence
v1 = p9.k & v2 = p9.(k+1) & q.k joins v1, v2 by A1,A3,A11,A4,A20,A21,A25
,A30,A28,A24,A29,A26,A23,Lm2,FINSEQ_4:15;
end;
thus q is Chain of G
proof
hereby
let k be Nat;
assume that
A31: 1<=k and
A32: k<=len q;
k in dom q by A31,A32,FINSEQ_3:25;
then
A33: q.k in rng q by FUNCT_1:def 3;
rng q c= rng c by A11,FINSEQ_6:137;
then
A34: q.k in rng c by A33;
rng c c= the carrier' of G by FINSEQ_1:def 4;
hence q.k in the carrier' of G by A34;
end;
take p9;
thus len p9 = len q + 1 by A12,A15;
thus for n st 1<=n & n<=len p9 holds p9.n in the carrier of G by A6;
thus thesis by A17;
end;
end;
theorem Th42:
1<=m & m<=n & n<=len c & c1 = (m,n)-cut c & vs is_vertex_seq_of
c & vs1 = (m,n+1)-cut vs implies vs1 is_vertex_seq_of c1
proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
A4: m<=n+1 by A2,NAT_1:12;
assume
A5: c1 = (m,n)-cut c;
then
A6: len c1 +m= n+1 by A1,A3,A4,Lm2;
assume that
A7: vs is_vertex_seq_of c and
A8: vs1 = (m,n+1)-cut vs;
A9: len vs = len c + 1 by A7;
then
A10: n+1<=len vs by A3,XREAL_1:6;
then len vs1 +m = n+1+1 by A1,A8,A4,FINSEQ_6:def 4;
hence
A11: len vs1 = len c1 + 1 by A6;
let k be Nat;
assume that
A12: 1<=k and
A13: k<=len c1;
0+1<=k by A12;
then consider j such that
0<=j and
A14: j<len c1 and
A15: k=j+1 by A13,FINSEQ_6:127;
set i = m+j;
j<len vs1 by A11,A14,NAT_1:13;
then
A16: vs1.k = vs.i by A1,A8,A4,A10,A15,FINSEQ_6:def 4;
m+k<=len c1 +m by A13,XREAL_1:7;
then m+j+1-1<=len c1 +m-1 by A15,XREAL_1:9;
then
A17: i<=len c by A3,A6,XXREAL_0:2;
then i<=len vs by A9,NAT_1:12;
then
A18: vs/.i=vs.i by A1,FINSEQ_4:15,NAT_1:12;
A19: k<=len c1 by A14,A15,NAT_1:13;
then
A20: k<=len vs1 by A11,NAT_1:12;
1<=k+1 by NAT_1:12;
then
A21: vs1/.(k+1)=vs1.(k+1) by A11,A19,FINSEQ_4:15,XREAL_1:7;
0+1=1;
then 1<=k by A15,NAT_1:13;
then
A22: vs1/.k=vs1.k by A20,FINSEQ_4:15;
set v2 = vs/.(i+1);
set v1 = vs/.i;
A23: m+j+1 = m+(j+1);
1<=i by A1,NAT_1:12;
then
A24: c.i joins v1, v2 by A7,A17;
1<=i+1 by NAT_1:12;
then
A25: vs/.(i+1)=vs.(i+1) by A9,A17,FINSEQ_4:15,XREAL_1:7;
j+1<len vs1 by A11,A14,XREAL_1:6;
then vs1.(k+1) = vs.(i+1) by A1,A8,A4,A10,A15,A23,FINSEQ_6:def 4;
hence thesis by A1,A3,A5,A4,A14,A15,A24,A16,A18,A25,A22,A21,Lm2;
end;
theorem Th43:
vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1.len vs1
= vs2.1 implies c1^c2 is Chain of G
proof
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: vs2 is_vertex_seq_of c2 and
A3: vs1.len vs1 = vs2.1;
set q=c1^c2;
set p=vs1^'vs2;
A4: len vs2 = len c2 + 1 by A2;
then vs2 <> {};
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<len vs2 by A14,NAT_1:13;
then p.(len vs1 + m) = vs2.(m+1) by A13,FINSEQ_6:141;
hence p.n in the carrier of G by A12,A15,FINSEQ_2:11;
end;
end;
A16: len vs1 = len c1 + 1 by A1;
A17: now
let n be Nat;
assume that
A18: 1<=n and
A19: n<=len q;
A20: n in dom q by A18,A19,FINSEQ_3:25;
per cases by A20,FINSEQ_1:25;
suppose
A21: n in dom c1;
set v2=vs1/.(n+1);
set v1=vs1/.n;
A22: q.n = c1.n by A21,FINSEQ_1:def 7;
A23: 1<=n by A21,FINSEQ_3:25;
A24: n<=len c1 by A21,FINSEQ_3:25;
then
A25: n+1<=len vs1 by A1,XREAL_1:6;
then
A26: vs1/.(n+1)=vs1.(n+1) by FINSEQ_4:15,NAT_1:12;
A27: n<=len vs1 by A16,A24,NAT_1:12;
then
A28: vs1/.n=vs1.n by A23,FINSEQ_4:15;
A29: p.(n+1) = vs1.(n+1) by A25,FINSEQ_6:140,NAT_1:12;
A30: p.n = vs1.n by A23,A27,FINSEQ_6:140;
c1.n joins v1, v2 by A1,A23,A24;
hence
ex v1, v2 being Element of G st v1 = p.n & v2 = p.(n
+1) & q.n joins v1, v2 by A22,A28,A26,A30,A29;
end;
suppose
ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A31: k in dom c2 and
A32: n = len c1 + k;
A33: q.n = c2.k by A31,A32,FINSEQ_1:def 7;
A34: 1<=k+1 by NAT_1:12;
A35: 1<=k by A31,FINSEQ_3:25;
A36: k<=len c2 by A31,FINSEQ_3:25;
then
A37: k<=len vs2 by A4,NAT_1:12;
reconsider k as Element of NAT by A31;
A38: 0+1<=k by A31,FINSEQ_3:25;
A39: vs2/.(k+1)=vs2.(k+1) by A4,A36,A34,FINSEQ_4:15,XREAL_1:7;
A40: k<len vs2 by A4,A36,NAT_1:13;
k<=len vs2 by A4,A36,NAT_1:12;
then consider j such that
0<=j and
A41: j<len vs2 and
A42: k=j+1 by A38,FINSEQ_6:127;
A43: p.n = vs2.k
proof
per cases by A35,XXREAL_0:1;
suppose
A44: 1=k;
0+1<=len vs1 by A16,NAT_1:13;
hence thesis by A3,A16,A32,A44,FINSEQ_6:140;
end;
suppose
1<k;
then
A45: 1<=j by A42,NAT_1:13;
thus p.n = p.(len vs1 +j) by A16,A32,A42
.= vs2.k by A41,A42,A45,FINSEQ_6:141;
end;
end;
set v2 = vs2/.(k+1);
set v1 = vs2/.k;
A46: c2.k joins v1, v2 by A2,A35,A36;
A47: vs2/.k=vs2.k by A35,A37,FINSEQ_4:15;
p.(n+1) = p.(len c1 +1+k) by A32
.= vs2.(k+1) by A16,A35,A40,FINSEQ_6:141;
hence
ex v1, v2 being Element of G st v1 = p.n & v2 = p.(n
+1) & q.n joins v1, v2 by A33,A47,A39,A46,A43;
end;
end;
A48: len p = len c1 + len c2 + 1 by A16,A4,A5
.= len q + 1 by FINSEQ_1:22;
thus c1^c2 is Chain of G
proof
hereby
let n be Nat;
assume that
A49: 1<=n and
A50: n<=len q;
A51: n in dom q by A49,A50,FINSEQ_3:25;
per cases by A51,FINSEQ_1:25;
suppose
A52: n in dom c1;
then
A53: q.n = c1.n by FINSEQ_1:def 7;
A54: n<=len c1 by A52,FINSEQ_3:25;
1<=n by A52,FINSEQ_3:25;
hence (c1^c2).n in the carrier' of G by A54,A53,GRAPH_1:def 14;
end;
suppose
ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A55: k in dom c2 and
A56: n = len c1 + k;
A57: 1<=k by A55,FINSEQ_3:25;
A58: k<= len c2 by A55,FINSEQ_3:25;
q.n = c2.k by A55,A56,FINSEQ_1:def 7;
hence (c1^c2).n in the carrier' of G by A57,A58,GRAPH_1:def 14;
end;
end;
thus thesis by A48,A6,A17;
end;
end;
theorem Th44:
vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1.len vs1
= vs2.1 & c = c1^c2 & vs = vs1^'vs2 implies vs is_vertex_seq_of c
proof
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: vs2 is_vertex_seq_of c2 and
A3: vs1.len vs1 = vs2.1;
set p=vs1^'vs2;
set q=c1^c2;
assume that
A4: c = c1^c2 and
A5: vs = vs1^'vs2;
A6: len vs1 = len c1 + 1 by A1;
A7: len vs2 = len c2 + 1 by A2;
then vs2 <> {};
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<len vs2 by A7,NAT_1:13;
A28: 1<=k by A23,FINSEQ_3:25;
then
A29: c2.k joins v1, v2 by A2,A26;
k<=len vs2 by A7,A26,NAT_1:12;
then consider j such that
0<=j and
A30: j<len vs2 and
A31: k=j+1 by A25,FINSEQ_6:127;
A32: p.n = vs2.k
proof
per cases by A28,XXREAL_0:1;
suppose
A33: 1=k;
0+1<=len vs1 by A6,NAT_1:13;
hence thesis by A3,A6,A24,A33,FINSEQ_6:140;
end;
suppose
1<k;
then
A34: 1<=j by A31,NAT_1:13;
thus p.n = p.(len vs1 +j) by A6,A24,A31
.= vs2.k by A30,A31,A34,FINSEQ_6:141;
end;
end;
1<=k+1 by NAT_1:12;
then
A35: vs2/.(k+1)=vs2.(k+1) by A7,A26,FINSEQ_4:15,XREAL_1:7;
k<=len vs2 by A7,A26,NAT_1:12;
then
A36: vs2/.k=vs2.k by A28,FINSEQ_4:15;
p.(n+1) = p.(len c1 +1+k) by A24
.= vs2.(k+1) by A6,A28,A27,FINSEQ_6:141;
hence q.n joins p/.n,p/.(n+1) by A12,A13,A23,A24,A36,A35,A29,A32,
FINSEQ_1:def 7;
end;
end;
hence thesis by A4,A5,A8;
end;
begin :: Simple chains, paths and oriented chains
Lm8: <*v*> 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<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs;
end;
registration
let G;
cluster simple for Chain of G;
existence
proof
set x = the Element of G;
set q = the empty 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: n<m and
A3: m<=len p and
p.n = p.m;
1<m by A1,A2,XXREAL_0:2;
hence thesis by A3,FINSEQ_1:39;
end;
end;
reserve sc for simple Chain of G;
theorem
sc|(Seg n) is simple Chain of G
proof
reconsider q9 = sc|Seg n as Chain of G by GRAPH_1:4;
consider vs such that
A1: vs is_vertex_seq_of sc and
A2: for n, m st 1<=n & n < m & m<=len vs & vs.n = vs.m holds n=1 & m=
len vs by Def9;
reconsider p9 = vs|Seg(n+1) as FinSequence of the carrier of G by FINSEQ_1:18
;
now
take p9;
thus p9 is_vertex_seq_of q9 by A1,Th40;
let k, m;
assume that
A3: 1<=k and
A4: k < m and
A5: m<=len p9 and
A6: p9.k = p9.m;
k<=len p9 by A4,A5,XXREAL_0:2;
then
A7: p9.k = vs.k by A3,FINSEQ_6:128;
1<=m by A3,A4,XXREAL_0:2;
then
A8: p9.m = vs.m by A5,FINSEQ_6:128;
A9: len p9<=len vs by FINSEQ_6:128;
then
A10: m<=len vs by A5,XXREAL_0:2;
hence k=1 by A2,A3,A4,A6,A7,A8;
len p9 = len vs or len p9 < len vs by A9,XXREAL_0:1;
hence m = len p9 by A2,A3,A4,A5,A6,A7,A8,A10;
end;
hence thesis by Def9;
end;
theorem Th46:
2<len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc implies vs1=vs2
proof
assume that
A1: 2<len sc and
A2: vs1 is_vertex_seq_of sc and
A3: vs2 is_vertex_seq_of sc;
A4: len vs1 = len sc +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 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<m & m<=len vs & vs.n=vs.m holds n=1 & m=len
vs by Def9;
sc <>{} 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<k;
then 1+1<=k by NAT_1:13;
then consider k1 being Nat such that
A29: 1<=k1 and
A30: k1<k and
A31: k=k1+1 by FINSEQ_6:127;
A32: k<=len vs1 by A10,FINSEQ_3:25;
then
A33: k1<=len vs1 by A30,XXREAL_0:2;
then
A34: k1 in dom vs1 by A29,FINSEQ_3:25;
A35: vs1/.k1=vs1.k1 by A29,A33,FINSEQ_4:15;
A36: vs2/.k=vs2.k by A4,A7,A5,A6,A10,PARTFUN1:def 6;
A37: vs1/.k=vs1.k by A10,PARTFUN1:def 6;
A38: k1<=len sc by A4,A31,A32,XREAL_1:6;
then sc.k1 joins vs1/.k1, vs1/.(k1+1) by A2,A29;
then
A39: SG.(sc.k1)=vs1/.k1 & TG.(sc.k1)=vs1/.k or SG.(sc.k1)=vs1/.k & TG.(sc.
k1)=vs1/.k1 by A31;
sc.k1 joins vs2/.k1, vs2/.(k1+1) by A3,A29,A38;
then
A40: SG.(sc.k1)=vs2/.k1 & TG.(sc.k1)=vs2/.k or SG.(sc.k1)=vs2/.k & TG.(sc.
k1)=vs2/.k1 by A31;
vs2/.k1=vs2.k1 by A4,A7,A29,A33,FINSEQ_4:15;
hence contradiction by A10,A11,A30,A34,A35,A37,A36,A39,A40;
end;
end;
theorem
vs is_vertex_seq_of sc implies for n, m st 1<=n & n<m & m<=len vs & vs
.n = vs.m holds n=1 & m=len vs
proof
assume
A1: vs is_vertex_seq_of sc;
consider vs1 such that
A2: vs1 is_vertex_seq_of sc and
A3: for n,m st 1<=n & n<m & m<=len vs1 & vs1.n=vs1.m holds n=1 & m=len
vs1 by Def9;
per cases;
suppose
A4: len sc <= 2;
thus thesis
proof
len sc = 0 or ... or len sc = 2 by A4;
then per cases;
suppose
A5: len sc = 0;
let n,m;
len vs = 0+1 by A1,A5;
hence thesis by XXREAL_0:2;
end;
suppose
len sc = 1;
then
A6: len vs = 1+1 by A1;
let n,m;
assume that
A7: 1<=n and
A8: n<m and
A9: m<=len vs and
vs.n=vs.m;
A10: n+1<=m by A8,NAT_1:13;
then n+1<=1+1 by A6,A9,XXREAL_0:2;
then n<=1 by XREAL_1:6;
then n=1 by A7,XXREAL_0:1;
hence thesis by A6,A9,A10,XXREAL_0:1;
end;
suppose
A11: len sc = 2;
set v12=vs1/.(1+1);
set v2=vs/.(1+1);
set v11=vs1/.1;
A12: sc.1 joins v11,v12 by A2,A11;
set v1=vs/.1;
sc.1 joins v1, v2 by A1,A11;
then
A13: v1=v11 & v2=v12 or v1=v12 & v2=v11 by A12;
A14: len vs = 1+1+1 by A1,A11;
then
A15: v2=vs.(1+1) by FINSEQ_4:15;
set v3=vs/.(1+1+1);
set v13=vs1/.(1+1+1);
A16: sc.2 joins v12,v13 by A2,A11;
sc.2 joins v2, v3 by A1,A11;
then
A17: v2=v12 & v3=v13 or v2=v13 & v3=v12 by A16;
A18: len vs1 = 1+1+1 by A2,A11;
then
A19: v11=vs1.1 by FINSEQ_4:15;
A20: v13=vs1.(1+1+1) by A18,FINSEQ_4:15;
A21: v12=vs1.(1+1) by A18,FINSEQ_4:15;
let n,m;
assume that
A22: 1<=n and
A23: n<m and
A24: m<=len vs and
A25: vs.n=vs.m;
n+1<=m by A23,NAT_1:13;
then n+1<=1+1+1 by A14,A24,XXREAL_0:2;
then
A26: n<=1+1 by XREAL_1:6;
A27: v3=vs.(1+1+1) by A14,FINSEQ_4:15;
A28: v1=vs.1 by A14,FINSEQ_4:15;
thus thesis
proof
per cases by A22,A26,NAT_1:9;
suppose
A29: n=1;
1<m by A22,A23,XXREAL_0:2;
then
A30: 1+1<=m by NAT_1:13;
thus thesis
proof
per cases by A14,A24,A30,NAT_1:9;
suppose
m=1+1;
hence thesis by A3,A18,A28,A15,A19,A21,A13,A25,A29;
end;
suppose
m=1+1+1;
hence thesis by A1,A11,A29;
end;
end;
end;
suppose
A31: n=1+1;
then 1+1+1<=m by A23,NAT_1:13;
then m=1+1+1 by A14,A24,XXREAL_0:1;
hence thesis by A3,A18,A15,A27,A21,A20,A17,A25,A31;
end;
end;
end;
end;
end;
suppose
2<len sc;
then vs=vs1 by A1,A2,Th46;
hence thesis by A3;
end;
end;
:: A chain may have more than one simple chain spanning its endpoints.
:: The following chain:
:: .--->.
:: ^ |
:: | 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: n<m and
A5: m<=len vs and
A6: vs.n=vs.m and
A7: n<>1 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;
a38: DL is included_in_Seg & DR is included_in_Seg by A38,FINSEQ_1:def 13;
rng Sgm DR = DR by a38,FINSEQ_1:def 14;
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<len p2 by A54,A18,NAT_1:13;
lp21 -'1 = lp21 -1 by A54,A18,A49,XREAL_0:def 2;
then reconsider lp22 = lp21 -1 as Element of NAT;
A57: m+1+lp22 = m+lp21;
m+lc21 = len c by A18;
then
A58: card DR = len c2 + -1 +1 by FINSEQ_6:130
.= len c2;
A59: m+lc21 = m1+len c2;
now
let p be object;
hereby
assume
A60: p in c2;
then consider x, y being object such that
A61: p=[x,y] by RELAT_1:def 1;
A62: y=c2.x by A60,A61,FUNCT_1:1;
A63: x in dom c2 by A60,A61,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A64: k<=len c2 by A63,FINSEQ_3:25;
1<=k by A63,FINSEQ_3:25;
then
A65: m1+k=SR.k by A51,A18,A59,A64,FINSEQ_6:131;
0+1<=k by A63,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A66: i<len c2 and
A67: k=i+1 by A64,FINSEQ_6:127;
A68: x in dom SR by A58,A47,A63,FINSEQ_3:29;
then
A69: SR.k in rng SR by FUNCT_1:def 3;
then
A70: x in dom (fc*SR) by A45,A68,FUNCT_1:11;
then (fc*SR).x = fc.(m1+k) by A65,FUNCT_1:12
.= c.(m+i) by A45,A65,A69,A67,GRFUNC_1:2
.= y by A15,A17,A62,A66,A67,FINSEQ_6:def 4;
hence p in fc*(Sgm DR) by A61,A70,FUNCT_1:1;
end;
assume
A71: p in fc*(Sgm DR);
then consider x,y being object such that
A72: p=[x,y] by RELAT_1:def 1;
A73: y = (fc*SR).x by A71,A72,FUNCT_1:1;
A74: x in dom (fc*SR) by A71,A72,FUNCT_1:1;
then
A75: x in dom SR by FUNCT_1:11;
then reconsider k=x as Element of NAT;
A76: k<=len c2 by A58,A47,A75,FINSEQ_3:25;
1<=k by A75,FINSEQ_3:25;
then
A77: m1+k=SR.k by A51,A18,A59,A76,FINSEQ_6:131;
A78: k in dom c2 by A58,A47,A75,FINSEQ_3:29;
A79: SR.x in dom fc by A74,FUNCT_1:11;
0+1<=k by A75,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A80: i<len c2 and
A81: k=i+1 by A76,FINSEQ_6:127;
c2.k = c.(m1+1+i) by A15,A17,A80,A81,FINSEQ_6:def 4
.= fc.(SR.k) by A79,A77,A81,GRFUNC_1:2
.= y by A73,A75,FUNCT_1:13;
hence p in c2 by A72,A78,FUNCT_1:1;
end;
then
A82: c2 = fc*(Sgm DR) by TARSKI:2;
now
let i,j;
assume i in DL;
then consider k being Nat such that
A83: k=i and
1<=k and
A84: k<=n1;
assume j in DR;
then
A85: ex l being Nat st l=j & m<=l & l<=len c;
n1<m by A4,A12,NAT_1:13;
then k<m by A84,XXREAL_0:2;
hence i < j by A83,A85,XXREAL_0:2;
end;
then
A86: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by a38,FINSEQ_3:42;
set DR = {kk where kk is Nat: m+1<=kk & kk<= len vs};
A87: 1<=m+1 by NAT_1:12;
deffunc F(object) = vs.$1;
consider fvs being Function such that
A88: dom fvs = domfvs and
A89: for x being object st x in domfvs holds fvs.x = F(x) from FUNCT_1:sch 3;
A90: 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
A91: x = kk and
A92: 1<=kk & kk<=n or m+1<=kk & kk<= len vs;
A93: kk<=len vs by A90,A92,XXREAL_0:2;
1<=m+1 by NAT_1:12;
then 1<=kk by A92,XXREAL_0:2;
hence thesis by A91,A93;
end;
then reconsider fvs as FinSubsequence by A88,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A94: p in fvs;
then consider x, y being object such that
A95: [x,y] = p by RELAT_1:def 1;
A96: x in dom fvs by A94,A95,FUNCT_1:1;
then consider kk being Nat such that
A97: x = kk and
A98: 1<=kk & kk<=n or m+1<=kk & kk<= len vs by A88;
A99: kk<=len vs by A90,A98,XXREAL_0:2;
1<=m+1 by NAT_1:12;
then 1<=kk by A98,XXREAL_0:2;
then
A100: x in dom vs by A97,A99,FINSEQ_3:25;
y = fvs.x by A94,A95,FUNCT_1:1;
then y = vs.kk by A88,A89,A96,A97;
hence thesis by A95,A97,A100,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
A101: len c + 1<=len vs by A2;
A102: m<=len c + 1 by A2,A5;
then
A103: p2.1 = vs.m by A46,A101,FINSEQ_6:138;
A104: pp.len pp = vs.n by A3,A90,FINSEQ_6:138;
then reconsider c9 = c1^c2 as Chain of G by A6,A34,A53,A103,Th43;
take fvs;
take c9;
take p1=pp^'p2;
A105: 1<=n1+1 by NAT_1:12;
then
A106: len c1 +1 = n1+1 by A11,A21,Lm2;
then len c1 = n - 1 by A10,XREAL_0:def 2;
then len c9 = (n+-1)+(len c +(-m +1)) by A18,FINSEQ_1:22
.= len c + (n+ -m );
hence
A107: len c9 < len c by A50,XREAL_1:30;
A108: Sgm DL = idseq n1 by FINSEQ_3:48;
then
A109: dom Sgm DL = Seg n1;
now
let p be object;
hereby
assume
A110: p in c1;
then consider x, y being object such that
A111: p=[x,y] by RELAT_1:def 1;
A112: y=c1.x by A110,A111,FUNCT_1:1;
A113: x in dom c1 by A110,A111,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A114: k<=len c1 by A113,FINSEQ_3:25;
A115: 1<=k by A113,FINSEQ_3:25;
then
A116: k in domfc by A106,A114;
0+1<=k by A113,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A117: i<n1 and
A118: k=i+1 by A106,A114,FINSEQ_6:127;
A119: x in dom SL by A106,A109,A115,A114;
then
A120: k=SL.k by A108,FUNCT_1:18;
then
A121: x in dom (fc*SL) by A19,A119,A116,FUNCT_1:11;
then (fc*SL).x = fc.k by A120,FUNCT_1:12
.= c.(1+i) by A19,A116,A118,GRFUNC_1:2
.= y by A11,A21,A105,A106,A112,A117,A118,Lm2;
hence p in fc*(Sgm DL) by A111,A121,FUNCT_1:1;
end;
assume
A122: p in fc*(Sgm DL);
then consider x,y being object such that
A123: p=[x,y] by RELAT_1:def 1;
A124: y = (fc*SL).x by A122,A123,FUNCT_1:1;
A125: x in dom (fc*SL) by A122,A123,FUNCT_1:1;
then
A126: (fc*SL).x = fc.(SL.x) by FUNCT_1:12;
A127: x in dom SL by A125,FUNCT_1:11;
then consider k being Nat such that
A128: k=x and
A129: 1<=k and
A130: k<=n1 by A109;
A131: k in dom fc by A19,A129,A130;
A132: k in dom c1 by A106,A129,A130,FINSEQ_3:25;
A133: k=SL.k by A108,A127,A128,FUNCT_1:18;
0+1<=k by A129;
then ex i being Nat st 0<=i & i<n1 & k=i+1 by A130,FINSEQ_6:127;
then c1.k = c.k by A11,A21,A105,A106,Lm2
.= y by A124,A126,A128,A131,A133,GRFUNC_1:2;
hence p in c1 by A123,A128,A132,FUNCT_1:1;
end;
then
A134: c1 = fc*(Sgm DL) by TARSKI:2;
thus p1 is_vertex_seq_of c9 by A6,A34,A53,A103,A104,Th44;
then len p1 = len c9 + 1;
hence len p1 < len vs by A9,A107,XREAL_1:6;
1<=1 + len c1 by NAT_1:12;
then 1<=len pp by A34;
then p1.1 = pp.1 by FINSEQ_6:140;
hence vs.1 = p1.1 by A3,A90,FINSEQ_6:138;
p2.len p2 = vs.(len c + 1) by A46,A102,A101,FINSEQ_6:138;
hence vs.len vs = p1.len p1 by A9,A56,FINSEQ_6:142;
A135: p2 = (0+1, len p2)-cut p2 by FINSEQ_6:133
.= (0+1, 1)-cut p2 ^ (1+1, len p2)-cut p2 by A55,FINSEQ_6:134;
rng Sgm DL = DL by a38,FINSEQ_1:def 14;
then rng Sgm DL c= dom fc by A19,A37,XBOOLE_1:7;
hence Seq fc = c9 by A19,A37,A86,A45,A134,A82,FINSEQ_6:150;
set DL = {kk where kk is Nat: 1<=kk & kk<=n};
A136: DL c= Seg len vs & DR c= Seg len vs
proof
hereby
let x be object;
assume x in DL;
then consider k being Nat such that
A137: x=k and
A138: 1<=k and
A139: k<=n;
k<=len vs by A90,A139,XXREAL_0:2;
hence x in Seg len vs by A137,A138;
end;
let x be object;
assume x in DR;
then consider k being Nat such that
A140: x=k and
A141: m+1<=k and
A142: k<=len vs;
1<=m+1 by NAT_1:12;
then 1<=k by A141,XXREAL_0:2;
hence thesis by A140,A142;
end;
then
a136: DL is included_in_Seg & DR is included_in_Seg by FINSEQ_1:def 13;
now
let x be object;
hereby
assume x in domfvs;
then ex k being Nat st x=k &( 1<=k & k<=n or m+1<=k & k<=
len vs);
then x in DL or x in DR;
hence x in DL \/ DR by XBOOLE_0:def 3;
end;
assume
A143: x in DL \/ DR;
per cases by A143,XBOOLE_0:def 3;
suppose
x in DL;
then ex k being Nat st x=k & 1<=k & k<=n;
hence x in domfvs;
end;
suppose
x in DR;
then ex k being Nat st x=k & m+1<=k & k<=len vs;
hence x in domfvs;
end;
end;
then
A144: domfvs = DL \/ DR by TARSKI:2;
reconsider DR as finite set by A136;
rng Sgm DR = DR by a136,FINSEQ_1:def 14;
then
A145: rng Sgm DR c= dom fvs by A88,A144,XBOOLE_1:7;
reconsider DL as finite set by A136;
A146: m+1<=len c +1+1 by A5,A9,XREAL_1:6;
A147: m<=len c +1+1 by A5,A9,NAT_1:12;
then
A148: len p2 +m = len c +1+1 by A9,A15,Lm2
.= len p29 +(m+1) by A9,A14,A146,Lm2
.= (len p29+1)+m;
set SL = Sgm DL;
A149: Sgm DL = idseq n by FINSEQ_3:48;
then
A150: dom Sgm DL = Seg n;
now
let p be object;
hereby
assume
A151: p in pp;
then consider x, y being object such that
A152: p=[x,y] by RELAT_1:def 1;
A153: y=pp.x by A151,A152,FUNCT_1:1;
A154: x in dom pp by A151,A152,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A155: k<=len pp by A154,FINSEQ_3:25;
A156: 1<=k by A154,FINSEQ_3:25;
then
A157: k in domfvs by A11,A35,A106,A155;
0+1<=k by A154,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A158: i<n and
A159: k=i+1 by A11,A35,A106,A155,FINSEQ_6:127;
A160: x in dom SL by A11,A35,A106,A150,A156,A155;
then
A161: k=SL.k by A149,FUNCT_1:18;
then
A162: x in dom (fvs*SL) by A88,A160,A157,FUNCT_1:11;
then (fvs*SL).x = fvs.k by A161,FUNCT_1:12
.= vs.(1+i) by A88,A157,A159,GRFUNC_1:2
.= y by A3,A11,A90,A35,A106,A153,A158,A159,FINSEQ_6:def 4;
hence p in fvs*(Sgm DL) by A152,A162,FUNCT_1:1;
end;
assume
A163: p in fvs*(Sgm DL);
then consider x,y being object such that
A164: p=[x,y] by RELAT_1:def 1;
A165: y = (fvs*SL).x by A163,A164,FUNCT_1:1;
A166: x in dom (fvs*SL) by A163,A164,FUNCT_1:1;
then
A167: (fvs*SL).x = fvs.(SL.x) by FUNCT_1:12;
A168: x in dom SL by A166,FUNCT_1:11;
then consider k being Nat such that
A169: k=x and
A170: 1<=k and
A171: k<=n by A150;
A172: k in dom fvs by A88,A170,A171;
A173: k=SL.k by A149,A168,A169,FUNCT_1:18;
A174: k in dom pp by A11,A35,A106,A170,A171,FINSEQ_3:25;
0+1<=k by A170;
then ex i being Nat st 0<=i & i<n & k=i+1 by A171,FINSEQ_6:127;
then pp.k = vs.k by A3,A11,A90,A35,A106,FINSEQ_6:def 4
.= y by A165,A167,A169,A172,A173,GRFUNC_1:2;
hence p in pp by A164,A169,A174,FUNCT_1:1;
end;
then
A175: pp = fvs*(Sgm DL) by TARSKI:2;
set SR = Sgm DR;
A176: len Sgm DR = card DR by a136,FINSEQ_3:39;
A177: m+1+lp22 = m+((lp21 -1)+1) .= m+(len c -m +1 +1 -1) by A53,A18
.= len c +1;
then
A178: card DR = lp21 -1+1 by A9,FINSEQ_6:130
.= lp21;
A179: m+1<=len c +1+1 by A5,A9,XREAL_1:7;
now
let p be object;
hereby
assume
A180: p in p29;
then consider x, y being object such that
A181: p=[x,y] by RELAT_1:def 1;
A182: y=p29.x by A180,A181,FUNCT_1:1;
A183: x in dom p29 by A180,A181,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A184: k<=len p29 by A183,FINSEQ_3:25;
1<=k by A183,FINSEQ_3:25;
then
A185: m+k=SR.k by A9,A177,A148,A57,A184,FINSEQ_6:131;
0+1<=k by A183,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A186: i<len p29 and
A187: k=i+1 by A184,FINSEQ_6:127;
A188: x in dom SR by A178,A148,A176,A183,FINSEQ_3:29;
then
A189: SR.k in rng SR by FUNCT_1:def 3;
then
A190: x in dom (fvs*SR) by A145,A188,FUNCT_1:11;
then (fvs*SR).x = fvs.(m+k) by A185,FUNCT_1:12
.= vs.(m+1+i) by A145,A185,A189,A187,GRFUNC_1:2
.= y by A9,A87,A179,A182,A186,A187,Lm2;
hence p in fvs*(Sgm DR) by A181,A190,FUNCT_1:1;
end;
assume
A191: p in fvs*(Sgm DR);
then consider x,y being object such that
A192: p=[x,y] by RELAT_1:def 1;
A193: y = (fvs*SR).x by A191,A192,FUNCT_1:1;
A194: x in dom (fvs*SR) by A191,A192,FUNCT_1:1;
then
A195: x in dom SR by FUNCT_1:11;
then reconsider k=x as Element of NAT;
A196: k<=len p29 by A178,A148,A176,A195,FINSEQ_3:25;
1<=k by A195,FINSEQ_3:25;
then
A197: m+k=SR.k by A9,A177,A148,A57,A196,FINSEQ_6:131;
A198: k in dom p29 by A178,A148,A176,A195,FINSEQ_3:29;
A199: SR.x in dom fvs by A194,FUNCT_1:11;
0+1<=k by A195,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A200: i<len p29 and
A201: k=i+1 by A196,FINSEQ_6:127;
p29.k = vs.(m+1+i) by A9,A87,A179,A200,A201,Lm2
.= fvs.(SR.k) by A199,A197,A201,GRFUNC_1:2
.= y by A193,A195,FUNCT_1:13;
hence p in p29 by A192,A198,FUNCT_1:1;
end;
then
A202: p29 = fvs*(Sgm DR) by TARSKI:2;
now
let i,j;
assume i in DL;
then consider k being Nat such that
A203: k=i and
1<=k and
A204: k<=n;
A205: k<m by A4,A204,XXREAL_0:2;
assume j in DR;
then consider l being Nat such that
A206: l=j and
A207: m+1<=l and
l<=len vs;
m<=m+1 by NAT_1:12;
then m<=l by A207,XXREAL_0:2;
hence i < j by A203,A206,A205,XXREAL_0:2;
end;
then
A208: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by a136,FINSEQ_3:42;
(1,1)-cut p2 = <*p2.(0+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 14;
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;
then
a244: domfvs is included_in_Seg by FINSEQ_1:def 13;
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;
a248: domfc is included_in_Seg by A248,FINSEQ_1:def 13;
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,FINSEQ_1:def 14;
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,FINSEQ_1:def 14;
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: i<len c2 and
A266: k=i+1 by A263,FINSEQ_6:127;
A267: x in dom SR by A257,A252,A262,FINSEQ_3:29;
then
A268: SR.k in rng SR by FUNCT_1:def 3;
then
A269: x in dom (fc*SR) by A258,A267,FUNCT_1:11;
then (fc*SR).x = fc.(m1+k) by A264,FUNCT_1:12
.= c.(m+i) by A258,A264,A268,A266,GRFUNC_1:2
.= y by A4,A5,A9,A210,A261,A265,A266,Lm2;
hence p in fc*(Sgm domfc) by A260,A269,FUNCT_1:1;
end;
assume
A270: p in fc*(Sgm domfc);
then consider x,y being object such that
A271: p=[x,y] by RELAT_1:def 1;
A272: y = (fc*SR).x by A270,A271,FUNCT_1:1;
A273: x in dom (fc*SR) by A270,A271,FUNCT_1:1;
then
A274: x in dom SR by FUNCT_1:11;
then reconsider k=x as Element of NAT;
A275: k<=len c2 by A257,A252,A274,FINSEQ_3:25;
1<=k by A274,FINSEQ_3:25;
then
A276: m1+k=SR.k by A242,A215,A256,A275,FINSEQ_6:131;
A277: k in dom c2 by A257,A252,A274,FINSEQ_3:29;
A278: SR.x in dom fc by A273,FUNCT_1:11;
0+1<=k by A274,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A279: i<len c2 and
A280: k=i+1 by A275,FINSEQ_6:127;
c2.k = c.(m1+1+i) by A4,A5,A9,A210,A279,A280,Lm2
.= fc.(SR.k) by A278,A276,A280,GRFUNC_1:2
.= y by A272,A274,FUNCT_1:13;
hence p in c2 by A271,A277,FUNCT_1:1;
end;
hence Seq fc = c1 by A211,TARSKI:2;
set SR = Sgm domfvs;
A281: len Sgm domfvs = card domfvs by a244,FINSEQ_3:39;
A282: m<=len c +1+1 by A5,A9,NAT_1:12;
then
A283: len p2 +m = len c +1 +1 by A4,A210,A254,Lm2;
then len p2 = len c -m +1+1;
then 1<=len p2 by A242,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;
m+lp21 = len c+1 by A283;
then
A284: card domfvs = len p2 + -1 +1 by A9,FINSEQ_6:130
.= len p2;
A285: m+lp21 = m1+len p2;
now
let p be object;
hereby
assume
A286: p in p2;
then consider x, y being object such that
A287: p=[x,y] by RELAT_1:def 1;
A288: y=p2.x by A286,A287,FUNCT_1:1;
A289: x in dom p2 by A286,A287,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A290: k<=len p2 by A289,FINSEQ_3:25;
1<=k by A289,FINSEQ_3:25;
then
A291: m1+k=SR.k by A9,A215,A283,A285,A290,FINSEQ_6:131;
0+1<=k by A289,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A292: i<len p2 and
A293: k=i+1 by A290,FINSEQ_6:127;
A294: x in dom SR by A284,A281,A289,FINSEQ_3:29;
then
A295: SR.k in rng SR by FUNCT_1:def 3;
then
A296: x in dom (fvs*SR) by A253,A294,FUNCT_1:11;
then (fvs*SR).x = fvs.(m1+k) by A291,FUNCT_1:12
.= vs.(m+i) by A253,A291,A295,A293,GRFUNC_1:2
.= y by A4,A210,A282,A254,A288,A292,A293,Lm2;
hence p in fvs*(Sgm domfvs) by A287,A296,FUNCT_1:1;
end;
assume
A297: p in fvs*(Sgm domfvs);
then consider x,y being object such that
A298: p=[x,y] by RELAT_1:def 1;
A299: y = (fvs*SR).x by A297,A298,FUNCT_1:1;
A300: x in dom (fvs*SR) by A297,A298,FUNCT_1:1;
then
A301: x in dom SR by FUNCT_1:11;
then reconsider k=x as Element of NAT;
A302: k<=len p2 by A284,A281,A301,FINSEQ_3:25;
1<=k by A301,FINSEQ_3:25;
then
A303: m1+k=SR.k by A9,A215,A283,A285,A302,FINSEQ_6:131;
A304: k in dom p2 by A284,A281,A301,FINSEQ_3:29;
A305: SR.x in dom fvs by A300,FUNCT_1:11;
0+1<=k by A301,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A306: i<len p2 and
A307: k=i+1 by A302,FINSEQ_6:127;
p2.k = vs.(m1+1+i) by A4,A210,A282,A254,A306,A307,Lm2
.= fvs.(SR.k) by A305,A303,A307,GRFUNC_1:2
.= y by A299,A301,FUNCT_1:13;
hence p in p2 by A298,A304,FUNCT_1:1;
end;
hence thesis by A226,TARSKI:2;
end;
suppose
A308: n<>1 & 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<n1 and
A359: k=i+1 by A317,A355,FINSEQ_6:127;
A360: k in domfc by A317,A356,A355;
then
A361: x in dom (fc*SL) by A309,A350,A357,FUNCT_1:11;
then (fc*SL).x = fc.k by A357,FUNCT_1:12
.= c.(1+i) by A309,A360,A359,GRFUNC_1:2
.= y by A11,A311,A316,A317,A353,A358,A359,Lm2;
hence p in fc*(Sgm domfc) by A352,A361,FUNCT_1:1;
end;
assume
A362: p in fc*(Sgm domfc);
then consider x,y being object such that
A363: p=[x,y] by RELAT_1:def 1;
A364: y = (fc*SL).x by A362,A363,FUNCT_1:1;
A365: x in dom (fc*SL) by A362,A363,FUNCT_1:1;
then
A366: (fc*SL).x = fc.(SL.x) by FUNCT_1:12;
A367: x in dom SL by A365,FUNCT_1:11;
then consider k being Nat such that
A368: k=x and
A369: 1<=k and
A370: k<=n1 by A350;
A371: k in dom fc by A309,A369,A370;
A372: k in dom c1 by A317,A369,A370,FINSEQ_3:25;
A373: k=SL.k by A349,A367,A368,FUNCT_1:18;
0+1<=k by A369;
then ex i being Nat st 0<=i & i<n1 & k=i+1 by A370,FINSEQ_6:127;
then c1.k = c.k by A11,A311,A316,A317,Lm2
.= y by A364,A366,A368,A371,A373,GRFUNC_1:2;
hence p in c1 by A363,A368,A372,FUNCT_1:1;
end;
hence Seq fc = c9 by A309,TARSKI:2;
set SL = Sgm domfvs;
A374: Sgm domfvs = idseq n by FINSEQ_3:48;
then
A375: dom Sgm domfvs = Seg n;
now
let p be object;
hereby
assume
A376: p in pp;
then consider x, y being object such that
A377: p=[x,y] by RELAT_1:def 1;
A378: y=pp.x by A376,A377,FUNCT_1:1;
A379: x in dom pp by A376,A377,FUNCT_1:1;
then reconsider k = x as Element of NAT;
A380: k<=len pp by A379,FINSEQ_3:25;
A381: 1<=k by A379,FINSEQ_3:25;
then x in dom SL by A348,A318,A375,A380;
then
A382: k=SL.k by A374,FUNCT_1:18;
0+1<=k by A379,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A383: i<n and
A384: k=i+1 by A348,A318,A380,FINSEQ_6:127;
A385: k in domfvs by A348,A318,A381,A380;
then
A386: x in dom (fvs*SL) by A331,A375,A382,FUNCT_1:11;
then (fvs*SL).x = fvs.k by A382,FUNCT_1:12
.= vs.(1+i) by A331,A385,A384,GRFUNC_1:2
.= y by A3,A333,A348,A318,A378,A383,A384,FINSEQ_6:def 4;
hence p in fvs*(Sgm domfvs) by A377,A386,FUNCT_1:1;
end;
assume
A387: p in fvs*(Sgm domfvs);
then consider x,y being object such that
A388: p=[x,y] by RELAT_1:def 1;
A389: y = (fvs*SL).x by A387,A388,FUNCT_1:1;
A390: x in dom (fvs*SL) by A387,A388,FUNCT_1:1;
then
A391: (fvs*SL).x = fvs.(SL.x) by FUNCT_1:12;
A392: x in dom SL by A390,FUNCT_1:11;
then consider k being Nat such that
A393: k=x and
A394: 1<=k and
A395: k<=n by A375;
A396: k in dom fvs by A331,A394,A395;
A397: k in dom pp by A348,A318,A394,A395,FINSEQ_3:25;
A398: k=SL.k by A374,A392,A393,FUNCT_1:18;
0+1<=k by A394;
then ex i being Nat st 0<=i & i<n & k=i+1 by A395,FINSEQ_6:127;
then pp.k = vs.k by A3,A333,A348,A318,FINSEQ_6:def 4
.= y by A389,A391,A393,A396,A398,GRFUNC_1:2;
hence p in pp by A388,A393,A397,FUNCT_1:1;
end;
hence thesis by A331,TARSKI:2;
end;
end;
theorem
vs is_vertex_seq_of c implies ex fc being Subset of c, fvs being
Subset of vs, sc, vs1 st Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc
& vs.1 = vs1.1 & vs.len vs = vs1.len vs1
proof
assume
A1: vs is_vertex_seq_of c;
per cases;
suppose
c is simple Chain of G;
then reconsider sc = c as simple Chain of G;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider fc = c as Subset of c by FINSEQ_6:152;
take fc, fvs, sc, vs;
thus Seq fc = sc & Seq fvs = vs by FINSEQ_3:116;
thus vs is_vertex_seq_of sc by A1;
thus thesis;
end;
suppose
A2: not c is simple Chain of G;
defpred P[Nat] means ex fc being Subset of c, fvs being Subset of vs, c1,
vs1 st Seq fc = c1 & Seq fvs = vs1 & vs1 is_vertex_seq_of c1 & vs.1 = vs1.1 &
vs.len vs = vs1.len vs1 & len c1 = $1 & not c1 is simple Chain of G;
P[len c qua Element of NAT]
proof
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider fc = c as Subset of c by FINSEQ_6:152;
take fc, fvs, c,vs;
thus Seq fc = c & Seq fvs = vs by FINSEQ_3:116;
thus vs is_vertex_seq_of c by A1;
thus vs.1 = vs.1 & vs.len vs = vs.len vs;
thus thesis by A2;
end;
then
A3: ex k be Nat st P[k];
consider k be Nat such that
A4: P[k] & for n being Nat st P[n] holds k<=n from NAT_1:sch 5(A3);
consider fc being Subset of c, fvs being Subset of vs, c1, vs1 such that
A5: Seq fc = c1 and
A6: Seq fvs = vs1 and
A7: vs1 is_vertex_seq_of c1 and
A8: vs.1 = vs1.1 and
A9: vs.len vs = vs1.len vs1 and
A10: len c1 = k and
A11: not c1 is simple Chain of G by A4;
consider fc1 being Subset of c1, fvs1 being Subset of vs1, c2, vs2 such
that
A12: len c2 < len c1 and
A13: vs2 is_vertex_seq_of c2 and
len vs2 < len vs1 and
A14: vs1.1 = vs2.1 and
A15: vs1.len vs1 = vs2.len vs2 and
A16: Seq fc1 = c2 and
A17: Seq fvs1 = vs2 by A7,A11,Th48;
reconsider fc9=fc|rng((Sgm dom fc)|dom fc1) as Subset of c
by FINSEQ_6:153;
reconsider fvs9=fvs|rng((Sgm dom fvs)|dom fvs1) as Subset of vs
by FINSEQ_6:153;
A18: Seq fvs9 = vs2 by A6,A17,FINSEQ_6:154;
A19: Seq fc9 = c2 by A5,A16,FINSEQ_6:154;
then c2 is simple Chain of G implies thesis by A8,A9,A13,A14,A15,A18;
hence thesis by A4,A8,A9,A10,A12,A13,A14,A15,A19,A18;
end;
end;
registration
let G;
cluster empty -> 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<m1 by A2,A3,XXREAL_0:2;
then m1 in dom q by A4,FINSEQ_3:25;
then
A5: q.m1=p.m1 by FUNCT_1:47;
n1 < len q by A3,A4,XXREAL_0:2;
then n1 in dom q by A2,FINSEQ_3:25;
then
A6: q.n1=p.n1 by FUNCT_1:47;
dom q c= dom p by RELAT_1:60;
then dom q c= Seg len p by FINSEQ_1:def 3;
then Seg len q c= Seg len p by FINSEQ_1:def 3;
then len q<=len p by FINSEQ_1:5;
then m1<=len p by A4,XXREAL_0:2;
hence q.n1 <> 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: n<m and
A3: m<=len p and
p.n = p.m;
1<m by A1,A2,XXREAL_0:2;
hence thesis by A3,FINSEQ_1:39;
end;
end;
theorem
2<len sc implies sc is Path of G
proof
assume
A1: 2 < len sc;
assume not sc is Path of G;
then consider m, n such that
A2: 1<=m and
A3: m<n and
A4: n<=len sc and
A5: sc.m = sc.n by GRAPH_1:def 16;
consider vs such that
A6: vs is_vertex_seq_of sc and
A7: for n, m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
by Def9;
A8: len vs = len sc + 1 by A6;
then
A9: n+1<=len vs by A4,XREAL_1:6;
set v29 = vs/.(n+1);
set v19 = vs/.n;
A10: 1<=n by A2,A3,XXREAL_0:2;
then
A11: sc.n joins v19, v29 by A4,A6;
A12: n<=len vs by A4,A8,NAT_1:12;
then
A13: v19=vs.n by A10,FINSEQ_4:15;
set v1 = vs/.m;
set v2 = vs/.(m+1);
m<=len sc by A3,A4,XXREAL_0:2;
then
A14: sc.m joins v1, v2 by A2,A6;
A15: n+1<=len vs by A4,A8,XREAL_1:6;
then
A16: v29=vs.(n+1) by FINSEQ_4:15,NAT_1:12;
A17: m+1<n+1 by A3,XREAL_1:6;
then
A18: m<n+1 by NAT_1:12;
then m<=len vs by A15,XXREAL_0:2;
then
A19: v1=vs.m by A2,FINSEQ_4:15;
m+1<=len vs by A17,A15,XXREAL_0:2;
then
A20: v2=vs.(m+1) by FINSEQ_4:15,NAT_1:12;
per cases by A5,A14,A11;
suppose
A21: v1=v19 & v2=v29;
then m=1 by A2,A3,A7,A12,A19,A13;
hence contradiction by A7,A17,A15,A20,A16,A21;
end;
suppose
A22: v1=v29 & v2=v19;
then
A23: n+1=len vs by A2,A7,A18,A9,A19,A16;
m=1 by A2,A7,A18,A9,A19,A16,A22;
hence contradiction by A1,A7,A8,A12,A20,A13,A22,A23;
end;
end;
theorem
sc is Path of G iff len sc = 0 or len sc = 1 or sc.1<>sc.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 & n<m & m<=len sc holds sc.n<>sc.m;
hence thesis by GRAPH_1:def 16;
end;
suppose
len sc = 1;
then for n,m st 1<=n & n<m & m<=len sc holds sc.n<>sc.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: n<m and
A8: m<=len sc;
thus sc.n<>sc.m
proof
consider vs such that
A9: vs is_vertex_seq_of sc and
A10: for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=
len vs by Def9;
set vm1 = vs/.(m+1);
A11: len vs = len sc +1 by A9;
then
A12: m+1<=len vs by A8,XREAL_1:6;
then
A13: vm1=vs.(m+1) by FINSEQ_4:15,NAT_1:12;
set vn1 = vs/.(n+1);
set vn = vs/.n;
A14: n<=len sc by A7,A8,XXREAL_0:2;
then
A15: sc.n joins vn, vn1 by A6,A9;
n+1<=len vs by A11,A14,XREAL_1:6;
then
A16: vn1=vs.(n+1) by FINSEQ_4:15,NAT_1:12;
n<=len vs by A11,A14,NAT_1:12;
then
A17: vn=vs.n by A6,FINSEQ_4:15;
set vm = vs/.m;
A18: 1<=m by A6,A7,XXREAL_0:2;
then
A19: sc.m joins vm, vm1 by A8,A9;
A20: m<=len vs by A8,A11,NAT_1:12;
then
A21: vm=vs.m by A18,FINSEQ_4:15;
assume
A22: not thesis;
per cases by A22,A15,A19;
suppose
A23: vn=vm & vn1=vm1;
A24: n+1<m+1 by A7,XREAL_1:6;
n=1 by A6,A7,A10,A20,A17,A21,A23;
hence contradiction by A10,A12,A16,A13,A23,A24;
end;
suppose
A25: vn=vm1 & vn1=vm;
thus contradiction
proof
A26: n+1<=m by A7,NAT_1:13;
A27: n+0<m+1 by A7,XREAL_1:8;
per cases by A26,XXREAL_0:1;
suppose
A28: n+1=m;
n=1 by A6,A10,A12,A17,A13,A25,A27;
hence contradiction by A5,A22,A28;
end;
suppose
A29: n+1<m;
n=1 by A6,A10,A12,A17,A13,A25,A27;
hence contradiction by A10,A20,A16,A21,A25,A29;
end;
end;
end;
end;
end;
hence thesis by GRAPH_1:def 16;
end;
end;
registration
let G;
cluster empty -> 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<len oc;
then n+1<=len oc by NAT_1:13;
then
A27: n+1 in dom oc by A23,FINSEQ_3:25;
hence vsn1 = z.(n+1) by A2,A5,A4,FINSEQ_1:def 7
.= SG.(oc.(n+1)) by A2,A5,A4,A27
.= TG.(oc.n) by A21,A26,GRAPH_1:def 15;
end;
suppose
n=len oc;
hence thesis by A2,FINSEQ_1:42;
end;
end;
A28: n<=len vs by A3,A22,NAT_1:12;
then n in dom vs by A21,FINSEQ_3:25;
then reconsider vsn = vs.n as Element of G by FINSEQ_2:11;
A29: vsn = vs/.n by A21,A28,FINSEQ_4:15;
A30: n in dom oc by A21,A22,FINSEQ_3:25;
then vsn = z.n by A2,A5,A4,FINSEQ_1:def 7
.= SG.(oc.n) by A2,A5,A4,A30;
hence oc.n joins vs/.n, vs/.(n+1) by A25,A29,A24;
end;
hence vs is_vertex_seq_of oc;
A31: 1 in dom z by A2,A6,FINSEQ_3:25;
then z.1 = SG.(oc.1) by A2;
hence thesis by A31,FINSEQ_1:def 7;
end;
uniqueness by A1,Th34;
end;