environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions 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;
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;
constructors HIDDEN, DOMAIN_1, FINSEQOP, DTCONSTR, ALG_1, RELSET_1, PRE_POLY;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities UNIALG_2, FINSEQ_2, FUNCOP_1, ORDINAL1;
expansions TARSKI, UNIALG_2, DTCONSTR, XBOOLE_0, MARGREL1;
Lm1:
( not 0 in rng <*1*> & 0 in rng <*0*> )
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 )
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
;
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;
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
;
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;
:: Free Universal Algebra - General Notions
::