:: Preliminaries to Circuits, II :: by Yatsuka Nakamura , Piotr Rudnicki , Andrzej Trybulec and Pauline N. Kawamoto :: :: Received December 13, 1994 :: Copyright (c) 1994-2021 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 MSUALG_1, GLIB_000, SUBSET_1, XBOOLE_0, UNIALG_2, STRUCT_0, RELAT_1, TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FINSEQ_1, MARGREL1, NAT_1, PARTFUN1, PRELAMB, MSAFREE, MSUALG_3, TREES_4, REALSET1, MSUALG_2, FINSET_1, PRALG_1, CARD_1, TREES_2, DTCONSTR, TREES_3, ZFMISC_1, LANG1, TDGROUP, TREES_1, MSAFREE2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, CARD_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FINSEQ_1, FUNCT_2, CARD_3, TREES_1, TREES_2, TREES_3, TREES_4, PBOOLE, STRUCT_0, MSUALG_1, FINSEQ_2, MSAFREE, MSUALG_2, FUNCOP_1, DTCONSTR, LANG1, PRE_POLY, RELSET_1, MSUALG_3; constructors XXREAL_0, NAT_1, MSUALG_3, MSAFREE, SEQ_4, RELSET_1, PRE_POLY, FINSEQ_2, NUMBERS; registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, TREES_1, CARD_3, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, RELAT_1, MSUALG_1, MSUALG_2, MSAFREE, ORDINAL1, PBOOLE, FINSEQ_1; requirements BOOLE, SUBSET; begin ::--------------------------------------------------------------------------- :: Many Sorted Signatures ::--------------------------------------------------------------------------- definition let S be ManySortedSign; mode Vertex of S is Element of S; end; definition let S be non empty ManySortedSign; func SortsWithConstants S -> Subset of S equals :: MSAFREE2:def 1 { v where v is SortSymbol of S : v is with_const_op } if S is non void otherwise {}; end; definition let G be non empty ManySortedSign; func InputVertices G -> Subset of G equals :: MSAFREE2:def 2 (the carrier of G) \ rng the ResultSort of G; func InnerVertices G -> Subset of G equals :: MSAFREE2:def 3 rng the ResultSort of G; end; theorem :: MSAFREE2:1 for G being void non empty ManySortedSign holds InputVertices G = the carrier of G; theorem :: MSAFREE2:2 for G being non void non empty ManySortedSign, v being Vertex of G st v in InputVertices G holds not ex o being OperSymbol of G st the_result_sort_of o = v; theorem :: MSAFREE2:3 for G being non empty ManySortedSign holds SortsWithConstants G c= InnerVertices G; theorem :: MSAFREE2:4 for G being non empty ManySortedSign holds InputVertices G misses SortsWithConstants G; definition let IT be non empty ManySortedSign; attr IT is with_input_V means :: MSAFREE2:def 4 InputVertices IT <> {}; end; registration cluster non void with_input_V for non empty ManySortedSign; end; registration let G be with_input_V non empty ManySortedSign; cluster InputVertices G -> non empty; end; registration let G be non void non empty ManySortedSign; cluster InnerVertices G -> non empty; end; definition let S be non empty ManySortedSign; let MSA be non-empty MSAlgebra over S; mode InputValues of MSA -> ManySortedSet of InputVertices S means :: MSAFREE2:def 5 for v being Vertex of S st v in InputVertices S holds it.v in (the Sorts of MSA).v; end; :: Generalize this for arbitrary subset of the carrier definition let S be non empty ManySortedSign; attr S is Circuit-like means :: MSAFREE2:def 6 for S9 being non void non empty ManySortedSign st S9 = S for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2; end; registration cluster void -> Circuit-like for non empty ManySortedSign; end; registration cluster non void Circuit-like strict for non empty ManySortedSign; end; definition let IIG be Circuit-like non void non empty ManySortedSign; let v be Vertex of IIG such that v in InnerVertices IIG; func action_at v -> OperSymbol of IIG means :: MSAFREE2:def 7 the_result_sort_of it = v; end; begin ::--------------------------------------------------------------------------- :: Free Many Sorted Algebras ::--------------------------------------------------------------------------- theorem :: MSAFREE2:5 for S being non void non empty ManySortedSign, A being MSAlgebra over S, o being OperSymbol of S, p being FinSequence st len p = len the_arity_of o & for k being Nat st k in dom p holds p.k in (the Sorts of A).((the_arity_of o)/. k) holds p in Args (o, A); definition let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over S; func FreeEnv MSA -> free strict non-empty MSAlgebra over S equals :: MSAFREE2:def 8 FreeMSA (the Sorts of MSA); end; definition let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over S; func Eval MSA -> ManySortedFunction of FreeEnv MSA, MSA means :: MSAFREE2:def 9 it is_homomorphism FreeEnv MSA, MSA & for s being SortSymbol of S, x, y being set st y in FreeSort(the Sorts of MSA, s) & y = root-tree [x, s] & x in (the Sorts of MSA).s holds it.s.y = x; end; theorem :: MSAFREE2:6 for S being non void non empty ManySortedSign, A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A; definition let S be non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is finitely-generated means :: MSAFREE2:def 10 for S9 being non void non empty ManySortedSign st S9 = S for A being MSAlgebra over S9 st A = IT ex G being GeneratorSet of A st G is finite-yielding if S is not void otherwise the Sorts of IT is finite-yielding; end; definition let S be non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is finite-yielding means :: MSAFREE2:def 11 the Sorts of IT is finite-yielding; end; registration let S be non empty ManySortedSign; cluster finite-yielding -> finitely-generated for non-empty MSAlgebra over S; end; definition let S be non empty ManySortedSign; func Trivial_Algebra S -> strict MSAlgebra over S means :: MSAFREE2:def 12 the Sorts of it = (the carrier of S) --> {0}; end; registration let S be non empty ManySortedSign; cluster finite-yielding non-empty strict for MSAlgebra over S; end; definition let IT be non empty ManySortedSign; attr IT is monotonic means :: MSAFREE2:def 13 for A being finitely-generated non-empty MSAlgebra over IT holds A is finite-yielding; end; registration cluster non void finite monotonic Circuit-like for non empty ManySortedSign; end; theorem :: MSAFREE2:7 for S being non void non empty ManySortedSign for X being non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of FreeMSA X).v holds e is finite DecoratedTree; theorem :: MSAFREE2:8 for S being non void non empty ManySortedSign, X being non-empty finite-yielding ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated; theorem :: MSAFREE2:9 for S being non void non empty ManySortedSign, A being non-empty MSAlgebra over S, v being Vertex of S, e being Element of (the Sorts of FreeEnv A).v st v in InputVertices S ex x being Element of (the Sorts of A).v st e = root-tree [x, v]; theorem :: MSAFREE2:10 for S being non void non empty ManySortedSign, X being non-empty ManySortedSet of the carrier of S, o being OperSymbol of S, p being DTree-yielding FinSequence st [o,the carrier of S]-tree p in (the Sorts of FreeMSA X).(the_result_sort_of o) holds len p = len the_arity_of o; theorem :: MSAFREE2:11 for S being non void non empty ManySortedSign, X being non-empty ManySortedSet of the carrier of S, o being OperSymbol of S, p being DTree-yielding FinSequence st [o,the carrier of S]-tree p in (the Sorts of FreeMSA X).(the_result_sort_of o) holds for i being Nat st i in dom the_arity_of o holds p.i in (the Sorts of FreeMSA X).((the_arity_of o).i); registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S; cluster -> finite non empty Function-like Relation-like for Element of (the Sorts of FreeMSA X).v; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S; cluster Function-like Relation-like for Element of (the Sorts of FreeMSA X).v; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be Vertex of S; cluster -> DecoratedTree-like for Function-like Relation-like Element of (the Sorts of FreeMSA X).v; end; registration let IIG be non void non empty ManySortedSign; let X be non-empty ManySortedSet of the carrier of IIG, v be Vertex of IIG; cluster finite for Element of (the Sorts of FreeMSA X).v; end; theorem :: MSAFREE2:12 for S being non void non empty ManySortedSign, X being non-empty ManySortedSet of the carrier of S, v being Vertex of S, o being OperSymbol of S , e being Element of (the Sorts of FreeMSA X).v st e.{} = [o,the carrier of S] ex p being DTree-yielding FinSequence st len p = len the_arity_of o & for i being Nat st i in dom p holds p.i in (the Sorts of FreeMSA X).((the_arity_of o) .i); definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of FreeMSA X ).v; func depth e -> Nat means :: MSAFREE2:def 14 ex dt being finite DecoratedTree, t being finite Tree st dt = e & t = dom dt & it = height t; end;