:: Oriented Simple Chains Included in Oriented Chains :: by Yatsuka Nakamura and Piotr Rudnicki :: :: Received August 19, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, 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, 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; 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 :: GRAPH_4:def 1 (the Source of G).e = x & (the Target of G).e = y; end; theorem :: GRAPH_4:1 e orientedly_joins v1, v2 implies e joins v1, v2; definition let G; let x,y be Element of (the carrier of G); pred x,y are_orientedly_incident means :: GRAPH_4:def 2 ex v being set st v in the carrier' of G & v orientedly_joins x, y; end; theorem :: GRAPH_4:2 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 :: GRAPH_4:def 3 { v: ex e being Element of the carrier' of G st e in X & v = (the Source of G).e }; end; definition let G, X; func G-TVSet X -> set equals :: GRAPH_4:def 4 { v: ex e being Element of the carrier' of G st e in X & v = (the Target of G).e }; end; theorem :: GRAPH_4:3 G-SVSet {} = {} & G-TVSet {} = {}; definition let G, vs; let c be FinSequence; pred vs is_oriented_vertex_seq_of c means :: GRAPH_4:def 5 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 :: GRAPH_4:4 vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c; theorem :: GRAPH_4:5 vs is_oriented_vertex_seq_of c implies G-SVSet rng c c= rng vs; theorem :: GRAPH_4:6 vs is_oriented_vertex_seq_of c implies G-TVSet rng c c= rng vs; theorem :: GRAPH_4:7 c <>{} & vs is_oriented_vertex_seq_of c implies rng vs c= G-SVSet rng c \/ G-TVSet rng c; begin :: Cutting and glueing of oriented chains theorem :: GRAPH_4:8 <*v*> is_oriented_vertex_seq_of {}; theorem :: GRAPH_4:9 ex vs st vs is_oriented_vertex_seq_of c; theorem :: GRAPH_4:10 c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2; definition let G, c; assume c <>{}; func oriented-vertex-seq c -> FinSequence of the carrier of G means :: GRAPH_4:def 6 it is_oriented_vertex_seq_of c; end; theorem :: GRAPH_4:11 vs is_oriented_vertex_seq_of c & c1 = c|Seg n & vs1= vs|Seg (n+1) implies vs1 is_oriented_vertex_seq_of c1; theorem :: GRAPH_4:12 1<=m & m<=n & n<=len c & q = (m,n)-cut c implies q is oriented Chain of G; theorem :: GRAPH_4:13 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; theorem :: GRAPH_4:14 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; theorem :: GRAPH_4:15 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; begin definition let G; let IT be oriented Chain of G; attr IT is Simple means :: GRAPH_4:def 7 ex vs st vs is_oriented_vertex_seq_of IT & for n,m st 1<=n & n