The abstract of the Mizar article:

The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part II

by

Czeslaw Bylinski, and

Piotr Rudnicki

Received April 10, 1996

MML identifier: MSSCYC_2

[ Mizar article, MML identifier index ]

environ

 vocabulary MSUALG_1, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, AMI_1, ZF_REFLE,
      PBOOLE, MSAFREE, MSAFREE2, QUANTAL1, ORDERS_1, FINSEQ_1, GRAPH_2,
      MSATERM, FINSET_1, TREES_2, TREES_1, BOOLE, TREES_4, RFINSEQ, ARYTM_1,
      TREES_9, FREEALG, QC_LANG1, PARTFUN1, TREES_3, FUNCT_6, MSSCYC_1,
      PRE_CIRC, SQUARE_1, UNIALG_2, TARSKI, FINSEQ_4, PROB_1, MSSCYC_2, CARD_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, MCART_1, STRUCT_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, TOPREAL1,
      RFINSEQ, FINSET_1, TREES_1, TREES_2, TREES_3, TREES_4, PROB_1, CARD_3,
      GRAPH_1, GRAPH_2, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, MSAFREE2,
      PRE_CIRC, CIRCUIT1, TREES_9, MSATERM, MSSCYC_1, FINSEQ_1, FINSEQ_4;
 constructors MCART_1, RFINSEQ, GRAPH_2, WELLORD2, CIRCUIT1, TREES_9, MSATERM,
      MSSCYC_1, NAT_1, REAL_1, TOPREAL1, FINSOP_1, FINSEQ_4;
 clusters STRUCT_0, RELSET_1, FINSEQ_5, GRAPH_1, TREES_3, DTCONSTR, TREES_9,
      MSUALG_1, MSAFREE, PRE_CIRC, MSAFREE2, MSSCYC_1, GROUP_2, XREAL_0,
      FINSEQ_1, MSATERM, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve k, n for Nat;

definition let S be ManySortedSign;
 func InducedEdges S -> set means
:: 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, args being Element of (the carrier of S)*
     st (the Arity of S).op = args & n in dom args & args.n = v;
end;

theorem :: MSSCYC_2:1
for S being ManySortedSign
  holds InducedEdges S c= [: the OperSymbols of S, the carrier of S :];

definition let S be ManySortedSign;
 func InducedSource S -> Function of InducedEdges S, the carrier of S means
:: MSSCYC_2:def 2

 for e being set st e in InducedEdges S holds it.e = e`2;
 func InducedTarget S -> Function of InducedEdges S, the carrier of S means
:: MSSCYC_2:def 3

 for e being set st e in InducedEdges S holds it.e = (the ResultSort of S).e`1;
end;

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;

theorem :: MSSCYC_2:2
for S being non void (non empty ManySortedSign),
        X being non-empty ManySortedSet of the carrier of S,
        v being SortSymbol of S,
        n 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);

theorem :: MSSCYC_2:3
  for S being void non empty ManySortedSign
 holds S is monotonic iff InducedGraph S is well-founded;

theorem :: MSSCYC_2:4
  for S being non void (non empty ManySortedSign)
 st S is monotonic holds InducedGraph S is well-founded;

theorem :: MSSCYC_2:5
 for S being non void non empty ManySortedSign,
     X being non-empty locally-finite ManySortedSet of the carrier of S
  st S is finitely_operated
  for n being Nat, v being SortSymbol of S holds
 {t where t is Element of (the Sorts of FreeMSA X).v: depth t <= n} is finite;

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