:: The Class of Series-Parallel Graphs, {I}
:: by Krzysztof Retel
::
:: Copyright (c) 2002-2018 Association of Mizar Users

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

theorem :: NECKLACE:2
for x1, x2, x3, y1, y2, y3 being set holds [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
proof end;

theorem :: NECKLACE:3
canceled;

::\$CT
theorem Th3: :: NECKLACE:4
for x being non zero Nat holds 0 in x
proof end;

registration
let X be set ;
cluster K200(X) -> one-to-one ;
coherence
proof end;
end;

theorem Th4: :: NECKLACE:5
for X being set holds card (id X) = card X
proof end;

registration
coherence
for b1 being Function st b1 is trivial holds
b1 is one-to-one
proof end;
end;

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

theorem Th6: :: NECKLACE:7
for f, g being one-to-one Function st dom f misses dom g & rng f misses rng g holds
(f +* g) " = (f ") +* (g ")
proof end;

theorem :: NECKLACE:8
for A, a, b being set holds (A --> a) +* (A --> b) = A --> b
proof end;

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

theorem Th9: :: NECKLACE:10
for a, b, c, d being set holds
not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) )
proof end;

scheme :: NECKLACE:sch 1
Convers{ F1() -> non empty set , F2() -> Relation, F3( set ) -> set , F4( set ) -> set , P1[ set ] } :
F2() ~ = { [F3(x),F4(x)] where x is Element of F1() : P1[x] }
provided
A1: F2() = { [F4(x),F3(x)] where x is Element of F1() : P1[x] }
proof end;

theorem :: NECKLACE:11
for i, j, n being Nat st i < j & j in Segm n holds
i in Segm n
proof end;

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;

:: deftheorem defines embeds NECKLACE:def 1 :
for R, S being RelStr holds
( S embeds R iff 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 ) ) ) );

definition
let R, S be non empty RelStr ;
:: original: embeds
redefine pred S embeds R;
reflexivity
for S being non empty RelStr holds (b1,b1)
proof end;
end;

theorem Th11: :: NECKLACE:12
for R, S, T being non empty RelStr st R embeds S & S embeds T holds
R embeds T
proof end;

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
for R being non empty RelStr holds
( R embeds R & R embeds R )
;
symmetry
for R, S being non empty RelStr st R embeds S & S embeds R holds
( S embeds R & R embeds S )
;
end;

:: deftheorem defines is_equimorphic_to NECKLACE:def 2 :
for R, S being non empty RelStr holds
( R is_equimorphic_to S iff ( R embeds S & S embeds R ) );

theorem :: NECKLACE:13
for R, S, T being non empty RelStr st R is_equimorphic_to S & S is_equimorphic_to T holds
R is_equimorphic_to T by Th11;

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

definition
let R be RelStr ;
attr R is symmetric means :Def3: :: NECKLACE:def 3
the InternalRel of R is_symmetric_in the carrier of R;
end;

:: deftheorem Def3 defines symmetric NECKLACE:def 3 :
for R being RelStr holds
( R is symmetric iff the InternalRel of R is_symmetric_in the carrier of R );

definition
let R be RelStr ;
attr R is asymmetric means :: NECKLACE:def 4
the InternalRel of R is asymmetric ;
end;

:: deftheorem defines asymmetric NECKLACE:def 4 :
for R being RelStr holds
( R is asymmetric iff the InternalRel of R is asymmetric );

theorem :: NECKLACE:14
for R being RelStr st R is asymmetric holds
the InternalRel of R misses the InternalRel of R ~
proof end;

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;

:: deftheorem defines irreflexive NECKLACE:def 5 :
for R being RelStr holds
( R is irreflexive iff for x being set st x in the carrier of R holds
not [x,x] in the InternalRel of R );

definition
let n be Nat;
func n -SuccRelStr -> strict RelStr means :Def6: :: NECKLACE:def 6
( the carrier of it = n & the InternalRel of it = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } );
existence
ex b1 being strict RelStr st
( the carrier of b1 = n & the InternalRel of b1 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = n & the InternalRel of b1 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } & the carrier of b2 = n & the InternalRel of b2 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } holds
b1 = b2
;
end;

:: deftheorem Def6 defines -SuccRelStr NECKLACE:def 6 :
for n being Nat
for b2 being strict RelStr holds
( b2 = n -SuccRelStr iff ( the carrier of b2 = n & the InternalRel of b2 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) );

theorem :: NECKLACE:15
for n being Nat holds n -SuccRelStr is asymmetric
proof end;

theorem Th15: :: NECKLACE:16
for n being Nat st n > 0 holds
card the InternalRel of () = n - 1
proof end;

definition
let R be RelStr ;
func SymRelStr R -> strict RelStr means :Def7: :: NECKLACE:def 7
( the carrier of it = the carrier of R & the InternalRel of it = the InternalRel of R \/ ( the InternalRel of R ~) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R & the InternalRel of b1 = the InternalRel of R \/ ( the InternalRel of R ~) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R & the InternalRel of b1 = the InternalRel of R \/ ( the InternalRel of R ~) & the carrier of b2 = the carrier of R & the InternalRel of b2 = the InternalRel of R \/ ( the InternalRel of R ~) holds
b1 = b2
;
end;

:: deftheorem Def7 defines SymRelStr NECKLACE:def 7 :
for R being RelStr
for b2 being strict RelStr holds
( b2 = SymRelStr R iff ( the carrier of b2 = the carrier of R & the InternalRel of b2 = the InternalRel of R \/ ( the InternalRel of R ~) ) );

registration
let R be RelStr ;
coherence
proof end;
end;

registration
cluster non empty symmetric for RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is symmetric )
proof end;
end;

registration
let R be symmetric RelStr ;
cluster the InternalRel of R -> symmetric ;
coherence
the InternalRel of R is symmetric
proof end;
end;

Lm1: for S, R being non empty RelStr st S,R are_isomorphic holds
card the InternalRel of S = card the InternalRel of R

proof end;

definition
let R be RelStr ;
func ComplRelStr R -> strict RelStr means :Def8: :: NECKLACE:def 8
( the carrier of it = the carrier of R & the InternalRel of it = ( the InternalRel of R ) \ (id the carrier of R) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R & the InternalRel of b1 = ( the InternalRel of R ) \ (id the carrier of R) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R & the InternalRel of b1 = ( the InternalRel of R ) \ (id the carrier of R) & the carrier of b2 = the carrier of R & the InternalRel of b2 = ( the InternalRel of R ) \ (id the carrier of R) holds
b1 = b2
;
end;

:: deftheorem Def8 defines ComplRelStr NECKLACE:def 8 :
for R being RelStr
for b2 being strict RelStr holds
( b2 = ComplRelStr R iff ( the carrier of b2 = the carrier of R & the InternalRel of b2 = ( the InternalRel of R `) \ (id the carrier of R) ) );

registration
let R be non empty RelStr ;
coherence
not ComplRelStr R is empty
proof end;
end;

theorem Th16: :: NECKLACE:17
for S, R being RelStr st S,R are_isomorphic holds
card the InternalRel of S = card the InternalRel of R
proof end;

definition
let n be Nat;
coherence ;
end;

:: deftheorem defines Necklace NECKLACE:def 9 :
for n being Nat holds Necklace n = SymRelStr ();

registration
let n be Nat;
coherence ;
end;

theorem Th17: :: NECKLACE:18
for n being Nat holds the InternalRel of () = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n }
proof end;

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

registration
let n be Nat;
coherence
proof end;
end;

theorem Th19: :: NECKLACE:20
for n being Nat holds the carrier of () = n
proof end;

registration
let n be non zero Nat;
cluster Necklace n -> non empty strict ;
coherence
not Necklace n is empty
by Th19;
end;

registration
let n be Nat;
cluster the carrier of () -> finite ;
coherence
the carrier of () is finite
by Th19;
end;

theorem Th20: :: NECKLACE:21
for n, i being Nat st i + 1 < n holds
[i,(i + 1)] in the InternalRel of ()
proof end;

theorem Th21: :: NECKLACE:22
for n, i being Nat st i in the carrier of () holds
i < n
proof end;

theorem :: NECKLACE:23
for n being non zero Nat holds Necklace n is connected
proof end;

theorem Th23: :: NECKLACE:24
for n, i, j being Nat holds
( not [i,j] in the InternalRel of () or i = j + 1 or j = i + 1 )
proof end;

theorem Th24: :: NECKLACE:25
for n, i, j being Nat st ( i = j + 1 or j = i + 1 ) & i in the carrier of () & j in the carrier of () holds
[i,j] in the InternalRel of ()
proof end;

theorem Th25: :: NECKLACE:26
for n being Nat st n > 0 holds
card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1
proof end;

theorem Th26: :: NECKLACE:27
for n being Nat st n > 0 holds
card the InternalRel of () = 2 * (n - 1)
proof end;

theorem :: NECKLACE:28
proof end;

theorem :: NECKLACE:29
proof end;

theorem :: NECKLACE:30
for n being Nat holds
( not Necklace n, ComplRelStr () are_isomorphic or n = 0 or n = 1 or n = 4 )
proof end;