Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### The Class of Series -- Parallel Graphs. Part I

**by****Krzysztof Retel**- Received November 18, 2002
- MML identifier: NECKLACE

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL2, ARYTM_3, NECKLACE, FUNCT_3, ARYTM, FUNCT_2, PARTFUN1, ORDERS_1, PRE_TOPC, RELAT_1, RELAT_2, REALSET1, FUNCT_1, BOOLE, SEQM_3, SUBSET_1, WELLORD1, CAT_1, FUNCOP_1, FUNCT_4, ARYTM_1, TARSKI, CARD_1, CARD_2, FINSET_1, SQUARE_1, INCPROJ; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_1, CARD_2, WELLORD1, FINSET_1, SQUARE_1, QUIN_1, REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, STRUCT_0, ORDERS_1, RELAT_1, RELAT_2, BINARITH, BVFUNC24, FUNCT_3, CQC_LANG, FUNCOP_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, ORDINAL2, WAYBEL_0, WAYBEL_1, ORDERS_3, PRE_TOPC; constructors ORDERS_3, QUIN_1, ENUMSET1, CARD_2, BVFUNC24, SQUARE_1, WELLORD1, WAYBEL_1, SEQM_3, REAL_1, BINARITH, AMISTD_1, MEMBERED, PRE_TOPC; clusters RELSET_1, ORDERS_1, STRUCT_0, SUBSET_1, ARYTM_3, XREAL_0, HILBERT3, TEX_2, FUNCT_1, FUNCT_4, FINSET_1, AFINSQ_1, SQUARE_1, ORDERS_3, TOPREAL8, FUNCOP_1, AMISTD_1, MEMBERED, FUNCT_2, NUMBERS, ORDINAL2; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; begin :: Preliminaries reserve i,j,k,n for natural number; reserve x,x1,x2,x3,x4,x5,y1,y2,y3 for set; definition let x1,x2,x3,x4,x5 be set; pred x1, x2, x3, x4, x5 are_mutually_different means :: NECKLACE:def 1 x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5; end; theorem :: NECKLACE:1 x1,x2,x3,x4,x5 are_mutually_different implies card {x1,x2,x3,x4,x5} = 5; theorem :: NECKLACE:2 4 = {0,1,2,3}; theorem :: NECKLACE:3 [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}; theorem :: NECKLACE:4 for x being set, n be natural number holds x in n implies x is natural number; theorem :: NECKLACE:5 for x be non empty natural number holds 0 in x; definition cluster natural -> cardinal set; end; definition let X be set; cluster delta X -> one-to-one; end; theorem :: NECKLACE:6 for X being set holds Card id X = Card X; definition let R be trivial Relation; cluster dom R -> trivial; end; definition cluster trivial -> one-to-one Function; end; theorem :: NECKLACE:7 for f,g be Function st dom f misses dom g holds rng(f +* g) = rng f \/ rng g; theorem :: NECKLACE:8 for f,g be one-to-one Function st dom f misses dom g & rng f misses rng g holds (f+*g)" = f" +* g"; theorem :: NECKLACE:9 for A,a,b being set holds (A --> a) +* (A --> b) = A --> b; theorem :: NECKLACE:10 for a,b being set holds (a .--> b)" = b .--> a; theorem :: NECKLACE:11 for a,b,c,d being set st a = b iff c = d holds (a,b) --> (c,d)" = (c,d) --> (a,b); scheme Convers{X()-> non empty set, R() -> Relation, F,G(set)-> set, P[set]}: R()~ ={[F(x),G(x)] where x is Element of X(): P[x]} provided R() = {[G(x),F(x)] where x is Element of X(): P[x]}; theorem :: NECKLACE:12 for i,j,n be natural number holds i < j & j in n implies i in n; begin :: Auxiliary Concepts definition let R,S be RelStr; pred S embeds R means :: NECKLACE:def 2 ex f being map of R,S st f is one-to-one & for x,y being Element of R holds [x,y] in the InternalRel of R iff [f.x,f.y] in the InternalRel of S; end; definition let R,S be non empty RelStr; redefine pred S embeds R; reflexivity; end; theorem :: NECKLACE:13 for R,S,T be non empty RelStr holds R embeds S & S embeds T implies R embeds T; definition let R,S be non empty RelStr; pred R is_equimorphic_to S means :: NECKLACE:def 3 R embeds S & S embeds R; reflexivity; symmetry; end; theorem :: NECKLACE:14 for R,S,T be non empty RelStr holds R is_equimorphic_to S & S is_equimorphic_to T implies R is_equimorphic_to T; definition let R be non empty RelStr; redefine attr R is connected; antonym R is parallel; end; definition let R be RelStr; attr R is symmetric means :: NECKLACE:def 4 the InternalRel of R is_symmetric_in the carrier of R; end; definition let R be RelStr; attr R is asymmetric means :: NECKLACE:def 5 the InternalRel of R is asymmetric; end; theorem :: NECKLACE:15 for R be RelStr st R is asymmetric holds the InternalRel of R misses (the InternalRel of R)~; definition let R be RelStr; attr R is irreflexive means :: NECKLACE:def 6 for x being set st x in the carrier of R holds not [x,x] in the InternalRel of R; end; definition let n be natural number; func n-SuccRelStr -> strict RelStr means :: NECKLACE:def 7 the carrier of it = n & the InternalRel of it = {[i,i+1] where i is Nat:i+1 < n}; end; theorem :: NECKLACE:16 for n be natural number holds n-SuccRelStr is asymmetric; theorem :: NECKLACE:17 n > 0 implies Card the InternalRel of n-SuccRelStr = n-1; definition let R be RelStr; func SymRelStr R -> strict RelStr means :: NECKLACE:def 8 the carrier of it = the carrier of R & the InternalRel of it = (the InternalRel of R) \/ (the InternalRel of R)~; end; definition let R be RelStr; cluster SymRelStr R -> symmetric; end; definition cluster non empty symmetric RelStr; end; definition let R be symmetric RelStr; cluster the InternalRel of R -> symmetric; end; definition let R be RelStr; func ComplRelStr R -> strict RelStr means :: NECKLACE:def 9 the carrier of it = the carrier of R & the InternalRel of it = (the InternalRel of R)` \ id (the carrier of R); end; definition let R be non empty RelStr; cluster ComplRelStr R -> non empty; end; theorem :: NECKLACE:18 for S,R being RelStr holds S,R are_isomorphic implies Card the InternalRel of S = Card the InternalRel of R; begin :: Necklace n definition let n be natural number; func Necklace n -> strict RelStr equals :: NECKLACE:def 10 SymRelStr(n-SuccRelStr); end; definition let n be natural number; cluster Necklace n -> symmetric; end; theorem :: NECKLACE:19 the InternalRel of Necklace n = {[i,i+1] where i is Nat:i+1 < n} \/ {[i+1,i] where i is Nat:i+1 < n}; theorem :: NECKLACE:20 for x be set holds x in the InternalRel of Necklace n iff ex i being Nat st i+1 < n & (x = [i,i+1] or x = [i+1,i]); definition let n be natural number; cluster Necklace n -> irreflexive; end; theorem :: NECKLACE:21 for n be natural number holds the carrier of Necklace n = n; definition let n be non empty natural number; cluster Necklace n -> non empty; end; definition let n be natural number; cluster the carrier of Necklace n -> finite; end; theorem :: NECKLACE:22 for n,i be natural number st i+1 < n holds [i,i+1] in the InternalRel of Necklace n; theorem :: NECKLACE:23 for n be natural number, i being natural number st i in the carrier of Necklace n holds i < n; theorem :: NECKLACE:24 for n be non empty natural number holds Necklace n is connected; theorem :: NECKLACE:25 for i,j being natural number st [i,j] in the InternalRel of Necklace n holds i = j + 1 or j = i + 1; theorem :: NECKLACE:26 for i,j being natural number st (i = j + 1 or j = i + 1) & i in the carrier of Necklace n & j in the carrier of Necklace n holds [i,j] in the InternalRel of Necklace n; theorem :: NECKLACE:27 n > 0 implies Card ({[i+1,i] where i is Nat:i+1 < n}) = n-1; theorem :: NECKLACE:28 n > 0 implies Card the InternalRel of Necklace n = 2*(n-1); theorem :: NECKLACE:29 Necklace 1, ComplRelStr Necklace 1 are_isomorphic; theorem :: NECKLACE:30 Necklace 4, ComplRelStr Necklace 4 are_isomorphic; theorem :: NECKLACE:31 Necklace n, ComplRelStr Necklace n are_isomorphic implies n = 0 or n = 1 or n = 4;

Back to top