:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki

::

:: Received February 14, 1996

:: Copyright (c) 1996-2017 Association of Mizar Users

definition

let G be Graph;

for b_{1} being set holds

( b_{1} is Chain of G iff ( b_{1} is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b_{1} ) )

end;
redefine mode Chain of G means :Def1: :: MSSCYC_1:def 1

( it is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of it );

compatibility ( it is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of it );

for b

( b

proof end;

:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :

for G being Graph

for b_{2} being set holds

( b_{2} is Chain of G iff ( b_{2} is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b_{2} ) );

for G being Graph

for b

( b

::$CT

definition

let G be Graph;

let IT be Chain of G;

end;
let IT be Chain of G;

attr IT is cyclic means :: MSSCYC_1:def 2

ex p being FinSequence of the carrier of G st

( p is_vertex_seq_of IT & p . 1 = p . (len p) );

ex p being FinSequence of the carrier of G st

( p is_vertex_seq_of IT & p . 1 = p . (len p) );

:: deftheorem defines cyclic MSSCYC_1:def 2 :

for G being Graph

for IT being Chain of G holds

( IT is cyclic iff ex p being FinSequence of the carrier of G st

( p is_vertex_seq_of IT & p . 1 = p . (len p) ) );

for G being Graph

for IT being Chain of G holds

( IT is cyclic iff ex p being FinSequence of the carrier of G st

( p is_vertex_seq_of IT & p . 1 = p . (len p) ) );

registration

existence

ex b_{1} being Graph st

( b_{1} is finite & b_{1} is simple & b_{1} is connected & not b_{1} is void & b_{1} is strict )

end;
ex b

( b

proof end;

theorem Th3: :: MSSCYC_1:4

for G being Graph

for e being set

for s, t being Element of the carrier of G st s = the Source of G . e & t = the Target of G . e holds

<*s,t*> is_vertex_seq_of <*e*>

for e being set

for s, t being Element of the carrier of G st s = the Source of G . e & t = the Target of G . e holds

<*s,t*> is_vertex_seq_of <*e*>

proof end;

registration

let G be non void Graph;

ex b_{1} being Chain of G st

( b_{1} is directed & not b_{1} is empty & b_{1} is V17() )

end;
cluster Relation-like NAT -defined Function-like V17() non empty finite FinSequence-like FinSubsequence-like directed for Chain of G;

existence ex b

( b

proof end;

Lm1: for G being Graph

for c being Chain of G

for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds

p . 1 = p . (len p)

proof end;

theorem Th6: :: MSSCYC_1:7

for G being Graph

for e being set st e in the carrier' of G holds

for fe being directed Chain of G st fe = <*e*> holds

vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>

for e being set st e in the carrier' of G holds

for fe being directed Chain of G st fe = <*e*> holds

vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>

proof end;

theorem :: MSSCYC_1:9

for m, n being Nat

for G being non void Graph

for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds

(m,n) -cut c is directed Chain of G

for G being non void Graph

for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds

(m,n) -cut c is directed Chain of G

proof end;

theorem Th9: :: MSSCYC_1:10

for G being non void Graph

for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1

for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1

proof end;

registration

let G be non void Graph;

let oc be non empty directed Chain of G;

coherence

not vertex-seq oc is empty

end;
let oc be non empty directed Chain of G;

coherence

not vertex-seq oc is empty

proof end;

theorem Th10: :: MSSCYC_1:11

for G being non void Graph

for oc being non empty directed Chain of G

for n being Nat st 1 <= n & n <= len oc holds

( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )

for oc being non empty directed Chain of G

for n being Nat st 1 <= n & n <= len oc holds

( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )

proof end;

theorem Th11: :: MSSCYC_1:12

for m, n being Nat

for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds

not (m,n) -cut f is empty

for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds

not (m,n) -cut f is empty

proof end;

theorem :: MSSCYC_1:13

for m, n being Nat

for G being non void Graph

for c, c1 being directed Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c holds

vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)

for G being non void Graph

for c, c1 being directed Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c holds

vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)

proof end;

theorem Th13: :: MSSCYC_1:14

for G being non void Graph

for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))

for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))

proof end;

theorem Th14: :: MSSCYC_1:15

for G being non void Graph

for c1, c2 being non empty directed Chain of G holds

( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )

for c1, c2 being non empty directed Chain of G holds

( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )

proof end;

theorem Th15: :: MSSCYC_1:16

for G being non void Graph

for c, c1, c2 being non empty directed Chain of G st c = c1 ^ c2 holds

( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )

for c, c1, c2 being non empty directed Chain of G st c = c1 ^ c2 holds

( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )

proof end;

theorem Th16: :: MSSCYC_1:17

for G being non void Graph

for oc being non empty directed Chain of G st oc is cyclic holds

(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)

for oc being non empty directed Chain of G st oc is cyclic holds

(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)

proof end;

theorem Th17: :: MSSCYC_1:18

for G being non void Graph

for c being non empty directed Chain of G st c is cyclic holds

for n being Nat ex ch being directed Chain of G st

( len ch = n & ch ^ c is non empty directed Chain of G )

for c being non empty directed Chain of G st c is cyclic holds

for n being Nat ex ch being directed Chain of G st

( len ch = n & ch ^ c is non empty directed Chain of G )

proof end;

definition

let IT be Graph;

end;
attr IT is directed_cycle-less means :: MSSCYC_1:def 3

for dc being directed Chain of IT st not dc is empty holds

not dc is cyclic ;

for dc being directed Chain of IT st not dc is empty holds

not dc is cyclic ;

:: deftheorem defines directed_cycle-less MSSCYC_1:def 3 :

for IT being Graph holds

( IT is directed_cycle-less iff for dc being directed Chain of IT st not dc is empty holds

not dc is cyclic );

for IT being Graph holds

( IT is directed_cycle-less iff for dc being directed Chain of IT st not dc is empty holds

not dc is cyclic );

registration
end;

:: deftheorem defines well-founded MSSCYC_1:def 4 :

for IT being Graph holds

( IT is well-founded iff for v being Element of the carrier of IT ex n being Nat st

for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds

len c <= n );

for IT being Graph holds

( IT is well-founded iff for v being Element of the carrier of IT ex n being Nat st

for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds

len c <= n );

registration
end;

registration
end;

registration
end;

registration

coherence

for b_{1} being Graph st b_{1} is well-founded holds

b_{1} is directed_cycle-less

end;
for b

b

proof end;

theorem :: MSSCYC_1:20

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of the carrier of S

for t being Term of S,X st not t is root holds

ex o being OperSymbol of S st t . {} = [o, the carrier of S]

for X being V2() ManySortedSet of the carrier of S

for t being Term of S,X st not t is root holds

ex o being OperSymbol of S st t . {} = [o, the carrier of S]

proof end;

theorem Th20: :: MSSCYC_1:21

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for G being GeneratorSet of A

for B being MSSubset of A st G c= B holds

B is GeneratorSet of A

for A being MSAlgebra over S

for G being GeneratorSet of A

for B being MSSubset of A st G c= B holds

B is GeneratorSet of A

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty finitely-generated MSAlgebra over S;

ex b_{1} being GeneratorSet of A st

( b_{1} is V2() & b_{1} is V28() )

end;
let A be non-empty finitely-generated MSAlgebra over S;

cluster Relation-like V2() the carrier of S -defined Function-like non empty V28() total for GeneratorSet of A;

existence ex b

( b

proof end;

theorem Th21: :: MSSCYC_1:22

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A

for A being non-empty MSAlgebra over S

for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A

proof end;

theorem :: MSSCYC_1:23

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being V2() GeneratorSet of A st not A is finite-yielding holds

not FreeMSA X is finite-yielding

for A being non-empty MSAlgebra over S

for X being V2() GeneratorSet of A st not A is finite-yielding holds

not FreeMSA X is finite-yielding

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V2() V28() ManySortedSet of the carrier of S;

let v be SortSymbol of S;

coherence

FreeGen (v,X) is finite

end;
let X be V2() V28() ManySortedSet of the carrier of S;

let v be SortSymbol of S;

coherence

FreeGen (v,X) is finite

proof end;

theorem Th23: :: MSSCYC_1:24

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for o being OperSymbol of S st the Arity of S . o = {} holds

dom (Den (o,A)) = {{}}

for A being non-empty MSAlgebra over S

for o being OperSymbol of S st the Arity of S . o = {} holds

dom (Den (o,A)) = {{}}

proof end;

definition

let IT be non empty non void ManySortedSign ;

end;
attr IT is finitely_operated means :: MSSCYC_1:def 5

for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite ;

for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite ;

:: deftheorem defines finitely_operated MSSCYC_1:def 5 :

for IT being non empty non void ManySortedSign holds

( IT is finitely_operated iff for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite );

for IT being non empty non void ManySortedSign holds

( IT is finitely_operated iff for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite );

theorem :: MSSCYC_1:25

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for v being SortSymbol of S st S is finitely_operated holds

Constants (A,v) is finite

for A being non-empty MSAlgebra over S

for v being SortSymbol of S st S is finitely_operated holds

Constants (A,v) is finite

proof end;

theorem :: MSSCYC_1:26

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of the carrier of S

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))

for X being V2() ManySortedSet of the carrier of S

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))

proof end;

theorem :: MSSCYC_1:27

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of the carrier of S

for v, vk being SortSymbol of S

for o being OperSymbol of S

for t being Element of the Sorts of (FreeMSA X) . v

for a being ArgumentSeq of Sym (o,X)

for k being Element of NAT

for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds

depth ak < depth t

for X being V2() ManySortedSet of the carrier of S

for v, vk being SortSymbol of S

for o being OperSymbol of S

for t being Element of the Sorts of (FreeMSA X) . v

for a being ArgumentSeq of Sym (o,X)

for k being Element of NAT

for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a & k in dom a & ak = a . k holds

depth ak < depth t

proof end;