:: MSSCYC_1 semantic presentation

theorem Th1: :: MSSCYC_1:1
for b1 being finite Function st ( for b2 being set st b2 in dom b1 holds
b1 . b2 is finite ) holds
product b1 is finite
proof end;

definition
let c1 be Graph;
redefine mode Chain of c1 -> set means :Def1: :: MSSCYC_1:def 1
( a2 is FinSequence of the Edges of a1 & ex b1 being FinSequence of the Vertices of a1 st b1 is_vertex_seq_of a2 );
compatibility
for b1 being set holds
( b1 is Chain of c1 iff ( b1 is FinSequence of the Edges of c1 & ex b2 being FinSequence of the Vertices of c1 st b2 is_vertex_seq_of b1 ) )
proof end;
end;

:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :
for b1 being Graph
for b2 being set holds
( b2 is Chain of b1 iff ( b2 is FinSequence of the Edges of b1 & ex b3 being FinSequence of the Vertices of b1 st b3 is_vertex_seq_of b2 ) );

theorem Th2: :: MSSCYC_1:2
for b1 being Nat
for b2, b3 being FinSequence st b1 <= len b2 holds
1,b1 -cut b2 = 1,b1 -cut (b2 ^ b3)
proof end;

notation
let c1 be Graph;
let c2 be Chain of c1;
synonym directed c2 for oriented c2;
end;

definition
let c1 be Graph;
let c2 be Chain of c1;
attr a2 is cyclic means :Def2: :: MSSCYC_1:def 2
ex b1 being FinSequence of the Vertices of a1 st
( b1 is_vertex_seq_of a2 & b1 . 1 = b1 . (len b1) );
end;

:: deftheorem Def2 defines cyclic MSSCYC_1:def 2 :
for b1 being Graph
for b2 being Chain of b1 holds
( b2 is cyclic iff ex b3 being FinSequence of the Vertices of b1 st
( b3 is_vertex_seq_of b2 & b3 . 1 = b3 . (len b3) ) );

definition
let c1 be Graph;
attr a1 is empty means :Def3: :: MSSCYC_1:def 3
the Edges of a1 is empty;
end;

:: deftheorem Def3 defines empty MSSCYC_1:def 3 :
for b1 being Graph holds
( b1 is empty iff the Edges of b1 is empty );

registration
cluster empty MultiGraphStruct ;
existence
ex b1 being Graph st b1 is empty
proof end;
end;

theorem Th3: :: MSSCYC_1:3
for b1 being Graph holds (rng the Source of b1) \/ (rng the Target of b1) c= the Vertices of b1
proof end;

registration
cluster strict simple connected finite non empty MultiGraphStruct ;
existence
ex b1 being Graph st
( b1 is finite & b1 is simple & b1 is connected & not b1 is empty & b1 is strict )
proof end;
end;

registration
let c1 be non empty Graph;
cluster the Edges of a1 -> non empty ;
coherence
not the Edges of c1 is empty by Def3;
end;

theorem Th4: :: MSSCYC_1:4
for b1 being Graph
for b2 being set
for b3, b4 being Element of the Vertices of b1 st b3 = the Source of b1 . b2 & b4 = the Target of b1 . b2 holds
<*b3,b4*> is_vertex_seq_of <*b2*>
proof end;

theorem Th5: :: MSSCYC_1:5
for b1 being Graph
for b2 being set st b2 in the Edges of b1 holds
<*b2*> is directed Chain of b1
proof end;

registration
let c1 be non empty Graph;
cluster non empty V6 directed Chain of a1;
existence
ex b1 being Chain of c1 st
( b1 is directed & not b1 is empty & b1 is one-to-one )
proof end;
end;

Lemma7: for b1 being non empty Graph
for b2 being Chain of b1
for b3 being FinSequence of the Vertices of b1 st b2 is cyclic & b3 is_vertex_seq_of b2 holds
b3 . 1 = b3 . (len b3)
proof end;

theorem Th6: :: MSSCYC_1:6
for b1 being Graph
for b2 being Chain of b1
for b3 being FinSequence of the Vertices of b1 st b2 is cyclic & b3 is_vertex_seq_of b2 holds
b3 . 1 = b3 . (len b3)
proof end;

theorem Th7: :: MSSCYC_1:7
for b1 being Graph
for b2 being set st b2 in the Edges of b1 holds
for b3 being directed Chain of b1 st b3 = <*b2*> holds
vertex-seq b3 = <*(the Source of b1 . b2),(the Target of b1 . b2)*>
proof end;

theorem Th8: :: MSSCYC_1:8
for b1, b2 being Nat
for b3 being FinSequence holds len (b1,b2 -cut b3) <= len b3
proof end;

theorem Th9: :: MSSCYC_1:9
for b1, b2 being Nat
for b3 being non empty Graph
for b4 being directed Chain of b3 st 1 <= b1 & b1 <= b2 & b2 <= len b4 holds
b1,b2 -cut b4 is directed Chain of b3
proof end;

theorem Th10: :: MSSCYC_1:10
for b1 being non empty Graph
for b2 being non empty directed Chain of b1 holds len (vertex-seq b2) = (len b2) + 1
proof end;

registration
let c1 be non empty Graph;
let c2 be non empty directed Chain of c1;
cluster vertex-seq a2 -> non empty ;
coherence
not vertex-seq c2 is empty
proof end;
end;

theorem Th11: :: MSSCYC_1:11
for b1 being non empty Graph
for b2 being non empty directed Chain of b1
for b3 being Nat st 1 <= b3 & b3 <= len b2 holds
( (vertex-seq b2) . b3 = the Source of b1 . (b2 . b3) & (vertex-seq b2) . (b3 + 1) = the Target of b1 . (b2 . b3) )
proof end;

theorem Th12: :: MSSCYC_1:12
for b1, b2 being Nat
for b3 being non empty FinSequence st 1 <= b1 & b1 <= b2 & b2 <= len b3 holds
not b1,b2 -cut b3 is empty
proof end;

theorem Th13: :: MSSCYC_1:13
for b1, b2 being Nat
for b3 being non empty Graph
for b4, b5 being directed Chain of b3 st 1 <= b1 & b1 <= b2 & b2 <= len b4 & b5 = b1,b2 -cut b4 holds
vertex-seq b5 = b1,(b2 + 1) -cut (vertex-seq b4)
proof end;

theorem Th14: :: MSSCYC_1:14
for b1 being non empty Graph
for b2 being non empty directed Chain of b1 holds (vertex-seq b2) . ((len b2) + 1) = the Target of b1 . (b2 . (len b2))
proof end;

theorem Th15: :: MSSCYC_1:15
for b1 being non empty Graph
for b2, b3 being non empty directed Chain of b1 holds
( (vertex-seq b2) . ((len b2) + 1) = (vertex-seq b3) . 1 iff b2 ^ b3 is non empty directed Chain of b1 )
proof end;

theorem Th16: :: MSSCYC_1:16
for b1 being non empty Graph
for b2, b3, b4 being non empty directed Chain of b1 st b2 = b3 ^ b4 holds
( (vertex-seq b2) . 1 = (vertex-seq b3) . 1 & (vertex-seq b2) . ((len b2) + 1) = (vertex-seq b4) . ((len b4) + 1) )
proof end;

theorem Th17: :: MSSCYC_1:17
for b1 being non empty Graph
for b2 being non empty directed Chain of b1 st b2 is cyclic holds
(vertex-seq b2) . 1 = (vertex-seq b2) . ((len b2) + 1)
proof end;

theorem Th18: :: MSSCYC_1:18
for b1 being non empty Graph
for b2 being non empty directed Chain of b1 st b2 is cyclic holds
for b3 being Nat ex b4 being directed Chain of b1 st
( len b4 = b3 & b4 ^ b2 is non empty directed Chain of b1 )
proof end;

definition
let c1 be Graph;
attr a1 is directed_cycle-less means :Def4: :: MSSCYC_1:def 4
for b1 being directed Chain of a1 st not b1 is empty holds
not b1 is cyclic;
end;

:: deftheorem Def4 defines directed_cycle-less MSSCYC_1:def 4 :
for b1 being Graph holds
( b1 is directed_cycle-less iff for b2 being directed Chain of b1 st not b2 is empty holds
not b2 is cyclic );

notation
let c1 be Graph;
antonym with_directed_cycle c1 for directed_cycle-less c1;
end;

registration
cluster empty -> directed_cycle-less MultiGraphStruct ;
coherence
for b1 being Graph st b1 is empty holds
b1 is directed_cycle-less
proof end;
end;

definition
let c1 be Graph;
attr a1 is well-founded means :Def5: :: MSSCYC_1:def 5
for b1 being Element of the Vertices of a1 ex b2 being Nat st
for b3 being directed Chain of a1 st not b3 is empty & (vertex-seq b3) . ((len b3) + 1) = b1 holds
len b3 <= b2;
end;

:: deftheorem Def5 defines well-founded MSSCYC_1:def 5 :
for b1 being Graph holds
( b1 is well-founded iff for b2 being Element of the Vertices of b1 ex b3 being Nat st
for b4 being directed Chain of b1 st not b4 is empty & (vertex-seq b4) . ((len b4) + 1) = b2 holds
len b4 <= b3 );

registration
let c1 be empty Graph;
cluster -> empty Chain of a1;
coherence
for b1 being Chain of c1 holds b1 is empty
proof end;
end;

registration
cluster empty -> well-founded MultiGraphStruct ;
coherence
for b1 being Graph st b1 is empty holds
b1 is well-founded
proof end;
end;

registration
cluster non well-founded -> non empty MultiGraphStruct ;
coherence
for b1 being Graph st not b1 is well-founded holds
not b1 is empty
proof end;
end;

registration
cluster well-founded MultiGraphStruct ;
existence
ex b1 being Graph st b1 is well-founded
proof end;
end;

registration
cluster well-founded -> directed_cycle-less MultiGraphStruct ;
coherence
for b1 being Graph st b1 is well-founded holds
b1 is directed_cycle-less
proof end;
end;

registration
cluster non empty non well-founded MultiGraphStruct ;
existence
not for b1 being Graph holds b1 is well-founded
proof end;
end;

registration
cluster directed_cycle-less MultiGraphStruct ;
existence
ex b1 being Graph st b1 is directed_cycle-less
proof end;
end;

theorem Th19: :: MSSCYC_1:19
for b1 being DecoratedTree
for b2 being Node of b1
for b3 being Nat holds b2 | b3 is Node of b1
proof end;

theorem Th20: :: MSSCYC_1:20
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2 st not b3 is root holds
ex b4 being OperSymbol of b1 st b3 . {} = [b4,the carrier of b1]
proof end;

theorem Th21: :: MSSCYC_1:21
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being GeneratorSet of b2
for b4 being MSSubset of b2 st b3 c= b4 holds
b4 is GeneratorSet of b2
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty finitely-generated MSAlgebra of c1;
cluster V3 locally-finite GeneratorSet of a2;
existence
ex b1 being GeneratorSet of c2 st
( b1 is non-empty & b1 is locally-finite )
proof end;
end;

theorem Th22: :: MSSCYC_1:22
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V3 GeneratorSet of b2 ex b4 being ManySortedFunction of (FreeMSA b3),b2 st b4 is_epimorphism FreeMSA b3,b2
proof end;

theorem Th23: :: MSSCYC_1:23
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V3 GeneratorSet of b2 st not b2 is locally-finite holds
not FreeMSA b3 is locally-finite
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V3 locally-finite ManySortedSet of the carrier of c1;
let c3 be SortSymbol of c1;
cluster FreeGen a3,a2 -> finite ;
coherence
FreeGen c3,c2 is finite
proof end;
end;

theorem Th24: :: MSSCYC_1:24
canceled;

theorem Th25: :: MSSCYC_1:25
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being OperSymbol of b1 st the Arity of b1 . b3 = {} holds
dom (Den b3,b2) = {{} }
proof end;

definition
let c1 be non empty non void ManySortedSign ;
attr a1 is finitely_operated means :Def6: :: MSSCYC_1:def 6
for b1 being SortSymbol of a1 holds { b2 where B is OperSymbol of a1 : the_result_sort_of b2 = b1 } is finite;
end;

:: deftheorem Def6 defines finitely_operated MSSCYC_1:def 6 :
for b1 being non empty non void ManySortedSign holds
( b1 is finitely_operated iff for b2 being SortSymbol of b1 holds { b3 where B is OperSymbol of b1 : the_result_sort_of b3 = b2 } is finite );

theorem Th26: :: MSSCYC_1:26
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being SortSymbol of b1 st b1 is finitely_operated holds
Constants b2,b3 is finite
proof end;

theorem Th27: :: MSSCYC_1:27
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being SortSymbol of b1 holds { b4 where B is Element of the Sorts of (FreeMSA b2) . b3 : depth b4 = 0 } = (FreeGen b3,b2) \/ (Constants (FreeMSA b2),b3)
proof end;

theorem Th28: :: MSSCYC_1:28
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3, b4 being SortSymbol of b1
for b5 being OperSymbol of b1
for b6 being Element of the Sorts of (FreeMSA b2) . b3
for b7 being ArgumentSeq of Sym b5,b2
for b8 being Nat
for b9 being Element of the Sorts of (FreeMSA b2) . b4 st b6 = [b5,the carrier of b1] -tree b7 & b8 in dom b7 & b9 = b7 . b8 holds
depth b9 < depth b6
proof end;