:: MSSCYC_2 semantic presentation

definition
let c1 be ManySortedSign ;
defpred S1[ set ] means ex b1, b2 being set st
( a1 = [b1,b2] & b1 in the OperSymbols of c1 & b2 in the carrier of c1 & ex b3 being Natex b4 being Element of the carrier of c1 * st
( the Arity of c1 . b1 = b4 & b3 in dom b4 & b4 . b3 = b2 ) );
func InducedEdges c1 -> set means :Def1: :: MSSCYC_2:def 1
for b1 being set holds
( b1 in a2 iff ex b2, b3 being set st
( b1 = [b2,b3] & b2 in the OperSymbols of a1 & b3 in the carrier of a1 & ex b4 being Natex b5 being Element of the carrier of a1 * st
( the Arity of a1 . b2 = b5 & b4 in dom b5 & b5 . b4 = b3 ) ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3, b4 being set st
( b2 = [b3,b4] & b3 in the OperSymbols of c1 & b4 in the carrier of c1 & ex b5 being Natex b6 being Element of the carrier of c1 * st
( the Arity of c1 . b3 = b6 & b5 in dom b6 & b6 . b5 = b4 ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4, b5 being set st
( b3 = [b4,b5] & b4 in the OperSymbols of c1 & b5 in the carrier of c1 & ex b6 being Natex b7 being Element of the carrier of c1 * st
( the Arity of c1 . b4 = b7 & b6 in dom b7 & b7 . b6 = b5 ) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5 being set st
( b3 = [b4,b5] & b4 in the OperSymbols of c1 & b5 in the carrier of c1 & ex b6 being Natex b7 being Element of the carrier of c1 * st
( the Arity of c1 . b4 = b7 & b6 in dom b7 & b7 . b6 = b5 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines InducedEdges MSSCYC_2:def 1 :
for b1 being ManySortedSign
for b2 being set holds
( b2 = InducedEdges b1 iff for b3 being set holds
( b3 in b2 iff ex b4, b5 being set st
( b3 = [b4,b5] & b4 in the OperSymbols of b1 & b5 in the carrier of b1 & ex b6 being Natex b7 being Element of the carrier of b1 * st
( the Arity of b1 . b4 = b7 & b6 in dom b7 & b7 . b6 = b5 ) ) ) );

theorem Th1: :: MSSCYC_2:1
for b1 being ManySortedSign holds InducedEdges b1 c= [:the OperSymbols of b1,the carrier of b1:]
proof end;

definition
let c1 be ManySortedSign ;
set c2 = InducedEdges c1;
set c3 = the carrier of c1;
func InducedSource c1 -> Function of InducedEdges a1,the carrier of a1 means :Def2: :: MSSCYC_2:def 2
for b1 being set st b1 in InducedEdges a1 holds
a2 . b1 = b1 `2 ;
existence
ex b1 being Function of InducedEdges c1,the carrier of c1 st
for b2 being set st b2 in InducedEdges c1 holds
b1 . b2 = b2 `2
proof end;
uniqueness
for b1, b2 being Function of InducedEdges c1,the carrier of c1 st ( for b3 being set st b3 in InducedEdges c1 holds
b1 . b3 = b3 `2 ) & ( for b3 being set st b3 in InducedEdges c1 holds
b2 . b3 = b3 `2 ) holds
b1 = b2
proof end;
set c4 = the OperSymbols of c1;
set c5 = the ResultSort of c1;
func InducedTarget c1 -> Function of InducedEdges a1,the carrier of a1 means :Def3: :: MSSCYC_2:def 3
for b1 being set st b1 in InducedEdges a1 holds
a2 . b1 = the ResultSort of a1 . (b1 `1 );
existence
ex b1 being Function of InducedEdges c1,the carrier of c1 st
for b2 being set st b2 in InducedEdges c1 holds
b1 . b2 = the ResultSort of c1 . (b2 `1 )
proof end;
uniqueness
for b1, b2 being Function of InducedEdges c1,the carrier of c1 st ( for b3 being set st b3 in InducedEdges c1 holds
b1 . b3 = the ResultSort of c1 . (b3 `1 ) ) & ( for b3 being set st b3 in InducedEdges c1 holds
b2 . b3 = the ResultSort of c1 . (b3 `1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines InducedSource MSSCYC_2:def 2 :
for b1 being ManySortedSign
for b2 being Function of InducedEdges b1,the carrier of b1 holds
( b2 = InducedSource b1 iff for b3 being set st b3 in InducedEdges b1 holds
b2 . b3 = b3 `2 );

:: deftheorem Def3 defines InducedTarget MSSCYC_2:def 3 :
for b1 being ManySortedSign
for b2 being Function of InducedEdges b1,the carrier of b1 holds
( b2 = InducedTarget b1 iff for b3 being set st b3 in InducedEdges b1 holds
b2 . b3 = the ResultSort of b1 . (b3 `1 ) );

definition
let c1 be non empty ManySortedSign ;
func InducedGraph c1 -> Graph equals :: MSSCYC_2:def 4
 MultiGraphStruct(# the carrier of a1,(InducedEdges a1),(InducedSource a1),(InducedTarget a1) #);
coherence
MultiGraphStruct(# the carrier of c1,(InducedEdges c1),(InducedSource c1),(InducedTarget c1) #) is Graph by GRAPH_1:def 1;
end;

:: deftheorem Def4 defines InducedGraph MSSCYC_2:def 4 :
for b1 being non empty ManySortedSign holds InducedGraph b1 = MultiGraphStruct(# the carrier of b1,(InducedEdges b1),(InducedSource b1),(InducedTarget b1) #);

theorem Th2: :: MSSCYC_2:2
for b1 being non empty non void ManySortedSign
for b2 being V2 ManySortedSet of the carrier of b1
for b3 being SortSymbol of b1
for b4 being Nat st 1 <= b4 holds
( ex b5 being Element of the Sorts of (FreeMSA b2) . b3 st depth b5 = b4 iff ex b5 being directed Chain of InducedGraph b1 st
( len b5 = b4 & (vertex-seq b5) . ((len b5) + 1) = b3 ) )
proof end;

theorem Th3: :: MSSCYC_2:3
for b1 being non empty void ManySortedSign holds
( b1 is monotonic iff InducedGraph b1 is well-founded )
proof end;

theorem Th4: :: MSSCYC_2:4
for b1 being non empty non void ManySortedSign st b1 is monotonic holds
InducedGraph b1 is well-founded
proof end;

theorem Th5: :: MSSCYC_2:5
for b1 being non empty non void ManySortedSign
for b2 being V2 locally-finite ManySortedSet of the carrier of b1 st b1 is finitely_operated holds
for b3 being Nat
for b4 being SortSymbol of b1 holds { b5 where B is Element of the Sorts of (FreeMSA b2) . b4 : depth b5 <= b3 } is finite
proof end;

theorem Th6: :: MSSCYC_2:6
for b1 being non empty non void ManySortedSign st b1 is finitely_operated & InducedGraph b1 is well-founded holds
b1 is monotonic
proof end;