:: FREEALG semantic presentation begin definition let IT be set ; attrIT is disjoint_with_NAT means :Def1: :: FREEALG:def 1 IT misses NAT ; end; :: deftheorem Def1 defines disjoint_with_NAT FREEALG:def_1_:_ for IT being set holds ( IT is disjoint_with_NAT iff IT misses NAT ); registration cluster non empty disjoint_with_NAT for set ; existence ex b1 being set st ( not b1 is empty & b1 is disjoint_with_NAT ) proof take X = {(- 1)}; ::_thesis: ( not X is empty & X is disjoint_with_NAT ) thus not X is empty ; ::_thesis: X is disjoint_with_NAT now__::_thesis:_not_X_meets_NAT assume X meets NAT ; ::_thesis: contradiction then consider x being set such that A1: x in X and A2: x in NAT by XBOOLE_0:3; reconsider x = x as Element of NAT by A2; x = - 1 by A1, TARSKI:def_1; hence contradiction by NAT_1:2; ::_thesis: verum end; hence X is disjoint_with_NAT by Def1; ::_thesis: verum end; end; Lm1: ( not 0 in rng <*1*> & 0 in rng <*0*> ) proof ( rng <*0*> = {0} & rng <*1*> = {1} ) by FINSEQ_1:38; hence ( not 0 in rng <*1*> & 0 in rng <*0*> ) by TARSKI:def_1; ::_thesis: verum end; notation let IT be Relation; antonym with_zero IT for non-empty ; synonym without_zero IT for non-empty ; end; definition let IT be Relation; redefine attr IT is non-empty means :Def2: :: FREEALG:def 2 not 0 in rng IT; compatibility ( not IT is with_zero iff not 0 in rng IT ) by RELAT_1:def_9; end; :: deftheorem Def2 defines with_zero FREEALG:def_2_:_ for IT being Relation holds ( not IT is with_zero iff not 0 in rng IT ); registration cluster non empty Relation-like with_zero NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st ( not b1 is empty & b1 is with_zero ) proof reconsider f = <*0*> as FinSequence of NAT ; take f ; ::_thesis: ( not f is empty & f is with_zero ) thus not f is empty ; ::_thesis: f is with_zero thus 0 in rng f by Lm1; :: according to FREEALG:def_2 ::_thesis: verum end; cluster non empty Relation-like without_zero NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st ( not b1 is empty & b1 is without_zero ) proof reconsider f = <*1*> as FinSequence of NAT ; take f ; ::_thesis: ( not f is empty & f is without_zero ) thus not f is empty ; ::_thesis: f is without_zero thus not 0 in rng f by Lm1; :: according to FREEALG:def_2 ::_thesis: verum end; end; begin definition let U1 be Universal_Algebra; let n be Element of NAT ; assume A1: n in dom the charact of U1 ; func oper (n,U1) -> operation of U1 equals :Def3: :: FREEALG:def 3 the charact of U1 . n; coherence the charact of U1 . n is operation of U1 by A1, FUNCT_1:def_3; end; :: deftheorem Def3 defines oper FREEALG:def_3_:_ for U1 being Universal_Algebra for n being Element of NAT st n in dom the charact of U1 holds oper (n,U1) = the charact of U1 . n; definition let U0 be Universal_Algebra; mode GeneratorSet of U0 -> Subset of U0 means :: FREEALG:def 4 for A being Subset of U0 st A is opers_closed & it c= A holds A = the carrier of U0; existence ex b1 being Subset of U0 st for A being Subset of U0 st A is opers_closed & b1 c= A holds A = the carrier of U0 proof the carrier of U0 c= the carrier of U0 ; then reconsider GG = the carrier of U0 as non empty Subset of U0 ; take GG ; ::_thesis: for A being Subset of U0 st A is opers_closed & GG c= A holds A = the carrier of U0 thus for A being Subset of U0 st A is opers_closed & GG c= A holds A = the carrier of U0 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines GeneratorSet FREEALG:def_4_:_ for U0 being Universal_Algebra for b2 being Subset of U0 holds ( b2 is GeneratorSet of U0 iff for A being Subset of U0 st A is opers_closed & b2 c= A holds A = the carrier of U0 ); Lm2: for A being Universal_Algebra for B being Subset of A st B is opers_closed holds Constants A c= B proof let A be Universal_Algebra; ::_thesis: for B being Subset of A st B is opers_closed holds Constants A c= B let B be Subset of A; ::_thesis: ( B is opers_closed implies Constants A c= B ) assume A1: B is opers_closed ; ::_thesis: Constants A c= B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants A or x in B ) assume x in Constants A ; ::_thesis: x in B then consider a being Element of A such that A2: x = a and A3: ex o being Element of Operations A st ( arity o = 0 & a in rng o ) ; consider o being Element of Operations A such that A4: arity o = 0 and A5: a in rng o by A3; A6: B is_closed_on o by A1, UNIALG_2:def_4; consider s being set such that A7: s in dom o and A8: a = o . s by A5, FUNCT_1:def_3; reconsider s = s as Element of the carrier of A * by A7; A9: dom o = 0 -tuples_on the carrier of A by A4, MARGREL1:22; then s = {} by A7; then rng s c= B by RELAT_1:38, XBOOLE_1:2; then A10: s is FinSequence of B by FINSEQ_1:def_4; len s = 0 by A7, A9; hence x in B by A2, A4, A8, A10, A6, UNIALG_2:def_3; ::_thesis: verum end; Lm3: for A being Universal_Algebra for B being Subset of A st ( B <> {} or Constants A <> {} ) holds ( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A ) proof let A be Universal_Algebra; ::_thesis: for B being Subset of A st ( B <> {} or Constants A <> {} ) holds ( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A ) let G be Subset of A; ::_thesis: ( ( G <> {} or Constants A <> {} ) implies ( G is GeneratorSet of A iff the carrier of (GenUnivAlg G) = the carrier of A ) ) assume A1: ( G <> {} or Constants A <> {} ) ; ::_thesis: ( G is GeneratorSet of A iff the carrier of (GenUnivAlg G) = the carrier of A ) thus ( G is GeneratorSet of A implies the carrier of (GenUnivAlg G) = the carrier of A ) ::_thesis: ( the carrier of (GenUnivAlg G) = the carrier of A implies G is GeneratorSet of A ) proof reconsider C = the carrier of (GenUnivAlg G) as non empty Subset of A by UNIALG_2:def_7; assume A2: for B being Subset of A st B is opers_closed & G c= B holds B = the carrier of A ; :: according to FREEALG:def_4 ::_thesis: the carrier of (GenUnivAlg G) = the carrier of A ( G c= C & C is opers_closed ) by A1, UNIALG_2:def_7, UNIALG_2:def_12; hence the carrier of (GenUnivAlg G) = the carrier of A by A2; ::_thesis: verum end; assume A3: the carrier of (GenUnivAlg G) = the carrier of A ; ::_thesis: G is GeneratorSet of A let B be Subset of A; :: according to FREEALG:def_4 ::_thesis: ( B is opers_closed & G c= B implies B = the carrier of A ) assume that A4: B is opers_closed and A5: G c= B ; ::_thesis: B = the carrier of A reconsider C = B as non empty Subset of A by A1, A4, A5, Lm2, XBOOLE_1:3; thus B c= the carrier of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of A c= B A6: UniAlgSetClosed C = UAStr(# C,(Opers (A,C)) #) by A4, UNIALG_2:def_8; then GenUnivAlg G is SubAlgebra of UniAlgSetClosed C by A1, A5, UNIALG_2:def_12; then the carrier of A is Subset of C by A3, A6, UNIALG_2:def_7; hence the carrier of A c= B ; ::_thesis: verum end; definition let U0 be Universal_Algebra; let IT be GeneratorSet of U0; attrIT is free means :Def5: :: FREEALG:def 5 for U1 being Universal_Algebra st U0,U1 are_similar holds for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st ( h is_homomorphism U0,U1 & h | IT = f ); end; :: deftheorem Def5 defines free FREEALG:def_5_:_ for U0 being Universal_Algebra for IT being GeneratorSet of U0 holds ( IT is free iff for U1 being Universal_Algebra st U0,U1 are_similar holds for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st ( h is_homomorphism U0,U1 & h | IT = f ) ); definition let IT be Universal_Algebra; attrIT is free means :Def6: :: FREEALG:def 6 ex G being GeneratorSet of IT st G is free ; end; :: deftheorem Def6 defines free FREEALG:def_6_:_ for IT being Universal_Algebra holds ( IT is free iff ex G being GeneratorSet of IT st G is free ); registration cluster non empty strict V109() quasi_total non-empty free for UAStr ; existence ex b1 being Universal_Algebra st ( b1 is free & b1 is strict ) proof set x = the set ; reconsider A = { the set } as non empty set ; set a = the Element of A; reconsider w = (<*> A) .--> the Element of A as Element of PFuncs ((A *),A) by MARGREL1:19; reconsider ww = <*w*> as PFuncFinSequence of A ; set U0 = UAStr(# A,ww #); A1: ( the charact of UAStr(# A,ww #) is quasi_total & the charact of UAStr(# A,ww #) is homogeneous ) by MARGREL1:20; A2: the charact of UAStr(# A,ww #) is non-empty by MARGREL1:20; A3: len the charact of UAStr(# A,ww #) = 1 by FINSEQ_1:39; reconsider U0 = UAStr(# A,ww #) as Universal_Algebra by A1, A2, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; A4: dom the charact of U0 = {1} by A3, FINSEQ_1:2, FINSEQ_1:def_3; 1 in {1} by TARSKI:def_1; then reconsider o0 = the charact of U0 . 1 as operation of U0 by A4, FUNCT_1:def_3; take U0 ; ::_thesis: ( U0 is free & U0 is strict ) A5: GenUnivAlg ({} the carrier of U0) = U0 proof set P = {} the carrier of U0; reconsider B = the carrier of (GenUnivAlg ({} the carrier of U0)) as non empty Subset of U0 by UNIALG_2:def_7; A6: dom the charact of U0 = dom (Opers (U0,B)) by UNIALG_2:def_6; A7: B = the carrier of U0 by ZFMISC_1:33; for n being Nat st n in dom the charact of U0 holds the charact of U0 . n = (Opers (U0,B)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of U0 implies the charact of U0 . n = (Opers (U0,B)) . n ) assume A8: n in dom the charact of U0 ; ::_thesis: the charact of U0 . n = (Opers (U0,B)) . n then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def_3; (Opers (U0,B)) . n = o /. B by A6, A8, UNIALG_2:def_6; hence the charact of U0 . n = (Opers (U0,B)) . n by A7, UNIALG_2:4; ::_thesis: verum end; then the charact of U0 = Opers (U0,B) by A6, FINSEQ_1:13 .= the charact of (GenUnivAlg ({} the carrier of U0)) by UNIALG_2:def_7 ; hence GenUnivAlg ({} the carrier of U0) = U0 by A7; ::_thesis: verum end; A9: o0 = w by FINSEQ_1:40; then A10: dom o0 = {(<*> A)} by FUNCOP_1:13; now__::_thesis:_(_ex_x_being_FinSequence_st_x_in_dom_o0_&_(_for_x_being_FinSequence_st_x_in_dom_o0_holds_ len_x_=_0_)_) <*> A in dom o0 by A10, TARSKI:def_1; hence ex x being FinSequence st x in dom o0 ; ::_thesis: for x being FinSequence st x in dom o0 holds len x = 0 let x be FinSequence; ::_thesis: ( x in dom o0 implies len x = 0 ) assume x in dom o0 ; ::_thesis: len x = 0 then x = <*> A by A10, TARSKI:def_1; hence len x = 0 ; ::_thesis: verum end; then A11: arity o0 = 0 by MARGREL1:def_25; A12: {} in {(<*> A)} by TARSKI:def_1; then o0 . (<*> A) = the Element of A by A9, FUNCOP_1:7; then the Element of A in rng o0 by A10, A12, FUNCT_1:def_3; then the Element of A in Constants U0 by A11; then reconsider G = {} the carrier of U0 as GeneratorSet of U0 by A5, Lm3; now__::_thesis:_ex_G_being_GeneratorSet_of_U0_st_G_is_free take G = G; ::_thesis: G is free now__::_thesis:_for_U1_being_Universal_Algebra_st_U0,U1_are_similar_holds_ for_f_being_Function_of_G,_the_carrier_of_U1_ex_h_being_Function_of_U0,U1_st_ (_h_is_homomorphism_U0,U1_&_h_|_G_=_f_) let U1 be Universal_Algebra; ::_thesis: ( U0,U1 are_similar implies for f being Function of G, the carrier of U1 ex h being Function of U0,U1 st ( h is_homomorphism U0,U1 & h | G = f ) ) A13: 1 in {1} by TARSKI:def_1; assume A14: U0,U1 are_similar ; ::_thesis: for f being Function of G, the carrier of U1 ex h being Function of U0,U1 st ( h is_homomorphism U0,U1 & h | G = f ) then A15: signature U0 = signature U1 by UNIALG_2:def_1; len the charact of U1 = 1 by A3, A14, UNIALG_2:1; then dom the charact of U1 = {1} by FINSEQ_1:2, FINSEQ_1:def_3; then reconsider o1 = the charact of U1 . 1 as operation of U1 by A13, FUNCT_1:def_3; A16: rng o1 c= the carrier of U1 by RELAT_1:def_19; let f be Function of G, the carrier of U1; ::_thesis: ex h being Function of U0,U1 st ( h is_homomorphism U0,U1 & h | G = f ) consider aa being set such that A17: aa in dom o1 by XBOOLE_0:def_1; o1 . aa in rng o1 by A17, FUNCT_1:def_3; then reconsider u1 = o1 . aa as Element of U1 by A16; reconsider h = the carrier of U0 --> u1 as Function of U0,U1 ; take h = h; ::_thesis: ( h is_homomorphism U0,U1 & h | G = f ) A18: ( len (signature U0) = len the charact of U0 & dom (signature U0) = Seg (len (signature U0)) ) by FINSEQ_1:def_3, UNIALG_1:def_4; then (signature U0) . 1 = arity o0 by A3, A13, FINSEQ_1:2, UNIALG_1:def_4; then A19: arity o0 = arity o1 by A3, A13, A15, A18, FINSEQ_1:2, UNIALG_1:def_4; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_the_charact_of_U0_holds_ for_0o_being_operation_of_U0 for_1o_being_operation_of_U1_st_0o_=_the_charact_of_U0_._n_&_1o_=_the_charact_of_U1_._n_holds_ for_y_being_FinSequence_of_U0_st_y_in_dom_0o_holds_ h_._(0o_._y)_=_1o_._(h_*_y) let n be Element of NAT ; ::_thesis: ( n in dom the charact of U0 implies for 0o being operation of U0 for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds for y being FinSequence of U0 st y in dom 0o holds h . (0o . y) = 1o . (h * y) ) assume n in dom the charact of U0 ; ::_thesis: for 0o being operation of U0 for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds for y being FinSequence of U0 st y in dom 0o holds h . (0o . y) = 1o . (h * y) then A20: n = 1 by A4, TARSKI:def_1; let 0o be operation of U0; ::_thesis: for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds for y being FinSequence of U0 st y in dom 0o holds h . (0o . y) = 1o . (h * y) let 1o be operation of U1; ::_thesis: ( 0o = the charact of U0 . n & 1o = the charact of U1 . n implies for y being FinSequence of U0 st y in dom 0o holds h . (0o . y) = 1o . (h * y) ) assume that A21: 0o = the charact of U0 . n and A22: 1o = the charact of U1 . n ; ::_thesis: for y being FinSequence of U0 st y in dom 0o holds h . (0o . y) = 1o . (h * y) let y be FinSequence of U0; ::_thesis: ( y in dom 0o implies h . (0o . y) = 1o . (h * y) ) assume A23: y in dom 0o ; ::_thesis: h . (0o . y) = 1o . (h * y) then y = <*> the carrier of U0 by A10, A20, A21, TARSKI:def_1; then A24: h * y = <*> the carrier of U1 ; dom 1o = 0 -tuples_on the carrier of U1 by A11, A19, A20, A22, MARGREL1:22 .= {(<*> the carrier of U1)} by FINSEQ_2:94 ; then A25: 1o . (h * y) = u1 by A17, A20, A22, A24, TARSKI:def_1; A26: rng 0o c= the carrier of U0 by RELAT_1:def_19; 0o . y in rng 0o by A23, FUNCT_1:def_3; hence h . (0o . y) = 1o . (h * y) by A25, A26, FUNCOP_1:7; ::_thesis: verum end; hence h is_homomorphism U0,U1 by A14, ALG_1:def_1; ::_thesis: h | G = f f = {} ; hence h | G = f ; ::_thesis: verum end; hence G is free by Def5; ::_thesis: verum end; hence ( U0 is free & U0 is strict ) by Def6; ::_thesis: verum end; end; registration let U0 be free Universal_Algebra; cluster free for GeneratorSet of U0; existence ex b1 being GeneratorSet of U0 st b1 is free by Def6; end; theorem :: FREEALG:1 for U0 being strict Universal_Algebra for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 ) proof let U0 be strict Universal_Algebra; ::_thesis: for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 ) let A be Subset of U0; ::_thesis: ( ( Constants U0 <> {} or A <> {} ) implies ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 ) ) assume A1: ( Constants U0 <> {} or A <> {} ) ; ::_thesis: ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 ) thus ( A is GeneratorSet of U0 implies GenUnivAlg A = U0 ) ::_thesis: ( GenUnivAlg A = U0 implies A is GeneratorSet of U0 ) proof assume A is GeneratorSet of U0 ; ::_thesis: GenUnivAlg A = U0 then A2: the carrier of (GenUnivAlg A) = the carrier of U0 by A1, Lm3; U0 is strict SubAlgebra of U0 by UNIALG_2:8; hence GenUnivAlg A = U0 by A2, UNIALG_2:12; ::_thesis: verum end; assume GenUnivAlg A = U0 ; ::_thesis: A is GeneratorSet of U0 hence A is GeneratorSet of U0 by A1, Lm3; ::_thesis: verum end; begin definition let f be non empty FinSequence of NAT ; let X be set ; func REL (f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X) *) means :Def7: :: FREEALG:def 7 for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in it iff ( a in dom f & f . a = len b ) ); existence ex b1 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in b1 iff ( a in dom f & f . a = len b ) ) proof set A = (dom f) \/ X; defpred S1[ Element of (dom f) \/ X, Element of ((dom f) \/ X) * ] means ( $1 in dom f & f . $1 = len $2 ); consider R being Relation of ((dom f) \/ X),(((dom f) \/ X) *) such that A1: for x being Element of (dom f) \/ X for y being Element of ((dom f) \/ X) * holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); take R ; ::_thesis: for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in R iff ( a in dom f & f . a = len b ) ) let a be Element of (dom f) \/ X; ::_thesis: for b being Element of ((dom f) \/ X) * holds ( [a,b] in R iff ( a in dom f & f . a = len b ) ) let b be Element of ((dom f) \/ X) * ; ::_thesis: ( [a,b] in R iff ( a in dom f & f . a = len b ) ) thus ( [a,b] in R iff ( a in dom f & f . a = len b ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st ( for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in b1 iff ( a in dom f & f . a = len b ) ) ) & ( for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in b2 iff ( a in dom f & f . a = len b ) ) ) holds b1 = b2 proof set A = (dom f) \/ X; let R, T be Relation of ((dom f) \/ X),(((dom f) \/ X) *); ::_thesis: ( ( for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in R iff ( a in dom f & f . a = len b ) ) ) & ( for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in T iff ( a in dom f & f . a = len b ) ) ) implies R = T ) assume that A2: for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in R iff ( a in dom f & f . a = len b ) ) and A3: for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in T iff ( a in dom f & f . a = len b ) ) ; ::_thesis: R = T for x, y being set holds ( [x,y] in R iff [x,y] in T ) proof let x, y be set ; ::_thesis: ( [x,y] in R iff [x,y] in T ) thus ( [x,y] in R implies [x,y] in T ) ::_thesis: ( [x,y] in T implies [x,y] in R ) proof assume A4: [x,y] in R ; ::_thesis: [x,y] in T then reconsider x1 = x as Element of (dom f) \/ X by ZFMISC_1:87; reconsider y1 = y as Element of ((dom f) \/ X) * by A4, ZFMISC_1:87; [x1,y1] in R by A4; then A5: x1 in dom f by A2; f . x1 = len y1 by A2, A4; hence [x,y] in T by A3, A5; ::_thesis: verum end; assume A6: [x,y] in T ; ::_thesis: [x,y] in R then reconsider x1 = x as Element of (dom f) \/ X by ZFMISC_1:87; reconsider y1 = y as Element of ((dom f) \/ X) * by A6, ZFMISC_1:87; [x1,y1] in T by A6; then A7: x1 in dom f by A3; f . x1 = len y1 by A3, A6; hence [x,y] in R by A2, A7; ::_thesis: verum end; hence R = T by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def7 defines REL FREEALG:def_7_:_ for f being non empty FinSequence of NAT for X being set for b3 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) holds ( b3 = REL (f,X) iff for a being Element of (dom f) \/ X for b being Element of ((dom f) \/ X) * holds ( [a,b] in b3 iff ( a in dom f & f . a = len b ) ) ); definition let f be non empty FinSequence of NAT ; let X be set ; func DTConUA (f,X) -> strict DTConstrStr equals :: FREEALG:def 8 DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #); correctness coherence DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #) is strict DTConstrStr ; ; end; :: deftheorem defines DTConUA FREEALG:def_8_:_ for f being non empty FinSequence of NAT for X being set holds DTConUA (f,X) = DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #); registration let f be non empty FinSequence of NAT ; let X be set ; cluster DTConUA (f,X) -> non empty strict ; coherence not DTConUA (f,X) is empty ; end; theorem Th2: :: FREEALG:2 for f being non empty FinSequence of NAT for X being set holds ( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f ) proof let f be non empty FinSequence of NAT ; ::_thesis: for X being set holds ( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f ) let X be set ; ::_thesis: ( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f ) set A = DTConUA (f,X); set D = (dom f) \/ X; A1: the carrier of (DTConUA (f,X)) = (Terminals (DTConUA (f,X))) \/ (NonTerminals (DTConUA (f,X))) by LANG1:1; Terminals (DTConUA (f,X)) misses NonTerminals (DTConUA (f,X)) by DTCONSTR:8; then A2: (Terminals (DTConUA (f,X))) /\ (NonTerminals (DTConUA (f,X))) = {} by XBOOLE_0:def_7; thus Terminals (DTConUA (f,X)) c= X ::_thesis: NonTerminals (DTConUA (f,X)) = dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Terminals (DTConUA (f,X)) or x in X ) assume A3: x in Terminals (DTConUA (f,X)) ; ::_thesis: x in X then reconsider xd = x as Element of (dom f) \/ X by A1, XBOOLE_0:def_3; reconsider xa = x as Element of the carrier of (DTConUA (f,X)) by A1, A3, XBOOLE_0:def_3; A4: now__::_thesis:_not_x_in_dom_f A5: rng f c= NAT by FINSEQ_1:def_4; assume A6: x in dom f ; ::_thesis: contradiction then f . x in rng f by FUNCT_1:def_3; then reconsider fx = f . x as Element of NAT by A5; reconsider a = fx |-> xd as FinSequence of (dom f) \/ X ; reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def_11; len a = f . xd by CARD_1:def_7; then [xd,a] in REL (f,X) by A6, Def7; then xa ==> a by LANG1:def_1; then xa in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } ; then x in NonTerminals (DTConUA (f,X)) by LANG1:def_3; hence contradiction by A2, A3, XBOOLE_0:def_4; ::_thesis: verum end; x in (dom f) \/ X by A1, A3, XBOOLE_0:def_3; hence x in X by A4, XBOOLE_0:def_3; ::_thesis: verum end; thus NonTerminals (DTConUA (f,X)) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= NonTerminals (DTConUA (f,X)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NonTerminals (DTConUA (f,X)) or x in dom f ) assume x in NonTerminals (DTConUA (f,X)) ; ::_thesis: x in dom f then x in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } by LANG1:def_3; then consider t being Symbol of (DTConUA (f,X)) such that A7: x = t and A8: ex n being FinSequence st t ==> n ; consider n being FinSequence such that A9: t ==> n by A8; [t,n] in the Rules of (DTConUA (f,X)) by A9, LANG1:def_1; then reconsider n = n as Element of ((dom f) \/ X) * by ZFMISC_1:87; reconsider t = t as Element of (dom f) \/ X ; [t,n] in REL (f,X) by A9, LANG1:def_1; hence x in dom f by A7, Def7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in NonTerminals (DTConUA (f,X)) ) A10: rng f c= NAT by FINSEQ_1:def_4; assume A11: x in dom f ; ::_thesis: x in NonTerminals (DTConUA (f,X)) then reconsider xa = x as Symbol of (DTConUA (f,X)) by XBOOLE_0:def_3; f . x in rng f by A11, FUNCT_1:def_3; then reconsider fx = f . x as Element of NAT by A10; reconsider xd = x as Element of (dom f) \/ X by A11, XBOOLE_0:def_3; reconsider a = fx |-> xd as FinSequence of (dom f) \/ X ; reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def_11; len a = f . xd by CARD_1:def_7; then [xd,a] in REL (f,X) by A11, Def7; then xa ==> a by LANG1:def_1; then xa in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } ; hence x in NonTerminals (DTConUA (f,X)) by LANG1:def_3; ::_thesis: verum end; theorem Th3: :: FREEALG:3 for f being non empty FinSequence of NAT for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X proof let f be non empty FinSequence of NAT ; ::_thesis: for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X let X be disjoint_with_NAT set ; ::_thesis: Terminals (DTConUA (f,X)) = X set A = DTConUA (f,X); thus Terminals (DTConUA (f,X)) c= X by Th2; :: according to XBOOLE_0:def_10 ::_thesis: X c= Terminals (DTConUA (f,X)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Terminals (DTConUA (f,X)) ) assume A1: x in X ; ::_thesis: x in Terminals (DTConUA (f,X)) A2: NonTerminals (DTConUA (f,X)) = dom f by Th2; A3: now__::_thesis:_not_x_in_NonTerminals_(DTConUA_(f,X)) assume x in NonTerminals (DTConUA (f,X)) ; ::_thesis: contradiction then X meets NAT by A2, A1, XBOOLE_0:3; hence contradiction by Def1; ::_thesis: verum end; ( the carrier of (DTConUA (f,X)) = (Terminals (DTConUA (f,X))) \/ (NonTerminals (DTConUA (f,X))) & x in (dom f) \/ X ) by A1, LANG1:1, XBOOLE_0:def_3; hence x in Terminals (DTConUA (f,X)) by A3, XBOOLE_0:def_3; ::_thesis: verum end; registration let f be non empty FinSequence of NAT ; let X be set ; cluster DTConUA (f,X) -> strict with_nonterminals ; coherence DTConUA (f,X) is with_nonterminals proof NonTerminals (DTConUA (f,X)) = dom f by Th2; hence DTConUA (f,X) is with_nonterminals by DTCONSTR:def_4; ::_thesis: verum end; end; registration let f be non empty with_zero FinSequence of NAT ; let X be set ; cluster DTConUA (f,X) -> strict with_nonterminals with_useful_nonterminals ; coherence ( DTConUA (f,X) is with_nonterminals & DTConUA (f,X) is with_useful_nonterminals ) proof set A = DTConUA (f,X); set D = (dom f) \/ X; DTConUA (f,X) is with_useful_nonterminals proof set e = <*> (TS (DTConUA (f,X))); let s be Symbol of (DTConUA (f,X)); :: according to DTCONSTR:def_5 ::_thesis: ( not s in NonTerminals (DTConUA (f,X)) or ex b1 being FinSequence of TS (DTConUA (f,X)) st s ==> roots b1 ) assume A1: s in NonTerminals (DTConUA (f,X)) ; ::_thesis: ex b1 being FinSequence of TS (DTConUA (f,X)) st s ==> roots b1 A2: rng f c= NAT by FINSEQ_1:def_4; NonTerminals (DTConUA (f,X)) = dom f by Th2; then f . s in rng f by A1, FUNCT_1:def_3; then reconsider fs = f . s as Element of NAT by A2; reconsider sd = s as Element of (dom f) \/ X ; roots (<*> (TS (DTConUA (f,X)))) = <*> ((dom f) \/ X) by DTCONSTR:3; then reconsider re = roots (<*> (TS (DTConUA (f,X)))) as Element of ((dom f) \/ X) * ; 0 in rng f by Def2; then consider x being set such that A3: x in dom f and A4: f . x = 0 by FUNCT_1:def_3; A5: NonTerminals (DTConUA (f,X)) = dom f by Th2; then reconsider s0 = x as Symbol of (DTConUA (f,X)) by A3; set p = fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))); A6: len (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) = fs by CARD_1:def_7; len re = 0 by DTCONSTR:3; then [s0,(roots (<*> (TS (DTConUA (f,X)))))] in the Rules of (DTConUA (f,X)) by A3, A4, Def7; then s0 ==> roots (<*> (TS (DTConUA (f,X)))) by LANG1:def_1; then A7: s0 -tree (<*> (TS (DTConUA (f,X)))) in TS (DTConUA (f,X)) by DTCONSTR:def_1; A8: rng (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) c= TS (DTConUA (f,X)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) or y in TS (DTConUA (f,X)) ) assume y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) ; ::_thesis: y in TS (DTConUA (f,X)) then A9: ex n being Nat st ( n in dom (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) & (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) . n = y ) by FINSEQ_2:10; dom (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) = Seg (len (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))))) by FINSEQ_1:def_3; hence y in TS (DTConUA (f,X)) by A7, A6, A9, FUNCOP_1:7; ::_thesis: verum end; dom (roots (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))))) = dom (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) by TREES_3:def_18 .= Seg (len (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))))) by FINSEQ_1:def_3 ; then A10: len (roots (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))))) = fs by A6, FINSEQ_1:def_3; reconsider p = fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))) as FinSequence of TS (DTConUA (f,X)) by A8, FINSEQ_1:def_4; take p ; ::_thesis: s ==> roots p reconsider p = p as FinSequence of FinTrees the carrier of (DTConUA (f,X)) ; reconsider rp = roots p as Element of ((dom f) \/ X) * by FINSEQ_1:def_11; [sd,rp] in REL (f,X) by A1, A5, A10, Def7; hence s ==> roots p by LANG1:def_1; ::_thesis: verum end; hence ( DTConUA (f,X) is with_nonterminals & DTConUA (f,X) is with_useful_nonterminals ) ; ::_thesis: verum end; end; registration let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; cluster DTConUA (f,D) -> strict with_terminals with_nonterminals with_useful_nonterminals ; coherence ( DTConUA (f,D) is with_terminals & DTConUA (f,D) is with_nonterminals & DTConUA (f,D) is with_useful_nonterminals ) proof set A = DTConUA (f,D); A1: NonTerminals (DTConUA (f,D)) = dom f by Th2; A2: Terminals (DTConUA (f,D)) = D by Th3; DTConUA (f,D) is with_useful_nonterminals proof set d = the Element of D; let s be Symbol of (DTConUA (f,D)); :: according to DTCONSTR:def_5 ::_thesis: ( not s in NonTerminals (DTConUA (f,D)) or ex b1 being FinSequence of TS (DTConUA (f,D)) st s ==> roots b1 ) reconsider sd = the Element of D as Symbol of (DTConUA (f,D)) by XBOOLE_0:def_3; A3: rng f c= NAT by FINSEQ_1:def_4; assume A4: s in NonTerminals (DTConUA (f,D)) ; ::_thesis: ex b1 being FinSequence of TS (DTConUA (f,D)) st s ==> roots b1 then f . s in rng f by A1, FUNCT_1:def_3; then reconsider fs = f . s as Element of NAT by A3; reconsider sdd = s as Element of (dom f) \/ D ; set p = fs |-> (root-tree sd); A5: len (fs |-> (root-tree sd)) = fs by CARD_1:def_7; A6: root-tree sd in TS (DTConUA (f,D)) by A2, DTCONSTR:def_1; A7: rng (fs |-> (root-tree sd)) c= TS (DTConUA (f,D)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (fs |-> (root-tree sd)) or y in TS (DTConUA (f,D)) ) assume y in rng (fs |-> (root-tree sd)) ; ::_thesis: y in TS (DTConUA (f,D)) then consider n being Nat such that A8: n in dom (fs |-> (root-tree sd)) and A9: (fs |-> (root-tree sd)) . n = y by FINSEQ_2:10; n in Seg (len (fs |-> (root-tree sd))) by A8, FINSEQ_1:def_3; hence y in TS (DTConUA (f,D)) by A6, A5, A9, FUNCOP_1:7; ::_thesis: verum end; dom (roots (fs |-> (root-tree sd))) = dom (fs |-> (root-tree sd)) by TREES_3:def_18 .= Seg (len (fs |-> (root-tree sd))) by FINSEQ_1:def_3 ; then A10: len (roots (fs |-> (root-tree sd))) = fs by A5, FINSEQ_1:def_3; reconsider p = fs |-> (root-tree sd) as FinSequence of TS (DTConUA (f,D)) by A7, FINSEQ_1:def_4; take p ; ::_thesis: s ==> roots p reconsider p = p as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ; reconsider rp = roots p as Element of ((dom f) \/ D) * by FINSEQ_1:def_11; [sdd,rp] in REL (f,D) by A1, A4, A10, Def7; hence s ==> roots p by LANG1:def_1; ::_thesis: verum end; hence ( DTConUA (f,D) is with_terminals & DTConUA (f,D) is with_nonterminals & DTConUA (f,D) is with_useful_nonterminals ) by A2, DTCONSTR:def_3; ::_thesis: verum end; end; definition let f be non empty FinSequence of NAT ; let X be set ; let n be Nat; assume A1: n in dom f ; func Sym (n,f,X) -> Symbol of (DTConUA (f,X)) equals :Def9: :: FREEALG:def 9 n; coherence n is Symbol of (DTConUA (f,X)) by A1, XBOOLE_0:def_3; end; :: deftheorem Def9 defines Sym FREEALG:def_9_:_ for f being non empty FinSequence of NAT for X being set for n being Nat st n in dom f holds Sym (n,f,X) = n; begin definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; let n be Nat; assume A1: n in dom f ; func FreeOpNSG (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def10: :: FREEALG:def 10 ( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds it . p = (Sym (n,f,D)) -tree p ) ); existence ex b1 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st ( dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds b1 . p = (Sym (n,f,D)) -tree p ) ) proof set A = DTConUA (f,D); set i = f /. n; set Y = (dom f) \/ D; set smm = Sym (n,f,D); defpred S1[ set , set ] means ( $1 in (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p = $1 holds $2 = (Sym (n,f,D)) -tree p ) ); set tu = { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } ; A2: f /. n = f . n by A1, PARTFUN1:def_6; A3: for x, y being set st x in (TS (DTConUA (f,D))) * & S1[x,y] holds y in TS (DTConUA (f,D)) proof reconsider sm = Sym (n,f,D) as Element of (dom f) \/ D ; let x, y be set ; ::_thesis: ( x in (TS (DTConUA (f,D))) * & S1[x,y] implies y in TS (DTConUA (f,D)) ) assume that x in (TS (DTConUA (f,D))) * and A4: S1[x,y] ; ::_thesis: y in TS (DTConUA (f,D)) consider s being Element of (TS (DTConUA (f,D))) * such that A5: s = x and A6: len s = f /. n by A4; A7: y = (Sym (n,f,D)) -tree s by A4, A5; reconsider s = s as FinSequence of TS (DTConUA (f,D)) ; ( dom (roots s) = dom s & Seg (len (roots s)) = dom (roots s) ) by FINSEQ_1:def_3, TREES_3:def_18; then A8: len (roots s) = f /. n by A6, FINSEQ_1:def_3; reconsider s = s as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ; reconsider rs = roots s as Element of ((dom f) \/ D) * by FINSEQ_1:def_11; sm = n by A1, Def9; then [sm,rs] in REL (f,D) by A1, A2, A8, Def7; then Sym (n,f,D) ==> roots s by LANG1:def_1; hence y in TS (DTConUA (f,D)) by A7, DTCONSTR:def_1; ::_thesis: verum end; A9: for x, y1, y2 being set st x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that x in (TS (DTConUA (f,D))) * and A10: S1[x,y1] and A11: S1[x,y2] ; ::_thesis: y1 = y2 consider s being Element of (TS (DTConUA (f,D))) * such that A12: s = x and len s = f /. n by A10; y1 = (Sym (n,f,D)) -tree s by A10, A12; hence y1 = y2 by A11, A12; ::_thesis: verum end; consider F being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) such that A13: for x being set holds ( x in dom F iff ( x in (TS (DTConUA (f,D))) * & ex y being set st S1[x,y] ) ) and A14: for x being set st x in dom F holds S1[x,F . x] from PARTFUN1:sch_2(A3, A9); A15: dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) proof thus dom F c= (f /. n) -tuples_on (TS (DTConUA (f,D))) :: according to XBOOLE_0:def_10 ::_thesis: (f /. n) -tuples_on (TS (DTConUA (f,D))) c= dom F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ) assume x in dom F ; ::_thesis: x in (f /. n) -tuples_on (TS (DTConUA (f,D))) then ex y being set st S1[x,y] by A13; hence x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: verum end; reconsider sm = Sym (n,f,D) as Symbol of (DTConUA (f,D)) ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f /. n) -tuples_on (TS (DTConUA (f,D))) or x in dom F ) assume x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: x in dom F then consider s being Element of (TS (DTConUA (f,D))) * such that A16: s = x and A17: len s = f /. n ; S1[s,sm -tree s] by A17; hence x in dom F by A13, A16; ::_thesis: verum end; A18: for x, y being FinSequence of TS (DTConUA (f,D)) st len x = len y & x in dom F holds y in dom F proof let x, y be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( len x = len y & x in dom F implies y in dom F ) assume that A19: len x = len y and A20: x in dom F ; ::_thesis: y in dom F reconsider sy = y as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; ex sx being Element of (TS (DTConUA (f,D))) * st ( sx = x & len sx = f /. n ) by A15, A20; then sy in { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } by A19; hence y in dom F by A15; ::_thesis: verum end; A21: ex x being FinSequence st x in dom F proof set a = the Element of (f /. n) -tuples_on (TS (DTConUA (f,D))); the Element of (f /. n) -tuples_on (TS (DTConUA (f,D))) in dom F by A15; hence ex x being FinSequence st x in dom F ; ::_thesis: verum end; dom F is with_common_domain proof let x, y be FinSequence; :: according to MARGREL1:def_1 ::_thesis: ( not x in dom F or not y in dom F or len x = len y ) assume ( x in dom F & y in dom F ) ; ::_thesis: len x = len y then ( ex sx being Element of (TS (DTConUA (f,D))) * st ( sx = x & len sx = f /. n ) & ex sy being Element of (TS (DTConUA (f,D))) * st ( sy = y & len sy = f /. n ) ) by A15; hence len x = len y ; ::_thesis: verum end; then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) by A18, A21, MARGREL1:def_21, MARGREL1:def_22; take F ; ::_thesis: ( dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds F . p = (Sym (n,f,D)) -tree p ) ) thus dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) by A15; ::_thesis: for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds F . p = (Sym (n,f,D)) -tree p let p be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( p in dom F implies F . p = (Sym (n,f,D)) -tree p ) assume p in dom F ; ::_thesis: F . p = (Sym (n,f,D)) -tree p hence F . p = (Sym (n,f,D)) -tree p by A14; ::_thesis: verum end; uniqueness for b1, b2 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds b1 . p = (Sym (n,f,D)) -tree p ) & dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b2 holds b2 . p = (Sym (n,f,D)) -tree p ) holds b1 = b2 proof set A = TS (DTConUA (f,D)); let f1, f2 be non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds f1 . p = (Sym (n,f,D)) -tree p ) & dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds f2 . p = (Sym (n,f,D)) -tree p ) implies f1 = f2 ) assume that A22: dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and A23: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds f1 . p = (Sym (n,f,D)) -tree p and A24: dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and A25: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds f2 . p = (Sym (n,f,D)) -tree p ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_(f_/._n)_-tuples_on_(TS_(DTConUA_(f,D)))_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in (f /. n) -tuples_on (TS (DTConUA (f,D))) implies f1 . x = f2 . x ) assume A26: x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: f1 . x = f2 . x then consider s being Element of (TS (DTConUA (f,D))) * such that A27: s = x and len s = f /. n ; f1 . s = (Sym (n,f,D)) -tree s by A22, A23, A26, A27; hence f1 . x = f2 . x by A24, A25, A26, A27; ::_thesis: verum end; hence f1 = f2 by A22, A24, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def10 defines FreeOpNSG FREEALG:def_10_:_ for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set for n being Nat st n in dom f holds for b4 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds ( b4 = FreeOpNSG (n,f,D) iff ( dom b4 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b4 holds b4 . p = (Sym (n,f,D)) -tree p ) ) ); definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; func FreeOpSeqNSG (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def11: :: FREEALG:def 11 ( len it = len f & ( for n being Element of NAT st n in dom it holds it . n = FreeOpNSG (n,f,D) ) ); existence ex b1 being PFuncFinSequence of (TS (DTConUA (f,D))) st ( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = FreeOpNSG (n,f,D) ) ) proof defpred S1[ Nat, set ] means $2 = FreeOpNSG ($1,f,D); set A = TS (DTConUA (f,D)); A1: for n being Nat st n in Seg (len f) holds ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] proof let n be Nat; ::_thesis: ( n in Seg (len f) implies ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] ) assume n in Seg (len f) ; ::_thesis: ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] reconsider O = FreeOpNSG (n,f,D) as Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) by PARTFUN1:45; take O ; ::_thesis: S1[n,O] thus S1[n,O] ; ::_thesis: verum end; consider p being FinSequence of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) such that A2: ( dom p = Seg (len f) & ( for n being Nat st n in Seg (len f) holds S1[n,p . n] ) ) from FINSEQ_1:sch_5(A1); reconsider p = p as PFuncFinSequence of (TS (DTConUA (f,D))) ; take p ; ::_thesis: ( len p = len f & ( for n being Element of NAT st n in dom p holds p . n = FreeOpNSG (n,f,D) ) ) thus len p = len f by A2, FINSEQ_1:def_3; ::_thesis: for n being Element of NAT st n in dom p holds p . n = FreeOpNSG (n,f,D) let n be Element of NAT ; ::_thesis: ( n in dom p implies p . n = FreeOpNSG (n,f,D) ) assume n in dom p ; ::_thesis: p . n = FreeOpNSG (n,f,D) hence p . n = FreeOpNSG (n,f,D) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of (TS (DTConUA (f,D))) st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = FreeOpNSG (n,f,D) ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = FreeOpNSG (n,f,D) ) holds b1 = b2 proof let f1, f2 be PFuncFinSequence of (TS (DTConUA (f,D))); ::_thesis: ( len f1 = len f & ( for n being Element of NAT st n in dom f1 holds f1 . n = FreeOpNSG (n,f,D) ) & len f2 = len f & ( for n being Element of NAT st n in dom f2 holds f2 . n = FreeOpNSG (n,f,D) ) implies f1 = f2 ) assume that A3: len f1 = len f and A4: for n being Element of NAT st n in dom f1 holds f1 . n = FreeOpNSG (n,f,D) and A5: len f2 = len f and A6: for n being Element of NAT st n in dom f2 holds f2 . n = FreeOpNSG (n,f,D) ; ::_thesis: f1 = f2 for n being Nat st n in dom f1 holds f1 . n = f2 . n proof let n be Nat; ::_thesis: ( n in dom f1 implies f1 . n = f2 . n ) A7: ( dom f1 = Seg (len f1) & dom f2 = Seg (len f2) ) by FINSEQ_1:def_3; assume A8: n in dom f1 ; ::_thesis: f1 . n = f2 . n then f1 . n = FreeOpNSG (n,f,D) by A4; hence f1 . n = f2 . n by A3, A5, A6, A7, A8; ::_thesis: verum end; hence f1 = f2 by A3, A5, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def11 defines FreeOpSeqNSG FREEALG:def_11_:_ for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set for b3 being PFuncFinSequence of (TS (DTConUA (f,D))) holds ( b3 = FreeOpSeqNSG (f,D) iff ( len b3 = len f & ( for n being Element of NAT st n in dom b3 holds b3 . n = FreeOpNSG (n,f,D) ) ) ); definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; func FreeUnivAlgNSG (f,D) -> strict Universal_Algebra equals :: FREEALG:def 12 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #); coherence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is strict Universal_Algebra proof set A = TS (DTConUA (f,D)); set AA = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #); for n being Nat for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n holds h is quasi_total let h be PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n implies h is quasi_total ) assume ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n ) ; ::_thesis: h is quasi_total then h = FreeOpNSG (n,f,D) by Def11; hence h is quasi_total ; ::_thesis: verum end; then A1: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is quasi_total by MARGREL1:def_24; for n being Nat for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n holds h is homogeneous let h be PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n implies h is homogeneous ) assume ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n ) ; ::_thesis: h is homogeneous then h = FreeOpNSG (n,f,D) by Def11; hence h is homogeneous ; ::_thesis: verum end; then A2: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is homogeneous by MARGREL1:def_23; for n being set st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) holds not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n is empty proof let n be set ; ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) implies not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n is empty ) assume A3: n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) ; ::_thesis: not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n is empty then reconsider n = n as Element of NAT ; the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n = FreeOpNSG (n,f,D) by A3, Def11; hence not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) . n is empty ; ::_thesis: verum end; then A4: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is non-empty by FUNCT_1:def_9; len (FreeOpSeqNSG (f,D)) = len f by Def11; then the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) <> {} ; hence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is strict Universal_Algebra by A1, A2, A4, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; end; :: deftheorem defines FreeUnivAlgNSG FREEALG:def_12_:_ for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set holds FreeUnivAlgNSG (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #); theorem Th4: :: FREEALG:4 for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f proof let f be non empty FinSequence of NAT ; ::_thesis: for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f let D be non empty disjoint_with_NAT set ; ::_thesis: signature (FreeUnivAlgNSG (f,D)) = f set fa = FreeUnivAlgNSG (f,D); set A = TS (DTConUA (f,D)); A1: len the charact of (FreeUnivAlgNSG (f,D)) = len f by Def11; A2: len (signature (FreeUnivAlgNSG (f,D))) = len the charact of (FreeUnivAlgNSG (f,D)) by UNIALG_1:def_4; then A3: dom (signature (FreeUnivAlgNSG (f,D))) = Seg (len f) by A1, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_(signature_(FreeUnivAlgNSG_(f,D)))_holds_ (signature_(FreeUnivAlgNSG_(f,D)))_._n_=_f_._n let n be Nat; ::_thesis: ( n in dom (signature (FreeUnivAlgNSG (f,D))) implies (signature (FreeUnivAlgNSG (f,D))) . n = f . n ) reconsider h = FreeOpNSG (n,f,D) as non empty homogeneous quasi_total PartFunc of ( the carrier of (FreeUnivAlgNSG (f,D)) *), the carrier of (FreeUnivAlgNSG (f,D)) ; A4: dom h = (arity h) -tuples_on the carrier of (FreeUnivAlgNSG (f,D)) by MARGREL1:22; assume A5: n in dom (signature (FreeUnivAlgNSG (f,D))) ; ::_thesis: (signature (FreeUnivAlgNSG (f,D))) . n = f . n then A6: n in dom f by A3, FINSEQ_1:def_3; then dom h = (f /. n) -tuples_on (TS (DTConUA (f,D))) by Def10; then A7: arity h = f /. n by A4, FINSEQ_2:110; n in dom (FreeOpSeqNSG (f,D)) by A1, A3, A5, FINSEQ_1:def_3; then the charact of (FreeUnivAlgNSG (f,D)) . n = FreeOpNSG (n,f,D) by Def11; hence (signature (FreeUnivAlgNSG (f,D))) . n = arity h by A5, UNIALG_1:def_4 .= f . n by A6, A7, PARTFUN1:def_6 ; ::_thesis: verum end; hence signature (FreeUnivAlgNSG (f,D)) = f by A2, A1, FINSEQ_2:9; ::_thesis: verum end; definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; func FreeGenSetNSG (f,D) -> Subset of (FreeUnivAlgNSG (f,D)) equals :: FREEALG:def 13 { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ; coherence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgNSG (f,D)) proof set X = DTConUA (f,D); set A = { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } ; { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } c= the carrier of (FreeUnivAlgNSG (f,D)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } or x in the carrier of (FreeUnivAlgNSG (f,D)) ) assume x in { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } ; ::_thesis: x in the carrier of (FreeUnivAlgNSG (f,D)) then ex d being Symbol of (DTConUA (f,D)) st ( x = root-tree d & d in Terminals (DTConUA (f,D)) ) ; hence x in the carrier of (FreeUnivAlgNSG (f,D)) by DTCONSTR:def_1; ::_thesis: verum end; hence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgNSG (f,D)) ; ::_thesis: verum end; end; :: deftheorem defines FreeGenSetNSG FREEALG:def_13_:_ for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ; theorem Th5: :: FREEALG:5 for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty proof let f be non empty FinSequence of NAT ; ::_thesis: for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty let D be non empty disjoint_with_NAT set ; ::_thesis: not FreeGenSetNSG (f,D) is empty set X = DTConUA (f,D); set d = the Element of D; reconsider d1 = the Element of D as Symbol of (DTConUA (f,D)) by XBOOLE_0:def_3; Terminals (DTConUA (f,D)) = D by Th3; then root-tree d1 in { (root-tree k) where k is Symbol of (DTConUA (f,D)) : k in Terminals (DTConUA (f,D)) } ; hence not FreeGenSetNSG (f,D) is empty ; ::_thesis: verum end; definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; :: original: FreeGenSetNSG redefine func FreeGenSetNSG (f,D) -> GeneratorSet of FreeUnivAlgNSG (f,D); coherence FreeGenSetNSG (f,D) is GeneratorSet of FreeUnivAlgNSG (f,D) proof set fgs = FreeGenSetNSG (f,D); set fua = FreeUnivAlgNSG (f,D); A1: the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) = the carrier of (FreeUnivAlgNSG (f,D)) proof set A = DTConUA (f,D); defpred S1[ DecoratedTree of the carrier of (DTConUA (f,D))] means $1 in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))); the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) is Subset of (FreeUnivAlgNSG (f,D)) by UNIALG_2:def_7; hence the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) c= the carrier of (FreeUnivAlgNSG (f,D)) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (FreeUnivAlgNSG (f,D)) c= the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) A2: for nt being Symbol of (DTConUA (f,D)) for ts being FinSequence of TS (DTConUA (f,D)) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng ts holds S1[t] ) holds S1[nt -tree ts] proof reconsider B = the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) as Subset of (FreeUnivAlgNSG (f,D)) by UNIALG_2:def_7; let s be Symbol of (DTConUA (f,D)); ::_thesis: for ts being FinSequence of TS (DTConUA (f,D)) st s ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng ts holds S1[t] ) holds S1[s -tree ts] let p be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( s ==> roots p & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng p holds S1[t] ) implies S1[s -tree p] ) assume that A3: s ==> roots p and A4: for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng p holds t in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) ; ::_thesis: S1[s -tree p] rng p c= the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) ) assume A5: x in rng p ; ::_thesis: x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) rng p c= FinTrees the carrier of (DTConUA (f,D)) by FINSEQ_1:def_4; then reconsider x1 = x as Element of FinTrees the carrier of (DTConUA (f,D)) by A5; x1 in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) by A4, A5; hence x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) ; ::_thesis: verum end; then reconsider cp = p as FinSequence of the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) by FINSEQ_1:def_4; reconsider tp = p as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; [s,(roots p)] in the Rules of (DTConUA (f,D)) by A3, LANG1:def_1; then reconsider rp = roots p as Element of ((dom f) \/ D) * by ZFMISC_1:87; reconsider s0 = s as Element of (dom f) \/ D ; A6: [s0,rp] in REL (f,D) by A3, LANG1:def_1; then A7: s0 in dom f by Def7; then reconsider ns = s as Element of NAT ; A8: f . s0 = len rp by A6, Def7; len (FreeOpSeqNSG (f,D)) = len f by Def11; then A9: dom (FreeOpSeqNSG (f,D)) = Seg (len f) by FINSEQ_1:def_3 .= dom f by FINSEQ_1:def_3 ; then (FreeOpSeqNSG (f,D)) . ns in rng (FreeOpSeqNSG (f,D)) by A7, FUNCT_1:def_3; then reconsider o = FreeOpNSG (ns,f,D) as operation of (FreeUnivAlgNSG (f,D)) by A7, A9, Def11; B is opers_closed by UNIALG_2:def_7; then A10: B is_closed_on o by UNIALG_2:def_4; A11: dom (FreeOpNSG (ns,f,D)) = (f /. ns) -tuples_on (TS (DTConUA (f,D))) by A7, Def10; dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgNSG (f,D)) by MARGREL1:22; then A12: arity o = f /. ns by A11, FINSEQ_2:110; dom (roots p) = dom p by TREES_3:def_18 .= Seg (len p) by FINSEQ_1:def_3 ; then A13: len p = len rp by FINSEQ_1:def_3 .= f /. ns by A7, A8, PARTFUN1:def_6 ; then tp in { w where w is Element of (TS (DTConUA (f,D))) * : len w = f /. ns } ; then o . cp = (Sym (ns,f,D)) -tree p by A7, A11, Def10 .= s -tree p by A7, Def9 ; hence S1[s -tree p] by A10, A13, A12, UNIALG_2:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (FreeUnivAlgNSG (f,D)) or x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) ) assume A14: x in the carrier of (FreeUnivAlgNSG (f,D)) ; ::_thesis: x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) then reconsider x1 = x as Element of FinTrees the carrier of (DTConUA (f,D)) ; A15: x1 in TS (DTConUA (f,D)) by A14; A16: for s being Symbol of (DTConUA (f,D)) st s in Terminals (DTConUA (f,D)) holds S1[ root-tree s] proof let s be Symbol of (DTConUA (f,D)); ::_thesis: ( s in Terminals (DTConUA (f,D)) implies S1[ root-tree s] ) assume s in Terminals (DTConUA (f,D)) ; ::_thesis: S1[ root-tree s] then A17: root-tree s in { (root-tree q) where q is Symbol of (DTConUA (f,D)) : q in Terminals (DTConUA (f,D)) } ; FreeGenSetNSG (f,D) <> {} by Th5; then FreeGenSetNSG (f,D) c= the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) by UNIALG_2:def_12; hence S1[ root-tree s] by A17; ::_thesis: verum end; for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in TS (DTConUA (f,D)) holds S1[t] from DTCONSTR:sch_7(A16, A2); hence x in the carrier of (GenUnivAlg (FreeGenSetNSG (f,D))) by A15; ::_thesis: verum end; FreeGenSetNSG (f,D) <> {} by Th5; hence FreeGenSetNSG (f,D) is GeneratorSet of FreeUnivAlgNSG (f,D) by A1, Lm3; ::_thesis: verum end; end; definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; let C be non empty set ; let s be Symbol of (DTConUA (f,D)); let F be Function of (FreeGenSetNSG (f,D)),C; assume A1: s in Terminals (DTConUA (f,D)) ; func pi (F,s) -> Element of C equals :Def14: :: FREEALG:def 14 F . (root-tree s); coherence F . (root-tree s) is Element of C proof ( root-tree s in FreeGenSetNSG (f,D) & dom F = FreeGenSetNSG (f,D) ) by A1, FUNCT_2:def_1; then ( rng F c= C & F . (root-tree s) in rng F ) by FUNCT_1:def_3, RELAT_1:def_19; hence F . (root-tree s) is Element of C ; ::_thesis: verum end; end; :: deftheorem Def14 defines pi FREEALG:def_14_:_ for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set for C being non empty set for s being Symbol of (DTConUA (f,D)) for F being Function of (FreeGenSetNSG (f,D)),C st s in Terminals (DTConUA (f,D)) holds pi (F,s) = F . (root-tree s); definition let f be non empty FinSequence of NAT ; let D be set ; let s be Symbol of (DTConUA (f,D)); given p being FinSequence such that A1: s ==> p ; func @ s -> Element of NAT equals :Def15: :: FREEALG:def 15 s; coherence s is Element of NAT proof reconsider s0 = s as Element of (dom f) \/ D ; set A = DTConUA (f,D); [s,p] in the Rules of (DTConUA (f,D)) by A1, LANG1:def_1; then reconsider p0 = p as Element of ((dom f) \/ D) * by ZFMISC_1:87; [s0,p0] in REL (f,D) by A1, LANG1:def_1; then s0 in dom f by Def7; hence s is Element of NAT ; ::_thesis: verum end; end; :: deftheorem Def15 defines @ FREEALG:def_15_:_ for f being non empty FinSequence of NAT for D being set for s being Symbol of (DTConUA (f,D)) st ex p being FinSequence st s ==> p holds @ s = s; theorem Th6: :: FREEALG:6 for f being non empty FinSequence of NAT for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free proof let f be non empty FinSequence of NAT ; ::_thesis: for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free let D be non empty disjoint_with_NAT set ; ::_thesis: FreeGenSetNSG (f,D) is free set fgs = FreeGenSetNSG (f,D); set fua = FreeUnivAlgNSG (f,D); let U1 be Universal_Algebra; :: according to FREEALG:def_5 ::_thesis: ( FreeUnivAlgNSG (f,D),U1 are_similar implies for f being Function of (FreeGenSetNSG (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st ( h is_homomorphism FreeUnivAlgNSG (f,D),U1 & h | (FreeGenSetNSG (f,D)) = f ) ) assume A1: FreeUnivAlgNSG (f,D),U1 are_similar ; ::_thesis: for f being Function of (FreeGenSetNSG (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st ( h is_homomorphism FreeUnivAlgNSG (f,D),U1 & h | (FreeGenSetNSG (f,D)) = f ) set A = DTConUA (f,D); set c1 = the carrier of U1; set cf = the carrier of (FreeUnivAlgNSG (f,D)); let F be Function of (FreeGenSetNSG (f,D)), the carrier of U1; ::_thesis: ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st ( h is_homomorphism FreeUnivAlgNSG (f,D),U1 & h | (FreeGenSetNSG (f,D)) = F ) deffunc H1( Symbol of (DTConUA (f,D))) -> Element of the carrier of U1 = pi (F,$1); deffunc H2( Symbol of (DTConUA (f,D)), FinSequence, set ) -> Element of the carrier of U1 = (oper ((@ $1),U1)) /. $3; consider ff being Function of (TS (DTConUA (f,D))), the carrier of U1 such that A2: for t being Symbol of (DTConUA (f,D)) st t in Terminals (DTConUA (f,D)) holds ff . (root-tree t) = H1(t) and A3: for nt being Symbol of (DTConUA (f,D)) for ts being FinSequence of TS (DTConUA (f,D)) st nt ==> roots ts holds ff . (nt -tree ts) = H2(nt, roots ts,ff * ts) from DTCONSTR:sch_8(); reconsider ff = ff as Function of (FreeUnivAlgNSG (f,D)),U1 ; take ff ; ::_thesis: ( ff is_homomorphism FreeUnivAlgNSG (f,D),U1 & ff | (FreeGenSetNSG (f,D)) = F ) for n being Element of NAT st n in dom the charact of (FreeUnivAlgNSG (f,D)) holds for o1 being operation of (FreeUnivAlgNSG (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) proof A4: Seg (len the charact of U1) = dom the charact of U1 by FINSEQ_1:def_3; let n be Element of NAT ; ::_thesis: ( n in dom the charact of (FreeUnivAlgNSG (f,D)) implies for o1 being operation of (FreeUnivAlgNSG (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) ) assume A5: n in dom the charact of (FreeUnivAlgNSG (f,D)) ; ::_thesis: for o1 being operation of (FreeUnivAlgNSG (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let o1 be operation of (FreeUnivAlgNSG (f,D)); ::_thesis: for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let o2 be operation of U1; ::_thesis: ( o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n implies for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) ) assume that A6: o1 = the charact of (FreeUnivAlgNSG (f,D)) . n and A7: o2 = the charact of U1 . n ; ::_thesis: for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let x be FinSequence of (FreeUnivAlgNSG (f,D)); ::_thesis: ( x in dom o1 implies ff . (o1 . x) = o2 . (ff * x) ) assume A8: x in dom o1 ; ::_thesis: ff . (o1 . x) = o2 . (ff * x) reconsider xa = x as FinSequence of TS (DTConUA (f,D)) ; dom (roots xa) = dom xa by TREES_3:def_18 .= Seg (len xa) by FINSEQ_1:def_3 ; then A9: len (roots xa) = len xa by FINSEQ_1:def_3; reconsider xa = xa as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ; reconsider rxa = roots xa as FinSequence of (dom f) \/ D ; reconsider rxa = rxa as Element of ((dom f) \/ D) * by FINSEQ_1:def_11; dom o1 = (arity o1) -tuples_on the carrier of (FreeUnivAlgNSG (f,D)) by MARGREL1:22 .= { w where w is Element of the carrier of (FreeUnivAlgNSG (f,D)) * : len w = arity o1 } ; then A10: ex w being Element of the carrier of (FreeUnivAlgNSG (f,D)) * st ( x = w & len w = arity o1 ) by A8; A11: o1 = FreeOpNSG (n,f,D) by A5, A6, Def11; reconsider fx = ff * x as Element of the carrier of U1 * ; A12: dom o2 = (arity o2) -tuples_on the carrier of U1 by MARGREL1:22 .= { v where v is Element of the carrier of U1 * : len v = arity o2 } ; A13: ( len the charact of (FreeUnivAlgNSG (f,D)) = len the charact of U1 & Seg (len the charact of (FreeUnivAlgNSG (f,D))) = dom the charact of (FreeUnivAlgNSG (f,D)) ) by A1, FINSEQ_1:def_3, UNIALG_2:1; A14: dom (FreeOpSeqNSG (f,D)) = Seg (len (FreeOpSeqNSG (f,D))) by FINSEQ_1:def_3; A15: ( len (FreeOpSeqNSG (f,D)) = len f & Seg (len f) = dom f ) by Def11, FINSEQ_1:def_3; then reconsider nt = n as Symbol of (DTConUA (f,D)) by A5, A14, XBOOLE_0:def_3; reconsider nd = n as Element of (dom f) \/ D by A5, A15, A14, XBOOLE_0:def_3; A16: f = signature (FreeUnivAlgNSG (f,D)) by Th4; then A17: (signature (FreeUnivAlgNSG (f,D))) . n = arity o1 by A5, A6, A15, A14, UNIALG_1:def_4; then [nd,rxa] in REL (f,D) by A5, A15, A14, A16, A10, A9, Def7; then A18: nt ==> roots xa by LANG1:def_1; then A19: ff . (nt -tree xa) = (oper ((@ nt),U1)) /. (ff * x) by A3; @ nt = n by A18, Def15; then A20: oper ((@ nt),U1) = o2 by A5, A7, A13, A4, Def3; signature (FreeUnivAlgNSG (f,D)) = signature U1 by A1, UNIALG_2:def_1; then ( len (ff * x) = len x & arity o2 = len x ) by A5, A7, A15, A14, A16, A10, A17, FINSEQ_3:120, UNIALG_1:def_4; then A21: fx in { v where v is Element of the carrier of U1 * : len v = arity o2 } ; reconsider xa = xa as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; Sym (n,f,D) = nt by A5, A15, A14, Def9; then o1 . x = nt -tree xa by A5, A8, A15, A14, A11, Def10; hence ff . (o1 . x) = o2 . (ff * x) by A19, A20, A12, A21, PARTFUN1:def_6; ::_thesis: verum end; hence ff is_homomorphism FreeUnivAlgNSG (f,D),U1 by A1, ALG_1:def_1; ::_thesis: ff | (FreeGenSetNSG (f,D)) = F A22: the carrier of (FreeUnivAlgNSG (f,D)) /\ (FreeGenSetNSG (f,D)) = FreeGenSetNSG (f,D) by XBOOLE_1:28; A23: ( dom (ff | (FreeGenSetNSG (f,D))) = (dom ff) /\ (FreeGenSetNSG (f,D)) & dom ff = the carrier of (FreeUnivAlgNSG (f,D)) ) by FUNCT_2:def_1, RELAT_1:61; A24: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (ff_|_(FreeGenSetNSG_(f,D)))_._x_=_F_._x let x be set ; ::_thesis: ( x in dom F implies (ff | (FreeGenSetNSG (f,D))) . x = F . x ) assume A25: x in dom F ; ::_thesis: (ff | (FreeGenSetNSG (f,D))) . x = F . x then x in { (root-tree t) where t is Symbol of (DTConUA (f,D)) : t in Terminals (DTConUA (f,D)) } ; then consider s being Symbol of (DTConUA (f,D)) such that A26: ( x = root-tree s & s in Terminals (DTConUA (f,D)) ) ; thus (ff | (FreeGenSetNSG (f,D))) . x = ff . x by A23, A22, A25, FUNCT_1:47 .= pi (F,s) by A2, A26 .= F . x by A26, Def14 ; ::_thesis: verum end; FreeGenSetNSG (f,D) = dom F by FUNCT_2:def_1; hence ff | (FreeGenSetNSG (f,D)) = F by A23, A22, A24, FUNCT_1:2; ::_thesis: verum end; registration let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; cluster FreeUnivAlgNSG (f,D) -> strict free ; coherence FreeUnivAlgNSG (f,D) is free proof FreeGenSetNSG (f,D) is free by Th6; hence FreeUnivAlgNSG (f,D) is free by Def6; ::_thesis: verum end; end; definition let f be non empty FinSequence of NAT ; let D be non empty disjoint_with_NAT set ; :: original: FreeGenSetNSG redefine func FreeGenSetNSG (f,D) -> free GeneratorSet of FreeUnivAlgNSG (f,D); coherence FreeGenSetNSG (f,D) is free GeneratorSet of FreeUnivAlgNSG (f,D) by Th6; end; begin definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; let n be Nat; assume A1: n in dom f ; func FreeOpZAO (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def16: :: FREEALG:def 16 ( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds it . p = (Sym (n,f,D)) -tree p ) ); existence ex b1 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st ( dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds b1 . p = (Sym (n,f,D)) -tree p ) ) proof set A = DTConUA (f,D); set i = f /. n; set Y = (dom f) \/ D; set smm = Sym (n,f,D); defpred S1[ set , set ] means ( $1 in (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p = $1 holds $2 = (Sym (n,f,D)) -tree p ) ); set tu = { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } ; A2: f /. n = f . n by A1, PARTFUN1:def_6; A3: for x, y being set st x in (TS (DTConUA (f,D))) * & S1[x,y] holds y in TS (DTConUA (f,D)) proof reconsider sm = Sym (n,f,D) as Element of (dom f) \/ D ; let x, y be set ; ::_thesis: ( x in (TS (DTConUA (f,D))) * & S1[x,y] implies y in TS (DTConUA (f,D)) ) assume that x in (TS (DTConUA (f,D))) * and A4: S1[x,y] ; ::_thesis: y in TS (DTConUA (f,D)) consider s being Element of (TS (DTConUA (f,D))) * such that A5: s = x and A6: len s = f /. n by A4; A7: y = (Sym (n,f,D)) -tree s by A4, A5; reconsider s = s as FinSequence of TS (DTConUA (f,D)) ; ( dom (roots s) = dom s & Seg (len (roots s)) = dom (roots s) ) by FINSEQ_1:def_3, TREES_3:def_18; then A8: len (roots s) = f /. n by A6, FINSEQ_1:def_3; reconsider s = s as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ; reconsider rs = roots s as Element of ((dom f) \/ D) * by FINSEQ_1:def_11; sm = n by A1, Def9; then [sm,rs] in REL (f,D) by A1, A2, A8, Def7; then Sym (n,f,D) ==> roots s by LANG1:def_1; hence y in TS (DTConUA (f,D)) by A7, DTCONSTR:def_1; ::_thesis: verum end; A9: for x, y1, y2 being set st x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in (TS (DTConUA (f,D))) * & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that x in (TS (DTConUA (f,D))) * and A10: S1[x,y1] and A11: S1[x,y2] ; ::_thesis: y1 = y2 consider s being Element of (TS (DTConUA (f,D))) * such that A12: s = x and len s = f /. n by A10; y1 = (Sym (n,f,D)) -tree s by A10, A12; hence y1 = y2 by A11, A12; ::_thesis: verum end; consider F being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) such that A13: for x being set holds ( x in dom F iff ( x in (TS (DTConUA (f,D))) * & ex y being set st S1[x,y] ) ) and A14: for x being set st x in dom F holds S1[x,F . x] from PARTFUN1:sch_2(A3, A9); A15: dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) proof thus dom F c= (f /. n) -tuples_on (TS (DTConUA (f,D))) :: according to XBOOLE_0:def_10 ::_thesis: (f /. n) -tuples_on (TS (DTConUA (f,D))) c= dom F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ) assume x in dom F ; ::_thesis: x in (f /. n) -tuples_on (TS (DTConUA (f,D))) then ex y being set st S1[x,y] by A13; hence x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: verum end; reconsider sm = Sym (n,f,D) as Symbol of (DTConUA (f,D)) ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f /. n) -tuples_on (TS (DTConUA (f,D))) or x in dom F ) assume x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: x in dom F then consider s being Element of (TS (DTConUA (f,D))) * such that A16: s = x and A17: len s = f /. n ; S1[s,sm -tree s] by A17; hence x in dom F by A13, A16; ::_thesis: verum end; A18: for x, y being FinSequence of TS (DTConUA (f,D)) st len x = len y & x in dom F holds y in dom F proof let x, y be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( len x = len y & x in dom F implies y in dom F ) assume that A19: len x = len y and A20: x in dom F ; ::_thesis: y in dom F reconsider sy = y as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; ex sx being Element of (TS (DTConUA (f,D))) * st ( sx = x & len sx = f /. n ) by A15, A20; then sy in { s where s is Element of (TS (DTConUA (f,D))) * : len s = f /. n } by A19; hence y in dom F by A15; ::_thesis: verum end; A21: ex x being FinSequence st x in dom F proof set a = the Element of (f /. n) -tuples_on (TS (DTConUA (f,D))); the Element of (f /. n) -tuples_on (TS (DTConUA (f,D))) in dom F by A15; hence ex x being FinSequence st x in dom F ; ::_thesis: verum end; dom F is with_common_domain proof let x, y be FinSequence; :: according to MARGREL1:def_1 ::_thesis: ( not x in dom F or not y in dom F or len x = len y ) assume ( x in dom F & y in dom F ) ; ::_thesis: len x = len y then ( ex sx being Element of (TS (DTConUA (f,D))) * st ( sx = x & len sx = f /. n ) & ex sy being Element of (TS (DTConUA (f,D))) * st ( sy = y & len sy = f /. n ) ) by A15; hence len x = len y ; ::_thesis: verum end; then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) by A18, A21, MARGREL1:def_21, MARGREL1:def_22; take F ; ::_thesis: ( dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds F . p = (Sym (n,f,D)) -tree p ) ) thus dom F = (f /. n) -tuples_on (TS (DTConUA (f,D))) by A15; ::_thesis: for p being FinSequence of TS (DTConUA (f,D)) st p in dom F holds F . p = (Sym (n,f,D)) -tree p let p be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( p in dom F implies F . p = (Sym (n,f,D)) -tree p ) assume p in dom F ; ::_thesis: F . p = (Sym (n,f,D)) -tree p hence F . p = (Sym (n,f,D)) -tree p by A14; ::_thesis: verum end; uniqueness for b1, b2 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds b1 . p = (Sym (n,f,D)) -tree p ) & dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b2 holds b2 . p = (Sym (n,f,D)) -tree p ) holds b1 = b2 proof set A = TS (DTConUA (f,D)); let f1, f2 be non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds f1 . p = (Sym (n,f,D)) -tree p ) & dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds f2 . p = (Sym (n,f,D)) -tree p ) implies f1 = f2 ) assume that A22: dom f1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and A23: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f1 holds f1 . p = (Sym (n,f,D)) -tree p and A24: dom f2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) and A25: for p being FinSequence of TS (DTConUA (f,D)) st p in dom f2 holds f2 . p = (Sym (n,f,D)) -tree p ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_(f_/._n)_-tuples_on_(TS_(DTConUA_(f,D)))_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in (f /. n) -tuples_on (TS (DTConUA (f,D))) implies f1 . x = f2 . x ) assume A26: x in (f /. n) -tuples_on (TS (DTConUA (f,D))) ; ::_thesis: f1 . x = f2 . x then consider s being Element of (TS (DTConUA (f,D))) * such that A27: s = x and len s = f /. n ; f1 . s = (Sym (n,f,D)) -tree s by A22, A23, A26, A27; hence f1 . x = f2 . x by A24, A25, A26, A27; ::_thesis: verum end; hence f1 = f2 by A22, A24, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def16 defines FreeOpZAO FREEALG:def_16_:_ for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set for n being Nat st n in dom f holds for b4 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds ( b4 = FreeOpZAO (n,f,D) iff ( dom b4 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b4 holds b4 . p = (Sym (n,f,D)) -tree p ) ) ); definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; func FreeOpSeqZAO (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def17: :: FREEALG:def 17 ( len it = len f & ( for n being Element of NAT st n in dom it holds it . n = FreeOpZAO (n,f,D) ) ); existence ex b1 being PFuncFinSequence of (TS (DTConUA (f,D))) st ( len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = FreeOpZAO (n,f,D) ) ) proof defpred S1[ Nat, set ] means $2 = FreeOpZAO ($1,f,D); set A = TS (DTConUA (f,D)); A1: for n being Nat st n in Seg (len f) holds ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] proof let n be Nat; ::_thesis: ( n in Seg (len f) implies ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] ) assume n in Seg (len f) ; ::_thesis: ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S1[n,x] reconsider O = FreeOpZAO (n,f,D) as Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) by PARTFUN1:45; take O ; ::_thesis: S1[n,O] thus S1[n,O] ; ::_thesis: verum end; consider p being FinSequence of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) such that A2: ( dom p = Seg (len f) & ( for n being Nat st n in Seg (len f) holds S1[n,p . n] ) ) from FINSEQ_1:sch_5(A1); reconsider p = p as PFuncFinSequence of (TS (DTConUA (f,D))) ; take p ; ::_thesis: ( len p = len f & ( for n being Element of NAT st n in dom p holds p . n = FreeOpZAO (n,f,D) ) ) thus len p = len f by A2, FINSEQ_1:def_3; ::_thesis: for n being Element of NAT st n in dom p holds p . n = FreeOpZAO (n,f,D) let n be Element of NAT ; ::_thesis: ( n in dom p implies p . n = FreeOpZAO (n,f,D) ) assume n in dom p ; ::_thesis: p . n = FreeOpZAO (n,f,D) hence p . n = FreeOpZAO (n,f,D) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of (TS (DTConUA (f,D))) st len b1 = len f & ( for n being Element of NAT st n in dom b1 holds b1 . n = FreeOpZAO (n,f,D) ) & len b2 = len f & ( for n being Element of NAT st n in dom b2 holds b2 . n = FreeOpZAO (n,f,D) ) holds b1 = b2 proof let f1, f2 be PFuncFinSequence of (TS (DTConUA (f,D))); ::_thesis: ( len f1 = len f & ( for n being Element of NAT st n in dom f1 holds f1 . n = FreeOpZAO (n,f,D) ) & len f2 = len f & ( for n being Element of NAT st n in dom f2 holds f2 . n = FreeOpZAO (n,f,D) ) implies f1 = f2 ) assume that A3: len f1 = len f and A4: for n being Element of NAT st n in dom f1 holds f1 . n = FreeOpZAO (n,f,D) and A5: len f2 = len f and A6: for n being Element of NAT st n in dom f2 holds f2 . n = FreeOpZAO (n,f,D) ; ::_thesis: f1 = f2 A7: dom f1 = Seg (len f1) by FINSEQ_1:def_3; A8: dom f = Seg (len f) by FINSEQ_1:def_3; A9: dom f2 = Seg (len f2) by FINSEQ_1:def_3; for n being Nat st n in dom f holds f1 . n = f2 . n proof let n be Nat; ::_thesis: ( n in dom f implies f1 . n = f2 . n ) assume A10: n in dom f ; ::_thesis: f1 . n = f2 . n then f1 . n = FreeOpZAO (n,f,D) by A3, A4, A8, A7; hence f1 . n = f2 . n by A5, A6, A8, A9, A10; ::_thesis: verum end; hence f1 = f2 by A3, A5, A8, A7, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def17 defines FreeOpSeqZAO FREEALG:def_17_:_ for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set for b3 being PFuncFinSequence of (TS (DTConUA (f,D))) holds ( b3 = FreeOpSeqZAO (f,D) iff ( len b3 = len f & ( for n being Element of NAT st n in dom b3 holds b3 . n = FreeOpZAO (n,f,D) ) ) ); definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; func FreeUnivAlgZAO (f,D) -> strict Universal_Algebra equals :: FREEALG:def 18 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #); coherence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra proof set A = TS (DTConUA (f,D)); set AA = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #); for n being Nat for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds h is quasi_total let h be PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n implies h is quasi_total ) assume ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n ) ; ::_thesis: h is quasi_total then h = FreeOpZAO (n,f,D) by Def17; hence h is quasi_total ; ::_thesis: verum end; then A1: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is quasi_total by MARGREL1:def_24; for n being Nat for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds h is homogeneous let h be PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))); ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n implies h is homogeneous ) assume ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n ) ; ::_thesis: h is homogeneous then h = FreeOpZAO (n,f,D) by Def17; hence h is homogeneous ; ::_thesis: verum end; then A2: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is homogeneous by MARGREL1:def_23; for n being set st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) holds not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty proof let n be set ; ::_thesis: ( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) implies not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty ) assume A3: n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) ; ::_thesis: not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty then reconsider n = n as Element of NAT ; the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n = FreeOpZAO (n,f,D) by A3, Def17; hence not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty ; ::_thesis: verum end; then A4: the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is non-empty by FUNCT_1:def_9; len (FreeOpSeqZAO (f,D)) = len f by Def17; then the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) <> {} ; hence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra by A1, A2, A4, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; end; :: deftheorem defines FreeUnivAlgZAO FREEALG:def_18_:_ for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #); theorem Th7: :: FREEALG:7 for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f proof let f be non empty with_zero FinSequence of NAT ; ::_thesis: for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f let D be disjoint_with_NAT set ; ::_thesis: signature (FreeUnivAlgZAO (f,D)) = f set fa = FreeUnivAlgZAO (f,D); set A = TS (DTConUA (f,D)); A1: len the charact of (FreeUnivAlgZAO (f,D)) = len f by Def17; A2: len (signature (FreeUnivAlgZAO (f,D))) = len the charact of (FreeUnivAlgZAO (f,D)) by UNIALG_1:def_4; then A3: dom (signature (FreeUnivAlgZAO (f,D))) = Seg (len f) by A1, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_(signature_(FreeUnivAlgZAO_(f,D)))_holds_ (signature_(FreeUnivAlgZAO_(f,D)))_._n_=_f_._n let n be Nat; ::_thesis: ( n in dom (signature (FreeUnivAlgZAO (f,D))) implies (signature (FreeUnivAlgZAO (f,D))) . n = f . n ) reconsider h = FreeOpZAO (n,f,D) as non empty homogeneous quasi_total PartFunc of ( the carrier of (FreeUnivAlgZAO (f,D)) *), the carrier of (FreeUnivAlgZAO (f,D)) ; A4: dom h = (arity h) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22; assume A5: n in dom (signature (FreeUnivAlgZAO (f,D))) ; ::_thesis: (signature (FreeUnivAlgZAO (f,D))) . n = f . n then A6: n in dom f by A3, FINSEQ_1:def_3; then dom h = (f /. n) -tuples_on (TS (DTConUA (f,D))) by Def16; then A7: arity h = f /. n by A4, FINSEQ_2:110; n in dom (FreeOpSeqZAO (f,D)) by A1, A3, A5, FINSEQ_1:def_3; then the charact of (FreeUnivAlgZAO (f,D)) . n = FreeOpZAO (n,f,D) by Def17; hence (signature (FreeUnivAlgZAO (f,D))) . n = arity h by A5, UNIALG_1:def_4 .= f . n by A6, A7, PARTFUN1:def_6 ; ::_thesis: verum end; hence signature (FreeUnivAlgZAO (f,D)) = f by A2, A1, FINSEQ_2:9; ::_thesis: verum end; theorem Th8: :: FREEALG:8 for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op proof let f be non empty with_zero FinSequence of NAT ; ::_thesis: for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op let D be disjoint_with_NAT set ; ::_thesis: FreeUnivAlgZAO (f,D) is with_const_op set A = DTConUA (f,D); set AA = FreeUnivAlgZAO (f,D); A1: dom f = Seg (len f) by FINSEQ_1:def_3; 0 in rng f by Def2; then consider n being Nat such that A2: n in dom f and A3: f . n = 0 by FINSEQ_2:10; A4: ( len (FreeOpSeqZAO (f,D)) = len f & dom (FreeOpSeqZAO (f,D)) = Seg (len (FreeOpSeqZAO (f,D))) ) by Def17, FINSEQ_1:def_3; then the charact of (FreeUnivAlgZAO (f,D)) . n = FreeOpZAO (n,f,D) by A2, A1, Def17; then reconsider o = FreeOpZAO (n,f,D) as operation of (FreeUnivAlgZAO (f,D)) by A2, A4, A1, FUNCT_1:def_3; take o ; :: according to UNIALG_2:def_11 ::_thesis: arity o = 0 A5: dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22; ( f /. n = f . n & dom (FreeOpZAO (n,f,D)) = (f /. n) -tuples_on (TS (DTConUA (f,D))) ) by A2, Def16, PARTFUN1:def_6; hence arity o = 0 by A3, A5, FINSEQ_2:110; ::_thesis: verum end; theorem Th9: :: FREEALG:9 for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {} proof let f be non empty with_zero FinSequence of NAT ; ::_thesis: for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {} let D be disjoint_with_NAT set ; ::_thesis: Constants (FreeUnivAlgZAO (f,D)) <> {} set A = DTConUA (f,D); set AA = FreeUnivAlgZAO (f,D); A1: dom f = Seg (len f) by FINSEQ_1:def_3; set ca = the carrier of (FreeUnivAlgZAO (f,D)); 0 in rng f by Def2; then consider n being Nat such that A2: n in dom f and A3: f . n = 0 by FINSEQ_2:10; A4: ( len (FreeOpSeqZAO (f,D)) = len f & dom (FreeOpSeqZAO (f,D)) = Seg (len (FreeOpSeqZAO (f,D))) ) by Def17, FINSEQ_1:def_3; then the charact of (FreeUnivAlgZAO (f,D)) . n = FreeOpZAO (n,f,D) by A2, A1, Def17; then reconsider o = FreeOpZAO (n,f,D) as operation of (FreeUnivAlgZAO (f,D)) by A2, A4, A1, FUNCT_1:def_3; A5: ( f /. n = f . n & dom (FreeOpZAO (n,f,D)) = (f /. n) -tuples_on (TS (DTConUA (f,D))) ) by A2, Def16, PARTFUN1:def_6; then dom o = {(<*> (TS (DTConUA (f,D))))} by A3, FINSEQ_2:94; then <*> (TS (DTConUA (f,D))) in dom o by TARSKI:def_1; then A6: o . (<*> (TS (DTConUA (f,D)))) in rng o by FUNCT_1:def_3; rng o c= the carrier of (FreeUnivAlgZAO (f,D)) by RELAT_1:def_19; then reconsider e = o . (<*> (TS (DTConUA (f,D)))) as Element of the carrier of (FreeUnivAlgZAO (f,D)) by A6; dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22; then arity o = 0 by A3, A5, FINSEQ_2:110; then e in { a where a is Element of the carrier of (FreeUnivAlgZAO (f,D)) : ex o being operation of (FreeUnivAlgZAO (f,D)) st ( arity o = 0 & a in rng o ) } by A6; hence Constants (FreeUnivAlgZAO (f,D)) <> {} ; ::_thesis: verum end; definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; func FreeGenSetZAO (f,D) -> Subset of (FreeUnivAlgZAO (f,D)) equals :: FREEALG:def 19 { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ; coherence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgZAO (f,D)) proof set X = DTConUA (f,D); set A = { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } ; { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } c= the carrier of (FreeUnivAlgZAO (f,D)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } or x in the carrier of (FreeUnivAlgZAO (f,D)) ) assume x in { (root-tree d) where d is Symbol of (DTConUA (f,D)) : d in Terminals (DTConUA (f,D)) } ; ::_thesis: x in the carrier of (FreeUnivAlgZAO (f,D)) then ex d being Symbol of (DTConUA (f,D)) st ( x = root-tree d & d in Terminals (DTConUA (f,D)) ) ; hence x in the carrier of (FreeUnivAlgZAO (f,D)) by DTCONSTR:def_1; ::_thesis: verum end; hence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgZAO (f,D)) ; ::_thesis: verum end; end; :: deftheorem defines FreeGenSetZAO FREEALG:def_19_:_ for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ; definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; :: original: FreeGenSetZAO redefine func FreeGenSetZAO (f,D) -> GeneratorSet of FreeUnivAlgZAO (f,D); coherence FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D) proof set fgs = FreeGenSetZAO (f,D); set fua = FreeUnivAlgZAO (f,D); A1: the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) = the carrier of (FreeUnivAlgZAO (f,D)) proof set A = DTConUA (f,D); defpred S1[ DecoratedTree of the carrier of (DTConUA (f,D))] means $1 in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))); the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) is Subset of (FreeUnivAlgZAO (f,D)) by UNIALG_2:def_7; hence the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) c= the carrier of (FreeUnivAlgZAO (f,D)) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (FreeUnivAlgZAO (f,D)) c= the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) A2: for nt being Symbol of (DTConUA (f,D)) for ts being FinSequence of TS (DTConUA (f,D)) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng ts holds S1[t] ) holds S1[nt -tree ts] proof reconsider B = the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) as Subset of (FreeUnivAlgZAO (f,D)) by UNIALG_2:def_7; let s be Symbol of (DTConUA (f,D)); ::_thesis: for ts being FinSequence of TS (DTConUA (f,D)) st s ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng ts holds S1[t] ) holds S1[s -tree ts] let p be FinSequence of TS (DTConUA (f,D)); ::_thesis: ( s ==> roots p & ( for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng p holds S1[t] ) implies S1[s -tree p] ) assume that A3: s ==> roots p and A4: for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in rng p holds t in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) ; ::_thesis: S1[s -tree p] rng p c= the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) ) assume A5: x in rng p ; ::_thesis: x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) rng p c= FinTrees the carrier of (DTConUA (f,D)) by FINSEQ_1:def_4; then reconsider x1 = x as Element of FinTrees the carrier of (DTConUA (f,D)) by A5; x1 in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) by A4, A5; hence x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) ; ::_thesis: verum end; then reconsider cp = p as FinSequence of the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) by FINSEQ_1:def_4; reconsider tp = p as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; [s,(roots p)] in the Rules of (DTConUA (f,D)) by A3, LANG1:def_1; then reconsider rp = roots p as Element of ((dom f) \/ D) * by ZFMISC_1:87; reconsider s0 = s as Element of (dom f) \/ D ; A6: [s0,rp] in REL (f,D) by A3, LANG1:def_1; then A7: s0 in dom f by Def7; then reconsider ns = s as Element of NAT ; A8: f . s0 = len rp by A6, Def7; len (FreeOpSeqZAO (f,D)) = len f by Def17; then A9: dom (FreeOpSeqZAO (f,D)) = Seg (len f) by FINSEQ_1:def_3 .= dom f by FINSEQ_1:def_3 ; then (FreeOpSeqZAO (f,D)) . ns in rng (FreeOpSeqZAO (f,D)) by A7, FUNCT_1:def_3; then reconsider o = FreeOpZAO (ns,f,D) as operation of (FreeUnivAlgZAO (f,D)) by A7, A9, Def17; B is opers_closed by UNIALG_2:def_7; then A10: B is_closed_on o by UNIALG_2:def_4; A11: dom (FreeOpZAO (ns,f,D)) = (f /. ns) -tuples_on (TS (DTConUA (f,D))) by A7, Def16; dom o = (arity o) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22; then A12: arity o = f /. ns by A11, FINSEQ_2:110; dom (roots p) = dom p by TREES_3:def_18 .= Seg (len p) by FINSEQ_1:def_3 ; then A13: len p = len rp by FINSEQ_1:def_3 .= f /. ns by A7, A8, PARTFUN1:def_6 ; then tp in { w where w is Element of (TS (DTConUA (f,D))) * : len w = f /. ns } ; then o . cp = (Sym (ns,f,D)) -tree p by A7, A11, Def16 .= s -tree p by A7, Def9 ; hence S1[s -tree p] by A10, A13, A12, UNIALG_2:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (FreeUnivAlgZAO (f,D)) or x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) ) assume A14: x in the carrier of (FreeUnivAlgZAO (f,D)) ; ::_thesis: x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) then reconsider x1 = x as Element of FinTrees the carrier of (DTConUA (f,D)) ; A15: x1 in TS (DTConUA (f,D)) by A14; A16: for s being Symbol of (DTConUA (f,D)) st s in Terminals (DTConUA (f,D)) holds S1[ root-tree s] proof let s be Symbol of (DTConUA (f,D)); ::_thesis: ( s in Terminals (DTConUA (f,D)) implies S1[ root-tree s] ) assume s in Terminals (DTConUA (f,D)) ; ::_thesis: S1[ root-tree s] then A17: root-tree s in { (root-tree q) where q is Symbol of (DTConUA (f,D)) : q in Terminals (DTConUA (f,D)) } ; Constants (FreeUnivAlgZAO (f,D)) <> {} by Th9; then FreeGenSetZAO (f,D) c= the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) by UNIALG_2:def_12; hence S1[ root-tree s] by A17; ::_thesis: verum end; for t being DecoratedTree of the carrier of (DTConUA (f,D)) st t in TS (DTConUA (f,D)) holds S1[t] from DTCONSTR:sch_7(A16, A2); hence x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) by A15; ::_thesis: verum end; Constants (FreeUnivAlgZAO (f,D)) <> {} by Th9; hence FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D) by A1, Lm3; ::_thesis: verum end; end; definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; let C be non empty set ; let s be Symbol of (DTConUA (f,D)); let F be Function of (FreeGenSetZAO (f,D)),C; assume A1: s in Terminals (DTConUA (f,D)) ; func pi (F,s) -> Element of C equals :Def20: :: FREEALG:def 20 F . (root-tree s); coherence F . (root-tree s) is Element of C proof ( root-tree s in FreeGenSetZAO (f,D) & dom F = FreeGenSetZAO (f,D) ) by A1, FUNCT_2:def_1; then ( rng F c= C & F . (root-tree s) in rng F ) by FUNCT_1:def_3, RELAT_1:def_19; hence F . (root-tree s) is Element of C ; ::_thesis: verum end; end; :: deftheorem Def20 defines pi FREEALG:def_20_:_ for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set for C being non empty set for s being Symbol of (DTConUA (f,D)) for F being Function of (FreeGenSetZAO (f,D)),C st s in Terminals (DTConUA (f,D)) holds pi (F,s) = F . (root-tree s); theorem Th10: :: FREEALG:10 for f being non empty with_zero FinSequence of NAT for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free proof let f be non empty with_zero FinSequence of NAT ; ::_thesis: for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free let D be disjoint_with_NAT set ; ::_thesis: FreeGenSetZAO (f,D) is free set fgs = FreeGenSetZAO (f,D); set fua = FreeUnivAlgZAO (f,D); let U1 be Universal_Algebra; :: according to FREEALG:def_5 ::_thesis: ( FreeUnivAlgZAO (f,D),U1 are_similar implies for f being Function of (FreeGenSetZAO (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgZAO (f,D)),U1 st ( h is_homomorphism FreeUnivAlgZAO (f,D),U1 & h | (FreeGenSetZAO (f,D)) = f ) ) assume A1: FreeUnivAlgZAO (f,D),U1 are_similar ; ::_thesis: for f being Function of (FreeGenSetZAO (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgZAO (f,D)),U1 st ( h is_homomorphism FreeUnivAlgZAO (f,D),U1 & h | (FreeGenSetZAO (f,D)) = f ) set A = DTConUA (f,D); set c1 = the carrier of U1; set cf = the carrier of (FreeUnivAlgZAO (f,D)); let F be Function of (FreeGenSetZAO (f,D)), the carrier of U1; ::_thesis: ex h being Function of (FreeUnivAlgZAO (f,D)),U1 st ( h is_homomorphism FreeUnivAlgZAO (f,D),U1 & h | (FreeGenSetZAO (f,D)) = F ) deffunc H1( Symbol of (DTConUA (f,D))) -> Element of the carrier of U1 = pi (F,$1); deffunc H2( Symbol of (DTConUA (f,D)), FinSequence, set ) -> Element of the carrier of U1 = (oper ((@ $1),U1)) /. $3; consider ff being Function of (TS (DTConUA (f,D))), the carrier of U1 such that A2: for t being Symbol of (DTConUA (f,D)) st t in Terminals (DTConUA (f,D)) holds ff . (root-tree t) = H1(t) and A3: for nt being Symbol of (DTConUA (f,D)) for ts being FinSequence of TS (DTConUA (f,D)) st nt ==> roots ts holds ff . (nt -tree ts) = H2(nt, roots ts,ff * ts) from DTCONSTR:sch_8(); reconsider ff = ff as Function of (FreeUnivAlgZAO (f,D)),U1 ; take ff ; ::_thesis: ( ff is_homomorphism FreeUnivAlgZAO (f,D),U1 & ff | (FreeGenSetZAO (f,D)) = F ) for n being Element of NAT st n in dom the charact of (FreeUnivAlgZAO (f,D)) holds for o1 being operation of (FreeUnivAlgZAO (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) proof A4: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3; let n be Element of NAT ; ::_thesis: ( n in dom the charact of (FreeUnivAlgZAO (f,D)) implies for o1 being operation of (FreeUnivAlgZAO (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) ) assume A5: n in dom the charact of (FreeUnivAlgZAO (f,D)) ; ::_thesis: for o1 being operation of (FreeUnivAlgZAO (f,D)) for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let o1 be operation of (FreeUnivAlgZAO (f,D)); ::_thesis: for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO (f,D)) . n & o2 = the charact of U1 . n holds for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let o2 be operation of U1; ::_thesis: ( o1 = the charact of (FreeUnivAlgZAO (f,D)) . n & o2 = the charact of U1 . n implies for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) ) assume that A6: o1 = the charact of (FreeUnivAlgZAO (f,D)) . n and A7: o2 = the charact of U1 . n ; ::_thesis: for x being FinSequence of (FreeUnivAlgZAO (f,D)) st x in dom o1 holds ff . (o1 . x) = o2 . (ff * x) let x be FinSequence of (FreeUnivAlgZAO (f,D)); ::_thesis: ( x in dom o1 implies ff . (o1 . x) = o2 . (ff * x) ) assume A8: x in dom o1 ; ::_thesis: ff . (o1 . x) = o2 . (ff * x) reconsider xa = x as FinSequence of TS (DTConUA (f,D)) ; dom (roots xa) = dom xa by TREES_3:def_18 .= Seg (len xa) by FINSEQ_1:def_3 ; then A9: len (roots xa) = len xa by FINSEQ_1:def_3; reconsider xa = xa as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ; reconsider rxa = roots xa as FinSequence of (dom f) \/ D ; reconsider rxa = rxa as Element of ((dom f) \/ D) * by FINSEQ_1:def_11; dom o1 = (arity o1) -tuples_on the carrier of (FreeUnivAlgZAO (f,D)) by MARGREL1:22 .= { w where w is Element of the carrier of (FreeUnivAlgZAO (f,D)) * : len w = arity o1 } ; then A10: ex w being Element of the carrier of (FreeUnivAlgZAO (f,D)) * st ( x = w & len w = arity o1 ) by A8; A11: o1 = FreeOpZAO (n,f,D) by A5, A6, Def17; reconsider fx = ff * x as Element of the carrier of U1 * ; A12: dom o2 = (arity o2) -tuples_on the carrier of U1 by MARGREL1:22 .= { v where v is Element of the carrier of U1 * : len v = arity o2 } ; A13: ( len the charact of (FreeUnivAlgZAO (f,D)) = len the charact of U1 & dom the charact of (FreeUnivAlgZAO (f,D)) = Seg (len the charact of (FreeUnivAlgZAO (f,D))) ) by A1, FINSEQ_1:def_3, UNIALG_2:1; A14: Seg (len (FreeOpSeqZAO (f,D))) = dom (FreeOpSeqZAO (f,D)) by FINSEQ_1:def_3; A15: ( len (FreeOpSeqZAO (f,D)) = len f & dom f = Seg (len f) ) by Def17, FINSEQ_1:def_3; then reconsider nt = n as Symbol of (DTConUA (f,D)) by A5, A14, XBOOLE_0:def_3; reconsider nd = n as Element of (dom f) \/ D by A5, A15, A14, XBOOLE_0:def_3; A16: f = signature (FreeUnivAlgZAO (f,D)) by Th7; then A17: (signature (FreeUnivAlgZAO (f,D))) . n = arity o1 by A5, A6, A15, A14, UNIALG_1:def_4; then [nd,rxa] in REL (f,D) by A5, A15, A14, A16, A10, A9, Def7; then A18: nt ==> roots xa by LANG1:def_1; then A19: ff . (nt -tree xa) = (oper ((@ nt),U1)) /. (ff * x) by A3; @ nt = n by A18, Def15; then A20: oper ((@ nt),U1) = o2 by A5, A7, A13, A4, Def3; signature (FreeUnivAlgZAO (f,D)) = signature U1 by A1, UNIALG_2:def_1; then ( len (ff * x) = len x & arity o2 = len x ) by A5, A7, A15, A14, A16, A10, A17, FINSEQ_3:120, UNIALG_1:def_4; then A21: fx in { v where v is Element of the carrier of U1 * : len v = arity o2 } ; reconsider xa = xa as Element of (TS (DTConUA (f,D))) * by FINSEQ_1:def_11; Sym (n,f,D) = nt by A5, A15, A14, Def9; then o1 . x = nt -tree xa by A5, A8, A15, A14, A11, Def16; hence ff . (o1 . x) = o2 . (ff * x) by A19, A20, A12, A21, PARTFUN1:def_6; ::_thesis: verum end; hence ff is_homomorphism FreeUnivAlgZAO (f,D),U1 by A1, ALG_1:def_1; ::_thesis: ff | (FreeGenSetZAO (f,D)) = F A22: the carrier of (FreeUnivAlgZAO (f,D)) /\ (FreeGenSetZAO (f,D)) = FreeGenSetZAO (f,D) by XBOOLE_1:28; A23: ( dom (ff | (FreeGenSetZAO (f,D))) = (dom ff) /\ (FreeGenSetZAO (f,D)) & dom ff = the carrier of (FreeUnivAlgZAO (f,D)) ) by FUNCT_2:def_1, RELAT_1:61; A24: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (ff_|_(FreeGenSetZAO_(f,D)))_._x_=_F_._x let x be set ; ::_thesis: ( x in dom F implies (ff | (FreeGenSetZAO (f,D))) . x = F . x ) assume A25: x in dom F ; ::_thesis: (ff | (FreeGenSetZAO (f,D))) . x = F . x then x in { (root-tree t) where t is Symbol of (DTConUA (f,D)) : t in Terminals (DTConUA (f,D)) } ; then consider s being Symbol of (DTConUA (f,D)) such that A26: ( x = root-tree s & s in Terminals (DTConUA (f,D)) ) ; thus (ff | (FreeGenSetZAO (f,D))) . x = ff . x by A23, A22, A25, FUNCT_1:47 .= pi (F,s) by A2, A26 .= F . x by A26, Def20 ; ::_thesis: verum end; FreeGenSetZAO (f,D) = dom F by FUNCT_2:def_1; hence ff | (FreeGenSetZAO (f,D)) = F by A23, A22, A24, FUNCT_1:2; ::_thesis: verum end; registration let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; cluster FreeUnivAlgZAO (f,D) -> strict free ; coherence FreeUnivAlgZAO (f,D) is free proof FreeGenSetZAO (f,D) is free by Th10; hence FreeUnivAlgZAO (f,D) is free by Def6; ::_thesis: verum end; end; definition let f be non empty with_zero FinSequence of NAT ; let D be disjoint_with_NAT set ; :: original: FreeGenSetZAO redefine func FreeGenSetZAO (f,D) -> free GeneratorSet of FreeUnivAlgZAO (f,D); coherence FreeGenSetZAO (f,D) is free GeneratorSet of FreeUnivAlgZAO (f,D) by Th10; end; registration cluster non empty strict V109() quasi_total non-empty with_const_op free for UAStr ; existence ex b1 being Universal_Algebra st ( b1 is strict & b1 is free & b1 is with_const_op ) proof set D = the disjoint_with_NAT set ; set f = the non empty with_zero FinSequence of NAT ; take FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) ; ::_thesis: ( FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is strict & FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is free & FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is with_const_op ) thus ( FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is strict & FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is free & FreeUnivAlgZAO ( the non empty with_zero FinSequence of NAT , the disjoint_with_NAT set ) is with_const_op ) by Th8; ::_thesis: verum end; end;