:: 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;