:: Free Universal Algebra Construction
:: by Beata Perkowska
::
:: Received October 20, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, ARYTM_1, CARD_1, RELAT_1, FINSEQ_1,
QUANTAL1, UNIALG_1, UNIALG_2, FUNCT_1, MSAFREE, TARSKI, STRUCT_0,
FINSEQ_2, PRELAMB, CQC_SIM1, MSUALG_3, FUNCOP_1, PARTFUN1, FUNCT_2,
NAT_1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, CARD_3, TREES_2,
QC_LANG1, FREEALG;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1,
RELSET_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, FUNCOP_1, FINSEQ_2,
TREES_2, TREES_3, TREES_4, MARGREL1, STRUCT_0, UNIALG_1, UNIALG_2, LANG1,
DTCONSTR, PRE_POLY, ALG_1;
constructors DOMAIN_1, FINSEQOP, DTCONSTR, ALG_1, RELSET_1, PRE_POLY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, XREAL_0,
FINSEQ_1, FINSEQ_2, TREES_3, STRUCT_0, UNIALG_2, DTCONSTR, CARD_1,
RELSET_1, MARGREL1, FUNCT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, UNIALG_2, DTCONSTR, XBOOLE_0, MARGREL1;
equalities UNIALG_2, FINSEQ_2, FUNCOP_1, ORDINAL1;
expansions TARSKI, UNIALG_2, DTCONSTR, XBOOLE_0, MARGREL1;
theorems FINSEQ_1, FINSEQ_2, PARTFUN1, FUNCT_1, FUNCT_2, NAT_1, ZFMISC_1,
UNIALG_1, ALG_1, TARSKI, FUNCOP_1, UNIALG_2, LANG1, DTCONSTR, RELAT_1,
XBOOLE_0, XBOOLE_1, TREES_3, MARGREL1, FINSEQ_3, CARD_1;
schemes PARTFUN1, FINSEQ_1, RELSET_1, DTCONSTR;
begin
::
:: Preliminaries
::
reserve x,y for set,
n for Nat;
definition
let IT be set;
attr IT is disjoint_with_NAT means
:Def1:
IT misses NAT;
end;
registration
cluster non empty disjoint_with_NAT for set;
existence
proof
take X = {-1};
thus X is non empty;
now
assume X meets NAT;
then consider x being object such that
A1: x in X and
A2: x in NAT by XBOOLE_0:3;
reconsider x as Nat by A2;
x = -1 by A1,TARSKI:def 1;
hence contradiction by NAT_1:2;
end;
hence thesis;
end;
end;
Lm1: not 0 in rng <*1*> & 0 in rng <*0*>
proof
rng <*0*> = {0} & rng <*1*> = {1} by FINSEQ_1:38;
hence thesis by TARSKI:def 1;
end;
notation
let IT be Relation;
antonym IT is with_zero for IT is non-empty;
synonym IT is without_zero for IT is non-empty;
end;
definition
let IT be Relation;
redefine attr IT is with_zero means :: redefines with_zero (FREEALG, antonym) → non-empty (RELAT_1, definition)
:Def2:
0 in rng IT;
compatibility by RELAT_1:def 9;
end;
registration
cluster non empty with_zero for FinSequence of NAT;
existence
proof
reconsider f = <*0*> as FinSequence of NAT;
take f;
thus f is non empty;
thus 0 in rng f by Lm1;
end;
cluster non empty without_zero for FinSequence of NAT;
existence
proof
reconsider f = <*1*> as FinSequence of NAT;
take f;
thus f is non empty;
thus not 0 in rng f by Lm1;
end;
end;
begin
::
:: Free Universal Algebra - General Notions
::
definition
let U1 be Universal_Algebra, n be Nat;
assume
A1: n in dom (the charact of U1);
func oper(n,U1) -> operation of U1 equals
:Def3:
(the charact of U1).n;
coherence by A1,FUNCT_1:def 3;
end;
definition
let U0 be Universal_Algebra;
mode GeneratorSet of U0 -> Subset of U0 means
for A being Subset of U0 st A
is opers_closed & it c= A holds A = the carrier of U0;
existence
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;
thus thesis;
end;
end;
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;
let B be Subset of A such that
A1: B is opers_closed;
let x be object;
assume x in Constants A;
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;
consider s being object such that
A7: s in dom o and
A8: a = o.s by A5,FUNCT_1:def 3;
reconsider 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;
then
A10: s is FinSequence of B by FINSEQ_1:def 4;
len s = 0 by A7,A9;
hence thesis by A2,A4,A8,A10,A6;
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;
let G be Subset of A;
assume
A1: G <> {} or Constants A <> {};
thus G is GeneratorSet of A implies the carrier of GenUnivAlg G = the
carrier 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;
G c= C & C is opers_closed by UNIALG_2:def 7,def 12;
hence thesis by A2;
end;
assume
A3: the carrier of GenUnivAlg G = the carrier of A;
let B be Subset of A such that
A4: B is opers_closed and
A5: G c= B;
reconsider C = B as non empty Subset of A by A1,A4,A5,Lm2,XBOOLE_1:3;
thus B c= the carrier of A;
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 thesis;
end;
definition
let U0 be Universal_Algebra;
let IT be GeneratorSet of U0;
attr IT is free means
for U1 be Universal_Algebra st U0,U1
are_similar holds for f be Function of IT,the carrier of U1 ex h be Function of
U0,U1 st h is_homomorphism & h|IT = f;
end;
definition
let IT be Universal_Algebra;
attr IT is free means
:Def6:
ex G being GeneratorSet of IT st G is free;
end;
registration
cluster free strict for Universal_Algebra;
existence
proof
set x = the set;
reconsider A = {x} as non empty set;
set a = the Element of A;
reconsider w = <*>A .--> 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(U0) is quasi_total & the charact of(U0) is homogeneous
by MARGREL1:20;
A2: the charact of(U0) is non-empty by MARGREL1:20;
A3: len the charact of(U0) = 1 by FINSEQ_1:39;
reconsider U0 as Universal_Algebra by A1,A2,UNIALG_1:def 1,def 2,def 3;
A4: dom the charact of(U0) = {1} by A3,FINSEQ_1:2,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;
A5: GenUnivAlg( {}(the carrier of U0) ) = U0
proof
set P = {}(the carrier of U0);
reconsider B = the carrier of GenUnivAlg(P) 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 be Nat st n in dom the charact of(U0) holds (the charact of(
U0)).n =(Opers(U0,B)).n
proof
let n be Nat;
assume
A8: n in dom the charact of(U0);
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 thesis by A7,UNIALG_2:4;
end;
then the charact of(U0) = Opers(U0,B) by A6,FINSEQ_1:13
.= the charact of GenUnivAlg(P) by UNIALG_2:def 7;
hence thesis by A7;
end;
A10: dom o0 = {<*>A} by FUNCOP_1:13;
now
<*>A in dom o0 by A10,TARSKI:def 1;
hence ex x being FinSequence st x in dom o0;
let x be FinSequence;
assume x in dom o0;
then x = <*>A by A10,TARSKI:def 1;
hence len x = 0;
end;
then
A11: arity o0 = 0 by MARGREL1:def 25;
A12: {} in {<*>A} by TARSKI:def 1;
then o0.<*>A = a by FUNCOP_1:7;
then a in rng o0 by A10,A12,FUNCT_1:def 3;
then a in Constants U0 by A11;
then reconsider G = {}(the carrier of U0) as GeneratorSet of U0 by A5,Lm3;
now
take G;
now
let U1 be Universal_Algebra;
A13: 1 in {1} by TARSKI:def 1;
assume
A14: U0,U1 are_similar;
then
A15: signature U0 = signature U1;
len the charact of(U1) = 1 by A3,A14,UNIALG_2:1;
then dom the charact of(U1) = {1} by FINSEQ_1:2,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;
consider aa be object 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;
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
let n be Nat;
assume n in dom the charact of(U0);
then
A20: n = 1 by A4,TARSKI:def 1;
let 0o be operation of U0,1o be operation of U1;
assume that
A21: 0o=(the charact of U0).n and
A22: 1o=(the charact of U1).n;
let y be FinSequence of U0;
assume
A23: y in dom 0o;
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;
end;
hence h is_homomorphism by A14,ALG_1:def 1;
f = {};
hence h|G = f;
end;
hence G is free;
end;
hence thesis;
end;
end;
registration
let U0 be free Universal_Algebra;
cluster free for GeneratorSet of U0;
existence by Def6;
end;
theorem
for U0 be strict Universal_Algebra,A be 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,A be Subset of U0 such that
A1: Constants U0 <> {} or A <> {};
thus A is GeneratorSet of U0 implies GenUnivAlg(A) = U0
proof
assume A is GeneratorSet of 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 thesis by A2,UNIALG_2:12;
end;
assume GenUnivAlg(A) = U0;
hence thesis by A1,Lm3;
end;
begin
::
:: Construction of a Decorated Tree Structure for Free Universal Algebra
::
definition
let f be non empty FinSequence of NAT, X be set;
func REL(f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X)*) means
:Def7:
for a be Element of (dom f) \/ X, b be Element of ((dom f) \/ X)* holds [a,b]
in it iff a in dom f & f.a = len b;
existence
proof
set A = (dom f) \/ X;
defpred P[Element of A, Element of A*] means $1 in dom f & f.$1 = len $2;
consider R being Relation of A,A* such that
A1: for x being (Element of A), y being Element of A* holds [x,y] in R
iff P[x,y] from RELSET_1:sch 2;
take R;
let a be Element of A, b be Element of A*;
thus thesis by A1;
end;
uniqueness
proof
set A = (dom f) \/ X;
let R,T be Relation of A,A*;
assume that
A2: for a be Element of A, b be Element of A* holds [a,b] in R iff a
in dom f & f.a = len b and
A3: for a be Element of A, b be Element of A* holds [a,b] in T iff a
in dom f & f.a = len b;
for x,y being object holds [x,y] in R iff [x,y] in T
proof
let x,y be object;
thus [x,y] in R implies [x,y] in T
proof
assume
A4: [x,y] in R;
then reconsider x1=x as Element of A by ZFMISC_1:87;
reconsider y1=y as Element of A* 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 thesis by A3,A5;
end;
assume
A6: [x,y] in T;
then reconsider x1=x as Element of A by ZFMISC_1:87;
reconsider y1=y as Element of A* 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 thesis by A2,A7;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let f be non empty FinSequence of NAT, X be set;
func DTConUA(f,X) -> strict DTConstrStr equals
DTConstrStr (# (dom f) \/ X,
REL(f,X) #);
correctness;
end;
registration
let f be non empty FinSequence of NAT, X be set;
cluster DTConUA(f,X) -> non empty;
coherence;
end;
theorem Th2:
for f be non empty FinSequence of NAT, X be set holds (Terminals
(DTConUA(f,X))) c= X & NonTerminals(DTConUA(f,X)) = dom f
proof
let f be non empty FinSequence of NAT, X be set;
set A = DTConUA(f,X), D = (dom f) \/ X;
A1: the carrier of A = (Terminals A) \/ (NonTerminals A) by LANG1:1;
(Terminals A) misses (NonTerminals A) by DTCONSTR:8;
then
A2: (Terminals A) /\ (NonTerminals A) = {};
thus Terminals A c= X
proof
let x be object;
assume
A3: x in Terminals A;
then reconsider xd = x as Element of D by A1,XBOOLE_0:def 3;
reconsider xa = x as Element of (the carrier of A) by A1,A3,XBOOLE_0:def 3;
A4: now
A5: rng f c= NAT by FINSEQ_1:def 4;
assume
A6: x in dom f;
then f.x in rng f by FUNCT_1:def 3;
then reconsider fx = f.x as Nat by A5;
reconsider a = fx |-> xd as FinSequence of D;
reconsider a as Element of D* 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 A: ex n be FinSequence st t ==> n};
then x in NonTerminals A by LANG1:def 3;
hence contradiction by A2,A3,XBOOLE_0:def 4;
end;
x in (dom f) \/ X by A1,A3,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 3;
end;
thus NonTerminals A c= dom f
proof
let x be object;
assume x in NonTerminals A;
then x in {t where t is Symbol of A: ex n be FinSequence st t ==> n} by
LANG1:def 3;
then consider t be Symbol of A such that
A7: x = t and
A8: ex n be FinSequence st t ==> n;
consider n be FinSequence such that
A9: t ==>n by A8;
[t,n] in the Rules of A by A9,LANG1:def 1;
then reconsider n as Element of D* by ZFMISC_1:87;
reconsider t as Element of D;
[t,n] in REL(f,X) by A9,LANG1:def 1;
hence thesis by A7,Def7;
end;
let x be object;
A10: rng f c= NAT by FINSEQ_1:def 4;
assume
A11: x in dom f;
then reconsider xa = x as Symbol of A by XBOOLE_0:def 3;
f.x in rng f by A11,FUNCT_1:def 3;
then reconsider fx = f.x as Nat by A10;
reconsider xd = x as Element of D by A11,XBOOLE_0:def 3;
reconsider a = fx |-> xd as FinSequence of D;
reconsider a as Element of D* 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 A: ex n be FinSequence st t ==> n};
hence thesis by LANG1:def 3;
end;
theorem Th3:
for f be non empty FinSequence of NAT, X be disjoint_with_NAT set
holds (Terminals (DTConUA(f,X))) = X
proof
let f be non empty FinSequence of NAT, X be disjoint_with_NAT set;
set A = DTConUA(f,X);
thus Terminals A c= X by Th2;
let x be object;
assume
A1: x in X;
A2: NonTerminals A = dom f by Th2;
A3: not x in NonTerminals A by A2,A1,Def1,XBOOLE_0:3;
the carrier of A = (Terminals A) \/ (NonTerminals A) & x in (dom f) \/ X
by A1,LANG1:1,XBOOLE_0:def 3;
hence thesis by A3,XBOOLE_0:def 3;
end;
registration
let f be non empty FinSequence of NAT, X be set;
cluster DTConUA(f,X) -> with_nonterminals;
coherence
by Th2;
end;
registration
let f be with_zero non empty FinSequence of NAT, X be set;
cluster DTConUA(f,X) -> with_nonterminals with_useful_nonterminals;
coherence
proof
set A = DTConUA(f,X), D = (dom f) \/ X;
A is with_useful_nonterminals
proof
set e = <*>(TS A);
let s be Symbol of A;
assume
A1: s in NonTerminals A;
A2: rng f c= NAT by FINSEQ_1:def 4;
NonTerminals A = dom f by Th2;
then f.s in rng f by A1,FUNCT_1:def 3;
then reconsider fs = f.s as Nat by A2;
reconsider sd = s as Element of D;
roots e = <*> D by DTCONSTR:3;
then reconsider re = (roots e) as Element of D*;
0 in rng f by Def2;
then consider x being object such that
A3: x in dom f and
A4: f.x = 0 by FUNCT_1:def 3;
A5: NonTerminals A = dom f by Th2;
then reconsider s0 = x as Symbol of A by A3;
set p = fs |-> (s0-tree e);
A6: len p = fs by CARD_1:def 7;
len re = 0 by DTCONSTR:3;
then [s0,roots e] in the Rules of A by A3,A4,Def7;
then s0 ==> roots e by LANG1:def 1;
then
A7: s0-tree(e) in (TS A) by DTCONSTR:def 1;
A8: rng p c= TS A
proof
let y be object;
assume y in rng p;
then
A9: ex n being Nat st n in dom p & p.n = y by FINSEQ_2:10;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by A7,A6,A9,FUNCOP_1:7;
end;
dom(roots p) = dom p by TREES_3:def 18
.= Seg len p by FINSEQ_1:def 3;
then
A10: len(roots p) = fs by A6,FINSEQ_1:def 3;
reconsider p as FinSequence of TS A by A8,FINSEQ_1:def 4;
take p;
reconsider p as FinSequence of FinTrees the carrier of A;
reconsider rp =roots p as Element of D* by FINSEQ_1:def 11;
[sd,rp] in REL(f,X) by A1,A5,A10,Def7;
hence thesis by LANG1:def 1;
end;
hence thesis;
end;
end;
registration
let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
cluster DTConUA(f,D) -> with_terminals with_nonterminals
with_useful_nonterminals;
coherence
proof
set A = DTConUA(f,D);
A1: NonTerminals A = dom f by Th2;
A2: Terminals A = D by Th3;
A is with_useful_nonterminals
proof
set d = the Element of D;
let s be Symbol of A;
reconsider sd = d as Symbol of A by XBOOLE_0:def 3;
A3: rng f c= NAT by FINSEQ_1:def 4;
assume
A4: s in NonTerminals A;
then f.s in rng f by A1,FUNCT_1:def 3;
then reconsider fs = f.s as Nat by A3;
reconsider sdd = s as Element of ((dom f) \/ D);
set p = fs |-> (root-tree sd);
A5: len p = fs by CARD_1:def 7;
A6: root-tree sd in TS(A) by A2,DTCONSTR:def 1;
A7: rng p c= TS A
proof
let y be object;
assume y in rng p;
then consider n being Nat such that
A8: n in dom p and
A9: p.n = y by FINSEQ_2:10;
n in Seg len p by A8,FINSEQ_1:def 3;
hence thesis by A6,A5,A9,FUNCOP_1:7;
end;
dom(roots p) = dom p by TREES_3:def 18
.= Seg len p by FINSEQ_1:def 3;
then
A10: len(roots p) = fs by A5,FINSEQ_1:def 3;
reconsider p as FinSequence of (TS A) by A7,FINSEQ_1:def 4;
take p;
reconsider p as FinSequence of FinTrees the carrier of A;
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 thesis by LANG1:def 1;
end;
hence thesis by A2;
end;
end;
definition
let f be non empty FinSequence of NAT, X be set, n be Nat;
assume
A1: n in dom f;
func Sym(n,f,X) -> Symbol of DTConUA(f,X) equals
:Def9:
n;
coherence by A1,XBOOLE_0:def 3;
end;
begin
::
:: Construction of Free Universal Algebra for Non Empty Set of Generators and
:: Given Signature
definition
let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set,
n be Nat;
assume
A1: n in dom f;
func FreeOpNSG(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
DTConUA(f,D))*, TS(DTConUA(f,D)) means
:Def10:
dom it = (f/.n)-tuples_on TS(
DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
it.p = Sym(n,f,D)-tree(p);
existence
proof
set A = DTConUA(f,D), i = f/.n, Y = (dom f) \/ D, smm = Sym(n,f,D);
defpred P[object,object] means
$1 in i-tuples_on (TS A) & for p be FinSequence
of (TS A) st p = $1 holds $2 = smm-tree(p);
set tu = {s where s is Element of (TS A)*: len s = f/.n};
A2: i = f.n by A1,PARTFUN1:def 6;
A3: for x,y being object st x in (TS A)* & P[x,y] holds y in (TS A)
proof
reconsider sm = Sym(n,f,D) as Element of Y;
let x,y be object;
assume that
x in (TS A)* and
A4: P[x,y];
consider s be Element of (TS A)* such that
A5: s = x and
A6: len s = i by A4;
A7: y = Sym(n,f,D)-tree(s) by A4,A5;
reconsider s as FinSequence of (TS A);
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) = i by A6,FINSEQ_1:def 3;
reconsider s as FinSequence of FinTrees the carrier of A;
reconsider rs = roots s as Element of Y* 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 thesis by A7,DTCONSTR:def 1;
end;
A9: for x,y1,y2 be object st x in (TS A)* & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object;
assume that
x in (TS A)* and
A10: P[x,y1] and
A11: P[x,y2];
consider s be Element of (TS A)* such that
A12: s = x and
len s = i by A10;
y1 = Sym(n,f,D)-tree(s) by A10,A12;
hence thesis by A11,A12;
end;
consider F being PartFunc of (TS A)*,(TS A) such that
A13: for x be object holds x in dom F iff x in (TS A)* &
ex y being object st P[x,y] and
A14: for x be object st x in dom F holds P[x,F.x] from PARTFUN1:sch 2(A3,
A9);
A15: dom F = i-tuples_on (TS A)
proof
thus dom F c= i-tuples_on(TS A)
proof
let x be object;
assume x in dom F;
then ex y being object st P[x,y] by A13;
hence thesis;
end;
reconsider sm = smm as Symbol of A;
let x be object;
assume x in i-tuples_on(TS A);
then consider s be Element of (TS A)* such that
A16: s = x and
A17: len s = i;
P[s,sm-tree(s)] by A17;
hence thesis by A13,A16;
end;
A18: for x,y be FinSequence of TS(A) st len x=len y & x in dom F holds y
in dom F
proof
let x,y be FinSequence of TS(A);
assume that
A19: len x = len y and
A20: x in dom F;
reconsider sy = y as Element of (TS A)* by FINSEQ_1:def 11;
ex sx be Element of (TS A)* st sx = x & len sx = f/.n by A15,A20;
then sy in tu by A19;
hence thesis by A15;
end;
A21: ex x being FinSequence st x in dom F
proof
set a = the Element of i-tuples_on(TS A);
a in dom F by A15;
hence ex x being FinSequence st x in dom F;
end;
dom F is with_common_domain
proof
let x,y be FinSequence;
assume x in dom F & y in dom F;
then (ex sx be Element of (TS A)* st sx = x & len sx = f/.n )& ex sy be
Element of (TS A)* st sy = y & len sy = f/.n by A15;
hence thesis;
end;
then reconsider
F as homogeneous quasi_total non empty PartFunc of (TS A)*, TS(
A) by A18,A21,MARGREL1:def 21,def 22;
take F;
thus dom F = i-tuples_on (TS A) by A15;
let p be FinSequence of (TS A);
assume p in dom F;
hence thesis by A14;
end;
uniqueness
proof
set A = TS DTConUA(f,D);
let f1,f2 be homogeneous quasi_total non empty PartFunc of A*,A;
assume that
A22: dom f1 = (f/.n)-tuples_on A and
A23: for p be FinSequence of A st p in dom f1 holds f1.p = Sym(n,f,D)
-tree(p) and
A24: dom f2 = (f/.n)-tuples_on A and
A25: for p be FinSequence of A st p in dom f2 holds f2.p = Sym(n,f,D) -tree(p);
now
let x be object;
assume
A26: x in (f/.n)-tuples_on A;
then consider s be Element of A* 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;
end;
hence thesis by A22,A24,FUNCT_1:2;
end;
end;
definition
let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
func FreeOpSeqNSG(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
:Def11:
len it = len f & for n st n in dom it holds it.n = FreeOpNSG(n,f,D);
existence
proof
defpred P[Nat,set] means $2 = FreeOpNSG($1,f,D);
set A = TS(DTConUA(f,D));
A1: for n be Nat st n in Seg len f ex x be Element of PFuncs(A*,A) st P[n, x]
proof
let n be Nat;
assume n in Seg len f;
reconsider O=FreeOpNSG(n,f,D) as Element of PFuncs(A*,A) by PARTFUN1:45;
take O;
thus thesis;
end;
consider p be FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len f & for n be Nat st n in Seg len f holds P[n,p.n]
from FINSEQ_1:sch 5(A1);
reconsider p as PFuncFinSequence of A;
take p;
thus len p = len f by A2,FINSEQ_1:def 3;
let n;
assume n in dom p;
hence thesis by A2;
end;
uniqueness
proof
let f1,f2 be PFuncFinSequence of TS DTConUA(f,D);
assume that
A3: len f1 = len f and
A4: for n st n in dom f1 holds f1.n = FreeOpNSG(n,f,D) and
A5: len f2 = len f and
A6: for n st n in dom f2 holds f2.n = FreeOpNSG(n,f,D);
for n being Nat st n in dom f1 holds f1.n = f2.n
proof
let n be Nat;
A7: dom f1 = Seg len f1 & dom f2 = Seg len f2 by FINSEQ_1:def 3;
assume
A8: n in dom f1;
then f1.n = FreeOpNSG(n,f,D) by A4;
hence thesis by A3,A5,A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
definition
let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
func FreeUnivAlgNSG(f,D) -> strict Universal_Algebra equals
UAStr (# TS(
DTConUA(f,D)), FreeOpSeqNSG(f,D)#);
coherence
proof
set A = TS DTConUA(f,D), AA = UAStr (# A, FreeOpSeqNSG(f,D) #);
for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
= (the charact of AA).n holds h is quasi_total
proof
let n be Nat,h be PartFunc of A*,A;
assume n in dom the charact of(AA) & h = (the charact of AA).n;
then h = FreeOpNSG(n,f,D) by Def11;
hence thesis;
end;
then
A1: the charact of(AA) is quasi_total;
for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
= (the charact of AA).n holds h is homogeneous
proof
let n be Nat,h be PartFunc of A*,A;
assume n in dom the charact of(AA) & h = (the charact of AA).n;
then h = FreeOpNSG(n,f,D) by Def11;
hence thesis;
end;
then
A2: the charact of(AA) is homogeneous;
for n be object st n in dom the charact of(AA) holds (the charact of AA)
.n is non empty
proof
let n be object;
assume
A3: n in dom the charact of(AA);
then reconsider n as Nat;
(the charact of AA).n = FreeOpNSG(n,f,D) by A3,Def11;
hence thesis;
end;
then
A4: the charact of(AA) is non-empty by FUNCT_1:def 9;
len FreeOpSeqNSG(f,D) = len f by Def11;
then the charact of(AA) <> {};
hence thesis by A1,A2,A4,UNIALG_1:def 1,def 2,def 3;
end;
end;
theorem Th4:
for f be non empty FinSequence of NAT, D be disjoint_with_NAT non
empty set holds signature (FreeUnivAlgNSG(f,D)) = f
proof
let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
set fa = FreeUnivAlgNSG(f,D), A = TS DTConUA(f,D);
A1: len the charact of(fa)= len f by Def11;
A2: len(signature fa) = len the charact of(fa) by UNIALG_1:def 4;
then
A3: dom (signature fa) = Seg len f by A1,FINSEQ_1:def 3;
now
let n be Nat;
reconsider h = FreeOpNSG(n,f,D) as homogeneous quasi_total non empty
PartFunc of (the carrier of fa)*,(the carrier of fa);
A4: dom h=(arity h)-tuples_on (the carrier of fa) by MARGREL1:22;
assume
A5: n in dom (signature fa);
then
A6: n in dom f by A3,FINSEQ_1:def 3;
then dom h = (f/.n)-tuples_on A 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 fa).n = FreeOpNSG(n,f,D) by Def11;
hence (signature fa).n = arity h by A5,UNIALG_1:def 4
.= f.n by A6,A7,PARTFUN1:def 6;
end;
hence thesis by A2,A1,FINSEQ_2:9;
end;
definition
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
func FreeGenSetNSG(f,D) -> Subset of FreeUnivAlgNSG(f,D) equals
{root-tree s
where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
coherence
proof
set X = DTConUA(f,D), A = {root-tree d where d is Symbol of X: d in
Terminals X};
A c= the carrier of FreeUnivAlgNSG(f,D)
proof
let x be object;
assume x in A;
then ex d be Symbol of X st x = root-tree d & d in Terminals X;
hence thesis by DTCONSTR:def 1;
end;
hence thesis;
end;
end;
theorem Th5:
for f be non empty FinSequence of NAT,D be non empty
disjoint_with_NAT set holds FreeGenSetNSG(f,D) is non empty
proof
let f be non empty FinSequence of NAT,D be disjoint_with_NAT non empty set;
set X = DTConUA(f,D);
set d = the Element of D;
reconsider d1 = d as Symbol of X by XBOOLE_0:def 3;
Terminals X = D by Th3;
then root-tree d1 in {root-tree k where k is Symbol of X: k in Terminals X};
hence thesis;
end;
definition
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
redefine func FreeGenSetNSG(f,D) -> GeneratorSet of FreeUnivAlgNSG(f,D); :: redefines FreeGenSetNSG (FREEALG, definition)
coherence
proof
set fgs = FreeGenSetNSG(f,D), fua = FreeUnivAlgNSG(f,D);
A1: the carrier of GenUnivAlg(fgs) = the carrier of fua
proof
set A = DTConUA(f,D);
defpred P[DecoratedTree of the carrier of A] means $1 in the carrier of
GenUnivAlg(fgs);
the carrier of GenUnivAlg(fgs) is Subset of fua by UNIALG_2:def 7;
hence the carrier of GenUnivAlg(fgs) c= the carrier of fua;
A2: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts & for t being DecoratedTree of the carrier of A st t in rng ts holds P
[t] holds P[nt-tree ts]
proof
reconsider B = the carrier of GenUnivAlg(fgs) as Subset of fua by
UNIALG_2:def 7;
let s be Symbol of A,p be FinSequence of TS(A);
assume that
A3: s ==> roots p and
A4: for t be DecoratedTree of the carrier of A st t in rng p
holds t in the carrier of GenUnivAlg(fgs);
rng p c= the carrier of GenUnivAlg(fgs)
proof
let x be object;
assume
A5: x in rng p;
rng p c= FinTrees(the carrier of A) by FINSEQ_1:def 4;
then reconsider
x1 = x as Element of FinTrees(the carrier of A) by A5;
x1 in the carrier of GenUnivAlg(fgs) by A4,A5;
hence thesis;
end;
then reconsider
cp = p as FinSequence of the carrier of GenUnivAlg(fgs) by
FINSEQ_1:def 4;
reconsider tp = p as Element of (TS A)* by FINSEQ_1:def 11;
[s,roots p] in the Rules of A 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 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 fua by A7,A9
,Def11;
B is opers_closed by UNIALG_2:def 7;
then
A10: B is_closed_on o;
A11: dom FreeOpNSG(ns,f,D) = (f/.ns)-tuples_on TS(A) by A7,Def10;
dom o = (arity o)-tuples_on the carrier of fua 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 A)* : len w = f/.ns};
then o.cp = Sym(ns,f,D)-tree p by A7,A11,Def10
.= s-tree p by A7,Def9;
hence thesis by A10,A13,A12;
end;
let x be object;
assume
A14: x in the carrier of fua;
then reconsider x1 = x as Element of FinTrees(the carrier of A);
A15: x1 in TS A by A14;
A16: for s being Symbol of A st s in Terminals A holds P[root-tree s]
proof
let s be Symbol of A;
assume s in Terminals A;
then
A17: root-tree s in {root-tree q where q is Symbol of A: q in Terminals A};
fgs c= the carrier of GenUnivAlg(fgs) by UNIALG_2:def 12;
hence thesis by A17;
end;
for t being DecoratedTree of the carrier of A st t in TS A holds P[
t] from DTCONSTR:sch 7(A16,A2);
hence thesis by A15;
end;
fgs <> {} by Th5;
hence thesis by A1,Lm3;
end;
end;
definition
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set,
C be non empty set, s be Symbol of (DTConUA(f,D)), 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:
F.(root-tree s);
coherence
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 thesis;
end;
end;
definition
let f be non empty FinSequence of NAT, D be set, s be Symbol of (DTConUA(f,D
));
given p be FinSequence such that
A1: s ==> p;
func @s -> Nat equals
:Def15:
s;
coherence
proof
reconsider s0 = s as Element of ((dom f) \/ D);
set A = DTConUA(f,D);
[s,p] in the Rules of A 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 thesis;
end;
end;
theorem Th6:
for f be non empty FinSequence of NAT,D be non empty
disjoint_with_NAT set holds FreeGenSetNSG(f,D) is free
proof
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
set fgs = FreeGenSetNSG(f,D), fua = FreeUnivAlgNSG(f,D);
let U1 be Universal_Algebra;
assume
A1: fua,U1 are_similar;
set A = DTConUA(f,D), c1 = the carrier of U1, cf = the carrier of fua;
let F be Function of fgs,the carrier of U1;
deffunc F(Symbol of A) = pi(F,$1);
deffunc G(Symbol of A,FinSequence,set) = (oper(@$1,U1))/.$3;
consider ff being Function of TS(A), c1 such that
A2: for t being Symbol of A st t in Terminals A holds ff.(root-tree t) =
F(t) and
A3: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts holds ff.(nt-tree ts) = G(nt,roots ts,ff * ts) from DTCONSTR:sch 8;
reconsider ff as Function of fua,U1;
take ff;
for n being Nat st n in dom the charact of(fua) for o1 be
operation of fua, o2 be operation of U1 st o1=(the charact of fua).n & o2=(the
charact of U1).n for x be FinSequence of fua 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 Nat;
assume
A5: n in dom the charact of fua;
let o1 be operation of fua, o2 be operation of U1;
assume that
A6: o1=(the charact of fua).n and
A7: o2=(the charact of U1).n;
let x be FinSequence of fua;
assume
A8: x in dom o1;
reconsider xa = x as FinSequence of TS(A);
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 as FinSequence of FinTrees the carrier of A;
reconsider rxa = roots xa as FinSequence of ((dom f) \/ D);
reconsider rxa as Element of ((dom f) \/ D)* by FINSEQ_1:def 11;
dom o1 = (arity o1)-tuples_on cf by MARGREL1:22
.= {w where w is Element of cf* : len w = arity o1};
then
A10: ex w be Element of cf* 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 c1*;
A12: dom o2 = (arity o2)-tuples_on c1 by MARGREL1:22
.= {v where v is Element of c1*: len v = arity o2};
A13: len the charact of(fua) = len the charact of(U1) & Seg len the
charact of( fua) = dom the charact of(fua) 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 A 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 fua by Th4;
then
A17: (signature fua).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 fua = signature U1 by A1;
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 c1*: len v = arity o2};
reconsider xa as Element of (TS A)* 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 thesis by A19,A20,A12,A21,PARTFUN1:def 6;
end;
hence ff is_homomorphism by A1,ALG_1:def 1;
A22: (the carrier of fua) /\ fgs = fgs by XBOOLE_1:28;
A23: dom (ff|fgs) = dom ff /\ fgs & dom ff = (the carrier of fua) by
FUNCT_2:def 1,RELAT_1:61;
A24: now
let x be object;
assume
A25: x in dom F;
then x in {root-tree t where t is Symbol of A: t in Terminals A};
then consider s be Symbol of A such that
A26: x = root-tree s & s in Terminals A;
thus (ff|fgs).x = ff.x by A23,A22,A25,FUNCT_1:47
.= pi(F,s) by A2,A26
.= F.x by A26,Def14;
end;
fgs = dom F by FUNCT_2:def 1;
hence thesis by A23,A22,A24,FUNCT_1:2;
end;
registration
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
cluster FreeUnivAlgNSG(f,D) -> free;
coherence
proof
FreeGenSetNSG(f,D) is free by Th6;
hence thesis;
end;
end;
definition
let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
redefine func FreeGenSetNSG(f,D) -> free GeneratorSet of FreeUnivAlgNSG(f,D); :: redefines FreeGenSetNSG (FREEALG, definition)
coherence by Th6;
end;
begin
::
:: Construction of Free Universal Algebra for Given Signature
:: (with at Last One Zero Argument Operation) and Set of Generators
::
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
n be Nat;
assume
A1: n in dom f;
func FreeOpZAO(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
DTConUA(f,D))*, TS(DTConUA(f,D)) means
:Def16:
dom it = (f/.n)-tuples_on TS(
DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
it.p = Sym(n,f,D)-tree(p);
existence
proof
set A = DTConUA(f,D), i = f/.n, Y = (dom f) \/ D, smm = Sym(n,f,D);
defpred P[object,object] means
$1 in i-tuples_on (TS A) & for p be FinSequence
of (TS A) st p = $1 holds $2 = smm-tree(p);
set tu = {s where s is Element of (TS A)*: len s = f/.n};
A2: i = f.n by A1,PARTFUN1:def 6;
A3: for x,y being object st x in (TS A)* & P[x,y] holds y in (TS A)
proof
reconsider sm = Sym(n,f,D) as Element of Y;
let x,y be object;
assume that
x in (TS A)* and
A4: P[x,y];
consider s be Element of (TS A)* such that
A5: s = x and
A6: len s = i by A4;
A7: y = Sym(n,f,D)-tree(s) by A4,A5;
reconsider s as FinSequence of (TS A);
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) = i by A6,FINSEQ_1:def 3;
reconsider s as FinSequence of FinTrees the carrier of A;
reconsider rs = roots s as Element of Y* 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 thesis by A7,DTCONSTR:def 1;
end;
A9: for x,y1,y2 be object st x in (TS A)* & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object;
assume that
x in (TS A)* and
A10: P[x,y1] and
A11: P[x,y2];
consider s be Element of (TS A)* such that
A12: s = x and
len s = i by A10;
y1 = Sym(n,f,D)-tree(s) by A10,A12;
hence thesis by A11,A12;
end;
consider F being PartFunc of (TS A)*,(TS A) such that
A13: for x be object holds x in dom F iff x in (TS A)* &
ex y being object st P[x,y] and
A14: for x be object st x in dom F holds P[x,F.x] from PARTFUN1:sch 2(A3,
A9);
A15: dom F = i-tuples_on (TS A)
proof
thus dom F c= i-tuples_on(TS A)
proof
let x be object;
assume x in dom F;
then ex y being object st P[x,y] by A13;
hence thesis;
end;
reconsider sm = smm as Symbol of A;
let x be object;
assume x in i-tuples_on(TS A);
then consider s be Element of (TS A)* such that
A16: s = x and
A17: len s = i;
P[s,sm-tree(s)] by A17;
hence thesis by A13,A16;
end;
A18: for x,y be FinSequence of TS(A) st len x=len y & x in dom F holds y
in dom F
proof
let x,y be FinSequence of TS(A);
assume that
A19: len x = len y and
A20: x in dom F;
reconsider sy = y as Element of (TS A)* by FINSEQ_1:def 11;
ex sx be Element of (TS A)* st sx = x & len sx = f/.n by A15,A20;
then sy in tu by A19;
hence thesis by A15;
end;
A21: ex x being FinSequence st x in dom F
proof
set a = the Element of i-tuples_on(TS A);
a in dom F by A15;
hence ex x being FinSequence st x in dom F;
end;
dom F is with_common_domain
proof
let x,y be FinSequence;
assume x in dom F & y in dom F;
then (ex sx be Element of (TS A)* st sx = x & len sx = f/.n )& ex sy be
Element of (TS A)* st sy = y & len sy = f/.n by A15;
hence thesis;
end;
then reconsider
F as homogeneous quasi_total non empty PartFunc of (TS A)*, TS(
A) by A18,A21,MARGREL1:def 21,def 22;
take F;
thus dom F = i-tuples_on (TS A) by A15;
let p be FinSequence of (TS A);
assume p in dom F;
hence thesis by A14;
end;
uniqueness
proof
set A = TS DTConUA(f,D);
let f1,f2 be homogeneous quasi_total non empty PartFunc of A*,A;
assume that
A22: dom f1 = (f/.n)-tuples_on A and
A23: for p be FinSequence of A st p in dom f1 holds f1.p = Sym(n,f,D)
-tree(p) and
A24: dom f2 = (f/.n)-tuples_on A and
A25: for p be FinSequence of A st p in dom f2 holds f2.p = Sym(n,f,D) -tree(p);
now
let x be object;
assume
A26: x in (f/.n)-tuples_on A;
then consider s be Element of A* 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;
end;
hence thesis by A22,A24,FUNCT_1:2;
end;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
func FreeOpSeqZAO(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
:Def17:
len it = len f & for n st n in dom it holds it.n = FreeOpZAO(n,f,D);
existence
proof
defpred P[Nat,set] means $2 = FreeOpZAO($1,f,D);
set A = TS(DTConUA(f,D));
A1: for n be Nat st n in Seg len f ex x be Element of PFuncs(A*,A) st P[n, x]
proof
let n be Nat;
assume n in Seg len f;
reconsider O=FreeOpZAO(n,f,D) as Element of PFuncs(A*,A) by PARTFUN1:45;
take O;
thus thesis;
end;
consider p be FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len f & for n be Nat st n in Seg len f holds P[n,p.n]
from FINSEQ_1:sch 5(A1);
reconsider p as PFuncFinSequence of A;
take p;
thus len p = len f by A2,FINSEQ_1:def 3;
let n;
assume n in dom p;
hence thesis by A2;
end;
uniqueness
proof
let f1,f2 be PFuncFinSequence of TS DTConUA(f,D);
assume that
A3: len f1 = len f and
A4: for n st n in dom f1 holds f1.n = FreeOpZAO(n,f,D) and
A5: len f2 = len f and
A6: for n st n in dom f2 holds f2.n = FreeOpZAO(n,f,D);
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;
assume
A10: n in dom f;
then f1.n = FreeOpZAO(n,f,D) by A3,A4,A8,A7;
hence thesis by A5,A6,A8,A9,A10;
end;
hence thesis by A3,A5,A8,A7,FINSEQ_2:9;
end;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
func FreeUnivAlgZAO(f,D) -> strict Universal_Algebra equals
UAStr (# TS(
DTConUA(f,D)), FreeOpSeqZAO(f,D)#);
coherence
proof
set A = TS DTConUA(f,D), AA = UAStr (# A, FreeOpSeqZAO(f,D) #);
for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
= (the charact of AA).n holds h is quasi_total
proof
let n be Nat,h be PartFunc of A*,A;
assume n in dom the charact of(AA) & h = (the charact of AA).n;
then h = FreeOpZAO(n,f,D) by Def17;
hence thesis;
end;
then
A1: the charact of(AA) is quasi_total;
for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
= (the charact of AA).n holds h is homogeneous
proof
let n be Nat,h be PartFunc of A*,A;
assume n in dom the charact of(AA) & h = (the charact of AA).n;
then h = FreeOpZAO(n,f,D) by Def17;
hence thesis;
end;
then
A2: the charact of(AA) is homogeneous;
for n be object st n in dom the charact of(AA) holds (the charact of AA)
.n is non empty
proof
let n be object;
assume
A3: n in dom the charact of AA;
then reconsider n as Nat;
(the charact of AA).n = FreeOpZAO(n,f,D) by A3,Def17;
hence thesis;
end;
then
A4: the charact of AA is non-empty by FUNCT_1:def 9;
len FreeOpSeqZAO(f,D) = len f by Def17;
then the charact of AA <> {};
hence thesis by A1,A2,A4,UNIALG_1:def 1,def 2,def 3;
end;
end;
theorem Th7:
for f be with_zero non empty FinSequence of NAT, D be
disjoint_with_NAT set holds signature (FreeUnivAlgZAO(f,D)) = f
proof
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
set fa = FreeUnivAlgZAO(f,D), A = TS DTConUA(f,D);
A1: len the charact of fa = len f by Def17;
A2: len(signature fa) = len the charact of(fa) by UNIALG_1:def 4;
then
A3: dom(signature fa) = Seg len f by A1,FINSEQ_1:def 3;
now
let n be Nat;
reconsider h = FreeOpZAO(n,f,D) as homogeneous quasi_total non empty
PartFunc of (the carrier of fa)*,(the carrier of fa);
A4: dom h = (arity h)-tuples_on (the carrier of fa) by MARGREL1:22;
assume
A5: n in dom(signature fa);
then
A6: n in dom f by A3,FINSEQ_1:def 3;
then dom h = (f/.n)-tuples_on A 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 fa).n = FreeOpZAO(n,f,D) by Def17;
hence (signature fa).n = arity h by A5,UNIALG_1:def 4
.= f.n by A6,A7,PARTFUN1:def 6;
end;
hence thesis by A2,A1,FINSEQ_2:9;
end;
theorem Th8:
for f be with_zero non empty FinSequence of NAT,D be
disjoint_with_NAT set holds FreeUnivAlgZAO(f,D) is with_const_op
proof
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
set A = DTConUA(f,D), 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 AA).n = FreeOpZAO(n,f,D) by A2,A1,Def17;
then reconsider o = FreeOpZAO(n,f,D) as operation of AA by A2,A4,A1,
FUNCT_1:def 3;
take o;
A5: dom o = (arity o)-tuples_on (the carrier of AA) by MARGREL1:22;
f/.n = f.n & dom(FreeOpZAO(n,f,D)) = (f/.n)-tuples_on (TS A) by A2,Def16,
PARTFUN1:def 6;
hence thesis by A3,A5,FINSEQ_2:110;
end;
theorem Th9:
for f be with_zero non empty FinSequence of NAT,D be
disjoint_with_NAT set holds Constants(FreeUnivAlgZAO(f,D)) <> {}
proof
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
set A = DTConUA(f,D), AA = FreeUnivAlgZAO(f,D);
A1: dom f = Seg len f by FINSEQ_1:def 3;
set ca = the carrier of AA;
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 AA).n = FreeOpZAO(n,f,D) by A2,A1,Def17;
then reconsider o = FreeOpZAO(n,f,D) as operation of AA by A2,A4,A1,
FUNCT_1:def 3;
A5: f/.n = f.n & dom(FreeOpZAO(n,f,D)) = (f/.n)-tuples_on (TS A) by A2,Def16,
PARTFUN1:def 6;
then dom o = {<*>(TS A)} by A3,FINSEQ_2:94;
then <*>(TS A) in dom o by TARSKI:def 1;
then
A6: o.(<*>(TS A)) in rng o by FUNCT_1:def 3;
rng o c= ca by RELAT_1:def 19;
then reconsider e = o.(<*>(TS A)) as Element of ca by A6;
dom o = (arity o)-tuples_on (the carrier of AA) by MARGREL1:22;
then arity o = 0 by A3,A5,FINSEQ_2:110;
then e in {a where a is Element of ca: ex o be operation of AA st arity o =
0 & a in rng o} by A6;
hence thesis;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
func FreeGenSetZAO(f,D) -> Subset of FreeUnivAlgZAO(f,D) equals
{root-tree s
where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
coherence
proof
set X = DTConUA(f,D), A = {root-tree d where d is Symbol of X: d in
Terminals X};
A c= the carrier of FreeUnivAlgZAO(f,D)
proof
let x be object;
assume x in A;
then ex d be Symbol of X st x = root-tree d & d in Terminals X;
hence thesis by DTCONSTR:def 1;
end;
hence thesis;
end;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
redefine func FreeGenSetZAO(f,D) -> GeneratorSet of FreeUnivAlgZAO(f,D); :: redefines FreeGenSetZAO (FREEALG, definition)
coherence
proof
set fgs = FreeGenSetZAO(f,D), fua = FreeUnivAlgZAO(f,D);
A1: the carrier of GenUnivAlg(fgs) = the carrier of fua
proof
set A = DTConUA(f,D);
defpred P[DecoratedTree of the carrier of A] means $1 in the carrier of
GenUnivAlg(fgs);
the carrier of GenUnivAlg(fgs) is Subset of fua by UNIALG_2:def 7;
hence the carrier of GenUnivAlg(fgs) c= the carrier of fua;
A2: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts & for t being DecoratedTree of the carrier of A st t in rng ts holds P
[t] holds P[nt-tree ts]
proof
reconsider B = the carrier of GenUnivAlg(fgs) as Subset of fua by
UNIALG_2:def 7;
let s be Symbol of A,p be FinSequence of TS(A);
assume that
A3: s ==> roots p and
A4: for t be DecoratedTree of the carrier of A st t in rng p
holds t in the carrier of GenUnivAlg(fgs);
rng p c= the carrier of GenUnivAlg(fgs)
proof
let x be object;
assume
A5: x in rng p;
rng p c= FinTrees(the carrier of A) by FINSEQ_1:def 4;
then reconsider
x1 = x as Element of FinTrees(the carrier of A) by A5;
x1 in the carrier of GenUnivAlg(fgs) by A4,A5;
hence thesis;
end;
then reconsider
cp = p as FinSequence of the carrier of GenUnivAlg(fgs) by
FINSEQ_1:def 4;
reconsider tp = p as Element of (TS A)* by FINSEQ_1:def 11;
[s,roots p] in the Rules of A 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 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 fua by A7,A9
,Def17;
B is opers_closed by UNIALG_2:def 7;
then
A10: B is_closed_on o;
A11: dom FreeOpZAO(ns,f,D) = (f/.ns)-tuples_on TS(A) by A7,Def16;
dom o = (arity o)-tuples_on the carrier of fua 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 A)* : len w = f/.ns};
then o.cp = Sym(ns,f,D)-tree p by A7,A11,Def16
.= s-tree p by A7,Def9;
hence thesis by A10,A13,A12;
end;
let x be object;
assume
A14: x in the carrier of fua;
then reconsider x1 = x as Element of FinTrees(the carrier of A);
A15: x1 in TS A by A14;
A16: for s being Symbol of A st s in Terminals A holds P[root-tree s]
proof
let s be Symbol of A;
assume s in Terminals A;
then
A17: root-tree s in {root-tree q where q is Symbol of A: q in Terminals A};
fgs c= the carrier of GenUnivAlg(fgs) by UNIALG_2:def 12;
hence thesis by A17;
end;
for t being DecoratedTree of the carrier of A st t in TS A holds P[
t] from DTCONSTR:sch 7(A16,A2);
hence thesis by A15;
end;
Constants(fua) <> {} by Th9;
hence thesis by A1,Lm3;
end;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
C be non empty set, s be Symbol of (DTConUA(f,D)), 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:
F.(root-tree s);
coherence
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 thesis;
end;
end;
theorem Th10:
for f be with_zero non empty FinSequence of NAT,D be
disjoint_with_NAT set holds FreeGenSetZAO(f,D) is free
proof
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
set fgs = FreeGenSetZAO(f,D), fua = FreeUnivAlgZAO(f,D);
let U1 be Universal_Algebra;
assume
A1: fua,U1 are_similar;
set A = DTConUA(f,D), c1 = the carrier of U1, cf = the carrier of fua;
let F be Function of fgs,the carrier of U1;
deffunc F(Symbol of A) = pi(F,$1);
deffunc G(Symbol of A,FinSequence,set) = (oper(@$1,U1))/.$3;
consider ff being Function of TS(A), c1 such that
A2: for t being Symbol of A st t in Terminals A holds ff.(root-tree t) =
F(t) and
A3: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts holds ff.(nt-tree ts) = G(nt,roots ts,ff * ts) from DTCONSTR:sch 8;
reconsider ff as Function of fua,U1;
take ff;
for n being Nat st n in dom the charact of(fua) for o1 be
operation of fua, o2 be operation of U1 st o1=(the charact of fua).n & o2=(the
charact of U1).n for x be FinSequence of fua 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 Nat;
assume
A5: n in dom the charact of(fua);
let o1 be operation of fua, o2 be operation of U1;
assume that
A6: o1=(the charact of fua).n and
A7: o2=(the charact of U1).n;
let x be FinSequence of fua;
assume
A8: x in dom o1;
reconsider xa = x as FinSequence of TS(A);
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 as FinSequence of FinTrees the carrier of A;
reconsider rxa = roots xa as FinSequence of ((dom f) \/ D);
reconsider rxa as Element of ((dom f) \/ D)* by FINSEQ_1:def 11;
dom o1 = (arity o1)-tuples_on cf by MARGREL1:22
.= {w where w is Element of cf* : len w = arity o1};
then
A10: ex w be Element of cf* 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 c1*;
A12: dom o2 = (arity o2)-tuples_on c1 by MARGREL1:22
.= {v where v is Element of c1*: len v = arity o2};
A13: len the charact of(fua) = len the charact of(U1) & dom the charact of
(fua) = Seg len the charact of(fua) 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 A 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 fua by Th7;
then
A17: (signature fua).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 fua = signature U1 by A1;
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 c1*: len v = arity o2};
reconsider xa as Element of (TS A)* 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 thesis by A19,A20,A12,A21,PARTFUN1:def 6;
end;
hence ff is_homomorphism by A1,ALG_1:def 1;
A22: (the carrier of fua) /\ fgs = fgs by XBOOLE_1:28;
A23: dom (ff|fgs) = dom ff /\ fgs & dom ff = (the carrier of fua) by
FUNCT_2:def 1,RELAT_1:61;
A24: now
let x be object;
assume
A25: x in dom F;
then x in {root-tree t where t is Symbol of A: t in Terminals A};
then consider s be Symbol of A such that
A26: x = root-tree s & s in Terminals A;
thus (ff|fgs).x = ff.x by A23,A22,A25,FUNCT_1:47
.= pi(F,s) by A2,A26
.= F.x by A26,Def20;
end;
fgs = dom F by FUNCT_2:def 1;
hence thesis by A23,A22,A24,FUNCT_1:2;
end;
registration
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
cluster FreeUnivAlgZAO(f,D) -> free;
coherence
proof
FreeGenSetZAO(f,D) is free by Th10;
hence thesis;
end;
end;
definition
let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
redefine func FreeGenSetZAO(f,D) -> free GeneratorSet of FreeUnivAlgZAO(f,D); :: redefines FreeGenSetZAO (FREEALG, definition)
coherence by Th10;
end;
registration
cluster strict free with_const_op for Universal_Algebra;
existence
proof
set D = the disjoint_with_NAT set;
set f = the with_zero non empty FinSequence of NAT;
take FreeUnivAlgZAO(f,D);
thus thesis by Th8;
end;
end;