MSSCYC_2: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {II}

:: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {II}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received April 10, 1996
:: Copyright (c) 1996-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, NAT_1, MSUALG_1, STRUCT_0, SUBSET_1, RELAT_1, FUNCT_1, ZFMISC_1, TARSKI, MCART_1, XBOOLE_0, GRAPH_1, PBOOLE, XXREAL_0, MSAFREE, MSAFREE2, WAYBEL_0, TREES_2, FINSEQ_1, GRAPH_2, ARYTM_3, MSATERM, FINSET_1, TREES_1, TREES_9, TREES_4, MARGREL1, ORDINAL4, RFINSEQ, ARYTM_1, CARD_1, PARTFUN1, FUNCT_6, TREES_3, TREES_A, MSSCYC_1, CARD_3, UNIALG_2, MSSCYC_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1, STRUCT_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, RFINSEQ, FINSET_1, TREES_1, TREES_2, TREES_3, TREES_4, CARD_3, GRAPH_1, GRAPH_2, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, MSAFREE2, XXREAL_2, CIRCUIT1, TREES_9, MSATERM, MSSCYC_1, FINSEQ_1, XXREAL_0;
definitions TARSKI, MSAFREE2;
theorems TARSKI, NAT_1, MCART_1, ZFMISC_1, MSSCYC_1, FUNCT_6, CARD_1, CARD_3, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR, MSUALG_1, MSAFREE, MSAFREE2, CIRCUIT1, TREES_9, MSATERM, XBOOLE_1, ORDINAL1, XREAL_1, XXREAL_0, PARTFUN1, XXREAL_2, FINSET_1, CARD_2, XTUPLE_0;
schemes NAT_1, FINSEQ_1, FUNCT_2, RECDEF_1, FRAENKEL, TOPREAL1, PBOOLE, XBOOLE_0;
registrations XBOOLE_0, ORDINAL1, FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, GRAPH_1, MSUALG_1, MSAFREE, MSATERM, MSAFREE2, MSSCYC_1, XXREAL_2, PBOOLE, RELSET_1, FUNCT_1, TREES_1, CARD_2, XTUPLE_0;
constructors HIDDEN, WELLORD2, REAL_1, NAT_1, RFINSEQ, MSUALG_2, MSATERM, CIRCUIT1, GRAPH_2, MSSCYC_1, XXREAL_2, RELSET_1, XTUPLE_0, XREAL_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MSAFREE2;
expansions TARSKI, MSAFREE2;

definition

let S be ManySortedSign ;
defpred S₁[ 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 ) );

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

proof end;

proof end;

end;

:: deftheorem Def1 defines InducedEdges MSSCYC_2:def 1 :

theorem Th1: :: MSSCYC_2:1

for S being ManySortedSign holds InducedEdges S c= [: the carrier' 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 object st e in InducedEdges S holds
it . e = e `2 ;

proof end;

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

proof end;

proof end;

end;

:: deftheorem Def2 defines InducedSource MSSCYC_2:def 2 :

:: deftheorem Def3 defines InducedTarget MSSCYC_2:def 3 :

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

end;

:: deftheorem defines InducedGraph MSSCYC_2:def 4 :

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

proof end;

theorem :: MSSCYC_2:3

for S being non empty void ManySortedSign holds
( 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

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

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

proof end;