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

::

:: Received April 10, 1996

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

definition

let S be ManySortedSign ;

defpred S_{1}[ object ] means ex op, v being set st

( $1 = [op,v] & op in the carrier' 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 ) );

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex op, v being set st

( x = [op,v] & op in the carrier' 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 b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex op, v being set st

( x = [op,v] & op in the carrier' 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 object holds

( x in b_{2} iff ex op, v being set st

( x = [op,v] & op in the carrier' 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

b_{1} = b_{2}

end;
defpred S

( $1 = [op,v] & op in the carrier' 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 object holds

( x in it iff ex op, v being set st

( x = [op,v] & op in the carrier' 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 for x being object holds

( x in it iff ex op, v being set st

( x = [op,v] & op in the carrier' 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 ) ) );

ex b

for x being object holds

( x in b

( x = [op,v] & op in the carrier' 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 b

( x in b

( x = [op,v] & op in the carrier' 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 object holds

( x in b

( x = [op,v] & op in the carrier' 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

b

proof end;

:: deftheorem Def1 defines InducedEdges MSSCYC_2:def 1 :

for S being ManySortedSign

for b_{2} being set holds

( b_{2} = InducedEdges S iff for x being object holds

( x in b_{2} iff ex op, v being set st

( x = [op,v] & op in the carrier' 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 S being ManySortedSign

for b

( b

( x in b

( x = [op,v] & op in the carrier' 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 ) ) ) );

definition

let S be ManySortedSign ;

set IE = InducedEdges S;

set IV = the carrier of S;

ex b_{1} being Function of (InducedEdges S), the carrier of S st

for e being object st e in InducedEdges S holds

b_{1} . e = e `2

for b_{1}, b_{2} being Function of (InducedEdges S), the carrier of S st ( for e being object st e in InducedEdges S holds

b_{1} . e = e `2 ) & ( for e being object st e in InducedEdges S holds

b_{2} . e = e `2 ) holds

b_{1} = b_{2}

set RS = the ResultSort of S;

ex b_{1} being Function of (InducedEdges S), the carrier of S st

for e being object st e in InducedEdges S holds

b_{1} . e = the ResultSort of S . (e `1)

for b_{1}, b_{2} being Function of (InducedEdges S), the carrier of S st ( for e being object st e in InducedEdges S holds

b_{1} . e = the ResultSort of S . (e `1) ) & ( for e being object st e in InducedEdges S holds

b_{2} . e = the ResultSort of S . (e `1) ) holds

b_{1} = b_{2}

end;
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 object st e in InducedEdges S holds

it . e = e `2 ;

existence for e being object st e in InducedEdges S holds

it . e = e `2 ;

ex b

for e being object st e in InducedEdges S holds

b

proof end;

uniqueness for b

b

b

b

proof end;

set OS = the carrier' 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 object st e in InducedEdges S holds

it . e = the ResultSort of S . (e `1);

existence for e being object st e in InducedEdges S holds

it . e = the ResultSort of S . (e `1);

ex b

for e being object st e in InducedEdges S holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines InducedSource MSSCYC_2:def 2 :

for S being ManySortedSign

for b_{2} being Function of (InducedEdges S), the carrier of S holds

( b_{2} = InducedSource S iff for e being object st e in InducedEdges S holds

b_{2} . e = e `2 );

for S being ManySortedSign

for b

( b

b

:: deftheorem Def3 defines InducedTarget MSSCYC_2:def 3 :

for S being ManySortedSign

for b_{2} being Function of (InducedEdges S), the carrier of S holds

( b_{2} = InducedTarget S iff for e being object st e in InducedEdges S holds

b_{2} . e = the ResultSort of S . (e `1) );

for S being ManySortedSign

for b

( b

b

definition

let S be non empty ManySortedSign ;

MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #) is Graph ;

end;
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) #);

MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #) is Graph ;

:: 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) #);

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

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 ) )

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

for S being non empty void ManySortedSign holds

( S is monotonic iff InducedGraph S is well-founded )

( S is monotonic iff InducedGraph S is well-founded )

proof end;

theorem :: MSSCYC_2:4

for S being non empty non void ManySortedSign st S is monotonic holds

InducedGraph S is well-founded

InducedGraph S is well-founded

proof end;

theorem Th5: :: MSSCYC_2:5

for S being non empty non void ManySortedSign

for X being V2() V39() 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

for X being V2() V39() 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

for S being non empty non void ManySortedSign st S is finitely_operated & InducedGraph S is well-founded holds

S is monotonic

S is monotonic

proof end;