:: The Class of Series-Parallel Graphs, {I}
::  by Krzysztof Retel
::
:: Received November 18, 2002
:: Copyright (c) 2002-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, NAT_1, CARD_1, ZFMISC_1, XBOOLE_0, SUBSET_1, ARYTM_3,
      FUNCT_3, FUNCT_1, RELAT_1, FUNCT_2, FUNCT_4, TARSKI, FUNCOP_1, ORDERS_2,
      STRUCT_0, RELAT_2, XXREAL_0, ARYTM_1, WELLORD1, CAT_1, SEQM_3, FINSET_1,
      ORDINAL1, CARD_2, SQUARE_1, NECKLACE, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_2, WELLORD1,
      FINSET_1, SQUARE_1, QUIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, REAL_1,
      NAT_1, NAT_D, RELAT_1, RELAT_2, FUNCT_3, FUNCOP_1, RELSET_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FUNCT_4, BINOP_1, XXREAL_0, STRUCT_0, ORDERS_2,
      WAYBEL_0, WAYBEL_1, ORDERS_3;
 constructors WELLORD1, REAL_1, SQUARE_1, NAT_1, QUIN_1, CARD_2, REALSET1,
      ORDERS_3, WAYBEL_1, NAT_D, RELSET_1, FUNCT_4;
 registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
      FUNCT_4, FINSET_1, XREAL_0, SQUARE_1, STRUCT_0, ORDERS_2, HILBERT3,
      CARD_1, RELAT_1, QUIN_1, NAT_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;


begin :: Preliminaries

reserve i,j,k,n for Nat;
reserve x,x1,x2,x3,y1,y2,y3 for set;

theorem :: NECKLACE:1
  4 = {0,1,2,3};

theorem :: NECKLACE:2
  [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[
  x2,y3],[x3,y1],[x3,y2],[x3,y3]};

::$CT

theorem :: NECKLACE:4
  for x be non zero Nat holds 0 in x;

registration
  let X be set;
  cluster delta X -> one-to-one;
end;

theorem :: NECKLACE:5
  for X being set holds card id X = card X;

registration
  cluster trivial -> one-to-one for Function;
end;

theorem :: NECKLACE:6
  for f,g be Function st dom f misses dom g holds rng(f +* g) = rng f \/
  rng g;

theorem :: NECKLACE:7
  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:8
  for A,a,b being set holds (A --> a) +* (A --> b) = A --> b;

theorem :: NECKLACE:9
  for a,b being set holds (a .--> b)" = b .--> a;

theorem :: NECKLACE:10
  for a,b,c,d being set st a = b iff c = d holds (a,b) --> (c,d)"
  = (c,d) --> (a,b);

scheme :: NECKLACE:sch 1
  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:11
  for i,j,n be Nat holds i < j & j in Segm n implies i in Segm n;

begin   :: Auxiliary Concepts

definition
  let R,S be RelStr;

  pred S embeds R means
:: NECKLACE:def 1

  ex f being Function 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:12
  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 2

  R embeds S & S embeds R;
  reflexivity;
  symmetry;
end;

theorem :: NECKLACE:13
  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;

notation
  let R be non empty RelStr;
  antonym R is parallel for R is connected;
end;

definition
  let R be RelStr;
  attr R is symmetric means
:: NECKLACE:def 3

  the InternalRel of R is_symmetric_in the carrier of R;
end;

definition
  let R be RelStr;
  attr R is asymmetric means
:: NECKLACE:def 4

  the InternalRel of R is asymmetric;
end;

theorem :: NECKLACE:14
  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 5
  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 Nat;
  func n-SuccRelStr -> strict RelStr means
:: NECKLACE:def 6

  the carrier of it = n & the
  InternalRel of it = {[i,i+1] where i is Element of NAT:i+1 < n};
end;

theorem :: NECKLACE:15
  for n be Nat holds n-SuccRelStr is asymmetric;

theorem :: NECKLACE:16
  n > 0 implies card the InternalRel of n-SuccRelStr = n-1;

definition
  let R be RelStr;
  func SymRelStr R -> strict RelStr means
:: NECKLACE:def 7

  the carrier of it = the
  carrier of R & the InternalRel of it = (the InternalRel of R) \/ (the
  InternalRel of R)~;
end;

registration
  let R be RelStr;
  cluster SymRelStr R -> symmetric;
end;

registration
  cluster non empty symmetric for RelStr;
end;

registration
  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 8

  the carrier of it = the carrier of R &
  the InternalRel of it = (the InternalRel of R)` \ id (the carrier of R);
end;

registration
  let R be non empty RelStr;
  cluster ComplRelStr R -> non empty;
end;

theorem :: NECKLACE:17
  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 Nat;
  func Necklace n -> strict RelStr equals
:: NECKLACE:def 9
  SymRelStr(n-SuccRelStr);
end;

registration
  let n be Nat;
  cluster Necklace n -> symmetric;
end;

theorem :: NECKLACE:18
  the InternalRel of Necklace n = {[i,i+1] where i is Element of
  NAT:i+1 < n} \/ {[i+1,i] where i is Element of NAT:i+1 < n};

theorem :: NECKLACE:19
  for x be set holds x in the InternalRel of Necklace n iff ex i
  being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i]);

registration
  let n be Nat;
  cluster Necklace n -> irreflexive;
end;

theorem :: NECKLACE:20
  for n be Nat holds the carrier of Necklace n = n;

registration
  let n be non zero Nat;
  cluster Necklace n -> non empty;
end;

registration
  let n be Nat;
  cluster the carrier of Necklace n -> finite;
end;

theorem :: NECKLACE:21
  for n,i be Nat st i+1 < n holds [i,i+1] in the InternalRel of Necklace n;

theorem :: NECKLACE:22
  for n be Nat, i being Nat st i in the carrier of Necklace n holds i < n;

theorem :: NECKLACE:23
  for n be non zero Nat holds Necklace n is connected;

theorem :: NECKLACE:24
  for i,j being Nat st [i,j] in the InternalRel of Necklace n
  holds i = j + 1 or j = i + 1;

theorem :: NECKLACE:25
  for i,j being Nat 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:26
  n > 0 implies card ({[i+1,i] where i is Element of NAT:i+1 < n}) = n-1;

theorem :: NECKLACE:27
  n > 0 implies card the InternalRel of Necklace n = 2*(n-1);

theorem :: NECKLACE:28
  Necklace 1, ComplRelStr Necklace 1 are_isomorphic;

theorem :: NECKLACE:29
  Necklace 4, ComplRelStr Necklace 4 are_isomorphic;

theorem :: NECKLACE:30
  Necklace n, ComplRelStr Necklace n are_isomorphic implies n = 0 or n =
  1 or n = 4;