### The Mizar article:

### Many Sorted Algebras

**by****Andrzej Trybulec**

- Received April 21, 1994
Copyright (c) 1994 Association of Mizar Users

- MML identifier: MSUALG_1
- [ MML identifier index ]

environ vocabulary ZF_REFLE, PBOOLE, BOOLE, RELAT_1, FUNCT_1, PRALG_1, TDGROUP, CARD_3, FINSEQ_2, FINSEQ_1, FUNCOP_1, FUNCT_2, AMI_1, QC_LANG1, UNIALG_1, PARTFUN1, REALSET1, MSUALG_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, FUNCOP_1, PARTFUN1, FINSEQ_2, CARD_3, PBOOLE, REALSET1, PRALG_1, UNIALG_1; constructors REALSET1, PRALG_1, MEMBERED, XBOOLE_0; clusters FUNCT_1, PBOOLE, UNIALG_1, TEX_2, PRALG_1, RELSET_1, STRUCT_0, FINSEQ_2, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements BOOLE, SUBSET; definitions TARSKI, PRALG_1, FINSEQ_1, UNIALG_1, PBOOLE, STRUCT_0, XBOOLE_0; theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, UNIALG_1, PBOOLE, FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, REALSET1, RELAT_1, RELSET_1, STRUCT_0; schemes ZFREFLE1, FUNCT_1, FRAENKEL, FUNCT_2; begin :: Preliminaries reserve i,j for set, I for set; theorem Th1: not ex M being non-empty ManySortedSet of I st {} in rng M proof let M be non-empty ManySortedSet of I; assume A1: {} in rng M; dom M = I by PBOOLE:def 3; then ex i st i in I & M.i = {} by A1,FUNCT_1:def 5; hence contradiction by PBOOLE:def 16; end; scheme MSSEx { I() -> set, P[set,set] }: ex f being ManySortedSet of I() st for i st i in I() holds P[i,f.i] provided A1: for i st i in I() ex j st P[i,j] proof defpred Q[set,set] means P[$1,$2]; A2: for i st i in I() ex j st Q[i,j] by A1; consider f being Function such that A3: dom f = I() and A4: for i st i in I() holds Q[i,f.i] from NonUniqFuncEx(A2); reconsider f as ManySortedSet of I() by A3,PBOOLE:def 3; take f; thus thesis by A4; end; scheme MSSLambda { I() -> set, F(set) -> set }: ex f being ManySortedSet of I() st for i st i in I() holds f.i = F(i) proof deffunc G(set)=F($1); consider f being Function such that A1: dom f = I() and A2: for i st i in I() holds f.i = G(i) from Lambda; reconsider f as ManySortedSet of I() by A1,PBOOLE:def 3; take f; thus thesis by A2; end; definition let I be set; let M be ManySortedSet of I; mode Component of M is Element of rng M; end; theorem Th2: for I being non empty set for M being ManySortedSet of I, A being Component of M ex i st i in I & A = M.i proof let I be non empty set; let M be ManySortedSet of I, A be Component of M; A1: dom M = I by PBOOLE:def 3; then rng M <> {} by RELAT_1:65; hence ex i st i in I & A = M.i by A1,FUNCT_1:def 5; end; theorem Th3: for M being ManySortedSet of I, i st i in I holds M.i is Component of M proof let M be ManySortedSet of I, i; A1: dom M = I by PBOOLE:def 3; assume i in I; hence thesis by A1,FUNCT_1:def 5; end; definition let I; let B be ManySortedSet of I; mode Element of B -> ManySortedSet of I means for i st i in I holds it.i is Element of B.i; existence proof defpred Q[set,set] means $2 is Element of B.$1; A1: for i st i in I ex j st Q[i,j] proof let i such that i in I; consider j being Element of B.i; reconsider j as set; take j; thus j is Element of B.i; end; thus ex f being ManySortedSet of I st for i st i in I holds Q[i,f.i] from MSSEx(A1); end; end; begin :: Many Sorted Functions definition let I; let A be ManySortedSet of I, B be ManySortedSet of I; mode ManySortedFunction of A,B -> ManySortedSet of I means :Def2: for i st i in I holds it.i is Function of A.i, B.i; correctness proof defpred P[set,set] means $2 is Function of A.$1,B.$1; A1: for i st i in I ex j st P[i,j] proof let i such that i in I; consider j being Function of A.i,B.i; reconsider j as set; take j; thus j is Function of A.i,B.i; end; consider f being ManySortedSet of I such that A2: for i st i in I holds P[i,f.i] from MSSEx(A1); f is Function-yielding proof let i; assume i in dom f; then i in I by PBOOLE:def 3; hence f.i is Function by A2; end; then reconsider f as ManySortedFunction of I; take f; let i; assume i in I; hence f.i is Function of A.i,B.i by A2; end; end; definition let I; let A be ManySortedSet of I, B be ManySortedSet of I; cluster ->Function-yielding ManySortedFunction of A,B; coherence proof let f be ManySortedFunction of A,B; let i; assume i in dom f; then i in I by PBOOLE:def 3; hence f.i is Function by Def2; end; end; definition let I be set; let M be ManySortedSet of I; func M# -> ManySortedSet of I* means :Def3: for i being Element of I* holds it.i = product(M*i); existence proof defpred P[set,set] means ex j being Element of I* st j = $1 & $2 = product(M*j); A1: for i st i in I* ex j st P[i,j] proof let i; assume i in I*; then reconsider j = i as Element of I*; reconsider e = product(M*j) as set; take e,j; thus j = i & e = product(M*j); end; consider f being ManySortedSet of I* such that A2: for i st i in I* holds P[i,f.i] from MSSEx(A1); take f; let i be Element of I*; ex j being Element of I* st j = i & f.i = product(M*j) by A2; hence thesis; end; uniqueness proof let N1,N2 be ManySortedSet of I* such that A3: for i being Element of I* holds N1.i = product(M*i) and A4: for i being Element of I* holds N2.i = product(M*i); now let i; assume i in I*; then reconsider e = i as Element of I*; thus N1.i = product(M*e) by A3 .= N2.i by A4; end; hence thesis by PBOOLE:3; end; end; definition let I be set; let M be non-empty ManySortedSet of I; cluster M# -> non-empty; coherence proof M# is non-empty proof let i; assume i in I*; then reconsider f = i as Element of I*; not {} in rng M by Th1; then not {} in rng(M*f) by FUNCT_1:25; then product(M*f) <> {} by CARD_3:37; hence M#.i is non empty by Def3; end; hence thesis; end; end; definition let I; let J be non empty set; let O be Function of I,J; let F be ManySortedSet of J; redefine func F*O -> ManySortedSet of I; coherence proof rng O c= J & dom O = I & dom F = J by FUNCT_2:def 1,PBOOLE:def 3,RELSET_1:12; hence dom(F*O) = I by RELAT_1:46; end; end; definition let I; let J be non empty set; let O be Function of I,J; let F be non-empty ManySortedSet of J; redefine func F*O -> non-empty ManySortedSet of I; coherence proof F*O is non-empty proof let i; assume A1: i in I; then O.i in J by FUNCT_2:7; then A2: F.(O.i) is non empty by PBOOLE:def 16; dom O = I by FUNCT_2:def 1; hence (F*O).i is non empty by A1,A2,FUNCT_1:23; end; hence thesis; end; end; definition let a be set; func *-->a -> Function of NAT,{a}* means :Def4: for n being Nat holds it.n = n |-> a; existence proof defpred P[Element of NAT,Element of {a}*] means $2 = $1 |-> a; A1: for x being Element of NAT ex y being Element of {a}* st P[x,y] proof let n be Nat; a is Element of {a} by TARSKI:def 1; then n |-> a is FinSequence of {a} by FINSEQ_2:77; then reconsider u = n |-> a as Element of {a}* by FINSEQ_1:def 11; take u; thus u = n |-> a; end; ex f being Function of NAT,{a}* st for x being Element of NAT holds P[x,f.x] from FuncExD(A1); hence thesis; end; uniqueness proof let f1,f2 be Function of NAT,{a}* such that A2: for n being Nat holds f1.n = n |-> a and A3: for n being Nat holds f2.n = n |-> a; now let k be Nat; thus f1.k = k |-> a by A2 .= f2.k by A3; end; hence f1 = f2 by FUNCT_2:113; end; end; reserve D for non empty set, n for Nat; theorem Th4: for a,b being set holds ({a} --> b)*(n|->a) = n |-> b proof let a,b be set; A1: now let x be set; hereby assume x in dom (n |-> b); then A2: x in Seg n by FINSEQ_2:68; hence x in dom(n|->a) by FINSEQ_2:68; A3: dom({a} --> b) = {a} by FUNCOP_1:19; (n|->a).x = a by A2,FINSEQ_2:70; hence (n|->a).x in dom({a} --> b) by A3,TARSKI:def 1; end; assume that A4: x in dom(n|->a) and (n|->a).x in dom({a} --> b); x in Seg n by A4,FINSEQ_2:68; hence x in dom (n |-> b) by FINSEQ_2:68; end; now let x be set; assume x in dom (n |-> b); then A5: x in Seg n by FINSEQ_2:68; A6: a in {a} by TARSKI:def 1; thus (n |-> b).x = b by A5,FINSEQ_2:70 .= ({a} --> b).a by A6,FUNCOP_1:13 .= ({a} --> b).((n|->a).x) by A5,FINSEQ_2:70; end; hence ({a} --> b)*(n|->a) = n |-> b by A1,FUNCT_1:20; end; theorem Th5: for a being set for M being ManySortedSet of {a} st M = {a} --> D holds (M#**-->a).n = Funcs(Seg n, D) proof let a be set; let M be ManySortedSet of {a} such that A1: M = {a} --> D; A2: dom(*-->a) = NAT by FUNCT_2:def 1; a is Element of {a} by TARSKI:def 1; then n |-> a is FinSequence of {a} by FINSEQ_2:77; then A3: n |-> a in {a}* by FINSEQ_1:def 11; thus (M#**-->a).n = M#.((*-->a).n) by A2,FUNCT_1:23 .= M#.(n|->a) by Def4 .= product(({a} --> D)*(n|->a)) by A1,A3,Def3 .= product(n |-> D) by Th4 .= product(Seg(n) --> D) by FINSEQ_2:def 2 .= Funcs(Seg n, D) by CARD_3:20; end; definition let I,i; redefine func I --> i -> Function of I,{i}; coherence proof dom (I --> i) = I & rng (I --> i) c= {i} by FUNCOP_1:19; hence I --> i is Function of I,{i} by FUNCT_2:def 1,RELSET_1:11; end; end; begin :: Many Sorted Signatures definition struct(1-sorted) ManySortedSign (# carrier -> set, OperSymbols -> set, Arity -> Function of the OperSymbols, the carrier*, ResultSort -> Function of the OperSymbols, the carrier #); end; definition let IT be ManySortedSign; attr IT is void means :Def5: the OperSymbols of IT = {}; end; definition cluster void strict non empty ManySortedSign; existence proof {} in {{}}* by FINSEQ_1:66; then reconsider f = {}-->{} as Function of {},{{}}* by FUNCOP_1:58; reconsider g = {}-->{} as Function of {},{{}}; take ManySortedSign(#{{}},{},f,g#); thus thesis by Def5,STRUCT_0:def 1; end; cluster non void strict non empty ManySortedSign; existence proof {} in {{}}* by FINSEQ_1:66; then reconsider f = {{}}-->{} as Function of {{}},{{}}* by FUNCOP_1:58; reconsider g = {{}}-->{} as Function of {{}},{{}}; take ManySortedSign(#{{}},{{}},f,g#); thus thesis by Def5,STRUCT_0:def 1; end; end; reserve S for non empty ManySortedSign; definition let S; mode SortSymbol of S is Element of S; mode OperSymbol of S is Element of the OperSymbols of S; end; definition let S be non void non empty ManySortedSign; let o be OperSymbol of S; func the_arity_of o -> Element of (the carrier of S)* equals :Def6: (the Arity of S).o; coherence proof the OperSymbols of S <> {} by Def5; then o in the OperSymbols of S; then o in dom(the Arity of S) by FUNCT_2:def 1; then A1: (the Arity of S).o in rng(the Arity of S) by FUNCT_1:def 5; rng(the Arity of S) c= (the carrier of S)* by RELSET_1:12; hence thesis by A1; end; correctness; func the_result_sort_of o -> Element of S equals (the ResultSort of S).o; coherence proof the OperSymbols of S <> {} by Def5; then o in the OperSymbols of S; then o in dom(the ResultSort of S) by FUNCT_2:def 1; then A2: (the ResultSort of S).o in rng(the ResultSort of S) by FUNCT_1: def 5; rng(the ResultSort of S) c= the carrier of S by RELSET_1:12; hence thesis by A2; end; end; begin :: Many Sorted Algebras definition let S be 1-sorted; struct many-sorted over S (# Sorts -> ManySortedSet of the carrier of S #); end; definition let S; struct(many-sorted over S) MSAlgebra over S (# Sorts -> ManySortedSet of the carrier of S, Charact -> ManySortedFunction of (the Sorts)# * the Arity of S, the Sorts * the ResultSort of S#); end; definition let S be 1-sorted; let A be many-sorted over S; attr A is non-empty means :Def8: the Sorts of A is non-empty; end; definition let S; cluster strict non-empty MSAlgebra over S; existence proof dom((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19; then reconsider s = (the carrier of S) --> {0} as ManySortedSet of the carrier of S by PBOOLE:def 3; consider o being ManySortedFunction of s# * the Arity of S, s * the ResultSort of S; take MSAlgebra(#s,o#); thus MSAlgebra(#s,o#) is strict; let i be set; assume i in the carrier of S; hence thesis by FUNCOP_1:13; end; end; definition let S be 1-sorted; cluster strict non-empty many-sorted over S; existence proof dom ((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19; then reconsider s = (the carrier of S) --> {0} as ManySortedSet of the carrier of S by PBOOLE:def 3; take many-sorted(#s#); thus many-sorted (#s#) is strict; let i be set; assume i in the carrier of S; hence thesis by FUNCOP_1:13; end; end; definition let S be 1-sorted; let A be non-empty many-sorted over S; cluster the Sorts of A -> non-empty; coherence by Def8; end; definition let S; let A be non-empty MSAlgebra over S; cluster -> non empty Component of the Sorts of A; coherence proof let C be Component of the Sorts of A; ex i st i in the carrier of S & C = (the Sorts of A).i by Th2; hence thesis by PBOOLE:def 16; end; cluster -> non empty Component of (the Sorts of A)#; coherence proof let C be Component of (the Sorts of A)#; ex i st i in (the carrier of S)* & C = (the Sorts of A)#.i by Th2; hence thesis by PBOOLE:def 16; end; end; definition let S be non void non empty ManySortedSign; let o be OperSymbol of S; let A be MSAlgebra over S; func Args(o,A) -> Component of (the Sorts of A)# equals :Def9: ((the Sorts of A)# * the Arity of S).o; coherence proof the OperSymbols of S <> {} by Def5; then o in the OperSymbols of S; then o in dom((the Sorts of A)# * the Arity of S) by PBOOLE:def 3; then ((the Sorts of A)# * the Arity of S).o in rng((the Sorts of A)# * the Arity of S) by FUNCT_1:def 5; hence thesis by FUNCT_1:25; end; correctness; func Result(o,A) -> Component of the Sorts of A equals :Def10: ((the Sorts of A) * the ResultSort of S).o; coherence proof the OperSymbols of S <> {} by Def5; then o in the OperSymbols of S; then o in dom((the Sorts of A) * the ResultSort of S) by PBOOLE:def 3; then ((the Sorts of A) * the ResultSort of S).o in rng((the Sorts of A) * the ResultSort of S) by FUNCT_1:def 5; hence thesis by FUNCT_1:25; end; correctness; end; definition let S be non void non empty ManySortedSign; let o be OperSymbol of S; let A be MSAlgebra over S; func Den(o,A) -> Function of Args(o,A), Result(o,A) equals :Def11: (the Charact of A).o; coherence proof A1: the OperSymbols of S <> {} by Def5; Result(o,A) = ((the Sorts of A) * the ResultSort of S).o & Args(o,A) = ((the Sorts of A)# * the Arity of S).o by Def9,Def10; hence thesis by A1,Def2; end; end; theorem Th6: for S being non void non empty ManySortedSign, o being OperSymbol of S, A being non-empty MSAlgebra over S holds Den(o,A) is non empty proof let S be non void non empty ManySortedSign, o be OperSymbol of S, A be non-empty MSAlgebra over S; thus Den(o,A) is non empty by FUNCT_2:def 1,RELAT_1:60; end; begin :: On the one-sorted algebras Lm1: for h being homogeneous quasi_total non empty PartFunc of D*,D holds dom h = (arity h)-tuples_on D proof let h be homogeneous quasi_total non empty PartFunc of D*,D; A1: dom h c= D* by RELSET_1:12; thus dom h c= (arity h)-tuples_on D proof let x be set; assume A2: x in dom h; then reconsider f = x as FinSequence of D by A1,FINSEQ_1:def 11; A3: len f = arity h by A2,UNIALG_1:def 10; f is Element of (len f)-tuples_on D by FINSEQ_2:110; hence x in (arity h)-tuples_on D by A3; end; let x be set; assume x in (arity h)-tuples_on D; then reconsider f = x as Element of (arity h)-tuples_on D; consider x0 being Element of dom h; A4: dom h <> {} by RELAT_1:64; then x0 in dom h; then reconsider x0 as FinSequence of D by A1,FINSEQ_1:def 11; len x0 = arity h by A4,UNIALG_1:def 10 .= len f by FINSEQ_2:109; hence x in dom h by A4,UNIALG_1:def 2; end; theorem Th7: for C being set, A,B being non empty set, F being PartFunc of C,A, G being Function of A,B holds G*F is Function of dom F,B proof let C be set; let A,B be non empty set; let F be PartFunc of C,A; let G be Function of A,B; now dom G = A by FUNCT_2:def 1; then rng F c= dom G by RELSET_1:12; hence dom(G*F) = dom F by RELAT_1:46; thus rng(G*F) c= B by RELSET_1:12; end; hence G*F is Function of dom F,B by FUNCT_2:def 1,RELSET_1:11; end; theorem Th8: for h being homogeneous quasi_total non empty PartFunc of D*,D holds dom h = Funcs(Seg(arity h),D) proof let h be homogeneous quasi_total non empty PartFunc of D*,D; thus dom h = (arity h)-tuples_on D by Lm1 .= Funcs(Seg(arity h),D) by FINSEQ_2:111; end; theorem Th9: for A being Universal_Algebra holds signature A is non empty proof let A be Universal_Algebra; len(the charact of A) <> 0 by FINSEQ_1:25; then len(signature A) <> 0 by UNIALG_1:def 11; hence signature A is non empty by FINSEQ_1:25; end; begin :: Relationship to one sorted algebras definition let A be Universal_Algebra; redefine func signature A -> FinSequence of NAT; coherence; end; definition let IT be ManySortedSign; attr IT is segmental means :Def12: ex n st the OperSymbols of IT = Seg n; end; theorem Th10: for S being non empty ManySortedSign st S is trivial for A being MSAlgebra over S, c1,c2 being Component of the Sorts of A holds c1 = c2 proof let S be non empty ManySortedSign such that A1: S is trivial; let A be MSAlgebra over S, c1,c2 be Component of the Sorts of A; consider i1 being set such that A2: i1 in the carrier of S and A3: c1 = (the Sorts of A).i1 by Th2; consider i2 being set such that A4: i2 in the carrier of S and A5: c2 = (the Sorts of A).i2 by Th2; thus c1 = c2 by A1,A2,A3,A4,A5,REALSET1:def 20; end; Lm2: for A being Universal_Algebra for f being Function of dom signature A, {0}* st f = (*-->0)*(signature A) holds ManySortedSign (#{0},dom signature(A),f,dom signature(A)-->0#) is non empty segmental trivial non void strict proof let A be Universal_Algebra; let f be Function of dom signature A, {0}* such that f = (*-->0)*(signature A); set S = ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#); thus the carrier of S is non empty; signature A <> {} by Th9; then A1: the OperSymbols of S <> {} by RELAT_1:64; S is segmental proof take len signature(A); thus the OperSymbols of S = Seg len signature(A) by FINSEQ_1:def 3; end; hence thesis by A1,Def5,REALSET1:def 13; end; definition cluster segmental trivial non void strict non empty ManySortedSign; existence proof consider A being Universal_Algebra; reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}* by Th7; ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#) is segmental trivial non void strict non empty by Lm2; hence thesis; end; end; definition let A be Universal_Algebra; func MSSign A -> non void strict segmental trivial ManySortedSign means :Def13: the carrier of it = {0} & the OperSymbols of it = dom signature A & the Arity of it = (*-->0)*signature A & the ResultSort of it = dom signature(A)-->0; correctness proof reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}* by Th7; ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#) is segmental trivial non void strict by Lm2; hence thesis; end; end; definition let A be Universal_Algebra; cluster MSSign A -> non empty; coherence proof thus the carrier of MSSign A is non empty by Def13; end; end; definition let A be Universal_Algebra; func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals :Def14: {0}-->the carrier of A; coherence proof A1: the carrier of MSSign A = {0} & the OperSymbols of MSSign A = dom signature A & the Arity of MSSign A = (*-->0)*signature A & the ResultSort of MSSign A = dom signature(A)-->0 by Def13; set M = {0}-->the carrier of A; dom M = the carrier of MSSign A by A1,FUNCOP_1:19; then reconsider M as ManySortedSet of the carrier of MSSign A by PBOOLE:def 3; M is non-empty proof let i; assume i in the carrier of MSSign A; hence thesis by A1,FUNCOP_1:13; end; hence thesis; end; correctness; end; definition let A be Universal_Algebra; func MSCharact A -> ManySortedFunction of (MSSorts A)# * the Arity of MSSign A, (MSSorts A)* the ResultSort of MSSign A equals :Def15: the charact of A; coherence proof reconsider OS = the OperSymbols of MSSign A as non empty set by Def5; A1: the carrier of MSSign A = {0} & the OperSymbols of MSSign A = dom signature A & the Arity of MSSign A = (*-->0)*signature A & the ResultSort of MSSign A = dom signature(A)-->0 by Def13; len signature A = len the charact of A by UNIALG_1:def 11; then A2: dom the charact of A = OS by A1,FINSEQ_3:31; then reconsider O = the charact of A as ManySortedSet of OS by PBOOLE:def 3; O is Function-yielding proof let i; assume A3: i in dom O; dom O = dom the charact of A; then reconsider n = i as Nat by A3; O.n is Function by A3,UNIALG_1:5; hence O.i is Function; end; then reconsider O as ManySortedFunction of OS; reconsider DO = (MSSorts A)# * the Arity of MSSign A, RO = (MSSorts A)* the ResultSort of MSSign A as ManySortedSet of OS; O is ManySortedFunction of DO,RO proof let i; assume A4: i in OS; then reconsider o = i as Element of OS; reconsider n = i as Nat by A1,A4; set D = the carrier of A; reconsider h = O.n as homogeneous quasi_total non empty PartFunc of D*,D by A2,A4,UNIALG_1:5,def 4,def 5,def 6; dom({0}-->D) = {0} by FUNCOP_1:19; then reconsider M = {0}-->D as ManySortedSet of {0} by PBOOLE:def 3; A5: n in dom(dom signature(A)-->0) by A1,A4,FUNCOP_1:19; A6: 0 in {0} by TARSKI:def 1; A7: DO.i = ((MSSorts A)#*(*-->0)*signature A).n by A1,RELAT_1:55 .= ((MSSorts A)#*(*-->0)).((signature A).n) by A1,A4,FUNCT_1:23 .= (M#*(*-->0)).((signature A).n) by A1,Def14 .= (M#*(*-->0)).arity h by A1,A4,UNIALG_1:def 11 .= Funcs(Seg arity h,D) by Th5 .= dom(O.o) by Th8; A8: RO.i = (MSSorts A).((dom signature(A)-->0).n) by A1,A5,FUNCT_1:23 .= (MSSorts A).0 by A1,A4,FUNCOP_1:13 .= ({0}-->the carrier of A).0 by Def14 .= the carrier of A by A6,FUNCOP_1:13; then rng h c= RO.i by RELSET_1:12; hence O.i is Function of DO.i,RO.i by A7,A8,FUNCT_2:def 1,RELSET_1:11; end; hence thesis; end; correctness; end; definition let A be Universal_Algebra; func MSAlg A -> strict MSAlgebra over MSSign A equals :Def16: MSAlgebra(#MSSorts A,MSCharact A#); correctness; end; definition let A be Universal_Algebra; cluster MSAlg A -> non-empty; coherence proof MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16; hence the Sorts of MSAlg A is non-empty; end; end; :: Manysorted Algebras with 1 Sort Only definition let MS be trivial non empty ManySortedSign; let A be MSAlgebra over MS; func the_sort_of A -> set means :Def17: ex c being Component of the Sorts of A st it = c; existence proof consider c being Component of the Sorts of A; take c; thus thesis; end; uniqueness by Th10; end; definition let MS be trivial non empty ManySortedSign; let A be non-empty MSAlgebra over MS; cluster the_sort_of A -> non empty; coherence proof ex c being Component of the Sorts of A st the_sort_of A = c by Def17; hence thesis; end; end; theorem Th11: for MS being segmental trivial non void non empty ManySortedSign, i being OperSymbol of MS, A being non-empty MSAlgebra over MS holds Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A proof let MS be segmental trivial non void non empty ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS; set m = len the_arity_of i; A1: the OperSymbols of MS <> {} by Def5; A2: dom(the Arity of MS) = the OperSymbols of MS by FUNCT_2:def 1; A3: Args(i,A) = ((the Sorts of A)# * the Arity of MS).i by Def9 .= (the Sorts of A)# .((the Arity of MS).i) by A1,A2,FUNCT_1:23 .= (the Sorts of A)# .the_arity_of i by Def6 .= product((the Sorts of A)*the_arity_of i) by Def3; consider n being Nat such that A4: dom the_arity_of i = Seg n by FINSEQ_1:def 2; A5: rng the_arity_of i c= the carrier of MS by FINSEQ_1:def 4; then rng the_arity_of i c= dom the Sorts of A by PBOOLE:def 3; then A6: dom((the Sorts of A)*the_arity_of i) = dom the_arity_of i by RELAT_1 :46; thus Args(i,A) c= m-tuples_on the_sort_of A proof let x be set; assume x in Args(i,A); then consider g being Function such that A7: x = g and A8: dom g = dom((the Sorts of A)*the_arity_of i) and A9: for j being set st j in dom((the Sorts of A)*the_arity_of i) holds g.j in ((the Sorts of A)*the_arity_of i).j by A3,CARD_3:def 5; reconsider p = g as FinSequence by A4,A6,A8,FINSEQ_1:def 2; rng p c= the_sort_of A proof let j be set; assume j in rng p; then consider u being set such that A10: u in dom g and A11: p.u = j by FUNCT_1:def 5; g.u in ((the Sorts of A)*the_arity_of i).u by A8,A9,A10; then A12: g.u in (the Sorts of A).((the_arity_of i).u) by A6,A8,A10, FUNCT_1:23; (the_arity_of i).u in rng the_arity_of i by A6,A8,A10,FUNCT_1:def 5; then (the Sorts of A).((the_arity_of i).u) is Component of the Sorts of A by A5,Th3; hence j in the_sort_of A by A11,A12,Def17; end; then A13: p is FinSequence of the_sort_of A by FINSEQ_1:def 4; len p = m by A6,A8,FINSEQ_3:31; then x is Element of m-tuples_on the_sort_of A by A7,A13,FINSEQ_2:110; hence x in m-tuples_on the_sort_of A; end; let x be set; assume x in m-tuples_on the_sort_of A; then x in Funcs(Seg m, the_sort_of A) by FINSEQ_2:111; then consider g being Function such that A14: x = g and A15: dom g = Seg m and A16: rng g c= the_sort_of A by FUNCT_2:def 2; A17: dom g = dom((the Sorts of A)*the_arity_of i) by A6,A15,FINSEQ_1:def 3; now let x be set; assume A18: x in dom((the Sorts of A)*the_arity_of i); then g.x in rng g by A17,FUNCT_1:def 5; then A19: g.x in the_sort_of A by A16; (the_arity_of i).x in rng the_arity_of i by A6,A18,FUNCT_1:def 5; then (the Sorts of A).((the_arity_of i).x) is Component of the Sorts of A by A5,Th3; then g.x in (the Sorts of A).((the_arity_of i).x) by A19,Def17; hence g.x in ((the Sorts of A)*the_arity_of i).x by A6,A18,FUNCT_1:23; end; hence x in Args(i,A) by A3,A14,A17,CARD_3:18; end; theorem Th12: for A being non empty set, n holds n-tuples_on A c= A* proof let A be non empty set, n; defpred P[Element of A*] means len $1 = n; { s where s is Element of A*: P[s] } c= A* from Fr_Set0; hence n-tuples_on A c= A* by FINSEQ_2:def 4; end; theorem Th13: for MS being segmental trivial non void non empty ManySortedSign, i being OperSymbol of MS, A being non-empty MSAlgebra over MS holds Args(i,A) c= (the_sort_of A)* proof let MS be segmental trivial non void non empty ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS; Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A by Th11; hence Args(i,A) c= (the_sort_of A)* by Th12; end; theorem Th14: for MS being segmental trivial non void non empty ManySortedSign, A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A) proof let MS be segmental trivial non void non empty ManySortedSign, A be non-empty MSAlgebra over MS; A1: dom the Charact of A = the OperSymbols of MS by PBOOLE:def 3; ex n st the OperSymbols of MS = Seg n by Def12; then reconsider f = the Charact of A as FinSequence by A1,FINSEQ_1:def 2; f is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A) proof let x be set; assume x in rng f; then consider i such that A2: i in the OperSymbols of MS and A3: f.i = x by A1,FUNCT_1:def 5; reconsider i as OperSymbol of MS by A2; A4: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1; A5: ((the Sorts of A)# * the Arity of MS).i = Args(i,A) by Def9; (the ResultSort of MS).i in the carrier of MS by A2,FUNCT_2:7; then A6: (the Sorts of A).((the ResultSort of MS).i) is Component of the Sorts of A by Th3; A7: Args(i,A) c= (the_sort_of A)* by Th13; ((the Sorts of A)*the ResultSort of MS).i = (the Sorts of A).((the ResultSort of MS).i) by A2,A4,FUNCT_1:23 .= the_sort_of A by A6,Def17; then x is Function of Args(i,A),the_sort_of A by A2,A3,A5,Def2; then x is PartFunc of (the_sort_of A)*,the_sort_of A by A7,PARTFUN1:30; hence x in PFuncs((the_sort_of A)*,the_sort_of A) by PARTFUN1:119; end; hence thesis; end; definition let MS be segmental trivial non void non empty ManySortedSign; let A be non-empty MSAlgebra over MS; func the_charact_of A -> PFuncFinSequence of the_sort_of A equals :Def18: the Charact of A; coherence by Th14; end; reserve MS for segmental trivial non void non empty ManySortedSign, A for non-empty MSAlgebra over MS, h for PartFunc of (the_sort_of A)*,(the_sort_of A), x,y for FinSequence of the_sort_of A; definition let MS,A; func 1-Alg A -> non-empty strict Universal_Algebra equals :Def19: UAStr(#the_sort_of A, the_charact_of A#); coherence proof A1: the_charact_of A is quasi_total proof let n,h such that A2: n in dom(the_charact_of A) and A3: h = (the_charact_of A).n; let x,y such that A4: len x = len y and A5: x in dom h; A6: dom(the_charact_of A) = dom the Charact of A by Def18 .= the OperSymbols of MS by PBOOLE:def 3; then reconsider o = n as OperSymbol of MS by A2; A7: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1; A8: ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9; (the ResultSort of MS).o in the carrier of MS by A2,A6,FUNCT_2:7; then A9: (the Sorts of A).((the ResultSort of MS).o) is Component of the Sorts of A by Th3; A10: ((the Sorts of A)*the ResultSort of MS).o = (the Sorts of A).((the ResultSort of MS).o) by A2,A6,A7,FUNCT_1:23 .= the_sort_of A by A9,Def17; h = (the Charact of A).o by A3,Def18; then h is Function of ((the Sorts of A)# * the Arity of MS).o, ((the Sorts of A) * the ResultSort of MS).o by A2,A6,Def2; then A11: dom h = ((the Sorts of A)# * the Arity of MS).o by A10, FUNCT_2:def 1 .= (len the_arity_of o)-tuples_on the_sort_of A by A8,Th11; then len y = len the_arity_of o by A4,A5,FINSEQ_2:109; then y is Element of dom h by A11,FINSEQ_2:110; hence y in dom h by A5; end; A12: the_charact_of A is homogeneous proof let n,h such that A13: n in dom(the_charact_of A) and A14: h = (the_charact_of A).n; let x,y such that A15: x in dom h & y in dom h; A16: dom(the_charact_of A) = dom the Charact of A by Def18 .= the OperSymbols of MS by PBOOLE:def 3; then reconsider o = n as OperSymbol of MS by A13; A17: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1; A18: ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9; (the ResultSort of MS).o in the carrier of MS by A13,A16,FUNCT_2:7; then A19: (the Sorts of A).((the ResultSort of MS).o) is Component of the Sorts of A by Th3; A20: ((the Sorts of A)*the ResultSort of MS).o = (the Sorts of A).((the ResultSort of MS).o) by A13,A16,A17,FUNCT_1: 23 .= the_sort_of A by A19,Def17; h = (the Charact of A).o by A14,Def18; then h is Function of ((the Sorts of A)# * the Arity of MS).o, ((the Sorts of A) * the ResultSort of MS).o by A13,A16,Def2; then A21: dom h = ((the Sorts of A)# * the Arity of MS).o by A20, FUNCT_2:def 1 .= (len the_arity_of o)-tuples_on the_sort_of A by A18,Th11; hence len x = len the_arity_of o by A15,FINSEQ_2:109 .= len y by A15,A21,FINSEQ_2:109; end; the OperSymbols of MS <> {} by Def5; then the Charact of A <> {} by PBOOLE:def 3,RELAT_1:60; then A22: the_charact_of A <> {} by Def18; the_charact_of A is non-empty proof let n be set such that A23: n in dom the_charact_of A; set h = (the_charact_of A).n; dom(the_charact_of A) = dom the Charact of A by Def18 .= the OperSymbols of MS by PBOOLE:def 3; then reconsider o = n as OperSymbol of MS by A23; h = (the Charact of A).o by Def18 .= Den(o,A) by Def11; hence h is non empty by Th6; end; hence thesis by A1,A12,A22,UNIALG_1:def 7,def 8,def 9; end; correctness; end; theorem for A being strict Universal_Algebra holds A = 1-Alg MSAlg A proof let A be strict Universal_Algebra; A1: MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16; the carrier of A in {the carrier of A} by TARSKI:def 1; then the carrier of A in rng({0}-->the carrier of A) by FUNCOP_1:14; then the carrier of A in rng the Sorts of MSAlg A by A1,Def14; then A2: the carrier of A = the_sort_of MSAlg A by Def17; the charact of A = MSCharact A by Def15 .= the_charact_of MSAlg A by A1,Def18; hence A = 1-Alg MSAlg A by A2,Def19; end; theorem for A being Universal_Algebra for f being Function of dom signature A, {0}* st f = (*-->0)*signature A holds MSSign A = ManySortedSign(#{0},dom signature A,f,dom signature(A)-->0#) proof let A be Universal_Algebra; the carrier of MSSign A = {0} & the OperSymbols of MSSign A = dom signature A & the Arity of MSSign A = (*-->0)*signature A & the ResultSort of MSSign A = dom signature(A)-->0 by Def13; hence thesis; end;

Back to top