begin
:: deftheorem Def1 defines disjoint_with_NAT FREEALG:def 1 :
for IT being set holds
( IT is disjoint_with_NAT iff IT misses NAT );
Lm1:
( not 0 in rng <*1*> & 0 in rng <*0 *> )
:: deftheorem Def2 defines with_zero FREEALG:def 2 :
for IT being Relation holds
( not IT is with_zero iff not 0 in rng IT );
begin
:: deftheorem FREEALG:def 3 :
canceled;
:: deftheorem Def4 defines oper FREEALG:def 4 :
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;
:: deftheorem defines GeneratorSet FREEALG:def 5 :
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
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 )
:: deftheorem Def6 defines free FREEALG:def 6 :
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 ) );
:: deftheorem Def7 defines free FREEALG:def 7 :
for IT being Universal_Algebra holds
( IT is free iff ex G being GeneratorSet of IT st G is free );
theorem
begin
:: deftheorem Def8 defines REL FREEALG:def 8 :
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 ) ) );
:: deftheorem defines DTConUA FREEALG:def 9 :
for f being non empty FinSequence of NAT
for X being set holds DTConUA f,X = DTConstrStr(# ((dom f) \/ X),(REL f,X) #);
theorem Th2:
theorem Th3:
:: deftheorem Def10 defines Sym FREEALG:def 10 :
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 :
Def11:
(
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 ) )
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
end;
:: deftheorem Def11 defines FreeOpNSG FREEALG:def 11 :
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 :
Def12:
(
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 ) )
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
end;
:: deftheorem Def12 defines FreeOpSeqNSG FREEALG:def 12 :
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 ) ) );
:: deftheorem defines FreeUnivAlgNSG FREEALG:def 13 :
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:
:: deftheorem defines FreeGenSetNSG FREEALG:def 14 :
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:
:: deftheorem Def15 defines pi FREEALG:def 15 :
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);
:: deftheorem Def16 defines @ FREEALG:def 16 :
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:
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 :
Def17:
(
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 ) )
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
end;
:: deftheorem Def17 defines FreeOpZAO FREEALG:def 17 :
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 :
Def18:
(
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 ) )
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
end;
:: deftheorem Def18 defines FreeOpSeqZAO FREEALG:def 18 :
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 ) ) );
:: deftheorem defines FreeUnivAlgZAO FREEALG:def 19 :
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:
theorem Th8:
theorem Th9:
:: deftheorem defines FreeGenSetZAO FREEALG:def 20 :
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) } ;
:: deftheorem Def21 defines pi FREEALG:def 21 :
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: