:: The Correspondence Between Monotonic Many Sorted Signatures
:: and Well-Founded Graphs. {P}art {I}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received February 14, 1996
:: Copyright (c) 1996-2016 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, FINSET_1, FUNCT_1, RELAT_1, CARD_3, GRAPH_1, SUBSET_1,
TREES_2, FINSEQ_1, STRUCT_0, GRAPH_2, ARYTM_3, XXREAL_0, NAT_1, PARTFUN1,
TARSKI, ORDINAL4, XBOOLE_0, CARD_1, WAYBEL_0, GLIB_000, RELAT_2,
FUNCOP_1, ARYTM_1, TREES_4, TREES_1, MSUALG_1, PBOOLE, MSATERM, TREES_9,
ZFMISC_1, MSAFREE, MSUALG_2, MSAFREE2, MSUALG_3, PRELAMB, REALSET1,
GROUP_6, FUNCT_6, MARGREL1, UNIALG_2, DTCONSTR, TDGROUP, TREES_3,
TREES_A, MSSCYC_1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, XCMPLX_0, CARD_1,
ORDINAL1, NUMBERS, NAT_1, FINSEQ_2, STRUCT_0, CARD_3, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, FINSET_1, FUNCOP_1, FINSEQ_1, GRAPH_1, GRAPH_2,
TREES_1, TREES_2, TREES_3, FUNCT_6, TREES_4, LANG1, DTCONSTR, PBOOLE,
MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, TREES_9, MSATERM,
XXREAL_0, PRE_POLY;
constructors WELLORD2, FINSEQ_4, MSUALG_3, MSATERM, MSAFREE2, GRAPH_2,
RELSET_1, PRE_POLY, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, PRE_CIRC, TREES_9, STRUCT_0,
MSUALG_1, MSAFREE, MSAFREE2, EXTENS_1, ORDINAL1, CARD_1, GRAPH_1,
RELSET_1, TREES_1, MSATERM;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Some properties of graphs and trees
reserve G for Graph,
k, m, n for Nat;
definition
let G be Graph;
redefine mode Chain of G means
:: MSSCYC_1:def 1
it is FinSequence of the carrier' of G
& ex p being FinSequence of the carrier of G st p is_vertex_seq_of it;
end;
::$CT
theorem :: MSSCYC_1:2
for p,q being FinSequence st n<=len p holds (1,n)-cut p = (1,n)-cut (p ^q);
notation
let G be Graph;
let IT be Chain of G;
synonym IT is directed for IT is oriented;
end;
definition
let G be Graph;
let IT be Chain of G;
attr IT is cyclic means
:: MSSCYC_1:def 2
ex p being FinSequence of the carrier of G st
p is_vertex_seq_of IT & p.1 = p.(len p);
end;
registration
cluster void for Graph;
end;
theorem :: MSSCYC_1:3
for G being Graph holds rng (the Source of G) \/ rng (the Target
of G) c= the carrier of G;
registration
cluster finite simple connected non void strict for Graph;
end;
theorem :: MSSCYC_1:4
for e being set for s, t being Element of the carrier of G st s =
(the Source of G).e & t = (the Target of G).e holds <*s, t*> is_vertex_seq_of
<*e*>;
theorem :: MSSCYC_1:5
for e being set st e in the carrier' of G holds <*e*> is directed Chain of G;
reserve G for non void Graph;
registration
let G;
cluster directed non empty one-to-one for Chain of G;
end;
theorem :: MSSCYC_1:6
for G being Graph, c being Chain of G, vs being FinSequence of
the carrier of G st c is cyclic & vs is_vertex_seq_of c
holds vs.1 = vs.(len vs);
theorem :: MSSCYC_1:7
for G being Graph, e being set st e in the carrier' of G for fe
being directed Chain of G st fe = <*e*> holds vertex-seq fe = <*(the Source of
G).e, (the Target of G).e*>;
theorem :: MSSCYC_1:8
for f being FinSequence holds len (m,n)-cut f <= len f;
theorem :: MSSCYC_1:9
for c being directed Chain of G st 1<=m & m<=n & n<=len c holds (m,n)
-cut c is directed Chain of G;
theorem :: MSSCYC_1:10
for oc being non empty directed Chain of G holds len vertex-seq
oc = len oc +1;
registration
let G;
let oc be directed non empty Chain of G;
cluster vertex-seq oc -> non empty;
end;
theorem :: MSSCYC_1:11
for oc being directed non empty Chain of G, n st 1<=n & n<=len
oc holds (vertex-seq oc).n = (the Source of G).(oc.n) & (vertex-seq oc).(n+1) =
(the Target of G).(oc.n);
theorem :: MSSCYC_1:12
for f being non empty FinSequence st 1<=m & m<=n & n<=len f
holds (m,n)-cut f is non empty;
theorem :: MSSCYC_1:13
for c, c1 being directed Chain of G st 1<=m & m<=n & n<=len c & c1 = (
m,n)-cut c holds vertex-seq c1 = (m,n+1)-cut vertex-seq c;
theorem :: MSSCYC_1:14
for oc being directed non empty Chain of G holds (vertex-seq oc)
.(len oc +1) = (the Target of G).(oc.len oc);
theorem :: MSSCYC_1:15
for c1, c2 being directed non empty Chain of G holds (vertex-seq
c1).(len c1 + 1) = (vertex-seq c2).1 iff c1^c2 is directed non empty Chain of G
;
theorem :: MSSCYC_1:16
for c, c1, c2 being directed non empty Chain of G st c =c1^c2
holds (vertex-seq c).1 = (vertex-seq c1).1 & (vertex-seq c).(len c +1) = (
vertex-seq c2).(len c2 +1);
theorem :: MSSCYC_1:17
for oc being directed non empty Chain of G st oc is cyclic holds
(vertex-seq oc).1 = (vertex-seq oc).(len oc +1);
theorem :: MSSCYC_1:18
for c being directed non empty Chain of G st c is cyclic for n
ex ch being directed Chain of G st len ch = n & ch^c is directed non empty
Chain of G;
definition
let IT be Graph;
attr IT is directed_cycle-less means
:: MSSCYC_1:def 3
for dc being directed Chain of IT st dc is non empty holds dc is non cyclic;
end;
notation
let IT be Graph;
antonym IT is with_directed_cycle for IT is directed_cycle-less;
end;
registration
cluster void -> directed_cycle-less for Graph;
end;
definition
let IT be Graph;
attr IT is well-founded means
:: MSSCYC_1:def 4
for v being Element of the carrier of
IT ex n st for c being directed Chain of IT st c is non empty & (vertex-seq c).
(len c +1) = v holds len c <= n;
end;
registration
let G be void Graph;
cluster -> empty for Chain of G;
end;
registration
cluster void -> well-founded for Graph;
end;
registration
cluster non well-founded -> non void for Graph;
end;
registration
cluster well-founded for Graph;
end;
registration
cluster well-founded -> directed_cycle-less for Graph;
end;
registration
cluster non well-founded for Graph;
end;
registration
cluster directed_cycle-less for Graph;
end;
theorem :: MSSCYC_1:19
for t being DecoratedTree, p being Node of t, k being Element of NAT
holds p|k is Node of t;
begin :: Some properties of many sorted algebras
theorem :: MSSCYC_1:20
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, t being Term of S,X st t is not root
ex o being OperSymbol of S st t.{} = [o,the carrier of S];
theorem :: MSSCYC_1:21
for S being non void non empty ManySortedSign, A being MSAlgebra
over S, G being GeneratorSet of A, B being MSSubset of A st G c= B holds B is
GeneratorSet of A;
registration
let S be non void non empty ManySortedSign, A be finitely-generated
non-empty MSAlgebra over S;
cluster non-empty finite-yielding for GeneratorSet of A;
end;
theorem :: MSSCYC_1:22
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, X being non-empty GeneratorSet of A ex F being
ManySortedFunction of FreeMSA X, A st F is_epimorphism FreeMSA X, A;
theorem :: MSSCYC_1:23
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, X being non-empty GeneratorSet of A st A is non
finite-yielding holds FreeMSA X is non finite-yielding;
registration
let S be non void non empty ManySortedSign, X be non-empty finite-yielding
ManySortedSet of the carrier of S, v be SortSymbol of S;
cluster FreeGen(v, X) -> finite;
end;
theorem :: MSSCYC_1:24
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, o be OperSymbol of S st (the Arity of S).o = {} holds dom Den
(o, A) = {{}};
definition
let IT be non void non empty ManySortedSign;
attr IT is finitely_operated means
:: MSSCYC_1:def 5
for s being SortSymbol of IT holds
{o where o is OperSymbol of IT: the_result_sort_of o = s} is finite;
end;
theorem :: MSSCYC_1:25
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, v be SortSymbol of S st S is finitely_operated holds
Constants(A, v) is finite;
theorem :: MSSCYC_1:26
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, v being SortSymbol of S holds {t where t is
Element of (the Sorts of FreeMSA X).v: depth t = 0} = FreeGen(v, X) \/
Constants(FreeMSA X, v);
theorem :: MSSCYC_1:27
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, v, vk being SortSymbol of S, o being
OperSymbol of S, t being Element of (the Sorts of FreeMSA X).v, a being (
ArgumentSeq of Sym(o,X)), k being Element of NAT, ak being Element of (the
Sorts of FreeMSA X).vk st t = [o,the carrier of S]-tree a & k in dom a & ak = a
.k holds depth ak < depth t;