:: Oriented Simple Chains Included in Oriented Chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received August 19, 1998
:: Copyright (c) 1998-2016 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;
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;
constructors RECDEF_1, GRAPH_2, NAT_D, FINSEQ_2, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
GRAPH_2, ORDINAL1, CARD_1, STRUCT_0, GRAPH_1;
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;
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;
klen c;
then
A22: n;
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
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,GRAPH_2:def 1;
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 {};
set q=c1^c2;
set p=vs1^'vs2;
len p +1 = len vs1 +len vs2 by A8,GRAPH_2:13;
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,GRAPH_2:14;
p.(n+1) = vs1.(n+1) by A22,GRAPH_2:14,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 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 as FinSequence of the carrier of G;
A1: p is_oriented_vertex_seq_of q by Lm1;
for n,m st 1<=n & n 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=len q;
then q|(Seg n)=q by FINSEQ_3:49;
hence thesis by A1,A2,GRAPH_1:def 15;
end;
suppose
A3: n1 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,GRAPH_2:def 1;
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 GRAPH_2:7
.= (0+1, 1)-cut p2 ^ (1+1, len p2)-cut p2 by A33,GRAPH_2:8;
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,GRAPH_2:8;
(1,1)-cut p2 = <*p2.(0+1)*> by A33,GRAPH_2:6
.= <*vs.(m+0)*> by A22,A23,A24,A28,GRAPH_2:def 1
.= (m,m)-cut vs by A5,A19,GRAPH_2:6;
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,GRAPH_2:12;
A64: pp.len pp = vs.n by A3,A21,GRAPH_2:12;
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,GRAPH_2:def 2;
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 GRAPH_2:14;
hence vs.1 = p1.1 by A3,A21,GRAPH_2:12;
A69: p2.len p2 = vs.(len c + 1) by A22,A23,A24,GRAPH_2:12;
m-m<=len c -m by A20,XREAL_1:9;
then 0+1<=len c -m+1 by XREAL_1:6;
then 1 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,GRAPH_2:12;
thus vs.len vs = p1.len p1 by A4,A5,A8,A217,GRAPH_2:12;
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;
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 GRAPH_2:4
.= len c2;
A265: len Sgm domfc = card domfc by A260,FINSEQ_3:39;
A266: rng Sgm domfc c= dom fc by A224,A260,FINSEQ_1:def 13;
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,GRAPH_2:5;
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: i1 & 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,GRAPH_2:12;
thus vs.len vs = p1.len p1 by A3,A4,A6,A324,GRAPH_2:12;
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 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