:: Free Many Sorted Universal Algebra :: by Beata Perkowska :: :: Received April 27, 1994 :: Copyright (c) 1994-2012 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 XBOOLE_0, FUNCT_1, RELAT_1, PBOOLE, SUBSET_1, CARD_3, REALSET1, TARSKI, ZFMISC_1, PARTFUN1, STRUCT_0, MSUALG_1, MSUALG_2, PRELAMB, MSUALG_3, FINSEQ_1, MARGREL1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, NAT_1, TREES_2, MCART_1, UNIALG_2, QC_LANG1, GROUP_6, MSAFREE; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NAT_1, RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, MCART_1, FUNCT_2, FINSEQ_1, PBOOLE, TREES_2, FINSEQ_2, CARD_3, LANG1, TREES_4, DTCONSTR, MSUALG_1, MSUALG_2, MSUALG_3; constructors XXREAL_0, NAT_1, NAT_D, CARD_3, FINSEQOP, DTCONSTR, MSUALG_3, RELSET_1, PBOOLE, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, FUNCT_2, PARTFUN1, RELSET_1, PRE_POLY, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3, XTUPLE_0; theorems TARSKI, FUNCT_1, FUNCT_2, MCART_1, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1, MSUALG_2, MSUALG_3, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, TREES_1, DOMAIN_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, TREES_3, PARTFUN1, FINSEQ_3, FINSEQ_2, XTUPLE_0; schemes CLASSES1, FUNCT_1, RELSET_1, DTCONSTR, XBOOLE_0; begin :: :: Preliminaries :: theorem Th1: for I be set, J be non empty set, f be Function of I,J*, X be ManySortedSet of J, p be Element of J*, x be set st x in I & p = f.x holds (X# * f).x = product (X * p) proof let I be set, J be non empty set, f be Function of I,J*, X be ManySortedSet of J, p be Element of J*, x be set; assume A1: x in I & p = f.x; A2: dom f = I by FUNCT_2:def 1; then dom (X# * f) = dom f by PARTFUN1:def 2; hence (X# * f).x =(X# qua ManySortedSet of J*).p by A1,A2,FUNCT_1:12 .= product (X * p) by FINSEQ_2:def 5; end; definition let I be set, A,B be ManySortedSet of I, C be ManySortedSubset of A, F be ManySortedFunction of A,B; func F || C -> ManySortedFunction of C,B means :Def1: for i be set st i in I for f be Function of A.i,B.i st f = F.i holds it.i = f | (C.i); existence proof defpred P[set,set] means for f be Function of A.$1,B.$1 st f = F.$1 holds $2 = f | (C.$1); A1: for i be set st i in I ex u be set st P[i,u] proof let i be set; assume i in I; then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15; take f | (C.i); thus thesis; end; consider H be Function such that A2: dom H = I & for i be set st i in I holds P[i,H.i] from CLASSES1: sch 1 (A1); reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18; for i be set st i in I holds H.i is Function of C.i,B.i proof let i be set; assume A3: i in I; then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15; A4: H.i = f | (C.i) by A2,A3; C c= A by PBOOLE:def 18; then A5: C.i c= A.i by A3,PBOOLE:def 2; per cases; suppose A6: B.i is empty; then A7: H.i = {} by A4; now per cases; suppose C.i = {}; hence thesis by A7,RELSET_1:12; end; suppose C.i <> {}; thus thesis by A6,A7,FUNCT_2:def 1,RELSET_1:12; end; end; hence thesis; end; suppose A8: B.i is non empty; then A9: dom f = A.i by FUNCT_2:def 1; A10: rng (f|(C.i)) c= B.i by RELAT_1:def 19; dom (f|(C.i)) = dom f /\ (C.i) by RELAT_1:61 .= C.i by A5,A9,XBOOLE_1:28; hence thesis by A4,A8,A10,FUNCT_2:def 1,RELSET_1:4; end; end; then reconsider H as ManySortedFunction of C,B by PBOOLE:def 15; take H; thus thesis by A2; end; uniqueness proof let X,Y be ManySortedFunction of C,B; assume that A11: for i be set st i in I for f be Function of A.i,B.i st f = F.i holds X.i = f | (C.i) and A12: for i be set st i in I for f be Function of A.i,B.i st f = F.i holds Y.i = f | (C.i); for i be set st i in I holds X.i = Y.i proof let i be set; assume A13: i in I; then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15; X.i = f|(C.i) by A11,A13; hence thesis by A12,A13; end; hence thesis by PBOOLE:3; end; end; definition let I be set, X be ManySortedSet of I, i be set; assume A1: i in I; func coprod(i,X) -> set means :Def2: for x be set holds x in it iff ex a be set st a in X.i & x = [a,i]; existence proof defpred P[set] means ex a be set st a in X.i & $1 = [a,i]; consider A be set such that A2: for x be set holds x in A iff x in [:X.i,I:] & P[x] from XBOOLE_0: sch 1; take A; let x be set; thus x in A implies ex a be set st a in X.i & x = [a,i] by A2; given a be set such that A3: a in X.i & x = [a,i]; x in [:X.i,I:] by A1,A3,ZFMISC_1:87; hence thesis by A2,A3; end; uniqueness proof let A,B be set; assume that A4: for x be set holds x in A iff ex a be set st a in X.i & x = [a,i] and A5: for x be set holds x in B iff ex a be set st a in X.i & x = [a,i]; thus A c= B proof let x be set; assume x in A; then ex a be set st a in X.i & x = [a,i] by A4; hence thesis by A5; end; let x be set; assume x in B; then ex a be set st a in X.i & x = [a,i] by A5; hence thesis by A4; end; end; notation let I be set, X be ManySortedSet of I; synonym coprod X for disjoin X; end; registration let I be set, X be ManySortedSet of I; cluster coprod X -> I-defined; coherence proof dom coprod X = dom X by CARD_3:def 3; then dom coprod X = I by PARTFUN1:def 2; hence thesis by RELAT_1:def 18; end; end; registration let I be set, X be ManySortedSet of I; cluster coprod X -> total; coherence proof dom coprod X = dom X by CARD_3:def 3; then dom coprod X = I by PARTFUN1:def 2; hence thesis by PARTFUN1:def 2; end; end; definition let I be set, X be ManySortedSet of I; redefine func coprod X means :Def3: dom it = I & for i be set st i in I holds it.i = coprod(i,X); compatibility proof let IT be Function; hereby assume A1: IT = disjoin X; hence dom IT = I by PARTFUN1:def 2; let i be set; assume A2: i in I; then i in dom X by PARTFUN1:def 2; then A3: IT.i = [:X.i,{i}:] by A1,CARD_3:def 3; now let x be set; hereby assume x in IT.i; then consider a,b being set such that A4: a in X.i and A5: b in {i} & x = [a,b] by A3,ZFMISC_1:def 2; take a; thus a in X.i by A4; thus x = [a,i] by A5,TARSKI:def 1; end; given a being set such that A6: a in X.i & x = [a,i]; i in {i} by TARSKI:def 1; hence x in IT.i by A3,A6,ZFMISC_1:def 2; end; hence IT.i = coprod(i,X) by A2,Def2; end; assume that A7: dom IT = I and A8: for i be set st i in I holds IT.i = coprod(i,X); A9: dom IT = dom X by A7,PARTFUN1:def 2; now let x be set; assume A10: x in dom X; then A11: x in I; A12: now let a be set; hereby assume a in coprod(x,X); then A13: ex b being set st b in X.x & a = [b,x] by A11,Def2; x in {x} by TARSKI:def 1; hence a in [:X.x,{x}:] by A13,ZFMISC_1:def 2; end; assume a in [:X.x,{x}:]; then consider a1,a2 being set such that A14: a1 in X.x and A15: a2 in {x} and A16: a = [a1,a2] by ZFMISC_1:def 2; a2 = x by A15,TARSKI:def 1; hence a in coprod(x,X) by A11,A14,A16,Def2; end; thus IT.x = coprod(x,X) by A8,A10 .= [:X.x,{x}:] by A12,TARSKI:1; end; hence thesis by A9,CARD_3:def 3; end; end; registration let I be non empty set, X be non-empty ManySortedSet of I; cluster coprod X -> non-empty; coherence proof now let x be set; assume x in I; then reconsider i = x as Element of I; consider a be set such that A1: a in X.i by XBOOLE_0:def 1; (coprod X).i = coprod(i,X) by Def3; then [a,i] in (coprod X).i by A1,Def2; hence (coprod X).x is non empty; end; hence thesis by PBOOLE:def 13; end; end; registration let I be non empty set, X be non-empty ManySortedSet of I; cluster Union X -> non empty; coherence proof set i = the Element of I; consider a be set such that A1: a in X.i by XBOOLE_0:def 1; dom X = I by PARTFUN1:def 2; then X.i in rng X by FUNCT_1:def 3; then a in union rng X by A1,TARSKI:def 4; hence thesis by CARD_3:def 4; end; end; theorem for I be set, X be ManySortedSet of I, i be set st i in I holds X.i <> {} iff (coprod X).i <> {} proof let I be set, X be ManySortedSet of I, i be set; assume A1: i in I; then A2: (coprod X).i = coprod(i,X) by Def3; thus X.i <> {} implies (coprod X).i <> {} proof assume X.i <> {}; then consider x be set such that A3: x in X.i by XBOOLE_0:def 1; [x,i] in (coprod X).i by A1,A2,A3,Def2; hence thesis; end; assume (coprod X).i <> {}; then consider a be set such that A4: a in coprod(i,X) by A2,XBOOLE_0:def 1; ex x be set st x in X.i & a = [x,i] by A1,A4,Def2; hence thesis; end; begin :: :: Free Many Sorted Universal Algebra - General Notions :: reserve S for non void non empty ManySortedSign, U0 for MSAlgebra over S; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; mode GeneratorSet of U0 -> MSSubset of U0 means :Def4: the Sorts of GenMSAlg (it) = the Sorts of U0; existence proof set A = the Sorts of U0; reconsider A as MSSubset of U0 by PBOOLE:def 18; take A; set G = GenMSAlg(A); the Sorts of G is MSSubset of U0 by MSUALG_2:def 9; then A1: the Sorts of G c= A by PBOOLE:def 18; A is MSSubset of G by MSUALG_2:def 17; then A c= the Sorts of G by PBOOLE:def 18; hence thesis by A1,PBOOLE:146; end; end; theorem for S be non void non empty ManySortedSign, U0 be strict non-empty MSAlgebra over S, A be MSSubset of U0 holds A is GeneratorSet of U0 iff GenMSAlg(A) = U0 proof let S be non void non empty ManySortedSign, U0 be strict non-empty MSAlgebra over S, A be MSSubset of U0; thus A is GeneratorSet of U0 implies GenMSAlg(A) = U0 proof reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5; assume A is GeneratorSet of U0; then the Sorts of GenMSAlg(A) = the Sorts of U1 by Def4; hence thesis by MSUALG_2:9; end; assume GenMSAlg(A) = U0; hence thesis by Def4; end; definition let S,U0; let IT be GeneratorSet of U0; attr IT is free means :Def5: for U1 be non-empty MSAlgebra over S for f be ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st h is_homomorphism U0,U1 & h || IT = f; end; definition let S be non void non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is free means :Def6: ex G being GeneratorSet of IT st G is free; end; theorem Th4: for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds Union coprod X misses [:the carrier' of S,{the carrier of S}:] proof let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; assume Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] <> {}; then consider x be set such that A1: x in Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] by XBOOLE_0:def 1; x in Union (coprod X) by A1,XBOOLE_0:def 4; then x in union rng (coprod X) by CARD_3:def 4; then consider A be set such that A2: x in A and A3: A in rng (coprod X) by TARSKI:def 4; consider s be set such that A4: s in dom (coprod X) and A5: (coprod X).s = A by A3,FUNCT_1:def 3; reconsider s as SortSymbol of S by A4; A = coprod(s,X) by A5,Def3; then A6: ex a be set st a in X.s & x = [a,s] by A2,Def2; x in [:the carrier' of S,{the carrier of S}:] by A1,XBOOLE_0:def 4; then s in {the carrier of S} by A6,ZFMISC_1:87; then s in the carrier of S & s = the carrier of S by TARSKI:def 1; hence contradiction; end; begin :: :: Construction of Free Many Sorted Algebras for Given Signature :: definition let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; func REL(X) -> Relation of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*) means :Def7: for a be Element of [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a 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)); existence proof set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X); defpred P[Element of O,Element of O*] means $1 in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = $1 holds len $2 = len (the_arity_of o) & for x be set st x in dom $2 holds ($2.x in [: the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1 ,the carrier of S] = $2.x holds the_result_sort_of o1 = (the_arity_of o).x) & ( $2.x in Union (coprod X) implies $2.x in coprod((the_arity_of o).x,X)); consider R be Relation of O,O* such that A1: for a be Element of O, b be Element of O* holds [a,b] in R iff P[a ,b] from RELSET_1:sch 2; take R; let a be Element of O, b be Element of O*; thus [a,b] in R implies a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a 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)) by A1; assume a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a 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)); hence thesis by A1; end; uniqueness proof set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X); let R,P be Relation of O,O*; assume that A2: for a be Element of O, b be Element of O* holds [a,b] in R iff a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o, the carrier of S] = a 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)) and A3: for a be Element of O, b be Element of O* holds [a,b] in P iff a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o, the carrier of S] = a 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)); for x,y be set holds [x,y] in R iff [x,y] in P proof let x,y be set; thus [x,y] in R implies [x,y] in P proof assume A4: [x,y] in R; then reconsider a = x as Element of O by ZFMISC_1:87; reconsider b = y as Element of O* by A4,ZFMISC_1:87; [a,b] in R by A4; then A5: a in [:the carrier' of S,{the carrier of S}:] by A2; for o be OperSymbol of S st [o,the carrier of S] = a 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)) by A2,A4; hence thesis by A3,A5; end; assume A6: [x,y] in P; then reconsider a = x as Element of O by ZFMISC_1:87; reconsider b = y as Element of O* by A6,ZFMISC_1:87; [a,b] in P by A6; then A7: a in [:the carrier' of S,{the carrier of S}:] by A3; for o be OperSymbol of S st [o,the carrier of S] = a 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)) by A3,A6; hence thesis by A2,A7; end; hence thesis by RELAT_1:def 2; end; end; reserve S for non void non empty ManySortedSign, X for ManySortedSet of the carrier of S, o for OperSymbol of S, b for Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*; theorem Th5: [[o,the carrier of S],b] in REL(X) iff 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)) proof defpred P[OperSymbol of S,Element of ([:the carrier' of S,{the carrier of S} :] \/ Union (coprod X))*] means len $2 = len (the_arity_of $1) & for x be set st x in dom $2 holds ($2.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x holds the_result_sort_of o1 = (the_arity_of $1).x) & ($2.x in Union (coprod X) implies b.x in coprod((the_arity_of $1).x,X)); set a = [o,the carrier of S]; the carrier of S in {the carrier of S} by TARSKI:def 1; then A1: a in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87; then reconsider a as Element of [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X) by XBOOLE_0:def 3; thus [[o,the carrier of S],b] in REL(X) implies P[o,b] proof assume [[o,the carrier of S],b] in REL(X); then for o1 be OperSymbol of S st [o1,the carrier of S] = a holds P[o1,b] by Def7; hence thesis; end; assume A2: P[o,b]; now let o1 be OperSymbol of S; assume [o1,the carrier of S] = a; then o1 = o by XTUPLE_0:1; hence P[o1,b] by A2; end; hence thesis by A1,Def7; end; definition let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; func DTConMSA(X) -> DTConstrStr equals DTConstrStr (# [:the carrier' of S,{ the carrier of S}:] \/ Union (coprod X), REL(X) #); correctness; end; registration let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; cluster DTConMSA(X) -> strict non empty; coherence; end; theorem Th6: for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds NonTerminals(DTConMSA(X))c= [:the carrier' of S,{the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA(X)) & (X is non-empty implies NonTerminals(DTConMSA(X)) = [:the carrier' of S,{the carrier of S}:] & Terminals (DTConMSA(X)) = Union (coprod X)) proof let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union ( coprod (X qua ManySortedSet of the carrier of S)); A1: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1; thus A2: NonTerminals D c= [:the carrier' of S,{the carrier of S}:] proof let x be set; assume x in NonTerminals D; then x in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by LANG1:def 3; then consider s be Symbol of D such that A3: s = x and A4: ex n being FinSequence st s ==> n; consider n be FinSequence such that A5: s ==> n by A4; [s,n] in the Rules of D by A5,LANG1:def 1; then reconsider n as Element of A* by ZFMISC_1:87; reconsider s as Element of A; [s,n] in REL X by A5,LANG1:def 1; hence thesis by A3,Def7; end; A6: Union(coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4; thus A7: Union (coprod X) c= Terminals (DTConMSA(X)) proof let x be set; assume A8: x in Union (coprod X); then x in A by XBOOLE_0:def 3; then x in Terminals D or x in NonTerminals D by A1,XBOOLE_0:def 3; hence thesis by A6,A2,A8,XBOOLE_0:3; end; assume A9: X is non-empty; thus NonTerminals D c= [:the carrier' of S,{the carrier of S}:] by A2; thus A10: [:the carrier' of S,{the carrier of S}:] c= NonTerminals D proof let x be set; assume A11: x in [:the carrier' of S,{the carrier of S}:]; then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that A12: x = [o,x2] by DOMAIN_1:1; set O = the_arity_of o; defpred P[set,set] means $2 in coprod (O.$1,X); A13: for a be set st a in Seg len O ex b be set st P[a,b] proof let a be set; assume a in Seg len O; then a in dom O by FINSEQ_1:def 3; then A14: O.a in rng O by FUNCT_1:def 3; A15: rng O c= the carrier of S by FINSEQ_1:def 4; then consider x be set such that A16: x in X.(O.a) by A9,A14,XBOOLE_0:def 1; take [x,O.a]; thus thesis by A14,A15,A16,Def2; end; consider b be Function such that A17: dom b = Seg len O & for a be set st a in Seg len O holds P[a,b.a] from CLASSES1:sch 1(A13); reconsider b as FinSequence by A17,FINSEQ_1:def 2; rng b c= A proof let a be set; A18: rng O c= the carrier of S by FINSEQ_1:def 4; assume a in rng b; then consider c be set such that A19: c in dom b and A20: b.c = a by FUNCT_1:def 3; dom O = Seg len O by FINSEQ_1:def 3; then A21: O.c in rng O by A17,A19,FUNCT_1:def 3; dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).(O.c) in rng coprod(X) by A21,A18,FUNCT_1:def 3; then A22: coprod(O.c,X) in rng coprod(X) by A21,A18,Def3; a in coprod(O.c,X) by A17,A19,A20; then a in union rng coprod(X) by A22,TARSKI:def 4; then a in Union coprod(X) by CARD_3:def 4; hence thesis by XBOOLE_0:def 3; end; then reconsider b as FinSequence of A by FINSEQ_1:def 4; reconsider b as Element of A* by FINSEQ_1:def 11; A23: now let c be set; assume A24: c in dom b; dom O = Seg len O by FINSEQ_1:def 3; then A25: O.c in rng O by A17,A24,FUNCT_1:def 3; A26: rng O c= the carrier of S by FINSEQ_1:def 4; dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).(O.c) in rng coprod(X) by A25,A26,FUNCT_1:def 3; then A27: coprod(O.c,X) in rng coprod(X) by A25,A26,Def3; P[c,b.c] by A17,A24; then b.c in union rng coprod(X) by A27,TARSKI:def 4; then b.c in Union coprod(X) by CARD_3:def 4; hence b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O. c by A6,XBOOLE_0:3; assume b.c in Union (coprod X); thus b.c in coprod(O.c,X) by A17,A24; end; A28: the carrier of S = x2 by TARSKI:def 1; then reconsider xa = [o,the carrier of S] as Element of (the carrier of D) by A11,A12, XBOOLE_0:def 3; len b = len O by A17,FINSEQ_1:def 3; then [xa,b] in REL(X) by A23,Th5; then xa ==> b by LANG1:def 1; then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n}; hence thesis by A12,A28,LANG1:def 3; end; A29: (Terminals D) misses (NonTerminals D) by DTCONSTR:8; thus Terminals D c= Union (coprod X) proof let x be set; assume x in Terminals D; then x in A & not x in [:the carrier' of S,{the carrier of S}:] by A1,A29 ,A10,XBOOLE_0:3,def 3; hence thesis by XBOOLE_0:def 3; end; thus thesis by A7; end; reserve x for set; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster DTConMSA(X) -> with_terminals with_nonterminals with_useful_nonterminals; coherence proof set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)); A1: Terminals D = Union (coprod X) by Th6; A2: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6; A3: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4; for nt being Symbol of D st nt in NonTerminals D ex p being FinSequence of TS(D) st nt ==> roots p proof let nt be Symbol of D; assume nt in NonTerminals D; then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that A4: nt = [o,x2] by A2,DOMAIN_1:1; set O = the_arity_of o; defpred P[set,set] means $2 in coprod(O.$1,X); A5: for a be set st a in Seg len O ex b be set st P[a,b] proof let a be set; assume a in Seg len O; then a in dom O by FINSEQ_1:def 3; then A6: O.a in rng O by FUNCT_1:def 3; A7: rng O c= the carrier of S by FINSEQ_1:def 4; then consider x be set such that A8: x in X.(O.a) by A6,XBOOLE_0:def 1; take [x,O.a]; thus thesis by A6,A7,A8,Def2; end; consider b be Function such that A9: dom b = Seg len O & for a be set st a in Seg len O holds P[a,b. a] from CLASSES1:sch 1(A5); reconsider b as FinSequence by A9,FINSEQ_1:def 2; A10: rng b c= A proof let a be set; A11: rng O c= the carrier of S by FINSEQ_1:def 4; assume a in rng b; then consider c be set such that A12: c in dom b and A13: b.c = a by FUNCT_1:def 3; dom O = Seg len O by FINSEQ_1:def 3; then A14: O.c in rng O by A9,A12,FUNCT_1:def 3; dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).(O.c) in rng coprod(X) by A14,A11,FUNCT_1:def 3; then A15: coprod(O.c,X) in rng coprod(X) by A14,A11,Def3; a in coprod (O.c,X) by A9,A12,A13; then a in union rng coprod(X) by A15,TARSKI:def 4; then a in Union coprod(X) by CARD_3:def 4; hence thesis by XBOOLE_0:def 3; end; then reconsider b as FinSequence of A by FINSEQ_1:def 4; reconsider b as Element of A* by FINSEQ_1:def 11; deffunc F(set)=root-tree (b.$1); consider f be Function such that A16: dom f = dom b & for x st x in dom b holds f.x = F(x) from FUNCT_1:sch 3; reconsider f as FinSequence by A9,A16,FINSEQ_1:def 2; rng f c= TS(D) proof let x; A17: rng O c= the carrier of S by FINSEQ_1:def 4; assume x in rng f; then consider y be set such that A18: y in dom f and A19: f.y = x by FUNCT_1:def 3; dom O = Seg len O by FINSEQ_1:def 3; then A20: O.y in rng O by A9,A16,A18,FUNCT_1:def 3; dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).(O.y) in rng coprod(X) by A20,A17,FUNCT_1:def 3; then A21: coprod(O.y,X) in rng coprod(X) by A20,A17,Def3; b.y in rng b by A16,A18,FUNCT_1:def 3; then reconsider a = b.y as Symbol of D by A10; P[y,b.y] by A9,A16,A18; then b.y in union rng coprod(X) by A21,TARSKI:def 4; then A22: a in Terminals D by A1,CARD_3:def 4; x = root-tree(b.y) by A16,A18,A19; hence thesis by A22,DTCONSTR:def 1; end; then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4; A23: for x st x in dom b holds (roots f).x = b.x proof let x; assume A24: x in dom b; then reconsider i = x as Nat; f.x = root-tree (b.x) & ex T be DecoratedTree st T = f.i & (roots f).i = T .{} by A16,A24,TREES_3:def 18; hence thesis by TREES_4:3; end; A25: now let c be set; assume A26: c in dom b; dom O = Seg len O by FINSEQ_1:def 3; then A27: O.c in rng O by A9,A26,FUNCT_1:def 3; A28: rng O c= the carrier of S by FINSEQ_1:def 4; dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).(O.c) in rng coprod(X) by A27,A28,FUNCT_1:def 3; then A29: coprod(O.c,X) in rng coprod(X) by A27,A28,Def3; P[c,b.c] by A9,A26; then b.c in union rng coprod(X) by A29,TARSKI:def 4; then b.c in Union coprod(X) by CARD_3:def 4; hence b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O. c by A3,XBOOLE_0:3; assume b.c in Union (coprod X); thus b.c in coprod(O.c,X) by A9,A26; end; the carrier of S = x2 & len b = len O by A9,FINSEQ_1:def 3,TARSKI:def 1; then [nt,b] in REL(X) by A4,A25,Th5; then A30: nt ==> b by LANG1:def 1; take f; dom (roots f) = dom f by TREES_3:def 18; hence thesis by A30,A16,A23,FUNCT_1:2; end; hence thesis by A1,A2,DTCONSTR:def 3,def 4,def 5; end; end; theorem Th7: for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S, t be set holds (t in Terminals DTConMSA(X) & X is non-empty implies ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]) & for s be SortSymbol of S, x be set st x in X.s holds [x,s] in Terminals DTConMSA(X) proof let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S, t be set; set D = DTConMSA(X); A1: Union (coprod X) c= Terminals (DTConMSA(X)) by Th6; A2: Union (coprod X) = union rng (coprod X) by CARD_3:def 4; thus t in Terminals D & X is non-empty implies ex s be SortSymbol of S, x be set st x in X.s & t = [x,s] proof assume that A3: t in Terminals D and A4: X is non-empty; Terminals D = Union (coprod X) by A4,Th6; then consider A be set such that A5: t in A and A6: A in rng(coprod X) by A2,A3,TARSKI:def 4; consider s be set such that A7: s in dom (coprod X) and A8: (coprod X).s = A by A6,FUNCT_1:def 3; reconsider s as SortSymbol of S by A7; (coprod X).s = coprod(s,X) by Def3; then consider x be set such that A9: x in X.s & t = [x,s] by A5,A8,Def2; take s; take x; thus thesis by A9; end; let s be SortSymbol of S, x be set such that A10: x in X.s; set t = [x,s]; dom(coprod X) = the carrier of S by PARTFUN1:def 2; then A11: (coprod X).s in rng (coprod X) by FUNCT_1:def 3; t in coprod(s,X) by A10,Def2; then t in (coprod X).s by Def3; then t in Union (coprod X) by A2,A11,TARSKI:def 4; hence thesis by A1; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S; func Sym(o,X) ->Symbol of DTConMSA(X) equals [o,the carrier of S]; coherence proof the carrier of S in {the carrier of S} by TARSKI:def 1; then [o,the carrier of S] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87; then [o,the carrier of S] in NonTerminals (DTConMSA X) by Th6; hence thesis; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func FreeSort(X,s) -> Subset of TS(DTConMSA(X)) equals {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s}; coherence proof set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a. {} & the_result_sort_of o = s}; A c= TS(DTConMSA(X)) proof let x be set; assume x in A; then ex a be Element of TS(DTConMSA(X)) st x = a &( (ex x be set st x in X .s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s); hence thesis; end; hence thesis; end; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; cluster FreeSort(X,s) -> non empty; coherence proof dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3; then A1: coprod(s,X) in rng coprod(X) by Def3; set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a. {} & the_result_sort_of o = s}; consider x be set such that A2: x in X.s by XBOOLE_0:def 1; set a = [x,s]; A3: (Terminals (DTConMSA(X))) = Union (coprod X) by Th6; a in coprod(s,X) by A2,Def2; then a in union rng coprod(X) by A1,TARSKI:def 4; then A4: a in Terminals (DTConMSA X) by A3,CARD_3:def 4; then reconsider a as Symbol of DTConMSA(X); reconsider b = root-tree a as Element of TS(DTConMSA X) by A4, DTCONSTR:def 1; b in A by A2; hence thesis; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeSort(X) -> ManySortedSet of the carrier of S means :Def11: for s be SortSymbol of S holds it.s = FreeSort(X,s); existence proof deffunc F(Element of S)=FreeSort(X,$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d =F(d) from FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; take f; thus thesis by A1; end; uniqueness proof let A,B be ManySortedSet of the carrier of S; assume that A2: for s be SortSymbol of S holds A.s = FreeSort(X,s) and A3: for s be SortSymbol of S holds B.s = FreeSort(X,s); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = FreeSort(X,s) by A2; hence thesis by A3; end; hence thesis by PBOOLE:3; end; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeSort(X) -> non-empty; coherence proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; (FreeSort(X)).s = FreeSort(X,s) by Def11; hence thesis; end; end; theorem Th8: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, x be set st x in (( FreeSort X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConMSA(X)) proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, x be set; set D = DTConMSA(X), ar = the_arity_of o, cr = the carrier of S; A1: (the Arity of S).o = ar by MSUALG_1:def 1; rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2; then A2: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27; assume x in ((FreeSort X)# * (the Arity of S)).o; then x in product ((FreeSort X) * ar) by A1,Th1; then consider f be Function such that A3: x = f and A4: dom f = dom ((FreeSort X) * ar) and A5: for y be set st y in dom ((FreeSort X)* ar) holds f.y in ((FreeSort X) * ar).y by CARD_3:def 5; dom ar = Seg len ar by FINSEQ_1:def 3; then reconsider f as FinSequence by A4,A2,FINSEQ_1:def 2; rng f c= TS D proof let a be set; assume a in rng f; then consider b be set such that A6: b in dom f and A7: f.b = a by FUNCT_1:def 3; A8: a in ((FreeSort X) * ar).b by A4,A5,A6,A7; reconsider b as Nat by A6; ((FreeSort X) * ar).b = (FreeSort X).(ar.b) by A4,A6,FUNCT_1:12 .= (FreeSort X). (ar/.b) by A4,A2,A6,PARTFUN1:def 6 .= FreeSort(X,ar/.b) by Def11 .= { s where s is Element of TS D: (ex x be set st x in X.(ar/.b) & s = root-tree [x,ar/.b]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = s .{} & the_result_sort_of o1=ar/.b}; then ex e be Element of TS D st a = e &( (ex x be set st x in X.(ar/.b) & e = root-tree [x,(ar/.b)]) or ex o be OperSymbol of S st [o,the carrier of S] = e .{} & the_result_sort_of o=ar/.b) by A8; hence thesis; end; then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4; f = x by A3; hence thesis; end; theorem Th9: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS (DTConMSA(X)) holds p in ((FreeSort X)# * (the Arity of S)).o iff dom p = dom ( the_arity_of o) & for n be Nat st n in dom p holds p.n in FreeSort(X,( the_arity_of o)/.n) proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X)); set AR = the Arity of S, cr = the carrier of S, ar = the_arity_of o; thus p in ((FreeSort X)# * AR).o implies dom p = dom (the_arity_of o) & for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n) proof A1: AR.o = ar by MSUALG_1:def 1; A2: rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2; then A3: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27; assume p in ((FreeSort X)# * (the Arity of S)).o; then A4: p in product ((FreeSort X) * ar) by A1,Th1; then A5: dom p = dom ((FreeSort X) * ar) by CARD_3:9; hence dom p = dom ar by A2,RELAT_1:27; let n be Nat; assume A6: n in dom p; then ((FreeSort X) * ar).n = (FreeSort X).(ar.n) by A5,FUNCT_1:12 .= (FreeSort X). (ar/.n) by A5,A3,A6,PARTFUN1:def 6 .= FreeSort(X,ar/.n) by Def11; hence thesis by A4,A5,A6,CARD_3:9; end; assume that A7: dom p = dom (the_arity_of o) and A8: for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o) /.n); rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2; then A9: dom p = dom ((FreeSort X) * ar) by A7,RELAT_1:27; A10: for x be set st x in dom((FreeSort X) * ar) holds p.x in ((FreeSort X) * ar).x proof let x be set; assume A11: x in dom ((FreeSort X) * ar); then reconsider n = x as Nat; FreeSort(X,ar/.n) = (FreeSort X). (ar/.n) by Def11 .= (FreeSort X).(ar.n) by A7,A9,A11,PARTFUN1:def 6 .= ((FreeSort X) * ar).x by A11,FUNCT_1:12; hence thesis by A8,A9,A11; end; AR.o = ar by MSUALG_1:def 1; then ((FreeSort X)# * AR).o = product ((FreeSort X) * ar) by Th1; hence thesis by A9,A10,CARD_3:9; end; theorem Th10: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS (DTConMSA(X)) holds Sym(o,X) ==> roots p iff p in ((FreeSort X)# * (the Arity of S)).o proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X)); set D = DTConMSA(X), ar = the_arity_of o; set r = roots p, OU = [:the carrier' of S,{the carrier of S}:] \/ Union ( coprod X); A1: dom p = dom r by TREES_3:def 18; thus Sym(o,X) ==> roots p implies p in ((FreeSort X)# * (the Arity of S)).o proof assume Sym(o,X) ==> roots p; then A2: [[o,the carrier of S],roots p] in REL(X) by LANG1:def 1; then reconsider r = roots p as Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))* by ZFMISC_1:87; A3: dom p = dom r by TREES_3:def 18; A4: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3; A5: len r = len ar by A2,Th5; for n be Nat st n in dom p holds p.n in FreeSort(X,ar/.n) proof let n be Nat; set s = ar/.n; assume A6: n in dom p; then consider T be DecoratedTree such that A7: T = p.n and A8: r.n = T.{} by TREES_3:def 18; rng p c= TS D & p.n in rng p by A6,FINSEQ_1:def 4,FUNCT_1:def 3; then reconsider T as Element of TS(D) by A7; A9: rng r c= [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X) & r.n in rng r by A3,A6,FINSEQ_1:def 4,FUNCT_1:def 3; per cases by A9,XBOOLE_0:def 3; suppose A10: r.n in [:the carrier' of S,{the carrier of S}:]; then consider o1 being OperSymbol of S, x2 being Element of {the carrier of S} such that A11: r.n = [o1,x2] by DOMAIN_1:1; A12: x2 = the carrier of S by TARSKI:def 1; then the_result_sort_of o1 = ar.n by A2,A3,A6,A10,A11,Th5 .= ar/.n by A5,A3,A4,A6,PARTFUN1:def 6; then (ex x be set st x in X.s & T = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = T.{} & the_result_sort_of o = s by A8 ,A11,A12; hence thesis by A7; end; suppose A13: r.n in Union (coprod X); then r.n in coprod(ar.n,X) by A2,A3,A6,Th5; then r.n in coprod(s,X) by A5,A3,A4,A6,PARTFUN1:def 6; then A14: ex a be set st a in X.s & r.n = [a,s] by Def2; reconsider t = r.n as Terminal of D by A13,Th6; T = root-tree t by A8,DTCONSTR:9; hence thesis by A7,A14; end; end; hence thesis by A5,A3,A4,Th9; end; A15: dom r = Seg len r by FINSEQ_1:def 3; reconsider r as FinSequence of OU; reconsider r as Element of OU* by FINSEQ_1:def 11; assume A16: p in ((FreeSort X)# * (the Arity of S)).o; then A17: dom p = dom ar by Th9; A18: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4; A19: for x be set st x in dom r holds (r.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r. x holds the_result_sort_of o1 = ar.x) & (r.x in Union (coprod X) implies r.x in coprod(ar.x,X)) proof let x be set; assume A20: x in dom r; then reconsider n = x as Nat; A21: ex T be DecoratedTree st T = p.n & r.n = T.{} by A1,A20,TREES_3:def 18; set s = ar/.n; p.n in FreeSort(X,s) by A16,A1,A20,Th9; then consider a be Element of TS D such that A22: a = p.n and A23: (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s; A24: s = ar.n by A17,A1,A20,PARTFUN1:def 6; thus r.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 = ar .x proof assume A25: r.x in [:the carrier' of S,{the carrier of S}:]; A26: now dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3; then A27: coprod(s,X) in rng coprod(X) by Def3; given y be set such that A28: y in X.s & a = root-tree [y,s]; r.x = [y,s] & [y,s] in coprod(s,X) by A22,A21,A28,Def2,TREES_4:3; then r.x in union rng coprod(X) by A27,TARSKI:def 4; then r.x in Union (coprod X) by CARD_3:def 4; hence contradiction by A18,A25,XBOOLE_0:3; end; let o1 be OperSymbol of S; assume [o1,the carrier of S] = r.x; hence thesis by A22,A23,A21,A24,A26,XTUPLE_0:1; end; assume A29: r.x in Union (coprod X); now given o1 be OperSymbol of S such that A30: [o1,the carrier of S] = a.{} and the_result_sort_of o1 = s; the carrier of S in {the carrier of S} by TARSKI:def 1; then [o1,the carrier of S] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87; hence contradiction by A18,A22,A21,A29,A30,XBOOLE_0:3; end; then consider y be set such that A31: y in X.s and A32: a = root-tree [y,s] by A23; r.x = [y,s] by A22,A21,A32,TREES_4:3; hence thesis by A24,A31,Def2; end; len r = len ar by A17,A1,A15,FINSEQ_1:def 3; then [[o,the carrier of S],r] in REL X by A19,Th5; hence thesis by LANG1:def 1; end; theorem Th11: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds union rng (FreeSort X) = TS (DTConMSA(X )) proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; set D = DTConMSA(X); A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def 2; thus union rng (FreeSort X) c= TS D proof let x; assume x in union rng (FreeSort X); then consider A be set such that A2: x in A and A3: A in rng (FreeSort X) by TARSKI:def 4; consider s be set such that A4: s in dom (FreeSort X) and A5: (FreeSort X).s = A by A3,FUNCT_1:def 3; reconsider s as SortSymbol of S by A4; A = FreeSort(X,s) by A5,Def11 .= {a where a is Element of TS(D): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s}; then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a = root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} & the_result_sort_of o1 = s) by A2; hence thesis; end; let x; assume x in TS D; then reconsider t = x as Element of TS(D); A6: rng t c= the carrier of D & the carrier of D = (Terminals D) \/ ( NonTerminals D) by LANG1:1,RELAT_1:def 19; {} in dom t by TREES_1:22; then A7: t.{} in rng t by FUNCT_1:def 3; A8: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6; A9: Terminals D = Union (coprod X) by Th6; per cases by A7,A6,XBOOLE_0:def 3; suppose A10: t.{} in Terminals D; then reconsider a = t.{} as Terminal of D; a in union rng(coprod X) by A9,A10,CARD_3:def 4; then consider A be set such that A11: a in A and A12: A in rng(coprod X) by TARSKI:def 4; consider s be set such that A13: s in dom(coprod X) and A14: (coprod X).s = A by A12,FUNCT_1:def 3; reconsider s as SortSymbol of S by A13; A = coprod(s,X) by A14,Def3; then t = root-tree a & ex b be set st b in X.s & a = [b,s] by A11,Def2, DTCONSTR:9; then t in FreeSort(X,s); then A15: t in (FreeSort X).s by Def11; (FreeSort X).s in rng (FreeSort X) by A1,FUNCT_1:def 3; hence thesis by A15,TARSKI:def 4; end; suppose t.{} in NonTerminals D; then reconsider a = t.{} as NonTerminal of D; consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that A16: a = [o,x2] by A8,DOMAIN_1:1; set rs = the_result_sort_of o; x2 = the carrier of S by TARSKI:def 1; then t in FreeSort(X,rs) by A16; then A17: t in (FreeSort X).rs by Def11; (FreeSort X).rs in rng (FreeSort X) by A1,FUNCT_1:def 3; hence thesis by A17,TARSKI:def 4; end; end; theorem Th12: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S st s1 <> s2 holds ( FreeSort X).s1 misses (FreeSort X).s2 proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S; assume that A1: s1 <> s2 and A2: (FreeSort X).s1 /\ (FreeSort X).s2 <> {}; consider x such that A3: x in (FreeSort X).s1 /\ (FreeSort X).s2 by A2,XBOOLE_0:def 1; set D = DTConMSA(X); A4: (FreeSort X).s1 = FreeSort(X,s1) by Def11; A5: (FreeSort X).s2 = FreeSort(X,s2) by Def11; x in (FreeSort X).s2 by A3,XBOOLE_0:def 4; then consider b be Element of TS D such that A6: b = x and A7: (ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]) or ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2 by A5; x in (FreeSort X).s1 by A3,XBOOLE_0:def 4; then consider a be Element of TS D such that A8: a = x and A9: (ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1 by A4; per cases by A9; suppose ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1]; then consider x1 be set such that x1 in X.s1 and A10: a = root-tree [x1,s1]; now per cases by A7; case ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]; then consider x2 be set such that x2 in X.s2 and A11: b = root-tree [x2,s2]; [x1,s1] = [x2,s2] by A8,A6,A10,A11,TREES_4:4; hence contradiction by A1,XTUPLE_0:1; end; case ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2; then consider o2 be OperSymbol of S such that A12: [o2,the carrier of S] = b.{} and the_result_sort_of o2 = s2; [o2,the carrier of S] = [x1,s1] by A8,A6,A10,A12,TREES_4:3; then A13: the carrier of S = s1 by XTUPLE_0:1; for X be set holds not X in X; hence contradiction by A13; end; end; hence contradiction; end; suppose ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1; then consider o1 be OperSymbol of S such that A14: [o1,the carrier of S] = a.{} and A15: the_result_sort_of o1 = s1; now per cases by A7; case ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]; then consider x2 be set such that x2 in X.s2 and A16: b = root-tree [x2,s2]; [o1,the carrier of S] = [x2,s2] by A8,A6,A14,A16,TREES_4:3; then A17: the carrier of S = s2 by XTUPLE_0:1; for X be set holds not X in X; hence contradiction by A17; end; case ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2; hence contradiction by A1,A8,A6,A14,A15,XTUPLE_0:1; end; end; hence contradiction; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S; func DenOp(o,X) -> Function of ((FreeSort X)# * (the Arity of S)).o, (( FreeSort X) * (the ResultSort of S)).o means :Def12: for p be FinSequence of TS (DTConMSA(X)) st Sym(o,X) ==> roots p holds it.p = (Sym(o,X))-tree p; existence proof set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the ResultSort of S)).o, D = DTConMSA(X), O = the carrier' of S, rs = the_result_sort_of o, RS = the ResultSort of S; defpred P[set,set] means for p be FinSequence of TS D st p = $1 holds $2 = (Sym(o,X))-tree p; A1: for x be set st x in AL ex y be set st y in AX & P[x,y] proof let x be set; assume A2: x in AL; then reconsider p = x as FinSequence of TS(D) by Th8; Sym(o,X) ==> roots p by A2,Th10; then reconsider a = (Sym(o,X))-tree p as Element of TS D by DTCONSTR:def 1; take y = (Sym(o,X))-tree p; o in O; then o in dom ((FreeSort X) * RS) by PARTFUN1:def 2; then A3: AX =(FreeSort X).(RS.o) by FUNCT_1:12 .= (FreeSort X).rs by MSUALG_1:def 2 .= FreeSort(X,rs) by Def11; a.{} = Sym(o,X) by TREES_4:def 4; hence y in AX by A3; thus thesis; end; consider f be Function such that A4: dom f = AL & rng f c= AX & for x be set st x in AL holds P[x,f.x] from FUNCT_1:sch 5(A1); reconsider g = f as Function of AL,rng f by A4,FUNCT_2:1; reconsider g as Function of AL,AX by A4,FUNCT_2:2; take g; let p be FinSequence of TS D; assume Sym(o,X) ==> roots p; then p in AL by Th10; hence thesis by A4; end; uniqueness proof set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the ResultSort of S)).o, D = DTConMSA(X); let f,g be Function of AL, AX; assume that A5: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds f.p = (Sym(o,X))-tree p and A6: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds g.p = (Sym(o,X))-tree p; A7: for x be set st x in AL holds f.x = g.x proof let x be set; assume A8: x in AL; then reconsider p = x as FinSequence of TS(D) by Th8; A9: Sym(o,X) ==> roots p by A8,Th10; then f.p = (Sym(o,X))-tree p by A5; hence thesis by A6,A9; end; dom f = AL & dom g = AL by FUNCT_2:def 1; hence thesis by A7,FUNCT_1:2; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeOper(X) -> ManySortedFunction of (FreeSort X)# * (the Arity of S), (FreeSort X) * (the ResultSort of S) means :Def13: for o be OperSymbol of S holds it.o = DenOp(o,X); existence proof defpred P[set,set] means for o be OperSymbol of S st $1 = o holds $2 = DenOp(o,X); set Y = the carrier' of S; A1: for x be set st x in Y ex y be set st P[x,y] proof let x be set; assume x in Y; then reconsider o = x as OperSymbol of S; take DenOp(o,X); thus thesis; end; consider f be Function such that A2: dom f = Y & for x be set st x in Y holds P[x,f.x] from CLASSES1: sch 1( A1); reconsider f as ManySortedSet of Y by A2,PARTFUN1:def 2,RELAT_1:def 18; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider o = x as OperSymbol of S; f.o = DenOp(o,X) by A2; hence thesis; end; then reconsider f as ManySortedFunction of Y by FUNCOP_1:def 6; for x be set st x in Y holds f.x is Function of ((FreeSort X)# * (the Arity of S)).x, ((FreeSort X) * (the ResultSort of S)).x proof let x be set; assume x in Y; then reconsider o = x as OperSymbol of S; f.o = DenOp(o,X) by A2; hence thesis; end; then reconsider f as ManySortedFunction of (FreeSort X)# * (the Arity of S), ( FreeSort X) * (the ResultSort of S) by PBOOLE:def 15; take f; let o be OperSymbol of S; thus thesis by A2; end; uniqueness proof let A,B be ManySortedFunction of (FreeSort X)# * (the Arity of S), ( FreeSort X) * (the ResultSort of S); assume that A3: for o be OperSymbol of S holds A.o = DenOp(o,X) and A4: for o be OperSymbol of S holds B.o = DenOp(o,X); for i be set st i in the carrier' of S holds A.i = B.i proof let i be set; assume i in the carrier' of S; then reconsider s = i as OperSymbol of S; A.s = DenOp(s,X) by A3; hence thesis by A4; end; hence thesis by PBOOLE:3; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeMSA(X) -> MSAlgebra over S equals MSAlgebra (# FreeSort(X), FreeOper(X) #); coherence; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeMSA(X) -> strict non-empty; coherence by MSUALG_1:def 3; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func FreeGen(s,X) -> Subset of (FreeSort(X)).s means :Def15: for x be set holds x in it iff ex a be set st a in X.s & x = root-tree [a,s]; existence proof defpred P[set] means ex a be set st a in X.s & $1 = root-tree [a,s]; set D = DTConMSA(X); consider A be set such that A1: for x holds x in A iff x in (FreeSort(X)).s & P[x] from XBOOLE_0: sch 1; A c= (FreeSort(X)).s proof let x; assume x in A; hence thesis by A1; end; then reconsider A as Subset of (FreeSort(X)).s; for x holds x in A iff P[x] proof dom coprod(X) = the carrier of S by PARTFUN1:def 2; then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3; then A2: coprod(s,X) in rng coprod(X) by Def3; A3: Terminals D = Union (coprod X) by Th6; let x; thus x in A implies P[x] by A1; set A = {aa where aa is Element of TS(D): (ex x be set st x in X.s & aa = root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = aa.{} & the_result_sort_of o1 = s}; assume A4: P[x]; then consider a be set such that A5: a in X.s and A6: x = root-tree [a,s]; A7: (FreeSort X).s = FreeSort(X,s) by Def11; set sa = [a,s]; sa in coprod(s,X) by A5,Def2; then sa in union rng coprod(X) by A2,TARSKI:def 4; then A8: sa in Terminals D by A3,CARD_3:def 4; then reconsider sa as Symbol of D; reconsider b = root-tree sa as Element of TS(D) by A8,DTCONSTR:def 1; b in A by A5; hence thesis by A1,A4,A6,A7; end; hence thesis; end; uniqueness proof let A,B be Subset of (FreeSort(X)).s; assume that A9: for x be set holds x in A iff ex a be set st a in X.s & x = root-tree [a,s] and A10: for x be set holds x in B iff ex a be set st a in X.s & x = root-tree [a,s]; thus A c= B proof let x be set; assume x in A; then ex a be set st a in X.s & x = root-tree [a,s] by A9; hence thesis by A10; end; let x be set; assume x in B; then ex a be set st a in X.s & x = root-tree [a,s] by A10; hence thesis by A9; end; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; cluster FreeGen(s,X) -> non empty; coherence proof consider x such that A1: x in X.s by XBOOLE_0:def 1; ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1; hence thesis by Def15; end; end; theorem Th13: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S holds FreeGen(s,X) = { root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X) & t`2 = s} proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; set D = DTConMSA(X), A = {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}; thus FreeGen(s,X) c= A proof let x be set; assume x in FreeGen(s,X); then consider a be set such that A1: a in X.s and A2: x = root-tree [a,s] by Def15; A3: [a,s] in Terminals D by A1,Th7; then reconsider t = [a,s] as Symbol of D; t`2 = s by MCART_1:7; hence thesis by A2,A3; end; let x be set; assume x in A; then consider t be Symbol of D such that A4: x = root-tree t and A5: t in Terminals D and A6: t`2 = s; consider s1 be SortSymbol of S, a be set such that A7: a in X.s1 and A8: t = [a,s1] by A5,Th7; s = s1 by A6,A8,MCART_1:7; hence thesis by A4,A7,A8,Def15; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeGen(X) -> GeneratorSet of FreeMSA(X) means :Def16: for s be SortSymbol of S holds it.s = FreeGen(s,X); existence proof deffunc F(Element of S)=FreeGen($1,X); set FM = FreeMSA(X), D = DTConMSA(X); consider f be Function such that A1: dom f = the carrier of S & for s be Element of S holds f.s = F(s) from FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; f c= the Sorts of FM proof let x; assume x in the carrier of S; then reconsider s = x as SortSymbol of S; f.s = FreeGen(s,X) by A1; hence thesis; end; then reconsider f as MSSubset of FM by PBOOLE:def 18; the Sorts of GenMSAlg(f) = the Sorts of FM proof defpred P[set] means $1 in union rng (the Sorts of GenMSAlg(f)); the Sorts of GenMSAlg(f) is MSSubset of FM by MSUALG_2:def 9; then A2: the Sorts of GenMSAlg(f) c= the Sorts of FM by PBOOLE:def 18; A3: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P [t] holds P[nt-tree ts] proof set G = GenMSAlg(f), OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)); let nt be Symbol of D, ts be FinSequence of TS(D); assume that A4: nt ==> roots ts and A5: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; reconsider sy = nt as Element of OU; A6: [nt,roots ts] in the Rules of D by A4,LANG1:def 1; then reconsider rt = roots ts as Element of OU* by ZFMISC_1:87; [sy,rt] in REL(X) by A4,LANG1:def 1; then sy in [:the carrier' of S,{the carrier of S}:] by Def7; then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that A7: sy = [o,x2] by DOMAIN_1:1; set ar = the_arity_of o, rs = the_result_sort_of o; A8: x2 = the carrier of S by TARSKI:def 1; [nt,roots ts] in REL(X) by A4,LANG1:def 1; then A9: len rt = len ar by A7,A8,Th5; reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 9; A10: dom B = the carrier of S by PARTFUN1:def 2; A11: dom (roots ts) = dom ts by TREES_3:def 18; rng ar c= the carrier of S by FINSEQ_1:def 4; then A12: dom (B * ar) = dom ar by A10,RELAT_1:27; A13: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3; then A14: dom ts = dom ar by A6,A7,A8,A11,Th5; A15: for x st x in dom (B * ar) holds ts.x in (B * ar).x proof let x; assume A16: x in dom (B * ar); then reconsider n = x as Nat; A17: ts.n in rng ts by A12,A11,A9,A13,A16,FUNCT_1:def 3; rng ts c= TS D by FINSEQ_1:def 4; then reconsider T = ts.x as Element of TS(D) by A17; P[T] by A5,A17; then consider A be set such that A18: T in A and A19: A in rng (the Sorts of G) by TARSKI:def 4; set b = ar/.n, A1 = {a where a is Element of TS D: (ex x be set st x in X.b & a = root-tree [x,b]) or ex o be OperSymbol of S st [o,the carrier of S ] = a.{} & the_result_sort_of o = b}; A20: A1 = FreeSort(X,b) .= (FreeSort X).b by Def11; A21: ex t be DecoratedTree st t = ts.n & rt.n = t.{} by A12,A11,A9,A13,A16 ,TREES_3:def 18; consider s be set such that A22: s in dom(the Sorts of G) and A23: (the Sorts of G).s = A by A19,FUNCT_1:def 3; reconsider s as SortSymbol of S by A22; A24: rng rt c= [:the carrier' of S,{the carrier of S}:] \/ Union ( coprod X) & rt. n in rng rt by A12,A9,A13,A16,FINSEQ_1:def 4,FUNCT_1:def 3; A25: now per cases by A24,XBOOLE_0:def 3; suppose A26: rt.n in [:the carrier' of S,{the carrier of S}:]; then consider o1 being OperSymbol of S, x2 being Element of {the carrier of S} such that A27: rt.n = [o1,x2] by DOMAIN_1:1; A28: x2 = the carrier of S by TARSKI:def 1; then the_result_sort_of o1 = ar.n by A6,A7,A8,A12,A11,A14,A16,A26,A27 ,Th5 .= b by A12,A16,PARTFUN1:def 6; hence T in (FreeSort X).b by A20,A21,A27,A28; end; suppose A29: rt.n in Union (coprod X); then rt.n in coprod(ar.n,X) by A6,A7,A8,A12,A11,A14,A16,Th5; then rt.n in coprod(b,X) by A12,A16,PARTFUN1:def 6; then A30: ex a be set st a in X.b & rt.n = [a,b] by Def2; reconsider tt = rt.n as Terminal of D by A29,Th6; T = root-tree tt by A21,DTCONSTR:9; hence T in (FreeSort X).b by A20,A30; end; end; A31: now assume b <> s; then A32: (FreeSort X).s misses (FreeSort X).b by Th12; (the Sorts of G).s c= (the Sorts of FM).s by A2,PBOOLE:def 2; hence contradiction by A18,A23,A25,A32,XBOOLE_0:3; end; (B * ar).x = B.(ar.n) by A16,FUNCT_1:12 .= B.(ar/.n) by A12,A16,PARTFUN1:def 6; hence thesis by A18,A23,A31; end; set AR = the Arity of S, RS = the ResultSort of S, BH = B# * the Arity of S, O = the carrier' of S; A33: Den(o,FM) = (FreeOper X).o by MSUALG_1:def 6 .= DenOp(o,X) by Def13; A34: Sym(o,X) = [o,the carrier of S] & nt = [o,the carrier of S] by A7, TARSKI:def 1; AR.o = ar by MSUALG_1:def 1; then BH.o = product (B * ar) by Th1; then A35: ts in BH.o by A12,A11,A9,A13,A15,CARD_3:9; dom DenOp(o,X) = ((FreeSort X)# * AR).o by FUNCT_2:def 1; then ts in dom DenOp(o,X) by A4,A34,Th10; then ts in (dom DenOp(o,X)) /\ (BH.o) by A35,XBOOLE_0:def 4; then A36: ts in dom (DenOp(o,X) | (BH.o)) by RELAT_1:61; then (DenOp(o,X) | (BH.o)).ts = (DenOp(o,X)).ts by FUNCT_1:47 .= nt-tree ts by A4,A34,Def12; then A37: nt-tree ts in rng ((Den(o,FM))|(BH.o)) by A33,A36,FUNCT_1:def 3; RS.o = rs & dom (B * RS) = O by MSUALG_1:def 2,PARTFUN1:def 2; then A38: (B * RS).o = B.rs by FUNCT_1:12; B is opers_closed by MSUALG_2:def 9; then B is_closed_on o by MSUALG_2:def 6; then A39: rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 5; B.rs in rng B by A10,FUNCT_1:def 3; hence thesis by A39,A37,A38,TARSKI:def 4; end; A40: for s be Symbol of D st s in Terminals D holds P[root-tree s] proof let t be Symbol of D; assume t in Terminals D; then t in Union (coprod X) by Th6; then t in union rng(coprod X) by CARD_3:def 4; then consider A be set such that A41: t in A and A42: A in rng (coprod X) by TARSKI:def 4; consider s be set such that A43: s in dom (coprod X) and A44: (coprod X).s = A by A42,FUNCT_1:def 3; reconsider s as SortSymbol of S by A43; A = coprod(s,X) by A44,Def3; then ex a be set st a in X.s & t = [a,s] by A41,Def2; then A45: root-tree t in FreeGen(s,X) by Def15; f is MSSubset of GenMSAlg(f) by MSUALG_2:def 17; then f c= the Sorts of GenMSAlg(f) by PBOOLE:def 18; then f.s c= (the Sorts of GenMSAlg(f)).s by PBOOLE:def 2; then A46: FreeGen(s,X) c= (the Sorts of GenMSAlg(f)).s by A1; dom (the Sorts of GenMSAlg(f)) = the carrier of S by PARTFUN1:def 2; then (the Sorts of GenMSAlg(f)).s in rng (the Sorts of GenMSAlg(f)) by FUNCT_1:def 3; hence thesis by A46,A45,TARSKI:def 4; end; A47: for t being DecoratedTree of the carrier of D st t in TS D holds P[ t] from DTCONSTR:sch 7(A40,A3); A48: union rng(the Sorts of FM) c= union rng (the Sorts of GenMSAlg(f)) proof set D = DTConMSA(X); let x; assume x in union rng(the Sorts of FM); then consider A be set such that A49: x in A and A50: A in rng(the Sorts of FM) by TARSKI:def 4; consider s be set such that A51: s in dom (FreeSort X) and A52: (FreeSort X).s = A by A50,FUNCT_1:def 3; reconsider s as SortSymbol of S by A51; A = FreeSort(X,s) by A52,Def11 .= {a where a is Element of TS(D): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s}; then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a = root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} & the_result_sort_of o1 = s) by A49; hence thesis by A47; end; let x be Element of S; reconsider s = x as SortSymbol of S; thus (the Sorts of GenMSAlg(f)).x c= (the Sorts of FM).x by A2,PBOOLE:def 2; let a be set; assume A53: a in (the Sorts of FM).x; the carrier of S = dom (the Sorts of FM) by PARTFUN1:def 2; then (the Sorts of FM).s in rng (the Sorts of FM) by FUNCT_1:def 3; then a in union rng (the Sorts of FM) by A53,TARSKI:def 4; then consider A be set such that A54: a in A and A55: A in rng (the Sorts of GenMSAlg(f)) by A48,TARSKI:def 4; consider b be set such that A56: b in dom (the Sorts of GenMSAlg(f)) and A57: (the Sorts of GenMSAlg(f)).b = A by A55,FUNCT_1:def 3; reconsider b as SortSymbol of S by A56; now assume b <> s; then (FreeSort X).s misses (FreeSort X).b by Th12; then A58: (FreeSort X).s /\ (FreeSort X).b = {} by XBOOLE_0:def 7; (the Sorts of GenMSAlg(f)).b c= (the Sorts of FM).b by A2, PBOOLE:def 2; hence contradiction by A53,A54,A57,A58,XBOOLE_0:def 4; end; hence thesis by A54,A57; end; then reconsider f as GeneratorSet of FM by Def4; take f; thus thesis by A1; end; uniqueness proof let A,B be GeneratorSet of FreeMSA(X); assume that A59: for s be SortSymbol of S holds A.s = FreeGen(s,X) and A60: for s be SortSymbol of S holds B.s = FreeGen(s,X); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = FreeGen(s,X) by A59; hence thesis by A60; end; hence thesis by PBOOLE:3; end; end; theorem for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeGen(X)is non-empty proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; let x; assume x in the carrier of S; then reconsider s = x as SortSymbol of S; (FreeGen(X)).s = FreeGen(s,X) by Def16; hence thesis; end; theorem for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds union rng FreeGen(X) = {root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X)} proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; set D = DTConMSA(X), A = union rng FreeGen(X), B = {root-tree t where t is Symbol of D : t in Terminals D}; thus A c= B proof let x; assume x in A; then consider C be set such that A1: x in C and A2: C in rng FreeGen(X) by TARSKI:def 4; consider s be set such that A3: s in dom FreeGen(X) and A4: (FreeGen(X)).s = C by A2,FUNCT_1:def 3; reconsider s as SortSymbol of S by A3; C = FreeGen(s,X) by A4,Def16 .= {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s} by Th13; then ex t be Symbol of D st x = root-tree t & t in Terminals D & t`2 = s by A1; hence thesis; end; let x; assume x in B; then consider t be Symbol of D such that A5: x = root-tree t and A6: t in Terminals D; consider s be SortSymbol of S, a be set such that a in X.s and A7: t = [a,s] by A6,Th7; t`2 = s by A7,MCART_1:7; then x in {root-tree tt where tt is Symbol of D : tt in Terminals D & tt`2 = s} by A5,A6; then x in FreeGen(s,X) by Th13; then A8: x in (FreeGen(X)).s by Def16; dom FreeGen(X) = the carrier of S by PARTFUN1:def 2; then (FreeGen(X)).s in rng (FreeGen(X)) by FUNCT_1:def 3; hence thesis by A8,TARSKI:def 4; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func Reverse(s,X) -> Function of FreeGen(s,X),X.s means :Def17: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds it.(root-tree t) = t `1; existence proof set A = FreeGen(s,X), D = DTConMSA(X); defpred P[set,set] means for t be Symbol of D st $1 = root-tree t holds $2 = t`1; A1: for x be set st x in A ex a be set st a in X.s & P[x,a] proof let x be set; assume x in A; then x in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s } by Th13; then consider t be Symbol of D such that A2: x = root-tree t and A3: t in Terminals D and A4: t`2 = s; consider s1 be SortSymbol of S, a be set such that A5: a in X.s1 and A6: t = [a,s1] by A3,Th7; take a; thus a in X.s by A4,A5,A6,MCART_1:7; let t1 be Symbol of D; assume x = root-tree t1; then t = t1 by A2,TREES_4:4; hence thesis by A6,MCART_1:7; end; consider f be Function such that A7: dom f = A & rng f c= X.s & for x be set st x in A holds P[x,f.x] from FUNCT_1:sch 5(A1); reconsider f as Function of A,X.s by A7,FUNCT_2:2; take f; let t be Symbol of D; assume root-tree t in A; hence thesis by A7; end; uniqueness proof set D = DTConMSA(X), C = {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}; let A,B be Function of FreeGen(s,X),X.s; assume that A8: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds A.(root-tree t) = t`1 and A9: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds B.(root-tree t) = t`1; A10: FreeGen(s,X) = C by Th13; A11: for i be set st i in C holds A.i = B.i proof let i be set; assume A12: i in C; then consider t be Symbol of D such that A13: i = root-tree t and t in Terminals D and t`2 = s; A.(root-tree t) = t`1 by A8,A10,A12,A13; hence thesis by A9,A10,A12,A13; end; dom A = C & dom B = C by A10,FUNCT_2:def 1; hence thesis by A11,FUNCT_1:2; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func Reverse(X) -> ManySortedFunction of FreeGen(X),X means :Def18: for s be SortSymbol of S holds it.s = Reverse(s,X); existence proof defpred P[set,set] means for s be SortSymbol of S st s = $1 holds $2 = Reverse(s,X); set I = the carrier of S, FG = FreeGen(X); A1: for i be set st i in I ex u be set st P[i,u] proof let i be set; assume i in I; then reconsider s = i as SortSymbol of S; take Reverse(s,X); let s1 be SortSymbol of S; assume s1 = i; hence thesis; end; consider H be Function such that A2: dom H = I & for i be set st i in I holds P[i,H.i] from CLASSES1: sch 1 (A1); reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18; for x be set st x in dom H holds H.x is Function proof let i be set; assume i in dom H; then reconsider s = i as SortSymbol of S; H.s = Reverse(s,X) by A2; hence thesis; end; then reconsider H as ManySortedFunction of I by FUNCOP_1:def 6; for i be set st i in I holds H.i is Function of FG.i,X.i proof let i be set; assume i in I; then reconsider s = i as SortSymbol of S; (FreeGen X).s = FreeGen(s,X) & H.i = Reverse(s,X) by A2,Def16; hence thesis; end; then reconsider H as ManySortedFunction of FG,X by PBOOLE:def 15; take H; let s be SortSymbol of S; thus thesis by A2; end; uniqueness proof let A,B be ManySortedFunction of FreeGen(X),X; assume that A3: for s be SortSymbol of S holds A.s = Reverse(s,X) and A4: for s be SortSymbol of S holds B.s = Reverse(s,X); for i be set st i in the carrier of S holds A.i = B.i proof let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A.s = Reverse(s,X) by A3; hence thesis by A4; end; hence thesis by PBOOLE:3; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, A be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of FreeGen(X), A, t be Symbol of DTConMSA(X); assume A1: t in Terminals (DTConMSA(X)); func pi(F,A,t) -> Element of Union A means :Def19: for f be Function st f = F.(t`2) holds it = f.(root-tree t); existence proof set FG = FreeGen(X), D = DTConMSA(X); consider s be SortSymbol of S, x be set such that x in X.s and A2: t = [x,s] by A1,Th7; FG.s = FreeGen(s,X) by Def16; then A3: dom (F.s) = FreeGen(s,X) by FUNCT_2:def 1 .= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s } by Th13; t`2 = s by A2,MCART_1:7; then root-tree t in dom (F.s) by A1,A3; then A4: (F.s).(root-tree t) in rng (F.s) by FUNCT_1:def 3; dom A = the carrier of S by PARTFUN1:def 2; then rng (F.s) c= A.s & A.s in rng A by FUNCT_1:def 3,RELAT_1:def 19; then (F.s).(root-tree t) in union rng A by A4,TARSKI:def 4; then reconsider eu = (F.s).(root-tree t) as Element of Union A by CARD_3:def 4; take eu; let f be Function; assume f = F.(t`2); hence thesis by A2,MCART_1:7; end; uniqueness proof consider s be SortSymbol of S, x be set such that x in X.s and A5: t = [x,s] by A1,Th7; reconsider f = F.s as Function; let a,b be Element of Union A; assume that A6: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and A7: for f be Function st f = F.(t`2) holds b = f.(root-tree t); A8: f = F.(t`2) by A5,MCART_1:7; then a = f.(root-tree t) by A6; hence thesis by A7,A8; end; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, t be Symbol of DTConMSA(X); assume A1: ex p be FinSequence st t ==> p; func @(X,t) -> OperSymbol of S means :Def20: [it,the carrier of S] = t; existence proof set D = DTConMSA(X), OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)); reconsider a = t as Element of OU; consider p be FinSequence such that A2: t ==> p by A1; [t,p] in the Rules of D by A2,LANG1:def 1; then reconsider p as Element of OU* by ZFMISC_1:87; [a,p] in REL(X) by A2,LANG1:def 1; then a in [:the carrier' of S,{the carrier of S}:] by Def7; then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that A3: a = [o,x2] by DOMAIN_1:1; take o; thus thesis by A3,TARSKI:def 1; end; uniqueness by XTUPLE_0:1; end; definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S , o be OperSymbol of S, p be FinSequence; assume A1: p in Args(o,U0); func pi(o,U0,p) -> Element of Union (the Sorts of U0) equals :Def21: Den(o, U0).p; coherence proof set F = Den(o,U0), S0 = the Sorts of U0; dom F = Args(o,U0) by FUNCT_2:def 1; then rng F c= Result(o,U0) & F.p in rng F by A1,FUNCT_1:def 3 ,RELAT_1:def 19; then F.p in union rng S0 by TARSKI:def 4; hence thesis by CARD_3:def 4; end; end; theorem Th16: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeGen(X) is free proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; set D = DTConMSA(X), FA = FreeMSA(X), FG = FreeGen(X); let U1 be non-empty MSAlgebra over S, F be ManySortedFunction of FG,the Sorts of U1; set SA =the Sorts of FA, AR = the Arity of S, S1 = the Sorts of U1, O = the carrier' of S, RS = the ResultSort of S, DU = Union (the Sorts of U1); deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1); deffunc NTermVal(Symbol of D, FinSequence, FinSequence) = pi(@(X,$1),U1,$3); consider G being Function of TS(D), DU such that A1: for t being Symbol of D st t in Terminals D holds G.(root-tree t) = TermVal(t) and A2: for nt be Symbol of D, ts be FinSequence of TS(D) st nt ==> roots ts holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts) from DTCONSTR:sch 8; deffunc F(set) = G | ((the Sorts of FA).$1); consider h be Function such that A3: dom h = the carrier of S & for s be set st s in the carrier of S holds h.s = F(s) from FUNCT_1:sch 3; reconsider h as ManySortedSet of the carrier of S by A3,PARTFUN1:def 2 ,RELAT_1:def 18; for s be set st s in dom h holds h.s is Function proof let s be set; assume s in dom h; then h.s = G | ((the Sorts of FA).s) by A3; hence thesis; end; then reconsider h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6 ; defpred P[set] means for s be SortSymbol of S st $1 in (the Sorts of FA).s holds (h.s).$1 in (the Sorts of U1).s; A4: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t] holds P[nt-tree ts] proof let nt be Symbol of D, ts be FinSequence of TS(D); assume that A5: nt ==> roots ts and A6: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]; set p = G * ts, o = @(X,nt), ar = the_arity_of o, rs = the_result_sort_of o, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)), rt = roots ts; A7: [o,the carrier of S] = nt by A5,Def20; then A8: [[o,the carrier of S],rt] in the Rules of D by A5,LANG1:def 1; A9: [o,the carrier of S] = Sym(o,X); then A10: (DenOp(o,X)).ts = nt-tree ts by A5,A7,Def12; dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1; then ts in dom (DenOp(o,X)) by A5,A7,A9,Th10; then rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & nt-tree ts in rng (DenOp (o,X)) by A10,FUNCT_1:def 3,RELAT_1:def 19; then A11: nt-tree ts in (SA * RS).o; set ppi = pi(o,U1,p); A12: rng RS c= the carrier of S by RELAT_1:def 19; A13: rng ar c= the carrier of S by FINSEQ_1:def 4; reconsider rt as Element of OU* by A8,ZFMISC_1:87; A14: len rt = len ar by A8,Th5; A15: dom rt = Seg len rt by FINSEQ_1:def 3; dom SA = the carrier of S by PARTFUN1:def 2; then A16: dom(SA* ar) = dom ar by A13,RELAT_1:27; A17: ar = AR.o by MSUALG_1:def 1; dom S1 = the carrier of S by PARTFUN1:def 2; then A18: dom(S1* ar) = dom ar by A13,RELAT_1:27; A19: dom rt = dom ts & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18; A20: dom p = dom ts by FINSEQ_3:120; then A21: dom p = dom (S1 * ar) by A18,A8,A15,A19,Th5; A22: for x st x in dom (S1 * ar) holds p.x in (S1 * ar).x proof let x; assume A23: x in dom (S1 * ar); then reconsider n = x as Nat; A24: ts.n in rng ts by A18,A14,A15,A19,A23,FUNCT_1:def 3; rng ts c= TS D by FINSEQ_1:def 4; then reconsider t = ts.n as Element of TS(D) by A24; A25: p.n = G.(ts.n) by A21,A23,FINSEQ_3:120; ar.x in rng ar by A18,A23,FUNCT_1:def 3; then reconsider s = ar.x as SortSymbol of S by A13; A26: h.s = G | (SA.s) by A3; dom SA = the carrier of S by PARTFUN1:def 2; then A27: SA.s in rng SA by FUNCT_1:def 3; dom G = TS D by FUNCT_2:def 1 .= union rng SA by Th11; then A28: dom (h.s) = SA.s by A26,A27,RELAT_1:62,ZFMISC_1:74; ts in ((FreeSort X)# * AR).o by A5,A7,A9,Th10; then ts in product ((FreeSort X) * ar) by A17,Th1; then ts.x in ((FreeSort X) * ar).x by A18,A16,A23,CARD_3:9; then A29: ts.x in (FreeSort X).(ar.x) by A18,A16,A23,FUNCT_1:12; then (h.s).t in S1.s by A6,A24; then G.t in S1.s by A29,A26,A28,FUNCT_1:47; hence thesis by A23,A25,FUNCT_1:12; end; dom S1 = the carrier of S by PARTFUN1:def 2; then A30: dom (S1 *RS) = dom RS by A12,RELAT_1:27; let s be SortSymbol of S; A31: dom Den(o,U1) = Args(o,U1) by FUNCT_2:def 1; A32: dom RS = O by FUNCT_2:def 1; dom SA = the carrier of S by PARTFUN1:def 2; then dom (SA * RS) = dom RS by A12,RELAT_1:27; then nt-tree ts in SA.(RS.o) by A32,A11,FUNCT_1:12; then A33: nt-tree ts in SA.rs by MSUALG_1:def 2; Args(o,U1) = (S1# * AR).o by MSUALG_1:def 4 .= product (S1 * ar) by A17,Th1; then A34: p in Args(o,U1) by A20,A18,A14,A15,A19,A22,CARD_3:9; then pi(o,U1,p) = Den(o,U1).p by Def21; then rng Den(o,U1) c= Result(o,U1) & ppi in rng Den(o,U1) by A34,A31, FUNCT_1:def 3,RELAT_1:def 19; then A35: ppi in Result(o,U1); assume A36: nt-tree ts in SA.s; A37: now assume A38: rs <> s; (FreeSort X).rs meets (FreeSort X).s by A33,A36,XBOOLE_0:3; hence contradiction by A38,Th12; end; G.(nt-tree ts) = ppi by A2,A5; then A39: ppi = (G | (SA.rs)).(nt-tree ts) by A33,FUNCT_1:49; Result(o,U1) = (S1 *RS).o by MSUALG_1:def 5 .= S1.(RS.o) by A30,A32,FUNCT_1:12 .= S1.rs by MSUALG_1:def 2; hence thesis by A3,A35,A39,A37; end; A40: for t being Symbol of D st t in Terminals D holds P[root-tree t] proof let t be Symbol of D; assume A41: t in Terminals D; then consider s be SortSymbol of S, x be set such that x in X.s and A42: t = [x,s] by Th7; set E = {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s}, a = root-tree t; A43: t`2 = s by A42,MCART_1:7; then A44: a in E by A41; let s1 be SortSymbol of S; reconsider f = F.s as Function of FG.s,S1.s; A45: dom f = FG.s by FUNCT_2:def 1; A46: E = FreeGen(s,X) by Th13; then FG.s = E by Def16; then A47: rng f c= S1.s & f.a in rng f by A44,A45,FUNCT_1:def 3,RELAT_1:def 19; assume A48: a in SA.s1; A49: now a in (FreeSort X).s /\ (FreeSort X).s1 by A44,A46,A48,XBOOLE_0:def 4; then A50: (FreeSort X).s meets (FreeSort X).s1 by XBOOLE_0:4; assume s <> s1; hence contradiction by A50,Th12; end; h.s = G | (SA.s) by A3; then (h.s).a = G.a by A44,A46,FUNCT_1:49 .= pi(F,S1,t) by A1,A41 .= f.a by A41,A43,Def19; hence thesis by A47,A49; end; A51: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t] from DTCONSTR:sch 7(A40,A4); for s be set st s in the carrier of S holds h.s is Function of (the Sorts of FA).s, (the Sorts of U1).s proof let x be set; assume x in the carrier of S; then reconsider s = x as SortSymbol of S; A52: dom G = TS D by FUNCT_2:def 1 .= union rng SA by Th11; dom SA = the carrier of S by PARTFUN1:def 2; then A53: SA.s in rng SA by FUNCT_1:def 3; A54: h.s = G | (SA.s) by A3; then A55: dom (h.s) = SA.s by A52,A53,RELAT_1:62,ZFMISC_1:74; A56: SA.s c= dom G by A52,A53,ZFMISC_1:74; rng (h.s) c= S1.s proof let a be set; assume a in rng (h.s); then consider T be set such that A57: T in dom (h.s) and A58: (h.s).T = a by FUNCT_1:def 3; reconsider T as Element of TS(D) by A56,A55,A57,FUNCT_2:def 1; T in SA.s by A54,A52,A53,A57,RELAT_1:62,ZFMISC_1:74; hence thesis by A51,A58; end; hence thesis by A55,FUNCT_2:def 1,RELSET_1:4; end; then reconsider h as ManySortedFunction of FA,U1 by PBOOLE:def 15; take h; thus h is_homomorphism FA,U1 proof rng RS c= the carrier of S & dom SA = the carrier of S by PARTFUN1:def 2 ,RELAT_1:def 19; then A59: dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:27; let o be OperSymbol of S such that Args(o,FA) <> {}; let x be Element of Args(o,FA); set rs = the_result_sort_of o, DA = Den(o,FA), D1 = Den(o,U1), OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)), ar = the_arity_of o; A60: ar = AR.o by MSUALG_1:def 1; A61: Args(o,FA) = ((FreeSort X)# * AR).o by MSUALG_1:def 4; then reconsider p = x as FinSequence of TS(D) by Th8; A62: Sym(o,X) ==> roots p by A61,Th10; then A63: @(X,Sym(o,X)) = o by Def20; A64: dom (G *p) = dom p by FINSEQ_3:120; A65: x in ((FreeSort X)# * AR).o by A61; A66: for a be set st a in dom p holds (G*p).a = (h#x).a proof rng ar c= the carrier of S & dom SA = the carrier of S by FINSEQ_1:def 4 ,PARTFUN1:def 2; then A67: dom(SA* ar) = dom ar by RELAT_1:27; set rt = roots p; let a be set; assume A68: a in dom p; then reconsider n = a as Nat; A69: [[o,the carrier of S],rt] in the Rules of D by A62,LANG1:def 1; then reconsider rt as Element of OU* by ZFMISC_1:87; A70: len rt = len ar by A69,Th5; A71: (G*p).n = G.(x.n) & (h#x).n = (h.(ar/.n)).(x.n) by A64,A68,FINSEQ_3:120 ,MSUALG_3:def 6; A72: h.(ar/.n) = G | (SA.(ar/.n)) by A3; A73: Seg len rt = dom rt by FINSEQ_1:def 3; A74: dom rt = dom p & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18; p in product((FreeSort X) * ar) by A65,A60,Th1; then A75: p.n in ((FreeSort X) * ar).n by A68,A67,A70,A73,A74,CARD_3:9; ((FreeSort X) * ar).n = SA.(ar.n) by A68,A67,A70,A73,A74,FUNCT_1:12 .= SA.(ar/.n) by A68,A70,A73,A74,PARTFUN1:def 6; hence thesis by A71,A72,A75,FUNCT_1:49; end; dom (h#x) = dom ar by MSUALG_3:6; then A76: G*p = h#x by A64,A66,FUNCT_1:2,MSUALG_3:6; A77: h.rs = G | (SA.rs) by A3; A78: dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1; (DenOp(o,X)).p = (Sym(o,X))-tree p by A62,Def12; then rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & (Sym(o,X))-tree p in rng (DenOp (o,X)) by A61,A78,FUNCT_1:def 3,RELAT_1:def 19; then (Sym(o,X))-tree p in (SA * RS).o; then (Sym(o,X))-tree p in SA.(RS.o) by A59,FUNCT_1:12; then A79: (Sym(o,X))-tree p in SA.rs by MSUALG_1:def 2; dom SA = the carrier of S by PARTFUN1:def 2; then A80: SA.rs in rng SA by FUNCT_1:def 3; dom G = TS D by FUNCT_2:def 1 .= union rng SA by Th11; then A81: dom (h.rs) = SA.rs by A77,A80,RELAT_1:62,ZFMISC_1:74; DA = (FreeOper(X)).o by MSUALG_1:def 6 .= DenOp(o,X) by Def13; then DA.x = (Sym(o,X))-tree p by A62,Def12; hence (h.rs).(DA.x) = G.((Sym(o,X))-tree p) by A79,A77,A81,FUNCT_1:47 .= pi(@(X,Sym(o,X)),U1,G*p) by A2,A62 .= D1.(h#x) by A63,A76,Def21; end; for x st x in the carrier of S holds (h || FG).x = F.x proof set hf = h || FG; let x; assume x in the carrier of S; then reconsider s = x as SortSymbol of S; A82: dom (h.s) = SA.s by FUNCT_2:def 1; A83: dom (hf.s) = FG.s by FUNCT_2:def 1; A84: FG.s = FreeGen(s,X) by Def16; A85: hf.s = (h.s) | (FG.s) by Def1; A86: for a be set st a in FG.s holds (hf.s).a = (F.s).a proof let a be set; A87: h.s = G | (SA.s) by A3; assume A88: a in FG.s; then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s } by A84,Th13; then consider t be Symbol of D such that A89: a = root-tree t & t in Terminals D and A90: t`2 = s; thus (hf.s).a = (h.s).a by A85,A83,A88,FUNCT_1:47 .= G.a by A82,A84,A88,A87,FUNCT_1:47 .= pi(F,S1,t) by A1,A89 .= (F.s).a by A89,A90,Def19; end; dom (F.s) = FG.s by FUNCT_2:def 1; hence thesis by A83,A86,FUNCT_1:2; end; hence thesis by PBOOLE:3; end; theorem Th17: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeMSA(X) is free proof let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; take FreeGen(X); thus thesis by Th16; end; registration let S be non void non empty ManySortedSign; cluster free strict for non-empty MSAlgebra over S; existence proof set U1 = the non-empty MSAlgebra over S; set X = the Sorts of U1; take FreeMSA(X); thus thesis by Th17; end; end; registration let S be non void non empty ManySortedSign, U0 be free MSAlgebra over S; cluster free for GeneratorSet of U0; existence by Def6; end; theorem Th18: for S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 proof let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S; set S1 = the Sorts of U1, FA = FreeMSA(S1), FG = FreeGen(S1); reconsider fa = FA as strict free non-empty MSAlgebra over S by Th17; set f = Reverse(S1); take fa; FG is free by Th16; then consider F be ManySortedFunction of FA,U1 such that A1: F is_homomorphism FA,U1 and A2: F || FG = f by Def5; reconsider a = F as ManySortedFunction of fa,U1; take a; thus a is_homomorphism fa,U1 by A1; thus a is "onto" proof let s be set; assume s in the carrier of S; then reconsider s0 = s as SortSymbol of S; reconsider g = a.s as Function of (the Sorts of fa).s0, S1.s0 by PBOOLE:def 15; A3: f.s0 = g | (FG.s0) by A2,Def1; then A4: rng (f.s0) c= rng g by RELAT_1:70; thus rng (a.s) c= S1.s by A3,RELAT_1:def 19; let x be set; set D = DTConMSA(S1), t = [x,s0]; assume x in S1.s; then A5: t in Terminals D by Th7; then reconsider t as Symbol of D; t`2 = s0 by MCART_1:7; then root-tree t in {root-tree tt where tt is Symbol of D : tt in Terminals D & tt`2 = s0} by A5; then A6: root-tree t in FreeGen(s0,S1) by Th13; A7: f.s0 = Reverse(s0,S1) by Def18; then dom (f.s0) = FreeGen(s0,S1) by FUNCT_2:def 1; then A8: (f.s0).(root-tree t) in rng (f.s0) by A6,FUNCT_1:def 3; (f.s0).(root-tree t) = t`1 by A7,A6,Def17 .= x by MCART_1:7; hence thesis by A4,A8; end; end; theorem for S be non void non empty ManySortedSign, U1 be strict non-empty MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 & Image F = U1 proof let S be non void non empty ManySortedSign, U1 be strict non-empty MSAlgebra over S; consider U0 be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0,U1 such that A1: F is_epimorphism U0,U1 by Th18; F is_homomorphism U0,U1 by A1,MSUALG_3:def 8; then Image F = U1 by A1,MSUALG_3:19; hence thesis by A1; end;