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;