:: MSSCYC_1 semantic presentation

theorem :: MSSCYC_1:1

for f being finite Function st ( for x being set st x in dom f holds
f . x is finite ) holds
product f is finite

proof end;

definition

let G be Graph;
redefine mode Chain of G means :Def1: :: MSSCYC_1:def 1
( it is FinSequence of the Edges of G & ex p being FinSequence of the Vertices of G st p is_vertex_seq_of it );
compatibility

proof end;

end;

:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :

theorem :: MSSCYC_1:2

for n being Nat
for p, q being FinSequence st n <= len p holds
1,n -cut p = 1,n -cut (p ^ q)

proof end;

notation

let G be Graph;
let IT be Chain of G;
synonym directed IT for oriented IT;

end;

definition

let G be Graph;
let IT be Chain of G;
attr IT is cyclic means :Def2: :: MSSCYC_1:def 2
ex p being FinSequence of the Vertices of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) );

end;

:: deftheorem Def2 defines cyclic MSSCYC_1:def 2 :

definition

let IT be Graph;
attr IT is empty means :Def3: :: MSSCYC_1:def 3
the Edges of IT is empty;

end;

:: deftheorem Def3 defines empty MSSCYC_1:def 3 :

registration

cluster empty MultiGraphStruct ;
existence

proof end;

end;

theorem Th3: :: MSSCYC_1:3

for G being Graph holds (rng the Source of G) \/ (rng the Target of G) c= the Vertices of G

proof end;

registration

cluster strict simple connected finite non empty MultiGraphStruct ;
existence

proof end;

end;

registration

let G be non empty Graph;
cluster the Edges of G -> non empty ;
coherence by Def3;

end;

theorem Th4: :: MSSCYC_1:4

for G being Graph
for e being set
for s, t being Element of the Vertices 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;

theorem Th5: :: MSSCYC_1:5

for G being Graph
for e being set st e in the Edges of G holds
<*e*> is directed Chain of G

proof end;

registration

let G be non empty Graph;
cluster non empty V6 directed Chain of G;
existence

proof end;

end;

Lm1: for G being non empty Graph
for c being Chain of G
for p being FinSequence of the Vertices of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)

proof end;

theorem Th6: :: MSSCYC_1:6

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices of G st c is cyclic & vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs)

proof end;

theorem Th7: :: MSSCYC_1:7

for G being Graph
for e being set st e in the Edges 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:8

for m, n being Nat
for f being FinSequence holds len (m,n -cut f) <= len f

proof end;

theorem :: MSSCYC_1:9

for m, n being Nat
for G being non empty 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 Th10: :: MSSCYC_1:10

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

proof end;

registration

let G be non empty Graph;
let oc be non empty directed Chain of G;
cluster vertex-seq oc -> non empty ;
coherence

proof end;

end;

theorem Th11: :: MSSCYC_1:11

for G being non empty 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) )

proof end;

theorem Th12: :: 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

proof end;

theorem :: MSSCYC_1:13

for m, n being Nat
for G being non empty 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 Th14: :: MSSCYC_1:14

for G being non empty Graph
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 Th15: :: MSSCYC_1:15

for G being non empty 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 )

proof end;

theorem Th16: :: MSSCYC_1:16

for G being non empty 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) )

proof end;

theorem Th17: :: MSSCYC_1:17

for G being non empty 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)

proof end;

theorem Th18: :: MSSCYC_1:18

for G being non empty 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 )

proof end;

definition

let IT be Graph;
attr IT is directed_cycle-less means :Def4: :: MSSCYC_1:def 4
for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic;

end;

:: deftheorem Def4 defines directed_cycle-less MSSCYC_1:def 4 :

notation

let IT be Graph;
antonym with_directed_cycle IT for directed_cycle-less IT;

end;

registration

cluster empty -> directed_cycle-less MultiGraphStruct ;
coherence

proof end;

end;

definition

let IT be Graph;
attr IT is well-founded means :Def5: :: MSSCYC_1:def 5
for v being Element of the Vertices 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;

end;

:: deftheorem Def5 defines well-founded MSSCYC_1:def 5 :

registration

let G be empty Graph;
cluster -> empty Chain of G;
coherence

proof end;

end;

registration

cluster empty -> well-founded MultiGraphStruct ;
coherence

proof end;

end;

registration

cluster non well-founded -> non empty MultiGraphStruct ;
coherence

proof end;

end;

registration

cluster well-founded MultiGraphStruct ;
existence

proof end;

end;

registration

cluster well-founded -> directed_cycle-less MultiGraphStruct ;
coherence

proof end;

end;

registration

cluster non empty non well-founded MultiGraphStruct ;
existence

proof end;

end;

registration

cluster directed_cycle-less MultiGraphStruct ;
existence

proof end;

end;

theorem :: MSSCYC_1:19

for t being DecoratedTree
for p being Node of t
for k being Nat holds p | k is Node of t

proof end;

theorem :: MSSCYC_1:20

for S being non empty non void ManySortedSign
for X being V3 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 Th21: :: MSSCYC_1:21

for S being non empty non void ManySortedSign
for A being MSAlgebra of 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 of S;
cluster V3 locally-finite GeneratorSet of A;
existence

proof end;

end;

theorem Th22: :: MSSCYC_1:22

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for X being V3 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 of S
for X being V3 GeneratorSet of A st not A is locally-finite holds
not FreeMSA X is locally-finite

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V3 locally-finite ManySortedSet of the carrier of S;
let v be SortSymbol of S;
cluster FreeGen v,X -> finite ;
coherence

proof end;

end;

theorem :: MSSCYC_1:24

canceled;

theorem Th25: :: MSSCYC_1:25

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 ;
attr IT is finitely_operated means :Def6: :: MSSCYC_1:def 6
for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite;

end;

:: deftheorem Def6 defines finitely_operated MSSCYC_1:def 6 :

theorem :: MSSCYC_1:26

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for v being SortSymbol of S st S is finitely_operated holds
Constants A,v is finite

proof end;

theorem :: MSSCYC_1:27

for S being non empty non void ManySortedSign
for X being V3 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:28

for S being non empty non void ManySortedSign
for X being V3 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 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;