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;