:: Oriented Simple Chains Included in Oriented Chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received August 19, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, GRAPH_1, FUNCT_1, STRUCT_0, TREES_2,
XBOOLE_0, ARYTM_3, XXREAL_0, PARTFUN1, GRAPH_2, RELAT_1, TARSKI, CARD_1,
NAT_1, ARYTM_1, ORDINAL4, GLIB_000, FINSET_1, FINSEQ_2, GRAPH_4,
NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1,
FINSEQ_2, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D,
STRUCT_0, GRAPH_1, GRAPH_2, XXREAL_0, FINSEQ_6;
constructors RECDEF_1, GRAPH_2, NAT_D, FINSEQ_2, RELSET_1, FINSEQ_6;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
ORDINAL1, CARD_1, STRUCT_0, GRAPH_1, FINSEQ_6;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities FINSEQ_2;
theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, GRAPH_1, RELAT_1, FUNCT_1,
GRFUNC_1, FUNCT_2, FINSET_1, FINSEQ_3, FINSEQ_4, GRAPH_2, XBOOLE_0,
XBOOLE_1, XREAL_1, CARD_1, XXREAL_0, ORDINAL1, NAT_D, XREAL_0, FINSEQ_6;
schemes NAT_1, FINSEQ_1, FUNCT_1;
begin :: Oriented vertex sequences and V-sets
reserve p, q for FinSequence,
e,X for set,
i, j, k, m, n for Nat,
G for Graph;
reserve x,y,v,v1,v2,v3,v4 for Element of G;
definition
let G;
let x, y;
let e;
pred e orientedly_joins x, y means
(the Source of G).e = x & (the Target of G).e = y;
end;
theorem Th1:
e orientedly_joins v1, v2 implies e joins v1, v2
by GRAPH_1:def 12;
definition
let G;
let x,y be Element of (the carrier of G);
pred x,y are_orientedly_incident means
ex v being set st v in the carrier' of G & v orientedly_joins x, y;
end;
theorem
e orientedly_joins v1,v2 & e orientedly_joins v3,v4 implies v1=v3 & v2=v4;
reserve vs, vs1, vs2 for FinSequence of the carrier of G,
c, c1, c2 for oriented Chain of G;
definition
let G, X;
func G-SVSet X -> set equals
{ v: ex e being Element of the carrier' of G st e in X &
v = (the Source of G).e };
correctness;
end;
definition
let G, X;
func G-TVSet X -> set equals
{ v: ex e being Element of the carrier' of G st e in X &
v = (the Target of G).e };
correctness;
end;
theorem
G-SVSet {} = {} & G-TVSet {} = {}
proof
set X = {};
A1: now
assume
A2: G-SVSet X<>{};
set x = the Element of G-SVSet X;
x in G-SVSet X by A2;
then ex v st ( v=x)&( ex e being Element of the carrier' of G st e
in X & v = (the Source of G).e);
hence contradiction;
end;
now
assume
A3: G-TVSet X<>{};
set x = the Element of G-TVSet X;
x in G-TVSet X by A3;
then ex v st ( v=x)&( ex e being Element of the carrier' of G st e
in X & v = (the Target of G).e);
hence contradiction;
end;
hence thesis by A1;
end;
definition
let G, vs;
let c be FinSequence;
pred vs is_oriented_vertex_seq_of c means
len vs = len c + 1 &
for n st 1<=n & n<=len c holds c.n orientedly_joins vs/.n, vs/.(n+1);
end;
theorem Th4:
vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c
proof
assume
A1: vs is_oriented_vertex_seq_of c;
then
A2: len vs = len c + 1;
for n st 1<=n & n<=len c holds c.n joins vs/.n, vs/.(n+1) by A1,Th1;
hence thesis by A2,GRAPH_2:def 6;
end;
theorem
vs is_oriented_vertex_seq_of c implies G-SVSet rng c c= rng vs
proof
assume
A1: vs is_oriented_vertex_seq_of c;
then
A2: len vs = len c + 1;
G-SVSet rng c c= rng vs
proof
let y be object;
assume y in G-SVSet rng c;
then consider v being Element of G such that
A3: v=y and
A4: ex e being Element of the carrier' of G st e in rng c & v = (the
Source of G).e;
consider e being Element of the carrier' of G such that
A5: e in rng c and
A6: v = (the Source of G).e by A4;
consider x being object such that
A7: x in dom c and
A8: e = c.x by A5,FUNCT_1:def 3;
reconsider x as Element of NAT by A7;
A9: 1<=x by A7,FINSEQ_3:25;
A10: x<=len c by A7,FINSEQ_3:25;
then
A11: x<=len vs by A2,NAT_1:12;
set v1 = vs/.x;
set v2 = vs/.(x+1);
A12: v1 = vs.x by A9,A11,FINSEQ_4:15;
c.x orientedly_joins v1, v2 by A1,A9,A10;
then
A13: v = v1 by A6,A8;
x in dom vs by A9,A11,FINSEQ_3:25;
hence thesis by A3,A12,A13,FUNCT_1:def 3;
end;
hence thesis;
end;
theorem
vs is_oriented_vertex_seq_of c implies G-TVSet rng c c= rng vs
proof
assume
A1: vs is_oriented_vertex_seq_of c;
then
A2: len vs = len c + 1;
let y be object;
assume y in G-TVSet rng c;
then consider v being Element of G such that
A3: v=y and
A4: ex e being Element of the carrier' of G st e in rng c & v = (the
Target of G).e;
consider e being Element of the carrier' of G such that
A5: e in rng c and
A6: v = (the Target of G).e by A4;
consider x being object such that
A7: x in dom c and
A8: e = c.x by A5,FUNCT_1:def 3;
reconsider x as Element of NAT by A7;
A9: 1<=x by A7,FINSEQ_3:25;
A10: x<=len c by A7,FINSEQ_3:25;
A11: 1<=x+1 by NAT_1:12;
A12: x+1<=len vs by A2,A10,XREAL_1:7;
set v1 = vs/.x;
set v2 = vs/.(x+1);
A13: v2 = vs.(x+1) by A2,A10,A11,FINSEQ_4:15,XREAL_1:7;
c.x orientedly_joins v1, v2 by A1,A9,A10;
then
A14: v = v2 by A6,A8;
x+1 in dom vs by A11,A12,FINSEQ_3:25;
hence thesis by A3,A13,A14,FUNCT_1:def 3;
end;
theorem
c <>{} & vs is_oriented_vertex_seq_of c implies
rng vs c= G-SVSet rng c \/ G-TVSet rng c
proof
assume that
A1: c <>{} and
A2: vs is_oriented_vertex_seq_of c;
A3: len vs = len c + 1 by A2;
let y be object;
assume y in rng vs;
then consider x being object such that
A4: x in dom vs and
A5: y = vs.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A4;
A6: 1<=x by A4,FINSEQ_3:25;
A7: x<=len vs by A4,FINSEQ_3:25;
per cases by A3,A7,NAT_1:8;
suppose
A8: x<=len c;
then x in dom c by A6,FINSEQ_3:25;
then
A9: 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 A9;
set v1 = vs/.x;
set v2 = vs/.(x+1);
A10: v1 = vs.x by A6,A7,FINSEQ_4:15;
c.x orientedly_joins v1, v2 by A2,A6,A8;
then
A11: v1 = (the Source of G).e;
x in dom c by A6,A8,FINSEQ_3:25;
then e in rng c by FUNCT_1:def 3;
then y in G-SVSet rng c by A5,A10,A11;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A12: x=len c+1;
set l = len c;
0+1=1;
then
A13: 1<=l by A1,NAT_1:13;
then l in dom c by FINSEQ_3:25;
then
A14: c.l in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e = c.l as Element of the carrier' of G by A14;
set v1 = vs/.l;
set v2 = vs/.(l+1);
A15: v2 = vs.(l+1) by A3,A6,A12,FINSEQ_4:15;
c.l orientedly_joins v1, v2 by A2,A13;
then
A16: v2 = (the Target of G).e;
l in dom c by A13,FINSEQ_3:25;
then e in rng c by FUNCT_1:def 3;
then y in G-TVSet rng c by A5,A12,A15,A16;
hence thesis by XBOOLE_0:def 3;
end;
end;
begin :: Cutting and glueing of oriented chains
theorem
<*v*> is_oriented_vertex_seq_of {}
by FINSEQ_1:40;
theorem Th9:
ex vs st vs is_oriented_vertex_seq_of c
proof
now per cases;
case
A1: c <>{};
defpred P[Nat,object] means
(($1=len c+1 implies $2=(the Target of G).(c.len c)) &
($1<>len c+1 implies $2=(the Source of G).(c.$1)));
A2: for k be Nat st k in Seg (len c+1) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg (len c+1);
now per cases;
case k=len c+1;
hence thesis;
end;
case k<>len c+1;
hence thesis;
end;
end;
hence thesis;
end;
ex p st dom p = Seg (len c+1) & for k be Nat st k in Seg (len c+1) holds
P[k,p.k] from FINSEQ_1:sch 1(A2);
then consider p such that
A3: dom p = Seg (len c+1) and
A4: for k be Nat st k in Seg (len c+1) holds (k=len c+1 implies p.k=(
the Target of G).(c.len c)) & (k<>len c+1 implies p.k=(the Source of G).(c.k));
A5: len p=len c+1 by A3,FINSEQ_1:def 3;
rng p c= (the carrier of G)
proof
let y be object;
assume y in rng p;
then consider x being object such that
A6: x in dom p and
A7: y=p.x by FUNCT_1:def 3;
reconsider k=x as Element of NAT by A6;
A8: 1<=k by A3,A6,FINSEQ_1:1;
A9: k<=len c+1 by A3,A6,FINSEQ_1:1;
now per cases;
case k=len c+1;
then
A10: y=(the Target of G).(c.len c) by A3,A4,A6,A7;
len c>=0+1 by A1,NAT_1:13;
then len c in Seg len c by FINSEQ_1:1;
then len c in dom c by FINSEQ_1:def 3;
then
A11: c.len c in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by FINSEQ_1:def 4;
hence thesis by A10,A11,FUNCT_2:5;
end;
case
A12: k<>len c+1;
then
A13: y=(the Source of G).(c.k) by A3,A4,A6,A7;
k<len c+1 by A9,A12,XXREAL_0:1;
then k<=len c by NAT_1:13;
then k in Seg len c by A8,FINSEQ_1:1;
then k in dom c by FINSEQ_1:def 3;
then
A14: c.k in rng c by FUNCT_1:def 3;
rng c c= the carrier' of G by FINSEQ_1:def 4;
hence thesis by A13,A14,FUNCT_2:5;
end;
end;
hence thesis;
end;
then reconsider vs=p as FinSequence of (the carrier of G) by FINSEQ_1:def 4;
for n st 1<=n & n<=len c holds c.n orientedly_joins vs/.n, vs/.(n+1)
proof
let n;
assume that
A15: 1<=n and
A16: n<=len c;
per cases;
suppose
A17: n=len c;
then
A18: n<len c+1 by NAT_1:13;
then n in Seg (len c +1) by A15,FINSEQ_1:1;
then
A19: p.n=(the Source of G).(c.n) by A4,A18;
1<n+1 by A15,NAT_1:13;
then n+1 in Seg (len c +1) by A17,FINSEQ_1:1;
then
A20: p.(n+1)=(the Target of G).(c.len c) by A4,A17;
A21: (the Source of G).(c.n) = vs/.n by A5,A15,A18,A19,FINSEQ_4:15;
1<n+1 by A15,NAT_1:13;
then (the Target of G).(c.n) = vs/.(n+1) by A5,A17,A20,FINSEQ_4:15;
hence thesis by A21;
end;
suppose n<>len c;
then
A22: n<len c by A16,XXREAL_0:1;
then n+1<=len c by NAT_1:13;
then
A23: n+1<len c+1 by NAT_1:13;
A24: n<len c+1 by A16,NAT_1:13;
then n in Seg (len c +1) by A15,FINSEQ_1:1;
then
A25: p.n=(the Source of G).(c.n) by A4,A24;
1<n+1 by A15,NAT_1:13;
then n+1 in Seg (len c +1) by A23,FINSEQ_1:1;
then
A26: p.(n+1)=(the Source of G).(c.(n+1)) by A4,A23;
A27: (the Source of G).(c.n) = vs/.n by A5,A15,A24,A25,FINSEQ_4:15;
1<n+1 by A15,NAT_1:13;
then vs/.(n+1)=p.(n+1) by A5,A23,FINSEQ_4:15;
then (the Target of G).(c.n) = vs/.(n+1) by A15,A22,A26,GRAPH_1:def 15;
hence thesis by A27;
end;
end;
then vs is_oriented_vertex_seq_of c by A5;
hence thesis;
end;
case
A28: c ={};
set x = the Element of G;
set vs=<*x*>;
len c =0 by A28;
then
A29: len vs = len c + 1 by FINSEQ_1:40;
for n st 1<=n & n<=len c holds c.n orientedly_joins vs/.n, vs/.(n+1)
by A28;
then vs is_oriented_vertex_seq_of c by A29;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th10:
c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c
implies vs1 = vs2
proof
assume that
A1: c <>{} and
A2: vs1 is_oriented_vertex_seq_of c and
A3: vs2 is_oriented_vertex_seq_of c;
A4: len vs1 = len c + 1 by A2;
A5: len vs2 = len c + 1 by A3;
for n be Nat st 1<=n & n<=len vs1 holds vs1.n=vs2.n
proof
let n be Nat;
assume that
A6: 1<=n and
A7: n<=len vs1;
A8: n<=len c +1 by A2,A7;
per cases;
suppose n<len c +1;
then
A9: n<=len c by NAT_1:13;
then c.n orientedly_joins vs1/.n, vs1/.(n+1) by A2,A6;
then
A10: (the Source of G).(c.n) = vs1/.n;
c.n orientedly_joins vs2/.n, vs2/.(n+1) by A3,A6,A9;
then
A11: (the Source of G).(c.n) = vs2/.n;
vs1.n=vs1/.n by A6,A7,FINSEQ_4:15;
hence thesis by A4,A5,A6,A7,A10,A11,FINSEQ_4:15;
end;
suppose n>=len c+1;
then
A12: n=len c+1 by A8,XXREAL_0:1;
then
A13: n-1=len c;
A14: 0+1<=len c by A1,NAT_1:13;
then
A15: n-1=n-'1 by A12,NAT_D:39;
A16: n-'1=len c by A13,A14,NAT_D:39;
then
c.(n-'1) orientedly_joins vs1/.(n-'1), vs1/.((n-'1)+1) by A2,A14;
then
A17: (the Target of G).(c.(n-'1)) = vs1/.((n-'1)+1);
c.(n-'1) orientedly_joins vs2/.(n-'1), vs2/.((n-'1)+1) by A3,A14,A16;
then
A18: (the Target of G).(c.(n-'1)) = vs2/.((n-'1)+1);
vs1.n=vs1/.n by A6,A7,FINSEQ_4:15;
hence thesis by A4,A5,A6,A7,A15,A17,A18,FINSEQ_4:15;
end;
end;
hence thesis by A4,A5,FINSEQ_1:14;
end;
definition
let G, c;
assume
A1: c <>{};
func oriented-vertex-seq c -> FinSequence of the carrier of G means
it is_oriented_vertex_seq_of c;
existence by Th9;
uniqueness by A1,Th10;
end;
theorem
vs is_oriented_vertex_seq_of c & c1 = c|Seg n & vs1= vs|Seg (n+1)
implies vs1 is_oriented_vertex_seq_of c1
proof
assume
A1: vs is_oriented_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;
A7: len c1 = n by A3,A5,FINSEQ_1:17;
A8: len vs1 = n+1 by A4,A6,FINSEQ_1:17;
thus len vs1 = len c1 + 1 by A4,A6,A7,FINSEQ_1:17;
let k be Nat;
assume that
A9: 1<=k and
A10: k<=len c1;
A11: k<=len c by A5,A7,A10,XXREAL_0:2;
k in Seg n by A7,A9,A10,FINSEQ_1:1;
then
A12: c1.k = c.k by A3,FUNCT_1:49;
A13: k<=len vs by A2,A11,NAT_1:12;
A14: k<=n+1 by A7,A10,NAT_1:12;
then
A15: k in Seg (n+1) by A9,FINSEQ_1:1;
A16: 1<=k+1 by NAT_1:12;
k+1<=len c1 +1 by A10,XREAL_1:7;
then
A17: k+1 in Seg (n+1) by A7,A16,FINSEQ_1:1;
A18: vs1.k=vs.k by A4,A15,FUNCT_1:49;
A19: vs1.(k+1)=vs.(k+1) by A4,A17,FUNCT_1:49;
A20: vs/.k=vs.k by A9,A13,FINSEQ_4:15;
A21: vs/.(k+1)=vs.(k+1) by A2,A11,A16,FINSEQ_4:15,XREAL_1:7;
A22: vs1/.k=vs1.k by A8,A9,A14,FINSEQ_4:15;
vs1/.(k+1)=vs1.(k+1) by A7,A8,A10,A16,FINSEQ_4:15,XREAL_1:7;
hence c1.k orientedly_joins vs1/.k,vs1/.(k+1)
by A1,A9,A11,A12,A18,A19,A20,A21,A22;
end;
suppose
A23: len c <=n;
then
A24: len vs<=n+1 by A2,XREAL_1:6;
A25: c1 = c by A3,A23,FINSEQ_2:20;
vs1 = vs by A4,A24,FINSEQ_2:20;
hence len vs1 = len c1 + 1 &
for k being Nat st 1<=k & k<=len c1
holds c1.k orientedly_joins vs1/.k,vs1/.(k+1) by A1,A25;
end;
end;
hence thesis;
end;
theorem Th12:
1<=m & m<=n & n<=len c & q = (m,n)-cut c implies q is oriented Chain of G
proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c and
A4: q = (m,n)-cut c;
consider vs such that
A5: vs is_oriented_vertex_seq_of c by Th9;
A6: len q +m-m=n+1-m by A1,A2,A3,A4,FINSEQ_6:def 4;
reconsider qq=q as Chain of G by A1,A2,A3,A4,GRAPH_2:41;
for n st 1 <= n & n < len q holds
(the Source of G).(q.(n+1)) = (the Target of G).(q.n)
proof
let k be Nat;
assume that
A7: 1<=k and
A8: k<len q;
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;
reconsider i = m1+k as Nat;
set v1 = vs/.i;
set v2 = vs/.(i+1);
0+1<=k by A7;
then consider j such that
0<=j and
A9: j<len q and
A10: k=j+1 by A8,FINSEQ_6:127;
A11: i= m+j by A10;
i+1= m+(j+1) by A10;
then
A12: c.(i+1)=q.(k+1) by A1,A2,A3,A4,A8,FINSEQ_6:def 4;
A13: c.i=q.k by A1,A2,A3,A4,A9,A10,A11,FINSEQ_6:def 4;
1-1<=m-1 by A1,XREAL_1:9;
then
A14: 0+1<=m-1+k by A7,XREAL_1:7;
i<=(m-1)+(n-(m-1)) by A6,A8,XREAL_1:6;
then i<=len c by A3,XXREAL_0:2;
then c.i orientedly_joins v1, v2 by A5,A14;
then
A15: (the Target of G).(c.i) = v2;
A16: 1<i+1 by A14,NAT_1:13;
k+m<n+1 by A6,A8,XREAL_1:6;
then k+m<=n by NAT_1:13;
then m+k<=len c by A3,XXREAL_0:2;
then c.(i+1) orientedly_joins v2, vs/.(i+1+1) by A5,A16;
hence thesis by A12,A13,A15;
end;
then qq is oriented by GRAPH_1:def 15;
hence thesis;
end;
theorem Th13:
1<=m & m<=n & n<=len c & c1 = (m,n)-cut c &
vs is_oriented_vertex_seq_of c & vs1 = (m,n+1)-cut vs
implies vs1 is_oriented_vertex_seq_of c1
proof
assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
assume
A4: c1 = (m,n)-cut c;
assume that
A5: vs is_oriented_vertex_seq_of c and
A6: vs1 = (m,n+1)-cut vs;
A7: len vs = len c + 1 by A5;
A8: m<=n+1 by A2,NAT_1:12;
A9: n+1<=len vs by A3,A7,XREAL_1:6;
A10: len c1 +m= n+1 by A1,A2,A3,A4,FINSEQ_6:def 4;
len vs1 +m = n+1+1 by A1,A6,A8,A9,FINSEQ_6:def 4;
hence
A11: len vs1 = len c1 + 1 by A10;
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;
set v1 = vs/.i;
set v2 = vs/.(i+1);
m+k<=len c1 +m by A13,XREAL_1:7;
then
A16: m+j+1-1<=len c1 +m-1 by A15,XREAL_1:9;
A17: 1<=i by A1,NAT_1:12;
A18: i<=len c by A3,A10,A16,XXREAL_0:2;
then
A19: c.i orientedly_joins v1, v2 by A5,A17;
j<len vs1 by A11,A14,NAT_1:13;
then
A20: vs1.k = vs.i by A1,A6,A8,A9,A15,FINSEQ_6:def 4;
A21: j+1<len vs1 by A11,A14,XREAL_1:6;
m+j+1 = m+(j+1);
then
A22: vs1.(k+1) = vs.(i+1) by A1,A6,A8,A9,A15,A21,FINSEQ_6:def 4;
A23: i<=len vs by A7,A18,NAT_1:12;
A24: 1<=i+1 by NAT_1:12;
A25: vs/.i=vs.i by A1,A23,FINSEQ_4:15,NAT_1:12;
A26: vs/.(i+1)=vs.(i+1) by A7,A18,A24,FINSEQ_4:15,XREAL_1:7;
0+1=1;
then
A27: 1<=k by A15,NAT_1:13;
A28: k<=len c1 by A14,A15,NAT_1:13;
then
A29: k<=len vs1 by A11,NAT_1:12;
A30: 1<=k+1 by NAT_1:12;
A31: vs1/.k=vs1.k by A27,A29,FINSEQ_4:15;
vs1/.(k+1)=vs1.(k+1) by A11,A28,A30,FINSEQ_4:15,XREAL_1:7;
hence thesis by A1,A2,A3,A4,A14,A15,A19,A20,A22,A25,A26,A31,FINSEQ_6:def 4;
end;
theorem Th14:
vs1 is_oriented_vertex_seq_of c1
& vs2 is_oriented_vertex_seq_of c2 & vs1.len vs1 = vs2.1
implies c1^c2 is oriented Chain of G
proof
assume that
A1: vs1 is_oriented_vertex_seq_of c1 and
A2: vs2 is_oriented_vertex_seq_of c2 and
A3: vs1.len vs1 = vs2.1;
A4: vs1 is_vertex_seq_of c1 by A1,Th4;
A5: vs2 is_vertex_seq_of c2 by A2,Th4;
A6: len vs1 = len c1 + 1 by A1;
A7: len vs2 = len c2 + 1 by A2;
set q=c1^c2;
set p=vs1^'vs2;
thus c1^c2 is oriented Chain of G
proof
reconsider cc=c1^c2 as Chain of G by A3,A4,A5,GRAPH_2:43;
for n st 1 <= n & n < len q holds
(the Source of G).(q.(n+1)) = (the Target of G).(q.n)
proof
let n;
assume that
A8: 1 <= n and
A9: n < len q;
A10: n in dom q by A8,A9,FINSEQ_3:25;
A11: n+1<=len q by A9,NAT_1:13;
A12: 1<n+1 by A8,NAT_1:13;
now per cases by A10,FINSEQ_1:25;
case
A13: n in dom c1;
then
A14: q.n = c1.n by FINSEQ_1:def 7;
set v1=vs1/.n;
set v2=vs1/.(n+1);
A15: 1<=n by A13,FINSEQ_3:25;
A16: n<=len c1 by A13,FINSEQ_3:25;
then
A17: c1.n orientedly_joins v1, v2 by A1,A15;
A18: n<=len vs1 by A6,A16,NAT_1:12;
n+1<=len c1+1 by A16,XREAL_1:6;
then
A19: n+1<=len vs1 by A1;
A20: vs1/.n=vs1.n by A15,A18,FINSEQ_4:15;
A21: vs1/.(n+1)=vs1.(n+1) by A19,FINSEQ_4:15,NAT_1:12;
A22: p.n = vs1.n by A15,A18,FINSEQ_6:140;
p.(n+1) = vs1.(n+1) by A19,FINSEQ_6:140,NAT_1:12;
hence ex v1, v2 being Element of G st
v1 = p.n & v2 = p.(n+1) & q.n orientedly_joins v1, v2 by A14,A17,A20
,A21,A22;
end;
case ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A23: k in dom c2 and
A24: n = len c1 + k;
reconsider k as Element of NAT by ORDINAL1:def 12;
A25: q.n = c2.k by A23,A24,FINSEQ_1:def 7;
A26: 1<=k by A23,FINSEQ_3:25;
A27: k<=len c2 by A23,FINSEQ_3:25;
A28: 1<=k+1 by NAT_1:12;
A29: k<=len vs2 by A7,A27,NAT_1:12;
set v1 = vs2/.k;
set v2 = vs2/.(k+1);
A30: vs2/.k=vs2.k by A26,A29,FINSEQ_4:15;
A31: vs2/.(k+1)=vs2.(k+1) by A7,A27,A28,FINSEQ_4:15,XREAL_1:7;
A32: c2.k orientedly_joins v1, v2 by A2,A26,A27;
A33: k<=len vs2 by A7,A27,NAT_1:12;
0+1<=k by A23,FINSEQ_3:25;
then consider j such that
0<=j and
A34: j<len vs2 and
A35: k=j+1 by A33,FINSEQ_6:127;
A36: p.n = vs2.k proof per cases by A26,XXREAL_0:1;
suppose
A37: 1=k;
A38: 0+1<=len vs1 by A6,NAT_1:13;
thus p.n = p.(len vs1) by A1,A24,A37
.= vs2.k by A3,A37,A38,FINSEQ_6:140;
end;
suppose 1<k;
then
A39: 1<=j by A35,NAT_1:13;
thus p.n = p.(len c1 +1+j) by A24,A35
.= p.(len vs1 +j) by A1
.= vs2.k by A34,A35,A39,FINSEQ_6:141;
end;
end;
A40: k<len vs2 by A7,A27,NAT_1:13;
p.(n+1) = p.(len c1 +1+k) by A24
.= p.(len vs1+k) by A1
.= vs2.(k+1) by A26,A40,FINSEQ_6:141;
hence ex v1, v2 being Element of G st v1 = p.n & v2 = p.(n+1)
& q.n orientedly_joins v1, v2 by A25,A30,A31,A32,A36;
end;
end;
then consider v1,v2 being Element of G such that
v1=p.n and
A41: v2=p.(n+1) and
A42: q.n orientedly_joins v1,v2;
A43: n+1 in dom q by A11,A12,FINSEQ_3:25;
A44: now per cases by A43,FINSEQ_1:25;
case
A45: n+1 in dom c1;
then
A46: q.(n+1) = c1.(n+1) by FINSEQ_1:def 7;
set v29=vs1/.(n+1),v3=vs1/.(n+1+1);
A47: 1<=n+1 by A45,FINSEQ_3:25;
A48: n+1<=len c1 by A45,FINSEQ_3:25;
then
A49: c1.(n+1) orientedly_joins v29, v3 by A1,A47;
A50: n+1<=len vs1 by A6,A48,NAT_1:12;
n+1+1<=len c1+1 by A48,XREAL_1:6;
then
A51: n+1+1<=len vs1 by A1;
A52: vs1/.(n+1)=vs1.(n+1) by A47,A50,FINSEQ_4:15;
A53: vs1/.(n+1+1)=vs1.(n+1+1) by A51,FINSEQ_4:15,NAT_1:12;
A54: p.(n+1) = vs1.(n+1) by A47,A50,FINSEQ_6:140;
p.(n+1+1) = vs1.(n+1+1) by A51,FINSEQ_6:140,NAT_1:12;
hence ex v299,v39 being Element of G st
v299 = p.(n+1) & v39 = p.(n+1+1)
& q.(n+1) orientedly_joins v299, v39 by A46,A49,A52,A53,A54;
end;
case ex k being Nat st k in dom c2 & (n+1)=len c1 + k;
then consider k being Nat such that
A55: k in dom c2 and
A56: (n+1) = len c1 + k;
reconsider k as Element of NAT by ORDINAL1:def 12;
A57: q.(n+1) = c2.k by A55,A56,FINSEQ_1:def 7;
A58: 1<=k by A55,FINSEQ_3:25;
A59: k<=len c2 by A55,FINSEQ_3:25;
A60: 1<=k+1 by NAT_1:12;
A61: k<=len vs2 by A7,A59,NAT_1:12;
set v29=vs2/.k, v3 = vs2/.(k+1);
A62: vs2/.k=vs2.k by A58,A61,FINSEQ_4:15;
A63: vs2/.(k+1)=vs2.(k+1) by A7,A59,A60,FINSEQ_4:15,XREAL_1:7;
A64: c2.k orientedly_joins v29, v3 by A2,A58,A59;
A65: k<=len vs2 by A7,A59,NAT_1:12;
0+1<=k by A55,FINSEQ_3:25;
then consider j such that
0<=j and
A66: j<len vs2 and
A67: k=j+1 by A65,FINSEQ_6:127;
A68: p.(n+1) = vs2.k proof per cases by A58,XXREAL_0:1;
suppose
A69: 1=k;
A70: 0+1<=len vs1 by A6,NAT_1:13;
thus p.(n+1) = p.(len vs1) by A1,A56,A69
.= vs2.k by A3,A69,A70,FINSEQ_6:140;
end;
suppose 1<k;
then
A71: 1<=j by A67,NAT_1:13;
thus p.(n+1) = p.(len c1 +1+j) by A56,A67
.= p.(len vs1 +j) by A1
.= vs2.k by A66,A67,A71,FINSEQ_6:141;
end;
end;
A72: k<len vs2 by A7,A59,NAT_1:13;
p.((n+1)+1) = p.(len c1 +1+k) by A56
.= p.(len vs1+k) by A1
.= vs2.(k+1) by A58,A72,FINSEQ_6:141;
hence ex v299,v39 being Element of G st
v299 = p.(n+1) & v39 = p.((n+1)+1)
& q.(n+1) orientedly_joins v299, v39 by A57,A62,A63,A64,A68;
end;
end;
(the Target of G).(q.n) = v2 by A42;
hence thesis by A41,A44;
end;
then cc is oriented by GRAPH_1:def 15;
hence thesis;
end;
end;
theorem Th15:
vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2
& vs1.len vs1 = vs2.1 & c = c1^c2 & vs = vs1^'vs2
implies vs is_oriented_vertex_seq_of c
proof
assume that
A1: vs1 is_oriented_vertex_seq_of c1 and
A2: vs2 is_oriented_vertex_seq_of c2 and
A3: vs1.len vs1 = vs2.1;
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
A8: vs2 <> {};
set q=c1^c2;
set p=vs1^'vs2;
len p +1 = len vs1 +len vs2 by A8,FINSEQ_6:139;
then
A9: 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
A10: 1<=n and
A11: n<=len q;
A12: n<=len p by A9,A11,NAT_1:12;
A13: 1<=n+1 by NAT_1:12;
A14: p/.n=p.n by A10,A12,FINSEQ_4:15;
A15: p/.(n+1)=p.(n+1) by A9,A11,A13,FINSEQ_4:15,XREAL_1:7;
A16: n in dom q by A10,A11,FINSEQ_3:25;
per cases by A16,FINSEQ_1:25;
suppose
A17: n in dom c1;
set v1=vs1/.n;
set v2=vs1/.(n+1);
A18: 1<=n by A17,FINSEQ_3:25;
A19: n<=len c1 by A17,FINSEQ_3:25;
then
A20: c1.n orientedly_joins v1, v2 by A1,A18;
A21: n<=len vs1 by A6,A19,NAT_1:12;
n+1<=len c1+1 by A19,XREAL_1:6;
then
A22: n+1<=len vs1 by A1;
A23: vs1/.n=vs1.n by A18,A21,FINSEQ_4:15;
A24: vs1/.(n+1)=vs1.(n+1) by A22,FINSEQ_4:15,NAT_1:12;
A25: p.n = vs1.n by A18,A21,FINSEQ_6:140;
p.(n+1) = vs1.(n+1) by A22,FINSEQ_6:140,NAT_1:12;
hence q.n orientedly_joins p/.n, p/.(n+1)
by A14,A15,A17,A20,A23,A24,A25,FINSEQ_1:def 7;
end;
suppose ex k being Nat st k in dom c2 & n=len c1 + k;
then consider k being Nat such that
A26: k in dom c2 and
A27: n = len c1 + k;
reconsider k as Element of NAT by ORDINAL1:def 12;
A28: q.n = c2.k by A26,A27,FINSEQ_1:def 7;
A29: 1<=k by A26,FINSEQ_3:25;
A30: k<=len c2 by A26,FINSEQ_3:25;
A31: 1<=k+1 by NAT_1:12;
k<=len vs2 by A7,A30,NAT_1:12;
then
A32: vs2/.k=vs2.k by A29,FINSEQ_4:15;
A33: vs2/.(k+1)=vs2.(k+1) by A7,A30,A31,FINSEQ_4:15,XREAL_1:7;
A34: k<=len vs2 by A7,A30,NAT_1:12;
0+1<=k by A26,FINSEQ_3:25;
then consider j such that
0<=j and
A35: j<len vs2 and
A36: k=j+1 by A34,FINSEQ_6:127;
A37: p.n = vs2.k proof per cases by A29,XXREAL_0:1;
suppose
A38: 1=k;
A39: 0+1<=len vs1 by A6,NAT_1:13;
thus p.n = p.(len vs1) by A1,A27,A38
.= vs2.k by A3,A38,A39,FINSEQ_6:140;
end;
suppose 1<k;
then
A40: 1<=j by A36,NAT_1:13;
thus p.n = p.(len c1 +1+j) by A27,A36
.= p.(len vs1 +j) by A1
.= vs2.k by A35,A36,A40,FINSEQ_6:141;
end;
end;
A41: k<len vs2 by A7,A30,NAT_1:13;
p.(n+1) = p.(len c1 +1+k) by A27
.= p.(len vs1+k) by A1
.= vs2.(k+1) by A29,A41,FINSEQ_6:141;
hence q.n orientedly_joins p/.n,p/.(n+1) by A2,A14,A15,A28,A29,A30,A32
,A33,A37;
end;
end;
hence thesis by A4,A5,A9;
end;
begin :: Oriented simple chains in oriented chains
Lm1: <*v*> is_oriented_vertex_seq_of {}
by FINSEQ_1:39;
definition
let G;
let IT be oriented Chain of G;
attr IT is Simple means
:Def7:
ex vs st vs is_oriented_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 oriented Chain of G;
existence
proof set q = the empty oriented Chain of G;
set x = the Element of G;
reconsider p =<*x*> as FinSequence of the carrier of G;
A1: p is_oriented_vertex_seq_of q by Lm1;
for n,m st 1<=n & n<m & m<=len p & p.n=p.m holds n=1 & m=len p
proof
let n,m;
assume that
A2: 1<=n and
A3: n<m and
A4: m<=len p and p.n = p.m;
1<m by A2,A3,XXREAL_0:2;
hence thesis by A4,FINSEQ_1:39;
end;
then q is Simple by A1;
hence thesis;
end;
end;
registration
let G;
cluster oriented simple for Chain of G;
existence
proof set q = the empty oriented Chain of G;
set x = the Element of G;
reconsider p =<*x*> as FinSequence of the carrier of G;
A1: p is_vertex_seq_of q by Lm1,Th4;
reconsider q9=q as Chain of G;
for n,m st 1<=n & n<m & m<=len p & p.n=p.m holds n=1 & m=len p
proof
let n,m;
assume that
A2: 1<=n and
A3: n<m and
A4: m<=len p and p.n = p.m;
1<m by A2,A3,XXREAL_0:2;
hence thesis by A4,FINSEQ_1:39;
end;
then q9 is simple by A1,GRAPH_2:def 9;
hence thesis;
end;
end;
theorem Th16:
for q being oriented Chain of G holds q|(Seg n) is oriented Chain of G
proof
let q be oriented Chain of G;
reconsider q9= q|(Seg n) as FinSequence;
for i st 1 <= i & i < len q9 holds (the Source of G).((q|(Seg n)).(i+1))
= (the Target of G).((q|(Seg n)).i)
proof
let i;
assume that
A1: 1 <= i and
A2: i < len q9;
per cases;
suppose n>=len q;
then q|(Seg n)=q by FINSEQ_3:49;
hence thesis by A1,A2,GRAPH_1:def 15;
end;
suppose
A3: n<len q;
then
A4: len q9=n by FINSEQ_1:17;
then
A5: i<len q by A2,A3,XXREAL_0:2;
i in Seg n by A1,A2,A4,FINSEQ_1:1;
then
A6: (q|(Seg n)).i=q.i by FUNCT_1:49;
A7: i+1<=n by A2,A4,NAT_1:13;
1<i+1 by A1,NAT_1:13;
then i+1 in Seg n by A7,FINSEQ_1:1;
then (q|(Seg n)).(i+1)=q.(i+1) by FUNCT_1:49;
hence thesis by A1,A5,A6,GRAPH_1:def 15;
end;
end;
hence thesis by GRAPH_1:4,def 15;
end;
reserve sc for oriented simple Chain of G;
theorem
sc|(Seg n) is oriented simple Chain of G by Th16,GRAPH_2:45;
theorem Th18:
for sc9 being oriented Chain of G st sc9=sc holds sc9 is Simple
proof
let sc9 be oriented Chain of G;
assume
A1: sc9=sc;
consider vs such that
A2: vs is_oriented_vertex_seq_of sc9 by Th9;
vs is_vertex_seq_of sc by A1,A2,Th4;
then for n, m st 1<=n & n<m & m<=len vs & vs.n = vs.m holds n=1 & m=len vs
by GRAPH_2:47;
hence thesis by A2;
end;
theorem Th19:
for sc9 being Simple oriented Chain of G
holds sc9 is oriented simple Chain of G
proof
let sc9 be Simple oriented Chain of G;
consider vs such that
A1: vs is_oriented_vertex_seq_of sc9 and
A2: for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs by Def7;
vs is_vertex_seq_of sc9 by A1,Th4;
hence thesis by A2,GRAPH_2:def 9;
end;
reserve x,y for set;
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)
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;
A7: not(1<=m & m<=n & n<=len p) by A5,XREAL_1:29;
(m, n)-cut p = {} by A6,FINSEQ_6:def 4;
hence len (m, n)-cut p +m = n+1 by A5;
thus thesis by A7,CARD_1:27,FINSEQ_6:def 4;
end;
suppose m<=n;
hence thesis by A1,A3,FINSEQ_6:def 4;
end;
end;
theorem Th20:
not c is Simple & vs is_oriented_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_oriented_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 and
A2: vs is_oriented_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;
A8: len vs = len c + 1 by A2;
A9: m-n>n-n by A4,XREAL_1:9;
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;
A12: n1+1 = n-1+1 by A10,XREAL_0:def 2
.= n;
per cases by A7;
suppose
A13: n<>1 & m <> len vs;
then 1 < n by A3,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A14: 1+1-1<=n-1 by XREAL_1:9;
n < len vs by A4,A5,XXREAL_0:2;
then
A15: n-1 < len c +1-1 by A8,XREAL_1:9;
A16: 1<=n1+1 by NAT_1:12;
A17: m < len vs by A5,A13,XXREAL_0:1;
then
A18: m<=len c by A8,NAT_1:13;
A19: 1<=m by A3,A4,XXREAL_0:2;
A20: m<=len c by A8,A17,NAT_1:13;
reconsider c1 = (1,n1)-cut c as oriented Chain of G by A11,A14,A15,Th12;
reconsider c2 = (m,len c)-cut c as oriented Chain of G by A19,A20,Th12;
set pp = (1,n)-cut vs;
set p2 = (m,len c+1)-cut vs;
set p29 = (m+1, len c +1)-cut vs;
reconsider pp as FinSequence of the carrier of G;
reconsider p2 as FinSequence of the carrier of G;
A21: n<=len vs by A4,A5,XXREAL_0:2;
A22: 1<=m by A3,A4,XXREAL_0:2;
A23: m<=len c + 1 by A2,A5;
A24: len c + 1<=len vs by A2;
A25: pp is_oriented_vertex_seq_of c1 by A2,A12,A14,A15,Th13;
A26: p2 is_oriented_vertex_seq_of c2 by A2,A19,A20,Th13;
A27: len pp = len c1 + 1 by A25;
A28: len p2 = len c2 + 1 by A26;
1-1<=m-1 by A19,XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A29: m = m1 +1;
A30: len c2 +m = len c +1 by A19,A20,FINSEQ_6:def 4;
A31: m-m<=len c -m by A18,XREAL_1:9;
then len c2 -'1 = len c2 -1 by A30,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
A32: m+lc21 = m1+len c2;
0+1=1;
then
A33: 1<=len p2 by A28,NAT_1:13;
A34: p2 = (0+1, len p2)-cut p2 by FINSEQ_6:133
.= (0+1, 1)-cut p2 ^ (1+1, len p2)-cut p2 by A33,FINSEQ_6:134;
m1<=m by A29,NAT_1:12;
then
A35: p2 = (m1+1, m)-cut vs ^ (m+1, len c +1)-cut vs by A5,A8,FINSEQ_6:134;
(1,1)-cut p2 = <*p2.(0+1)*> by A33,FINSEQ_6:132
.= <*vs.(m+0)*> by A22,A23,A24,A28,FINSEQ_6:def 4
.= (m,m)-cut vs by A5,A19,FINSEQ_6:132;
then
A36: p29 = (2, len p2)-cut p2 by A34,A35,FINSEQ_1:33;
set domfc = {k where k is Nat: 1<=k & k<=n1 or m<=k & k<= len c};
deffunc F(object) = c.$1;
consider fc being Function such that
A37: dom fc = domfc and
A38: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A39: x = kk and
A40: 1<=kk & kk<=n1 or m<=kk & kk<= len c;
A41: 1<=kk by A19,A40,XXREAL_0:2;
kk<=len c by A11,A15,A40,XXREAL_0:2;
hence thesis by A39,A41,FINSEQ_1:1;
end;
then reconsider fc as FinSubsequence by A37,FINSEQ_1:def 12;
fc c= c
proof
let p be object;
assume
A42: p in fc;
then consider x, y being object such that
A43: [x,y] = p by RELAT_1:def 1;
A44: x in dom fc by A42,A43,FUNCT_1:1;
A45: y = fc.x by A42,A43,FUNCT_1:1;
consider kk being Nat such that
A46: x = kk and
A47: 1<=kk & kk<=n1 or m<=kk & kk<= len c by A37,A44;
A48: 1<=kk by A19,A47,XXREAL_0:2;
kk<=len c by A11,A15,A47,XXREAL_0:2;
then
A49: x in dom c by A46,A48,FINSEQ_3:25;
y = c.kk by A37,A38,A44,A45,A46;
hence thesis by A43,A46,A49,FUNCT_1:1;
end;
then reconsider fc as Subset of c;
take fc;
set domfvs = {k where k is Nat: 1<=k & k<=n or m+1<=k & k<= len vs};
deffunc F(object) = vs.$1;
consider fvs being Function such that
A50: dom fvs = domfvs and
A51: 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
A52: x = kk and
A53: 1<=kk & kk<=n or m+1<=kk & kk<= len vs;
1<=m+1 by NAT_1:12;
then
A54: 1<=kk by A53,XXREAL_0:2;
kk<=len vs by A21,A53,XXREAL_0:2;
hence thesis by A52,A54,FINSEQ_1:1;
end;
then reconsider fvs as FinSubsequence by A50,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A55: p in fvs;
then consider x, y being object such that
A56: [x,y] = p by RELAT_1:def 1;
A57: x in dom fvs by A55,A56,FUNCT_1:1;
A58: y = fvs.x by A55,A56,FUNCT_1:1;
consider kk being Nat such that
A59: x = kk and
A60: 1<=kk & kk<=n or m+1<=kk & kk<= len vs by A50,A57;
1<=m+1 by NAT_1:12;
then
A61: 1<=kk by A60,XXREAL_0:2;
kk<=len vs by A21,A60,XXREAL_0:2;
then
A62: x in dom vs by A59,A61,FINSEQ_3:25;
y = vs.kk by A50,A51,A57,A58,A59;
hence thesis by A56,A59,A62,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
take fvs;
A63: p2.1 = vs.m by A22,A23,A24,FINSEQ_6:138;
A64: pp.len pp = vs.n by A3,A21,FINSEQ_6:138;
then reconsider c9 = c1^c2 as oriented Chain of G by A6,A25,A26,A63,Th14;
take c9;
take p1=pp^'p2;
A65: p1 = pp^p29 by A36,FINSEQ_6:def 5;
A66: len c1 +1 = n1+1 by A11,A15,A16,Lm2;
-(-(m-n)) = m-n;
then
A67: -(m-n) < 0 by A9;
len c9 = (n-1)+(len c -m+1) by A11,A30,A66,FINSEQ_1:22
.= len c + (n+ -m );
hence
A68: len c9 < len c by A67,XREAL_1:30;
thus p1 is_oriented_vertex_seq_of c9 by A6,A25,A26,A63,A64,Th15;
then len p1 = len c9 + 1;
hence len p1 < len vs by A8,A68,XREAL_1:6;
1<=1 + len c1 by NAT_1:12;
then 1<=len pp by A25;
then p1.1 = pp.1 by FINSEQ_6:140;
hence vs.1 = p1.1 by A3,A21,FINSEQ_6:138;
A69: p2.len p2 = vs.(len c + 1) by A22,A23,A24,FINSEQ_6:138;
m-m<=len c -m by A20,XREAL_1:9;
then 0+1<=len c -m+1 by XREAL_1:6;
then 1<len p2 by A28,A30,NAT_1:13;
hence vs.len vs = p1.len p1 by A8,A69,FINSEQ_6:142;
set DL = {kk where kk is Nat: 1<=kk & kk<=n1};
set DR = {kk where kk is Nat: m<=kk & kk<= len c};
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
A70: x in DL \/ DR;
per cases by A70,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
A71: domfc = DL \/ DR by TARSKI:2;
A72: 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
A73: x=k and
A74: 1<=k and
A75: k<=n1;
k<=len c by A11,A15,A75,XXREAL_0:2;
hence x in Seg len c by A73,A74,FINSEQ_1:1;
end;
let x be object;
assume x in DR;
then consider k being Nat such that
A76: x=k and
A77: m<=k and
A78: k<=len c;
1<=k by A22,A77,XXREAL_0:2;
hence thesis by A76,A78,FINSEQ_1:1;
end;
then reconsider DL as finite set by FINSET_1:1;
a72: DL is included_in_Seg & DR is included_in_Seg by A72,FINSEQ_1:def 13;
reconsider DR as finite set by A72,FINSET_1:1;
now
let i,j;
assume i in DL;
then consider k being Nat such that
A79: k=i and 1<=k and
A80: k<=n1;
assume j in DR;
then
A81: ex l being Nat st ( l=j)&( m<=l)&( l<=len c);
n1<m by A4,A12,NAT_1:13;
then k<m by A80,XXREAL_0:2;
hence i < j by A79,A81,XXREAL_0:2;
end;
then
A82: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by a72,FINSEQ_3:42;
m+lc21 = len c by A30;
then
A83: card DR = len c2 + -1 +1 by FINSEQ_6:130
.= len c2;
A84: len Sgm DR = card DR by a72,FINSEQ_3:39;
DL = Seg n1 by FINSEQ_1:def 1;
then
A85: Sgm DL = idseq n1 by FINSEQ_3:48;
then
A86: dom Sgm DL = Seg n1;
rng Sgm DL = DL by a72,FINSEQ_1:def 14;
then
A87: rng Sgm DL c= dom fc by A37,A71,XBOOLE_1:7;
rng Sgm DR = DR by a72,FINSEQ_1:def 14;
then
A88: rng Sgm DR c= dom fc by A37,A71,XBOOLE_1:7;
set SL = Sgm DL;
set SR = Sgm DR;
now
let p be object;
hereby
assume
A89: p in c1;
then consider x, y being object such that
A90: p=[x,y] by RELAT_1:def 1;
A91: x in dom c1 by A89,A90,FUNCT_1:1;
A92: y=c1.x by A89,A90,FUNCT_1:1;
reconsider k = x as Element of NAT by A91;
A93: 1<=k by A91,FINSEQ_3:25;
A94: k<=len c1 by A91,FINSEQ_3:25;
then
A95: x in dom SL by A66,A86,A93,FINSEQ_1:1;
then
A96: k=SL.k by A85,FUNCT_1:18;
A97: k in domfc by A66,A93,A94;
then
A98: x in dom (fc*SL) by A37,A95,A96,FUNCT_1:11;
0+1<=k by A91,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A99: i<n1 and
A100: k=i+1 by A66,A94,FINSEQ_6:127;
(fc*SL).x = fc.k by A96,A98,FUNCT_1:12
.= c.(1+i) by A37,A97,A100,GRFUNC_1:2
.= y by A11,A15,A16,A66,A92,A99,A100,Lm2;
hence p in fc*(Sgm DL) by A90,A98,FUNCT_1:1;
end;
assume
A101: p in fc*(Sgm DL);
then consider x,y being object such that
A102: p=[x,y] by RELAT_1:def 1;
A103: x in dom (fc*SL) by A101,A102,FUNCT_1:1;
A104: y = (fc*SL).x by A101,A102,FUNCT_1:1;
A105: (fc*SL).x = fc.(SL.x) by A103,FUNCT_1:12;
A106: x in dom SL by A103,FUNCT_1:11;
then x in {kk where kk is Nat: 1<=kk & kk<=n1}
by A86,FINSEQ_1:def 1;
then consider k being Nat such that
A107: k=x and
A108: 1<=k and
A109: k<=n1;
A110: k in dom fc by A37,A108,A109;
A111: k=SL.k by A85,A106,A107,FUNCT_1:18;
A112: k in dom c1 by A66,A108,A109,FINSEQ_3:25;
0+1<=k by A108;
then ex i being Nat st ( 0<=i)&( i<n1)&( k=i+1) by A109,
FINSEQ_6:127;
then c1.k = c.k by A11,A15,A16,A66,Lm2
.= y by A104,A105,A107,A110,A111,GRFUNC_1:2;
hence p in c1 by A102,A107,A112,FUNCT_1:1;
end;
then
A113: c1 = fc*(Sgm DL) by TARSKI:2;
now
let p be object;
hereby
assume
A114: p in c2;
then consider x, y being object such that
A115: p=[x,y] by RELAT_1:def 1;
A116: x in dom c2 by A114,A115,FUNCT_1:1;
A117: y=c2.x by A114,A115,FUNCT_1:1;
reconsider k = x as Element of NAT by A116;
A118: 1<=k by A116,FINSEQ_3:25;
A119: k<=len c2 by A116,FINSEQ_3:25;
A120: x in dom SR by A83,A84,A116,FINSEQ_3:29;
A121: m1+k=SR.k by A29,A30,A32,A118,A119,FINSEQ_6:131;
A122: SR.k in rng SR by A120,FUNCT_1:def 3;
then
A123: x in dom (fc*SR) by A88,A120,FUNCT_1:11;
0+1<=k by A116,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A124: i<len c2 and
A125: k=i+1 by A119,FINSEQ_6:127;
(fc*SR).x = fc.(m1+k) by A121,A123,FUNCT_1:12
.= c.(m+i) by A88,A121,A122,A125,GRFUNC_1:2
.= y by A19,A20,A117,A124,A125,FINSEQ_6:def 4;
hence p in fc*(Sgm DR) by A115,A123,FUNCT_1:1;
end;
assume
A126: p in fc*(Sgm DR);
then consider x,y being object such that
A127: p=[x,y] by RELAT_1:def 1;
A128: x in dom (fc*SR) by A126,A127,FUNCT_1:1;
A129: y = (fc*SR).x by A126,A127,FUNCT_1:1;
A130: x in dom SR by A128,FUNCT_1:11;
A131: SR.x in dom fc by A128,FUNCT_1:11;
reconsider k=x as Element of NAT by A130;
A132: k in dom c2 by A83,A84,A130,FINSEQ_3:29;
A133: 1<=k by A130,FINSEQ_3:25;
A134: k<=len c2 by A83,A84,A130,FINSEQ_3:25;
then
A135: m1+k=SR.k by A29,A30,A32,A133,FINSEQ_6:131;
0+1<=k by A130,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A136: i<len c2 and
A137: k=i+1 by A134,FINSEQ_6:127;
c2.k = c.(m1+1+i) by A19,A20,A136,A137,FINSEQ_6:def 4
.= fc.(SR.k) by A131,A135,A137,GRFUNC_1:2
.= y by A129,A130,FUNCT_1:13;
hence p in c2 by A127,A132,FUNCT_1:1;
end;
then
A138: c2 = fc*(Sgm DR) by TARSKI:2;
Seq fc = fc*((Sgm DL)^(Sgm DR)) by A37,A71,A82,FINSEQ_1:def 15;
hence Seq fc = c9 by A87,A88,A113,A138,FINSEQ_6:150;
set DL = {kk where kk is Nat: 1<=kk & kk<=n};
set DR = {kk where kk is Nat: m+1<=kk & kk<= len vs};
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
A139: x in DL \/ DR;
per cases by A139,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
A140: domfvs = DL \/ DR by TARSKI:2;
A141: 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
A142: x=k and
A143: 1<=k and
A144: k<=n;
k<=len vs by A21,A144,XXREAL_0:2;
hence x in Seg len vs by A142,A143,FINSEQ_1:1;
end;
let x be object;
assume x in DR;
then consider k being Nat such that
A145: x=k and
A146: m+1<=k and
A147: k<=len vs;
1<=m+1 by NAT_1:12;
then 1<=k by A146,XXREAL_0:2;
hence thesis by A145,A147,FINSEQ_1:1;
end;
then reconsider DL as finite set by FINSET_1:1;
a141: DL is included_in_Seg & DR is included_in_Seg by A141,FINSEQ_1:def 13;
reconsider DR as finite set by A141,FINSET_1:1;
now
let i,j;
assume i in DL;
then consider k being Nat such that
A148: k=i and 1<=k and
A149: k<=n;
assume j in DR;
then consider l being Nat such that
A150: l=j and
A151: m+1<=l and l<=len vs;
m<=m+1 by NAT_1:12;
then
A152: m<=l by A151,XXREAL_0:2;
k<m by A4,A149,XXREAL_0:2;
hence i < j by A148,A150,A152,XXREAL_0:2;
end;
then
A153: Sgm (DL \/ DR) = (Sgm DL)^(Sgm DR) by a141,FINSEQ_3:42;
1<=len p2 by A28,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;
lp21 -'1 = lp21 -1 by A28,A30,A31,XREAL_0:def 2;
then reconsider lp22 = lp21 -1 as Element of NAT;
A154: m+1+lp22 = m+((lp21 -1)+1) .= m+(len c -m +1 +1 -1) by A26,A30
.= len c +1;
then
A155: card DR = lp22 + 1 by A8,FINSEQ_6:130
.= lp21;
A156: 1<=m+1 by NAT_1:12;
A157: m+1<=len c +1+1 by A23,XREAL_1:6;
A158: len p2 +m = len c +1+1 by A22,A23,A24,FINSEQ_6:def 4
.= len p29 +(m+1) by A24,A156,A157,Lm2
.= (len p29+1)+m;
A159: len Sgm DR = card DR by a141,FINSEQ_3:39;
DL = Seg n by FINSEQ_1:def 1;
then
A160: Sgm DL = idseq n by FINSEQ_3:48;
then
A161: dom Sgm DL = Seg n;
rng Sgm DL = DL by a141,FINSEQ_1:def 14;
then
A162: rng Sgm DL c= dom fvs by A50,A140,XBOOLE_1:7;
rng Sgm DR = DR by a141,FINSEQ_1:def 14;
then
A163: rng Sgm DR c= dom fvs by A50,A140,XBOOLE_1:7;
set SL = Sgm DL;
set SR = Sgm DR;
now
let p be object;
hereby
assume
A164: p in pp;
then consider x, y being object such that
A165: p=[x,y] by RELAT_1:def 1;
A166: x in dom pp by A164,A165,FUNCT_1:1;
A167: y=pp.x by A164,A165,FUNCT_1:1;
reconsider k = x as Element of NAT by A166;
A168: 1<=k by A166,FINSEQ_3:25;
A169: k<=len pp by A166,FINSEQ_3:25;
then
A170: x in dom SL by A11,A27,A66,A161,A168,FINSEQ_1:1;
then
A171: k=SL.k by A160,FUNCT_1:18;
A172: k in domfvs by A11,A27,A66,A168,A169;
then
A173: x in dom (fvs*SL) by A50,A170,A171,FUNCT_1:11;
0+1<=k by A166,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A174: i<n and
A175: k=i+1 by A11,A27,A66,A169,FINSEQ_6:127;
(fvs*SL).x = fvs.k by A171,A173,FUNCT_1:12
.= vs.(1+i) by A50,A172,A175,GRFUNC_1:2
.= y by A3,A11,A21,A27,A66,A167,A174,A175,FINSEQ_6:def 4;
hence p in fvs*(Sgm DL) by A165,A173,FUNCT_1:1;
end;
assume
A176: p in fvs*(Sgm DL);
then consider x,y being object such that
A177: p=[x,y] by RELAT_1:def 1;
A178: x in dom (fvs*SL) by A176,A177,FUNCT_1:1;
A179: y = (fvs*SL).x by A176,A177,FUNCT_1:1;
A180: (fvs*SL).x = fvs.(SL.x) by A178,FUNCT_1:12;
A181: x in dom SL by A178,FUNCT_1:11;
then x in {kk where kk is Nat: 1<=kk & kk<=n}
by A161,FINSEQ_1:def 1;
then consider k being Nat such that
A182: k=x and
A183: 1<=k and
A184: k<=n;
A185: k in dom fvs by A50,A183,A184;
A186: k=SL.k by A160,A181,A182,FUNCT_1:18;
A187: k in dom pp by A11,A27,A66,A183,A184,FINSEQ_3:25;
0+1<=k by A183;
then ex i being Nat st ( 0<=i)&( i<n)&( k=i+1) by A184,
FINSEQ_6:127;
then pp.k = vs.k by A3,A11,A21,A27,A66,FINSEQ_6:def 4
.= y by A179,A180,A182,A185,A186,GRFUNC_1:2;
hence p in pp by A177,A182,A187,FUNCT_1:1;
end;
then
A188: pp = fvs*(Sgm DL) by TARSKI:2;
A189: m+1+lp22 = m+lp21;
A190: 1<=m+1 by NAT_1:12;
A191: m+1<=len c +1+1 by A5,A8,XREAL_1:7;
now
let p be object;
hereby
assume
A192: p in p29;
then consider x, y being object such that
A193: p=[x,y] by RELAT_1:def 1;
A194: x in dom p29 by A192,A193,FUNCT_1:1;
A195: y=p29.x by A192,A193,FUNCT_1:1;
reconsider k = x as Element of NAT by A194;
A196: 1<=k by A194,FINSEQ_3:25;
A197: k<=len p29 by A194,FINSEQ_3:25;
A198: x in dom SR by A155,A158,A159,A194,FINSEQ_3:29;
A199: m+k=SR.k by A8,A154,A158,A189,A196,A197,FINSEQ_6:131;
A200: SR.k in rng SR by A198,FUNCT_1:def 3;
then
A201: x in dom (fvs*SR) by A163,A198,FUNCT_1:11;
0+1<=k by A194,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A202: i<len p29 and
A203: k=i+1 by A197,FINSEQ_6:127;
(fvs*SR).x = fvs.(m+k) by A199,A201,FUNCT_1:12
.= vs.(m+1+i) by A163,A199,A200,A203,GRFUNC_1:2
.= y by A8,A190,A191,A195,A202,A203,Lm2;
hence p in fvs*(Sgm DR) by A193,A201,FUNCT_1:1;
end;
assume
A204: p in fvs*(Sgm DR);
then consider x,y being object such that
A205: p=[x,y] by RELAT_1:def 1;
A206: x in dom (fvs*SR) by A204,A205,FUNCT_1:1;
A207: y = (fvs*SR).x by A204,A205,FUNCT_1:1;
A208: x in dom SR by A206,FUNCT_1:11;
A209: SR.x in dom fvs by A206,FUNCT_1:11;
reconsider k=x as Element of NAT by A208;
A210: k in dom p29 by A155,A158,A159,A208,FINSEQ_3:29;
A211: 1<=k by A208,FINSEQ_3:25;
A212: k<=len p29 by A155,A158,A159,A208,FINSEQ_3:25;
then
A213: m+k=SR.k by A8,A154,A158,A189,A211,FINSEQ_6:131;
0+1<=k by A208,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A214: i<len p29 and
A215: k=i+1 by A212,FINSEQ_6:127;
p29.k = vs.(m+1+i) by A8,A190,A191,A214,A215,Lm2
.= fvs.(SR.k) by A209,A213,A215,GRFUNC_1:2
.= y by A207,A208,FUNCT_1:13;
hence p in p29 by A205,A210,FUNCT_1:1;
end;
then
A216: p29 = fvs*(Sgm DR) by TARSKI:2;
Seq fvs = fvs*((Sgm DL)^(Sgm DR)) by A50,A140,A153,FINSEQ_1:def 15;
hence thesis by A65,A162,A163,A188,A216,FINSEQ_6:150;
end;
suppose
A217: n=1 & m <> len vs;
then
A218: m < len vs by A5,XXREAL_0:1;
then
A219: m<=len c by A8,NAT_1:13;
A220: 1 < m by A3,A4,XXREAL_0:2;
A221: 1<=m by A3,A4,XXREAL_0:2;
A222: m<=len c by A8,A218,NAT_1:13;
reconsider c2 = (m,len c)-cut c as oriented Chain of G by A219,A220,Th12;
set p2 = (m,len c+1)-cut vs;
A223: p2 is_oriented_vertex_seq_of c2 by A2,A219,A220,Th13;
set domfc = {k where k is Nat: m<=k & k<= len c};
deffunc F(object) = c.$1;
consider fc being Function such that
A224: dom fc = domfc and
A225: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A226: x = kk and
A227: m<=kk and
A228: kk<= len c;
1<=kk by A220,A227,XXREAL_0:2;
hence thesis by A226,A228,FINSEQ_1:1;
end;
then reconsider fc as FinSubsequence by A224,FINSEQ_1:def 12;
fc c= c
proof
let p be object;
assume
A229: p in fc;
then consider x, y being object such that
A230: [x,y] = p by RELAT_1:def 1;
A231: x in dom fc by A229,A230,FUNCT_1:1;
A232: y = fc.x by A229,A230,FUNCT_1:1;
consider kk being Nat such that
A233: x = kk and
A234: m<=kk and
A235: kk<= len c by A224,A231;
1<=kk by A220,A234,XXREAL_0:2;
then
A236: x in dom c by A233,A235,FINSEQ_3:25;
y = c.kk by A224,A225,A231,A232,A233;
hence thesis by A230,A233,A236,FUNCT_1:1;
end;
then reconsider fc as Subset of c;
take fc;
set domfvs = {k where k is Nat: m<=k & k<= len vs};
deffunc F(object) = vs.$1;
consider fvs being Function such that
A237: dom fvs = domfvs and
A238: 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
A239: x = kk and
A240: m<=kk and
A241: kk<= len vs;
1<=kk by A220,A240,XXREAL_0:2;
hence thesis by A239,A241,FINSEQ_1:1;
end;
then reconsider fvs as FinSubsequence by A237,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A242: p in fvs;
then consider x, y being object such that
A243: [x,y] = p by RELAT_1:def 1;
A244: x in dom fvs by A242,A243,FUNCT_1:1;
A245: y = fvs.x by A242,A243,FUNCT_1:1;
consider kk being Nat such that
A246: x = kk and
A247: m<=kk and
A248: kk<= len vs by A237,A244;
1<=kk by A220,A247,XXREAL_0:2;
then
A249: x in dom vs by A246,A248,FINSEQ_3:25;
y = vs.kk by A237,A238,A244,A245,A246;
hence thesis by A243,A246,A249,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
take fvs;
take c1 = c2;
take p1 = p2;
A250: len c2 +m = len c +1 by A4,A5,A8,A217,Lm2;
A251: m-m<=len c -m by A219,XREAL_1:9;
1-1<=m-1 by A220,XREAL_1:9;
then m-'1 = m-1 by XREAL_0:def 2;
then reconsider m1 = m-1 as Element of NAT;
A252: m = m1 +1;
len c2 -'1 = len c2 -1 by A250,A251,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
A253: m+lc21 = m1+len c2;
A254: m<=len c +1+1 by A5,A8,NAT_1:12;
A255: len c +1<=len vs by A2;
then
A256: len p2 +m = len c +1 +1 by A4,A217,A254,Lm2;
then len p2 = len c -m +1+1;
then
A257: 1<=len p2 by A250,NAT_1:12;
A258: len c2 = len c +(-m+1) by A250;
1-1 < m-1 by A220,XREAL_1:9;
then 0 < -(-(m-1));
then -(m-1) < 0;
hence
A259: len c1 < len c by A258,XREAL_1:30;
thus p1 is_oriented_vertex_seq_of c1 by A2,A221,A222,Th13;
len p1 = len c1 + 1 by A223;
hence len p1 < len vs by A8,A259,XREAL_1:6;
thus vs.1 = p1.1 by A4,A5,A6,A8,A217,FINSEQ_6:138;
thus vs.len vs = p1.len p1 by A4,A5,A8,A217,FINSEQ_6:138;
A260: domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A261: x=k and
A262: m<=k and
A263: k<=len c;
1<=k by A220,A262,XXREAL_0:2;
hence thesis by A261,A263,FINSEQ_1:1;
end;
then reconsider domfc as finite set by FINSET_1:1;
a260: domfc is included_in_Seg by A260,FINSEQ_1:def 13;
len c2 -'1 = len c2 -1 by A250,A251,XREAL_0:def 2;
then reconsider lc21 = len c2 -1 as Element of NAT;
m+lc21 = len c by A250;
then
A264: card domfc = len c2 + -1 +1 by FINSEQ_6:130
.= len c2;
A265: len Sgm domfc = card domfc by a260,FINSEQ_3:39;
A266: rng Sgm domfc c= dom fc by A224,FINSEQ_1:def 14;
set SR = Sgm domfc;
now
let p be object;
hereby
assume
A267: p in c2;
then consider x, y being object such that
A268: p=[x,y] by RELAT_1:def 1;
A269: x in dom c2 by A267,A268,FUNCT_1:1;
A270: y=c2.x by A267,A268,FUNCT_1:1;
reconsider k = x as Element of NAT by A269;
A271: 1<=k by A269,FINSEQ_3:25;
A272: k<=len c2 by A269,FINSEQ_3:25;
A273: x in dom SR by A264,A265,A269,FINSEQ_3:29;
A274: m1+k=SR.k by A250,A252,A253,A271,A272,FINSEQ_6:131;
A275: SR.k in rng SR by A273,FUNCT_1:def 3;
then
A276: x in dom (fc*SR) by A266,A273,FUNCT_1:11;
0+1<=k by A269,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A277: i<len c2 and
A278: k=i+1 by A272,FINSEQ_6:127;
(fc*SR).x = fc.(m1+k) by A274,A276,FUNCT_1:12
.= c.(m+i) by A266,A274,A275,A278,GRFUNC_1:2
.= y by A4,A5,A8,A217,A270,A277,A278,Lm2;
hence p in fc*(Sgm domfc) by A268,A276,FUNCT_1:1;
end;
assume
A279: p in fc*(Sgm domfc);
then consider x,y being object such that
A280: p=[x,y] by RELAT_1:def 1;
A281: x in dom (fc*SR) by A279,A280,FUNCT_1:1;
A282: y = (fc*SR).x by A279,A280,FUNCT_1:1;
A283: x in dom SR by A281,FUNCT_1:11;
A284: SR.x in dom fc by A281,FUNCT_1:11;
reconsider k=x as Element of NAT by A283;
A285: k in dom c2 by A264,A265,A283,FINSEQ_3:29;
A286: 1<=k by A283,FINSEQ_3:25;
A287: k<=len c2 by A264,A265,A283,FINSEQ_3:25;
then
A288: m1+k=SR.k by A250,A252,A253,A286,FINSEQ_6:131;
0+1<=k by A283,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A289: i<len c2 and
A290: k=i+1 by A287,FINSEQ_6:127;
c2.k = c.(m1+1+i) by A4,A5,A8,A217,A289,A290,Lm2
.= fc.(SR.k) by A284,A288,A290,GRFUNC_1:2
.= y by A282,A283,FUNCT_1:13;
hence p in c2 by A280,A285,FUNCT_1:1;
end;
then c2 = fc*(Sgm domfc) by TARSKI:2;
hence Seq fc = c1 by A224,FINSEQ_1:def 15;
A291: domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A292: x=k and
A293: m<=k and
A294: k<=len vs;
1<=k by A220,A293,XXREAL_0:2;
hence thesis by A292,A294,FINSEQ_1:1;
end;
then reconsider domfvs as finite set by FINSET_1:1;
a291: domfvs is included_in_Seg by A291,FINSEQ_1:def 13;
1-1<=len p2 -1 by A257,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;
A295: m+lp21 = len c+1 by A256;
A296: m+lp21 = m1+len p2;
A297: card domfvs = len p2 + -1 +1 by A8,A295,FINSEQ_6:130
.= len p2;
A298: len Sgm domfvs = card domfvs by a291,FINSEQ_3:39;
A299: rng Sgm domfvs c= dom fvs by A237,FINSEQ_1:def 14;
set SR = Sgm domfvs;
now
let p be object;
hereby
assume
A300: p in p2;
then consider x, y being object such that
A301: p=[x,y] by RELAT_1:def 1;
A302: x in dom p2 by A300,A301,FUNCT_1:1;
A303: y=p2.x by A300,A301,FUNCT_1:1;
reconsider k = x as Element of NAT by A302;
A304: 1<=k by A302,FINSEQ_3:25;
A305: k<=len p2 by A302,FINSEQ_3:25;
A306: x in dom SR by A297,A298,A302,FINSEQ_3:29;
A307: m1+k=SR.k by A8,A252,A256,A296,A304,A305,FINSEQ_6:131;
A308: SR.k in rng SR by A306,FUNCT_1:def 3;
then
A309: x in dom (fvs*SR) by A299,A306,FUNCT_1:11;
0+1<=k by A302,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A310: i<len p2 and
A311: k=i+1 by A305,FINSEQ_6:127;
(fvs*SR).x = fvs.(m1+k) by A307,A309,FUNCT_1:12
.= vs.(m+i) by A299,A307,A308,A311,GRFUNC_1:2
.= y by A4,A217,A254,A255,A303,A310,A311,Lm2;
hence p in fvs*(Sgm domfvs) by A301,A309,FUNCT_1:1;
end;
assume
A312: p in fvs*(Sgm domfvs);
then consider x,y being object such that
A313: p=[x,y] by RELAT_1:def 1;
A314: x in dom (fvs*SR) by A312,A313,FUNCT_1:1;
A315: y = (fvs*SR).x by A312,A313,FUNCT_1:1;
A316: x in dom SR by A314,FUNCT_1:11;
A317: SR.x in dom fvs by A314,FUNCT_1:11;
reconsider k=x as Element of NAT by A316;
A318: k in dom p2 by A297,A298,A316,FINSEQ_3:29;
A319: 1<=k by A316,FINSEQ_3:25;
A320: k<=len p2 by A297,A298,A316,FINSEQ_3:25;
then
A321: m1+k=SR.k by A8,A252,A256,A296,A319,FINSEQ_6:131;
0+1<=k by A316,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A322: i<len p2 and
A323: k=i+1 by A320,FINSEQ_6:127;
p2.k = vs.(m1+1+i) by A4,A217,A254,A255,A322,A323,Lm2
.= fvs.(SR.k) by A317,A321,A323,GRFUNC_1:2
.= y
by A315,A316,FUNCT_1:13;
hence p in p2 by A313,A318,FUNCT_1:1;
end;
then p2 = fvs*(Sgm domfvs) by TARSKI:2;
hence thesis by A237,FINSEQ_1:def 15;
end;
suppose
A324: n<>1 & m = len vs;
then 1 < n by A3,XXREAL_0:1;
then 1 + 1<=n by NAT_1:13;
then
A325: 1+1-1<=n-1 by XREAL_1:9;
n < len vs by A4,A5,XXREAL_0:2;
then
A326: n-1 < len c +1-1 by A8,XREAL_1:9;
A327: 1<=n1+1 by NAT_1:12;
reconsider c1 = (1,n1)-cut c as oriented Chain of G by A11,A325,A326,Th12;
set pp = (1,n)-cut vs;
A328: n<=len vs by A4,A5,XXREAL_0:2;
A329: pp is_oriented_vertex_seq_of c1 by A2,A12,A325,A326,Th13;
then
A330: len pp = len c1 + 1;
set domfc = {k where k is Nat: 1<=k & k<=n1};
deffunc F(object) = c.$1;
consider fc being Function such that
A331: dom fc = domfc and
A332: for x being object st x in domfc holds fc.x = F(x) from FUNCT_1:sch 3;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider kk being Nat such that
A333: x = kk and
A334: 1<=kk and
A335: kk<=n1;
kk<=len c by A11,A326,A335,XXREAL_0:2;
hence thesis by A333,A334,FINSEQ_1:1;
end;
then reconsider fc as FinSubsequence by A331,FINSEQ_1:def 12;
fc c= c
proof
let p be object;
assume
A336: p in fc;
then consider x, y being object such that
A337: [x,y] = p by RELAT_1:def 1;
A338: x in dom fc by A336,A337,FUNCT_1:1;
A339: y = fc.x by A336,A337,FUNCT_1:1;
consider kk being Nat such that
A340: x = kk and
A341: 1<=kk and
A342: kk<=n1 by A331,A338;
kk<=len c by A11,A326,A342,XXREAL_0:2;
then
A343: x in dom c by A340,A341,FINSEQ_3:25;
y = c.kk by A331,A332,A338,A339,A340;
hence thesis by A337,A340,A343,FUNCT_1:1;
end;
then reconsider fc as Subset of c;
take fc;
set domfvs = { k where k is Nat : 1 <= k & k <= n};
deffunc F(object) = vs.$1;
consider fvs being Function such that
A344: dom fvs = domfvs and
A345: 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
A346: x = kk and
A347: 1<=kk and
A348: kk<=n;
kk<=len vs by A328,A348,XXREAL_0:2;
hence thesis by A346,A347,FINSEQ_1:1;
end;
then reconsider fvs as FinSubsequence by A344,FINSEQ_1:def 12;
fvs c= vs
proof
let p be object;
assume
A349: p in fvs;
then consider x, y being object such that
A350: [x,y] = p by RELAT_1:def 1;
A351: x in dom fvs by A349,A350,FUNCT_1:1;
A352: y = fvs.x by A349,A350,FUNCT_1:1;
consider kk being Nat such that
A353: x = kk and
A354: 1<=kk and
A355: kk<=n by A344,A351;
kk<=len vs by A328,A355,XXREAL_0:2;
then
A356: x in dom vs by A353,A354,FINSEQ_3:25;
y = vs.kk by A344,A345,A351,A352,A353;
hence thesis by A350,A353,A356,FUNCT_1:1;
end;
then reconsider fvs as Subset of vs;
take fvs;
take c9 = c1;
take p1 = pp;
A357: len c1+1=n1+1 by A11,A326,A327,Lm2;
then
A358: len c1 = n - 1 by A10,XREAL_0:def 2;
thus
len c9 < len c by A10,A326,A357,XREAL_0:def 2;
thus p1 is_oriented_vertex_seq_of c9 by A2,A12,A325,A326,Th13;
len p1 = len c1 + 1 by A329;
hence len p1 < len vs by A4,A5,A358,XXREAL_0:2;
thus vs.1 = p1.1 by A3,A328,FINSEQ_6:138;
thus vs.len vs = p1.len p1 by A3,A4,A6,A324,FINSEQ_6:138;
domfc c= Seg len c
proof
let x be object;
assume x in domfc;
then consider k being Nat such that
A359: x=k and
A360: 1<=k and
A361: k<=n1;
k<=len c by A11,A326,A361,XXREAL_0:2;
hence thesis by A359,A360,FINSEQ_1:1;
end;
then reconsider domfc as finite set by FINSET_1:1;
domfc = Seg n1 by FINSEQ_1:def 1;
then
A362: Sgm domfc = idseq n1 by FINSEQ_3:48;
then
A363: dom Sgm domfc = Seg n1;
set SL = Sgm domfc;
now
let p be object;
hereby
assume
A364: p in c1;
then consider x, y being object such that
A365: p=[x,y] by RELAT_1:def 1;
A366: x in dom c1 by A364,A365,FUNCT_1:1;
A367: y=c1.x by A364,A365,FUNCT_1:1;
reconsider k = x as Element of NAT by A366;
A368: 1<=k by A366,FINSEQ_3:25;
A369: k<=len c1 by A366,FINSEQ_3:25;
then
A370: x in dom SL by A357,A363,A368,FINSEQ_1:1;
then
A371: k=SL.k by A362,FUNCT_1:18;
A372: k in domfc by A357,A368,A369;
then
A373: x in dom (fc*SL) by A331,A370,A371,FUNCT_1:11;
0+1<=k by A366,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A374: i<n1 and
A375: k=i+1 by A357,A369,FINSEQ_6:127;
(fc*SL).x = fc.k by A371,A373,FUNCT_1:12
.= c.(1+i) by A331,A372,A375,GRFUNC_1:2
.= y by A11,A326,A327,A357,A367,A374,A375,Lm2;
hence p in fc*(Sgm domfc) by A365,A373,FUNCT_1:1;
end;
assume
A376: p in fc*(Sgm domfc);
then consider x,y being object such that
A377: p=[x,y] by RELAT_1:def 1;
A378: x in dom (fc*SL) by A376,A377,FUNCT_1:1;
A379: y = (fc*SL).x by A376,A377,FUNCT_1:1;
A380: (fc*SL).x = fc.(SL.x) by A378,FUNCT_1:12;
A381: x in dom SL by A378,FUNCT_1:11;
then x in {kk where kk is Nat: 1<=kk & kk<=n1}
by A363,FINSEQ_1:def 1;
then consider k being Nat such that
A382: k=x and
A383: 1<=k and
A384: k<=n1;
A385: k in dom fc by A331,A383,A384;
A386: k=SL.k by A362,A381,A382,FUNCT_1:18;
A387: k in dom c1 by A357,A383,A384,FINSEQ_3:25;
0+1<=k by A383;
then ex i being Nat st ( 0<=i)&( i<n1)&( k=i+1) by A384,
FINSEQ_6:127;
then c1.k = c.k by A11,A326,A327,A357,Lm2
.= y by A379,A380,A382,A385,A386,GRFUNC_1:2;
hence p in c1 by A377,A382,A387,FUNCT_1:1;
end;
then c1 = fc*(Sgm domfc) by TARSKI:2;
hence Seq fc = c9 by A331,FINSEQ_1:def 15;
domfvs c= Seg len vs
proof
let x be object;
assume x in domfvs;
then consider k being Nat such that
A388: x=k and
A389: 1<=k and
A390: k<=n;
k<=len vs by A328,A390,XXREAL_0:2;
hence thesis by A388,A389,FINSEQ_1:1;
end;
then reconsider domfvs as finite set by FINSET_1:1;
domfvs = Seg n by FINSEQ_1:def 1;
then
A391: Sgm domfvs = idseq n by FINSEQ_3:48;
then
A392: dom Sgm domfvs = Seg n;
set SL = Sgm domfvs;
now
let p be object;
hereby
assume
A393: p in pp;
then consider x, y being object such that
A394: p=[x,y] by RELAT_1:def 1;
A395: x in dom pp by A393,A394,FUNCT_1:1;
A396: y=pp.x by A393,A394,FUNCT_1:1;
reconsider k = x as Element of NAT by A395;
A397: 1<=k by A395,FINSEQ_3:25;
A398: k<=len pp by A395,FINSEQ_3:25;
then
A399: x in dom SL by A330,A358,A392,A397,FINSEQ_1:1;
then
A400: k=SL.k by A391,FUNCT_1:18;
A401: k in domfvs by A330,A358,A397,A398;
then
A402: x in dom (fvs*SL) by A344,A399,A400,FUNCT_1:11;
0+1<= k by A395,FINSEQ_3:25;
then consider i being Nat such that
0<=i and
A403: i<n and
A404: k=i+1 by A330,A358,A398,FINSEQ_6:127;
(fvs*SL).x = fvs.k by A400,A402,FUNCT_1:12
.= vs.(1+i) by A344,A401,A404,GRFUNC_1:2
.= y by A3,A328,A330,A358,A396,A403,A404,FINSEQ_6:def 4;
hence p in fvs*(Sgm domfvs) by A394,A402,FUNCT_1:1;
end;
assume
A405: p in fvs*(Sgm domfvs);
then consider x,y being object such that
A406: p=[x,y] by RELAT_1:def 1;
A407: x in dom (fvs*SL) by A405,A406,FUNCT_1:1;
A408: y = (fvs*SL).x by A405,A406,FUNCT_1:1;
A409: (fvs*SL).x = fvs.(SL.x) by A407,FUNCT_1:12;
A410: x in dom SL by A407,FUNCT_1:11;
then x in { kk where kk is Nat: 1<=kk & kk<=n}
by A392,FINSEQ_1:def 1;
then consider k being Nat such that
A411: k=x and
A412: 1<=k and
A413: k<=n;
A414: k in dom fvs by A344,A412,A413;
A415: k=SL.k by A391,A410,A411,FUNCT_1:18;
A416: k in dom pp by A330,A358,A412,A413,FINSEQ_3:25;
0+1<=k by A412;
then ex i being Nat st ( 0<=i)&( i<n)&( k=i+1) by A413,
FINSEQ_6:127;
then pp.k = vs.k by A3,A328,A330,A358,FINSEQ_6:def 4
.= y by A408,A409,A411,A414,A415,GRFUNC_1:2;
hence p in pp by A406,A411,A416,FUNCT_1:1;
end;
then pp = fvs*(Sgm domfvs) by TARSKI:2;
hence thesis by A344,FINSEQ_1:def 15;
end;
end;
theorem
vs is_oriented_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_oriented_vertex_seq_of sc &
vs.1 = vs1.1 & vs.len vs = vs1.len vs1
proof
assume
A1: vs is_oriented_vertex_seq_of c;
per cases;
suppose
A2: c is Simple;
reconsider fc = c as Subset of c by FINSEQ_6:152;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider sc = c as oriented simple Chain of G by A2,Th19;
take fc, fvs, sc, vs;
thus Seq fc = sc & Seq fvs = vs by FINSEQ_3:116;
thus vs is_oriented_vertex_seq_of sc by A1;
thus thesis;
end;
suppose
A3: not c is Simple;
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_oriented_vertex_seq_of c1 &
vs.1 = vs1.1 & vs.len vs = vs1.len vs1 & len c1 = $1 & not c1 is Simple;
P[len c]
proof
reconsider fc = c as Subset of c by FINSEQ_6:152;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
take fc, fvs, c,vs;
thus Seq fc = c & Seq fvs = vs by FINSEQ_3:116;
thus vs is_oriented_vertex_seq_of c by A1;
thus vs.1 = vs.1 & vs.len vs = vs.len vs;
thus thesis by A3;
end;
then
A4: ex k be Nat st P[k];
consider k be Nat such that
A5: P[k] & for n being Nat st P[n] holds k<=n from NAT_1:sch 5(A4);
consider fc being Subset of c, fvs being Subset of vs, c1, vs1 such that
A6: Seq fc = c1 and
A7: Seq fvs = vs1 and
A8: vs1 is_oriented_vertex_seq_of c1 and
A9: vs.1 = vs1.1 and
A10: vs.len vs = vs1.len vs1 and
A11: len c1 = k and
A12: not c1 is Simple by A5;
consider fc1 being Subset of c1, fvs1 being Subset of vs1,
c2, vs2 such that
A13: len c2 < len c1 and
A14: vs2 is_oriented_vertex_seq_of c2 and len vs2 < len vs1 and
A15: vs1.1 = vs2.1 and
A16: vs1.len vs1 = vs2.len vs2 and
A17: Seq fc1 = c2 and
A18: Seq fvs1 = vs2 by A8,A12,Th20;
reconsider fc9=fc|rng((Sgm dom fc)|dom fc1) as Subset of c
by FINSEQ_6:153;
A19: Seq fc9 = c2 by A6,A17,FINSEQ_6:154;
reconsider fvs9=fvs|rng((Sgm dom fvs)|dom fvs1) as Subset of vs
by FINSEQ_6:153;
A20: Seq fvs9 = vs2 by A7,A18,FINSEQ_6:154;
now
assume c2 is Simple oriented Chain of G;
then reconsider sc = c2 as oriented simple Chain of G by Th19;
take fc9,sc;
Seq fc9 = sc by A6,A17,FINSEQ_6:154;
hence thesis by A9,A10,A14,A15,A16,A20;
end;
hence thesis by A5,A9,A10,A11,A13,A14,A15,A16,A19,A20;
end;
end;
theorem
p is OrientedPath of G implies p|Seg(n) is OrientedPath of G
proof
assume
A1: p is OrientedPath of G;
then reconsider p9=p|(Seg n) as oriented Chain of G by Th16;
reconsider q=p|(Seg n) as FinSequence;
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;
then p9 is Path of G by GRAPH_1:def 16;
hence thesis;
end;
theorem Th23:
sc is OrientedPath of G
proof
assume not sc is OrientedPath of G;
then consider m, n such that
A1: 1<=m and
A2: m<n and
A3: n<=len sc and
A4: sc.m = sc.n by GRAPH_1:def 16;
sc is Simple by Th18;
then consider vs such that
A5: vs is_oriented_vertex_seq_of sc and
A6: for n, m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs;
A7: len vs = len sc + 1 by A5;
A8: m<=len sc by A2,A3,XXREAL_0:2;
A9: 1<=n by A1,A2,XXREAL_0:2;
A10: n<=len vs by A3,A7,NAT_1:12;
A11: m+1<n+1 by A2,XREAL_1:6;
A12: n+1<=len vs by A3,A7,XREAL_1:6;
A13: m<n+1 by A11,NAT_1:12;
set v1 = vs/.m;
set v2 = vs/.(m+1);
A14: sc.m orientedly_joins v1, v2 by A1,A5,A8;
set v19 = vs/.n;
set v29 = vs/.(n+1);
A15: sc.n orientedly_joins v19, v29 by A3,A5,A9;
then
A16: v1=v19 by A4,A14;
A17: v2=v29 by A4,A14,A15;
A18: m<=len vs by A12,A13,XXREAL_0:2;
A19: m+1<=len vs by A11,A12,XXREAL_0:2;
A20: v1=vs.m by A1,A18,FINSEQ_4:15;
A21: v2=vs.(m+1) by A19,FINSEQ_4:15,NAT_1:12;
A22: v19=vs.n by A9,A10,FINSEQ_4:15;
A23: v29=vs.(n+1) by A12,FINSEQ_4:15,NAT_1:12;
m=1 by A1,A2,A6,A10,A16,A20,A22;
hence contradiction by A6,A11,A12,A17,A21,A23;
end;
theorem
for c1 being FinSequence holds (c1 is Simple oriented Chain of G iff
c1 is oriented simple Chain of G)
&(c1 is oriented simple Chain of G implies c1 is OrientedPath of G)
by Th18,Th19,Th23;