:: 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-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors WELLORD2, REAL_1, NAT_1, RFINSEQ, MSUALG_2, MSATERM, CIRCUIT1,
GRAPH_2, MSSCYC_1, XXREAL_2, RELSET_1, XTUPLE_0, XREAL_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;
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 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, 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
carrier' 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 object 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 object 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
finite-yielding 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;