Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Yet Another Construction of Free Algebra

**by****Grzegorz Bancerek, and****Artur Kornilowicz**- Received August 8, 2001
- MML identifier: MSAFREE3

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, PROB_1, FUNCT_1, RELAT_1, PBOOLE, PRALG_1, MSUALG_3, FUNCT_6, CATALG_1, ZF_MODEL, MSUALG_2, MSAFREE, BOOLE, FUNCOP_1, ZF_REFLE, LANG1, FREEALG, TREES_4, MCART_1, QC_LANG1, MSATERM, UNIALG_2, TDGROUP, FINSEQ_1, MATRIX_1, DTCONSTR, TARSKI, FINSET_1, TREES_2, TREES_9, QC_LANG3, TREES_3, CARD_3, FINSEQ_4, MSUALG_6, PRELAMB; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0, NUMBERS, XREAL_0, NAT_1, MCART_1, FINSET_1, CARD_3, FINSEQ_1, PROB_1, TREES_1, TREES_2, FUNCT_6, TREES_3, TREES_4, DTCONSTR, LANG1, PBOOLE, TREES_9, MSUALG_1, MSUALG_2, PRALG_1, MSAFREE, PRE_CIRC, MSUALG_3, EXTENS_1, EQUATION, MSATERM, MSUALG_6, CATALG_1; constructors NAT_1, DOMAIN_1, MSAFREE1, TREES_9, PRE_CIRC, EXTENS_1, EQUATION, FINSEQ_4, MSATERM, MSUALG_6, CATALG_1; clusters SUBSET_1, RELSET_1, FUNCT_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, FINSEQ_1, TREES_9, PRALG_1, CARD_1, MSAFREE, CANTOR_1, TREES_3, MSUALG_6, MSUALG_9, MSATERM, TREES_2, INDEX_1, INSTALG1, CATALG_1, MEMBERED, RELAT_1, NUMBERS, ORDINAL2; requirements BOOLE, SUBSET, NUMERALS; begin reserve X,x,y,z for set; definition let S be non empty non void ManySortedSign; let A be non empty MSAlgebra over S; cluster Union the Sorts of A -> non empty; end; definition let S be non empty non void ManySortedSign; let A be non empty MSAlgebra over S; mode Element of A is Element of Union the Sorts of A; canceled; end; theorem :: MSAFREE3:1 for f being Function st X c= dom f & f is one-to-one holds f"(f.:X) = X; theorem :: MSAFREE3:2 for I being set, A being ManySortedSet of I for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds F""(F.:.:A) = A; definition let S be non void Signature; let X be ManySortedSet of the carrier of S; func Free(S, X) -> strict MSAlgebra over S means :: MSAFREE3:def 2 ex A being MSSubset of FreeMSA (X \/ ((the carrier of S) --> {0})) st it = GenMSAlg A & A = (Reverse (X \/ ((the carrier of S) --> {0})))""X; end; theorem :: MSAFREE3:3 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for s being SortSymbol of S holds [x,s] in the carrier of DTConMSA X iff x in X.s; theorem :: MSAFREE3:4 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds x in X.s & x in Y.s iff root-tree [x,s] in ((Reverse Y)""X).s; theorem :: MSAFREE3:5 for S being non void Signature for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in X.s holds root-tree [x,s] in (the Sorts of Free(S, X)).s; theorem :: MSAFREE3:6 for S being non void Signature for X being ManySortedSet of the carrier of S for o being OperSymbol of S st the_arity_of o = {} holds root-tree [o, the carrier of S] in (the Sorts of Free(S, X)).the_result_sort_of o; definition let S be non void Signature; let X be non empty-yielding ManySortedSet of the carrier of S; cluster Free(S, X) -> non empty; end; theorem :: MSAFREE3:7 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S holds x is Element of FreeMSA X iff x is Term of S, X; theorem :: MSAFREE3:8 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for s being SortSymbol of S for x being Term of S, X holds x in (the Sorts of FreeMSA X).s iff the_sort_of x = s; theorem :: MSAFREE3:9 for S being non void Signature for X being non empty-yielding ManySortedSet of the carrier of S for x being Element of Free(S, X) holds x is Term of S, X \/ ((the carrier of S) --> {0}); definition let S be non empty non void ManySortedSign; let X be non empty-yielding ManySortedSet of the carrier of S; cluster -> Relation-like Function-like Element of Free(S, X); end; definition let S be non empty non void ManySortedSign; let X be non empty-yielding ManySortedSet of the carrier of S; cluster -> finite DecoratedTree-like Element of Free(S, X); end; definition let S be non empty non void ManySortedSign; let X be non empty-yielding ManySortedSet of the carrier of S; cluster -> finite-branching Element of Free(S, X); end; definition cluster -> non empty DecoratedTree; end; definition let S be ManySortedSign; let t be non empty Relation; func S variables_in t -> ManySortedSet of the carrier of S means :: MSAFREE3:def 3 for s being set st s in the carrier of S holds it.s = {a`1 where a is Element of rng t: a`2 = s}; end; definition let S be ManySortedSign; let X be ManySortedSet of the carrier of S; let t be non empty Relation; func X variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 4 X /\ (S variables_in t); end; theorem :: MSAFREE3:10 for S being ManySortedSign, X being ManySortedSet of the carrier of S for t being non empty Relation, V being ManySortedSubset of X holds V = X variables_in t iff for s being set st s in the carrier of S holds V.s = (X.s) /\ {a`1 where a is Element of rng t: a`2 = s}; theorem :: MSAFREE3:11 for S being ManySortedSign, s,x being set holds (s in the carrier of S implies (S variables_in root-tree [x,s]).s = {x}) & for s' being set st s' <> s or not s in the carrier of S holds (S variables_in root-tree [x,s]).s' = {}; theorem :: MSAFREE3:12 for S being ManySortedSign, s being set st s in the carrier of S for p being DTree-yielding FinSequence holds x in (S variables_in ([z, the carrier of S]-tree p)).s iff ex t being DecoratedTree st t in rng p & x in (S variables_in t).s; theorem :: MSAFREE3:13 for S being ManySortedSign for X being ManySortedSet of the carrier of S for s,x being set holds (x in X.s implies (X variables_in root-tree [x,s]).s = {x}) & for s' being set st s' <> s or not x in X.s holds (X variables_in root-tree [x,s]).s' = {}; theorem :: MSAFREE3:14 for S being ManySortedSign for X being ManySortedSet of the carrier of S for s being set st s in the carrier of S for p being DTree-yielding FinSequence holds x in (X variables_in ([z, the carrier of S]-tree p)).s iff ex t being DecoratedTree st t in rng p & x in (X variables_in t).s; theorem :: MSAFREE3:15 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for t being Term of S, X holds S variables_in t c= X; definition let S be non void Signature; let X be non-empty ManySortedSet of the carrier of S; let t be Term of S, X; func variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 5 S variables_in t; end; theorem :: MSAFREE3:16 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for t being Term of S, X holds variables_in t = X variables_in t; definition let S be non void Signature; let Y be non-empty ManySortedSet of the carrier of S; let X be ManySortedSet of the carrier of S; func S-Terms(X,Y) -> MSSubset of FreeMSA Y means :: MSAFREE3:def 6 for s being SortSymbol of S holds it.s = {t where t is Term of S,Y: the_sort_of t = s & variables_in t c= X}; end; theorem :: MSAFREE3:17 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S st x in S-Terms(X,Y).s holds x is Term of S,Y; theorem :: MSAFREE3:18 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for t being Term of S, Y for s being SortSymbol of S st t in S-Terms(X,Y).s holds the_sort_of t = s & variables_in t c= X; theorem :: MSAFREE3:19 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for s being SortSymbol of S holds root-tree [x,s] in (S-Terms(X,Y)).s iff x in X.s & x in Y.s; theorem :: MSAFREE3:20 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S for o being OperSymbol of S for p being ArgumentSeq of Sym(o,Y) holds Sym(o,Y)-tree p in (S-Terms(X,Y)).the_result_sort_of o iff rng p c= Union (S-Terms(X,Y)); theorem :: MSAFREE3:21 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for A being MSSubset of FreeMSA X holds A is opers_closed iff for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st rng p c= Union A holds Sym(o,X)-tree p in A.the_result_sort_of o; theorem :: MSAFREE3:22 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds S-Terms(X,Y) is opers_closed; theorem :: MSAFREE3:23 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S holds (Reverse Y)""X c= S-Terms(X,Y); theorem :: MSAFREE3:24 for S being non void Signature for X being ManySortedSet of the carrier of S for t being Term of S, X \/ ((the carrier of S)-->{0}) for s being SortSymbol of S st t in S-Terms(X, X \/ ((the carrier of S)-->{0})).s holds t in (the Sorts of Free(S, X)).s; theorem :: MSAFREE3:25 for S being non void Signature for X being ManySortedSet of the carrier of S holds the Sorts of Free(S, X) = S-Terms(X, X \/ ((the carrier of S)-->{0})); theorem :: MSAFREE3:26 for S being non void Signature for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ ((the carrier of S)-->{0})))| (S-Terms(X, X \/ ((the carrier of S)-->{0}))) = Free(S, X); theorem :: MSAFREE3:27 for S being non void Signature for X,Y being non-empty ManySortedSet of the carrier of S for A being MSSubAlgebra of FreeMSA X for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds the MSAlgebra of A = the MSAlgebra of B; theorem :: MSAFREE3:28 for S being non void Signature for X being non empty-yielding ManySortedSet of the carrier of S for Y being ManySortedSet of the carrier of S for t being Element of Free(S, X) holds S variables_in t c= X; theorem :: MSAFREE3:29 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t c= X; theorem :: MSAFREE3:30 for S being non void Signature for X,Y being non-empty ManySortedSet of the carrier of S for t1 being Term of S,X, t2 being Term of S,Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2; theorem :: MSAFREE3:31 for S being non void Signature for X,Y being non-empty ManySortedSet of the carrier of S for t being Term of S,Y st variables_in t c= X holds t is Term of S,X; theorem :: MSAFREE3:32 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S holds Free(S, X) = FreeMSA X; theorem :: MSAFREE3:33 for S being non void Signature for Y being non-empty ManySortedSet of the carrier of S for t being Term of S,Y for p being Element of dom t holds variables_in (t|p) c= variables_in t; theorem :: MSAFREE3:34 for S being non void Signature for X being non empty-yielding ManySortedSet of the carrier of S for t being Element of Free(S, X) for p being Element of dom t holds t|p is Element of Free(S, X); theorem :: MSAFREE3:35 for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for t being Term of S,X for a being Element of rng t holds a = [a`1,a`2]; theorem :: MSAFREE3:36 for S being non void Signature for X being non empty-yielding ManySortedSet of the carrier of S for t being Element of Free(S, X) for s being SortSymbol of S holds (x in (S variables_in t).s implies [x,s] in rng t) & ([x,s] in rng t implies x in (S variables_in t).s & x in X.s); theorem :: MSAFREE3:37 for S being non void Signature for X being ManySortedSet of the carrier of S st for s being SortSymbol of S st X.s = {} ex o being OperSymbol of S st the_result_sort_of o = s & the_arity_of o = {} holds Free(S, X) is non-empty; theorem :: MSAFREE3:38 for S being non void non empty ManySortedSign for A being MSAlgebra over S for B being MSSubAlgebra of A for o being OperSymbol of S holds Args(o,B) c= Args(o,A); theorem :: MSAFREE3:39 for S being non void Signature for A being feasible MSAlgebra over S for B being MSSubAlgebra of A holds B is feasible; definition let S be non void Signature, A be feasible MSAlgebra over S; cluster -> feasible MSSubAlgebra of A; end; theorem :: MSAFREE3:40 for S being non void Signature for X being ManySortedSet of the carrier of S holds Free(S, X) is feasible free; definition let S be non void Signature, X be ManySortedSet of the carrier of S; cluster Free(S, X) -> feasible free; end;

Back to top