:: MSSCYC_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let S be ManySortedSign ;
defpred S1[ set ] means ex op, v being set st
( $1 = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) );
func InducedEdges S -> set means :Def1: :: MSSCYC_2:def 1
for x being set holds
( x in it iff ex op, v being set st
( x = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex op, v being set st
( x = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex op, v being set st
( x = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds
( x in b2 iff ex op, v being set st
( x = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines InducedEdges MSSCYC_2:def 1 :
for S being ManySortedSign
for b2 being set holds
( b2 = InducedEdges S iff for x being set holds
( x in b2 iff ex op, v being set st
( x = [op,v] & op in the OperSymbols of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) );

theorem Th1: :: MSSCYC_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being ManySortedSign holds InducedEdges S c= [:the OperSymbols of S,the carrier of S:]
proof end;

definition
let S be ManySortedSign ;
set IE = InducedEdges S;
set IV = the carrier of S;
func InducedSource S -> Function of InducedEdges S,the carrier of S means :Def2: :: MSSCYC_2:def 2
for e being set st e in InducedEdges S holds
it . e = e `2 ;
existence
ex b1 being Function of InducedEdges S,the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = e `2
proof end;
uniqueness
for b1, b2 being Function of InducedEdges S,the carrier of S st ( for e being set st e in InducedEdges S holds
b1 . e = e `2 ) & ( for e being set st e in InducedEdges S holds
b2 . e = e `2 ) holds
b1 = b2
proof end;
set OS = the OperSymbols of S;
set RS = the ResultSort of S;
func InducedTarget S -> Function of InducedEdges S,the carrier of S means :Def3: :: MSSCYC_2:def 3
for e being set st e in InducedEdges S holds
it . e = the ResultSort of S . (e `1 );
existence
ex b1 being Function of InducedEdges S,the carrier of S st
for e being set st e in InducedEdges S holds
b1 . e = the ResultSort of S . (e `1 )
proof end;
uniqueness
for b1, b2 being Function of InducedEdges S,the carrier of S st ( for e being set st e in InducedEdges S holds
b1 . e = the ResultSort of S . (e `1 ) ) & ( for e being set st e in InducedEdges S holds
b2 . e = the ResultSort of S . (e `1 ) ) holds
b1 = b2
proof end;
end;

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

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

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

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

theorem Th2: :: MSSCYC_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V2 ManySortedSet of the carrier of S
for v being SortSymbol of S
for n being Nat st 1 <= n holds
( ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n iff ex c being directed Chain of InducedGraph S st
( len c = n & (vertex-seq c) . ((len c) + 1) = v ) )
proof end;

theorem :: MSSCYC_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty void ManySortedSign holds
( S is monotonic iff InducedGraph S is well-founded )
proof end;

theorem :: MSSCYC_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign st S is monotonic holds
InducedGraph S is well-founded
proof end;

theorem Th5: :: MSSCYC_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V2 locally-finite ManySortedSet of the carrier of S st S is finitely_operated holds
for n being Nat
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite
proof end;

theorem :: MSSCYC_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign st S is finitely_operated & InducedGraph S is well-founded holds
S is monotonic
proof end;