Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### A Scheme for Extensions of Homomorphisms of Many Sorted Algebras

**by****Andrzej Trybulec**- Received December 13, 1994
- MML identifier: MSAFREE1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, CARD_3, RELAT_1, PROB_1, LANG1, DTCONSTR, TREES_4, FINSEQ_1, TDGROUP, TREES_2, TREES_3, AMI_1, MSUALG_1, PBOOLE, FREEALG, BOOLE, MSAFREE, QC_LANG1, ZF_REFLE, TARSKI, MATRIX_1, PROB_2, PRALG_1, FINSEQ_4, MCART_1, ALG_1, MSAFREE1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, MCART_1, FINSEQ_1, MULTOP_1, PROB_2, CARD_3, FINSEQ_4, TREES_2, TREES_3, TREES_4, AMI_1, LANG1, DTCONSTR, PROB_1, PBOOLE, MSUALG_1, MSAFREE, MSUALG_3; constructors MULTOP_1, PROB_2, AMI_1, MSAFREE, MSUALG_3, FINSOP_1, FINSEQ_4, MEMBERED, XBOOLE_0; clusters PBOOLE, MSAFREE, PRALG_1, DTCONSTR, AMI_1, MSUALG_1, MSUALG_3, FUNCT_1, RELSET_1, STRUCT_0, TREES_3, FINSEQ_1, SUBSET_1, ARYTM_3, ZFMISC_1, XBOOLE_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 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 FinSequence of TS(DT()) st nt ==> roots ts for x being FinSequence 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 FinSequence of TS(DT()) st nt ==> roots ts for x being FinSequence 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 set st [o,b] in REL(X) holds o in [:the OperSymbols of S,{the carrier of S}:] & b in ([:the OperSymbols 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 OperSymbols 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)); definition let D be set; redefine mode FinSequence of D -> Element of D*; end; definition let I be non empty set, M be non-empty ManySortedSet of I; cluster rng M -> non empty with_non-empty_elements; end; definition let D be non empty with_non-empty_elements set; cluster union D -> non empty; end; definition let I be set; cluster empty-yielding -> disjoint_valued ManySortedSet of I; end; definition let I be set; cluster disjoint_valued 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; definition let S be non empty ManySortedSign; cluster non-empty disjoint_valued MSAlgebra over S; end; definition let S be non empty ManySortedSign; cluster SingleAlg S -> non-empty disjoint_valued; end; definition 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; definition 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 FreeSortUniq{ S() -> non void non empty ManySortedSign, X,D() -> non-empty ManySortedSet of the carrier of S(), G(set) -> Element of Union D(), H(set, set, set) -> 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 FinSequence 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 FinSequence 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); definition 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; definition 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; definition 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; definition 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 ExtFreeGen{ S() -> non void non empty ManySortedSign, X() -> non-empty ManySortedSet of the carrier of S(), MSA() -> non-empty MSAlgebra over S(), P[set,set,set], 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];

Back to top