:: A Scheme for Extensions of Homomorphisms of Manysorted Algebras :: by Andrzej Trybulec :: :: 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 FUNCT_1, CARD_3, RELAT_1, TARSKI, XBOOLE_0, LANG1, SUBSET_1, DTCONSTR, TREES_4, FINSEQ_1, TDGROUP, TREES_3, TREES_2, STRUCT_0, MSUALG_1, PBOOLE, MSAFREE, ZFMISC_1, MARGREL1, PROB_2, NAT_1, PARTFUN1, MCART_1, MSUALG_3, MSAFREE1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_2, STRUCT_0, XTUPLE_0, MCART_1, FINSEQ_1, MULTOP_1, PROB_2, CARD_3, TREES_2, TREES_3, TREES_4, LANG1, DTCONSTR, PBOOLE, MSUALG_1, MSAFREE, MSUALG_3; constructors MULTOP_1, PROB_2, MSUALG_3, MSAFREE, RELSET_1, CAT_3, FINSEQ_2, XTUPLE_0; registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSEQ_1, RELAT_1, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, MSAFREE, ORDINAL1, PBOOLE, XTUPLE_0; requirements BOOLE, SUBSET; begin theorem :: MSAFREE1:1 for f,g being Function st g in product f holds rng g c= Union f; scheme :: MSAFREE1:sch 1 DTConstrUniq{DT()->non empty DTConstrStr, D()->non empty set, G(set) -> Element of D(), H(set, set, set) -> Element of D(), f1, f2() -> Function of TS( DT()), D() }: f1() = f2() provided for t being Symbol of DT() st t in Terminals DT() holds f1().(root-tree t) = G(t) and for nt being Symbol of DT(), ts being Element of (TS DT())* st nt ==> roots ts for x being Element of D()* st x = f1() * ts holds f1().(nt-tree ts) = H(nt, ts, x) and for t being Symbol of DT() st t in Terminals DT() holds f2().(root-tree t) = G(t) and for nt being Symbol of DT(), ts being Element of (TS DT())* st nt ==> roots ts for x being Element of D()* st x = f2() * ts holds f2().(nt-tree ts) = H(nt, ts, x); theorem :: MSAFREE1:2 :: MSAFREE:5 for S being non void non empty ManySortedSign, X being ManySortedSet of the carrier of S for o,b being object st [o,b] in REL(X) holds o in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the carrier of S}:] \/ Union coprod X)*; theorem :: MSAFREE1:3 :: MSAFREE:5 for S being non void non empty ManySortedSign, X being ManySortedSet of the carrier of S for o being OperSymbol of S, b being FinSequence st [[o,the carrier of S],b] in REL(X) holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union(coprod X) implies b.x in coprod(( the_arity_of o).x,X)); registration let I be non empty set, M be ManySortedSet of I; cluster rng M -> non empty; end; registration let I be set; cluster empty-yielding -> disjoint_valued for ManySortedSet of I; end; registration let I be set; cluster disjoint_valued for ManySortedSet of I; end; definition let I be non empty set; let X be disjoint_valued ManySortedSet of I; let D be non-empty ManySortedSet of I; let F be ManySortedFunction of X,D; func Flatten F -> Function of Union X, Union D means :: MSAFREE1:def 1 for i being Element of I, x being set st x in X.i holds it.x = F.i.x; end; theorem :: MSAFREE1:4 for I being non empty set, X being disjoint_valued ManySortedSet of I, D being non-empty ManySortedSet of I for F1,F2 be ManySortedFunction of X ,D st Flatten F1 = Flatten F2 holds F1 = F2; definition let S be non empty ManySortedSign; let A be MSAlgebra over S; attr A is disjoint_valued means :: MSAFREE1:def 2 the Sorts of A is disjoint_valued; end; definition let S be non empty ManySortedSign; func SingleAlg S -> strict MSAlgebra over S means :: MSAFREE1:def 3 for i being set st i in the carrier of S holds (the Sorts of it).i = {i}; end; registration let S be non empty ManySortedSign; cluster non-empty disjoint_valued for MSAlgebra over S; end; registration let S be non empty ManySortedSign; cluster SingleAlg S -> non-empty disjoint_valued; end; registration let S be non empty ManySortedSign; let A be disjoint_valued MSAlgebra over S; cluster the Sorts of A -> disjoint_valued; end; theorem :: MSAFREE1:5 for S being non void non empty ManySortedSign, o being OperSymbol of S, A1 be non-empty disjoint_valued MSAlgebra over S, A2 be non-empty MSAlgebra over S, f be ManySortedFunction of A1,A2, a be Element of Args(o,A1) holds (Flatten f)*a = f#a; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeSort X -> disjoint_valued; end; scheme :: MSAFREE1:sch 2 FreeSortUniq{ S() -> non void non empty ManySortedSign, X,D() -> non-empty ManySortedSet of the carrier of S(), G(set) -> Element of Union D(), H(object, object, object) -> Element of Union D(), f1, f2() -> ManySortedFunction of FreeSort X(),D() }: f1() = f2() provided for o being OperSymbol of S(), ts being Element of Args(o,FreeMSA X()) for x being Element of (Union D())* st x = (Flatten f1()) * ts holds f1().(the_result_sort_of o).(Den(o,FreeMSA X()).ts) = H(o, ts, x) and for s being SortSymbol of S(), y be set st y in FreeGen(s,X()) holds f1().s.y = G(y) and for o being OperSymbol of S(), ts being Element of Args(o,FreeMSA X()) for x being Element of (Union D())* st x = (Flatten f2()) * ts holds f2().(the_result_sort_of o).(Den(o,FreeMSA X()).ts) = H(o, ts, x) and for s being SortSymbol of S(), y be set st y in FreeGen(s,X()) holds f2().s.y = G(y); registration let S be non void non empty ManySortedSign; let X be non-empty ManySortedSet of the carrier of S; cluster FreeMSA X -> non-empty; end; registration let S be non void non empty ManySortedSign; let o be OperSymbol of S; let A be non-empty MSAlgebra over S; cluster Args(o,A) -> non empty; cluster Result(o,A) -> non empty; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster the Sorts of FreeMSA X -> disjoint_valued; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeMSA X -> disjoint_valued; end; scheme :: MSAFREE1:sch 3 ExtFreeGen{ S() -> non void non empty ManySortedSign, X() -> non-empty ManySortedSet of the carrier of S(), MSA() -> non-empty MSAlgebra over S(), P[object,object,object], IT1, IT2() -> ManySortedFunction of FreeMSA X(), MSA() }: IT1() = IT2() provided IT1() is_homomorphism FreeMSA X(), MSA() and for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X()) holds IT1().s.y = x iff P[s,x,y] and IT2() is_homomorphism FreeMSA X(), MSA() and for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X()) holds IT2().s.y = x iff P[s,x,y];