:: Yet another construction of free algebra
:: by Grzegorz Bancerek and Artur Korni{\l}owicz
::
:: Received August 8, 2001
:: Copyright (c) 2001-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 XBOOLE_0, STRUCT_0, MSUALG_1, CARD_3, RELAT_1, FUNCT_1, SUBSET_1,
PBOOLE, MSUALG_3, TARSKI, FUNCT_6, MEMBER_1, CATALG_1, ZF_MODEL,
MSUALG_2, MSAFREE, FUNCOP_1, CARD_1, LANG1, ZFMISC_1, TREES_4, MCART_1,
MARGREL1, FINSEQ_1, MSATERM, UNIALG_2, DTCONSTR, FINSET_1, TREES_2,
TREES_9, ZF_LANG1, TREES_3, TREES_A, NUMBERS, ARYTM_3, ORDINAL4,
XXREAL_0, NAT_1, PARTFUN1, MSUALG_6, PRELAMB, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1,
FUNCT_1, RELSET_1, STRUCT_0, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1,
FINSET_1, CARD_3, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, TREES_3,
TREES_4, DTCONSTR, LANG1, PBOOLE, TREES_9, MSUALG_1, MSUALG_2, MSAFREE,
FUNCOP_1, MSUALG_3, EQUATION, MSATERM, MSUALG_6, CATALG_1, XXREAL_0;
constructors DOMAIN_1, TREES_9, MSUALG_3, MSATERM, MSUALG_6, CATALG_1,
EQUATION, SEQ_4, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XREAL_0, FINSEQ_1, TREES_2, TREES_3, TREES_9, STRUCT_0, RELSET_1,
MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSATERM, INDEX_1, MSUALG_6,
MSUALG_9, INSTALG1, CATALG_1, MSSUBFAM, PBOOLE, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_2, MSUALG_6, CATALG_1;
equalities TARSKI;
expansions TARSKI, PBOOLE, MSUALG_2;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, NAT_1,
MCART_1, PBOOLE, RELAT_1, CARD_3, CARD_5, FUNCT_6, TREES_3, MSUALG_1,
INSTALG1, TREES_4, PRE_CIRC, TREES_1, TREES_2, MSUALG_2, MSUALG_3,
MSAFREE, MSATERM, EQUATION, MSUALG_6, XBOOLE_0, XBOOLE_1, ORDINAL1,
PARTFUN1, TREES_9, FINSEQ_2, XTUPLE_0;
schemes PBOOLE, MSATERM;
begin
reserve x,y,z for set;
registration
let S be non empty non void ManySortedSign;
let A be non empty MSAlgebra over S;
cluster Union the Sorts of A -> non empty;
coherence
proof
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
consider i being object such that
A2: i in the carrier of S and
A3: (the Sorts of A).i is non empty by PBOOLE:def 12;
set x = the Element of (the Sorts of A).i;
x in (the Sorts of A).i by A3;
hence thesis by A2,A1,CARD_5:2;
end;
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;
end;
theorem
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
proof
let I be set, A be ManySortedSet of I;
let F be ManySortedFunction of I such that
A1: F is "1-1" and
A2: A c= doms F;
A3: dom F = I by PARTFUN1:def 2;
now
let i be object;
assume
A4: i in I;
then
A5: F.i is one-to-one by A1,A3,MSUALG_3:def 2;
A.i c= (doms F).i by A2,A4;
then
A6: A.i c= dom (F.i) by A3,A4,FUNCT_6:22;
thus (F""(F.:.:A)).i = (F.i)"((F.:.:A).i) by A4,EQUATION:def 1
.= (F.i)"((F.i).:(A.i)) by A4,PBOOLE:def 20
.= A.i by A6,A5,FUNCT_1:94;
end;
hence thesis;
end;
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
:Def1:
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;
uniqueness;
existence
proof
set I = the carrier of S, Y = X (\/) (I --> {0});
set R = Reverse Y;
R""X is ManySortedSubset of FreeGen Y by EQUATION:8;
then
A1: R""X c= FreeGen Y by PBOOLE:def 18;
FreeGen Y c= the Sorts of FreeMSA Y by PBOOLE:def 18;
then R""X c= the Sorts of FreeMSA Y by A1,PBOOLE:13;
then reconsider Z = R""X as MSSubset of FreeMSA Y by PBOOLE:def 18;
take GenMSAlg Z, Z;
thus thesis;
end;
end;
theorem Th2:
for S being non void Signature for X being 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
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let s be SortSymbol of S;
A1: DTConMSA X = DTConstrStr (# [:the carrier' of S,{the carrier of S}:] \/
Union coprod X, REL(X) #) by MSAFREE:def 8;
A2: dom coprod X = the carrier of S by PARTFUN1:def 2;
s in the carrier of S;
then s <> the carrier of S;
then not s in {the carrier of S} by TARSKI:def 1;
then
A3: not [x,s] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
hereby
assume [x,s] in the carrier of DTConMSA X;
then [x,s] in Union coprod X by A1,A3,XBOOLE_0:def 3;
then consider y being object such that
A4: y in dom coprod X and
A5: [x,s] in (coprod X).y by CARD_5:2;
(coprod X).y = coprod(y,X) by A4,MSAFREE:def 3;
then consider z such that
A6: z in X.y and
A7: [x,s] = [z,y] by A4,A5,MSAFREE:def 2;
x = z by A7,XTUPLE_0:1;
hence x in X.s by A6,A7,XTUPLE_0:1;
end;
assume x in X.s;
then [x,s] in coprod(s,X) by MSAFREE:def 2;
then [x,s] in (coprod X).s by MSAFREE:def 3;
then [x,s] in Union coprod X by A2,CARD_5:2;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th3:
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
proof
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;
let s be SortSymbol of S;
A1: (Reverse Y).s = Reverse (s, Y) by MSAFREE:def 18;
A2: dom Reverse (s, Y) = FreeGen(s,Y) by FUNCT_2:def 1;
hereby
assume that
A3: x in X.s and
A4: x in Y.s;
A5: root-tree [x,s] in FreeGen(s,Y) by A4,MSAFREE:def 15;
[x,s] in the carrier of DTConMSA Y by A4,Th2;
then (Reverse Y).s.root-tree [x,s] = [x,s]`1 by A1,A5,MSAFREE:def 17
.= x;
then root-tree [x,s] in ((Reverse Y).s)"(X.s) by A1,A2,A3,A5,FUNCT_1:def 7;
hence root-tree [x,s] in ((Reverse Y)""X).s by EQUATION:def 1;
end;
assume root-tree [x,s] in ((Reverse Y)"" X).s;
then
A6: root-tree [x,s] in ((Reverse Y).s)"(X.s) by EQUATION:def 1;
then
A7: Reverse(s,Y).root-tree [x,s] in X. s by A1,FUNCT_1:def 7;
A8: root-tree [x,s] in FreeGen(s,Y) by A1,A2,A6,FUNCT_1:def 7;
then consider z such that
A9: z in Y.s and
A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def 15;
B: [z,s]`1 = z;
A11: [x,s] = [z,s] by A10,TREES_4:4;
then [x,s] in the carrier of DTConMSA Y by A9,Th2;
then [x,s]`1 in X.s by A8,A7,MSAFREE:def 17;
hence x in X.s & x in Y.s by A9,A11,B;
end;
theorem Th4:
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
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let s be SortSymbol of S such that
A1: x in X.s;
set Y = X (\/) ((the carrier of S) --> {0});
consider A being MSSubset of FreeMSA Y such that
A2: Free(S, X) = GenMSAlg A and
A3: A = (Reverse Y)""X by Def1;
A is MSSubset of Free(S,X) by A2,MSUALG_2:def 17;
then A c= the Sorts of Free(S,X) by PBOOLE:def 18;
then
A4: A.s c= (the Sorts of Free(S,X)).s;
X c= Y by PBOOLE:14;
then X.s c= Y.s;
then root-tree [x,s] in A.s by A1,A3,Th3;
hence thesis by A4;
end;
theorem Th5:
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
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let o be OperSymbol of S such that
A1: the_arity_of o = {};
set Y = X (\/) ((the carrier of S) --> {0});
A2: Args(o, FreeMSA Y) = ((the Sorts of FreeMSA Y)# * the Arity of S).o by
MSUALG_1:def 4
.= (the Sorts of FreeMSA Y)#.((the Arity of S).o) by FUNCT_2:15
.= (the Sorts of FreeMSA Y)#.<*>the carrier of S by A1,MSUALG_1:def 1
.= {{}} by PRE_CIRC:2;
then
A3: dom Den(o,FreeMSA Y) c= {{}};
A4: ex A being MSSubset of FreeMSA Y st Free(S, X) = GenMSAlg A & A = (
Reverse Y)""X by Def1;
then reconsider FX = the Sorts of Free(S,X) as MSSubset of FreeMSA Y by
MSUALG_2:def 9;
(FX# * the Arity of S).o = FX#.((the Arity of S).o) by FUNCT_2:15
.= FX#.<*>the carrier of S by A1,MSUALG_1:def 1
.= {{}} by PRE_CIRC:2;
then
A5: (Den(o,FreeMSA Y))|((FX# * the Arity of S).o) = Den(o,FreeMSA Y) by A3,
RELAT_1:68;
set a = the ArgumentSeq of Sym(o, Y);
reconsider a as Element of Args(o, FreeMSA Y) by INSTALG1:1;
a = {} by A2,TARSKI:def 1;
then root-tree [o, the carrier of S] = [o, the carrier of S]-tree a by
TREES_4:20;
then Den(o,FreeMSA Y).a = root-tree [o, the carrier of S] by INSTALG1:3;
then
A6: root-tree [o, the carrier of S] in rng Den(o,FreeMSA Y) by FUNCT_2:4;
FX is opers_closed by A4,MSUALG_2:def 9;
then FX is_closed_on o;
then
A7: rng ((Den(o,FreeMSA Y))|((FX# * the Arity of S).o)) c= (FX * the
ResultSort of S).o;
(FX * the ResultSort of S).o = FX.((the ResultSort of S).o) by FUNCT_2:15
.= FX.the_result_sort_of o by MSUALG_1:def 2;
hence thesis by A7,A5,A6;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster Free(S, X) -> non empty;
coherence
proof
consider s being object such that
A1: s in the carrier of S and
A2: X.s is non empty by PBOOLE:def 12;
reconsider s as SortSymbol of S by A1;
set x = the Element of X.s;
root-tree [x,s] in (the Sorts of Free(S,X)).s by A2,Th4;
hence the Sorts of Free(S, X) is not empty-yielding;
end;
end;
theorem
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
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
A1: S-Terms X = TS DTConMSA X by MSATERM:def 1
.= union rng FreeSort X by MSAFREE:11
.= Union FreeSort X by CARD_3:def 4;
FreeMSA X = MSAlgebra(# FreeSort X, FreeOper X #) by MSAFREE:def 14;
hence thesis by A1;
end;
theorem Th7:
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
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
let s be SortSymbol of S;
FreeMSA X = MSAlgebra(# FreeSort X, FreeOper X #) by MSAFREE:def 14;
then (the Sorts of FreeMSA X).s = FreeSort(X, s) by MSAFREE:def 11;
hence thesis by MSATERM:def 5;
end;
theorem Th8:
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})
proof
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S) --> {0});
let x be Element of Free(S, X);
A1: S -Terms Y = TS DTConMSA Y by MSATERM:def 1
.= union rng FreeSort Y by MSAFREE:11
.= Union FreeSort Y by CARD_3:def 4;
A2: FreeMSA Y = MSAlgebra(# FreeSort Y, FreeOper Y #) & dom the Sorts of
FreeMSA Y = the carrier of S by MSAFREE:def 14,PARTFUN1:def 2;
consider y being object such that
A3: y in dom the Sorts of Free(S, X) and
A4: x in (the Sorts of Free(S,X)).y by CARD_5:2;
ex A being MSSubset of FreeMSA Y st Free(S, X) = GenMSAlg A & A = (
Reverse Y)""X by Def1;
then the Sorts of Free(S, X) is MSSubset of FreeMSA Y by MSUALG_2:def 9;
then the Sorts of Free(S, X) c= the Sorts of FreeMSA Y by PBOOLE:def 18;
then (the Sorts of Free(S,X)).y c= (the Sorts of FreeMSA Y).y by A3;
hence thesis by A1,A3,A4,A2,CARD_5:2;
end;
registration
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 for Element of Free(S, X);
coherence by Th8;
end;
registration
let S be non empty non void ManySortedSign;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster -> finite DecoratedTree-like for Element of Free(S, X);
coherence by Th8;
end;
registration
let S be non empty non void ManySortedSign;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster -> finite-branching for Element of Free(S, X);
coherence;
end;
registration
cluster -> non empty for DecoratedTree;
coherence by RELAT_1:38;
end;
definition
let S be ManySortedSign;
let t be non empty Relation;
func S variables_in t -> ManySortedSet of the carrier of S means
: Def2:
for s being object st s in the carrier of S
holds it.s = {a`1 where a is Element of rng t: a`2 = s};
existence
proof
deffunc F(object) = {a`1 where a is Element of rng t: a`2 = $1};
ex f being ManySortedSet of the carrier of S st
for i be object st i in
the carrier of S holds f.i = F(i) from PBOOLE:sch 4;
hence thesis;
end;
uniqueness
proof
let V1, V2 be ManySortedSet of the carrier of S such that
A1: for s being object st s in the carrier of S holds V1.s = {a`1 where a
is Element of rng t: a`2 = s} and
A2: for s being object st s in the carrier of S holds V2.s = {a`1 where a
is Element of rng t: a`2 = s};
now
let s be object;
assume
A3: s in the carrier of S;
hence V1.s = {a`1 where a is Element of rng t: a`2 = s} by A1
.= V2.s by A2,A3;
end;
hence thesis;
end;
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
X (/\) (S variables_in t);
coherence
proof
thus X (/\) (S variables_in t) c= X by PBOOLE:15;
end;
end;
theorem Th9:
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}
proof
let S be ManySortedSign, X be ManySortedSet of the carrier of S;
let t be non empty Relation, V be ManySortedSubset of X;
hereby
assume
A1: V = X variables_in t;
let s be set;
assume
A2: s in the carrier of S;
then V.s = (X.s) /\ ((S variables_in t).s) by A1,PBOOLE:def 5;
hence V.s = (X.s) /\ {a`1 where a is Element of rng t: a`2 = s} by A2,Def2;
end;
assume
A3: 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};
now
let s be object;
assume
A4: s in the carrier of S;
hence V.s = (X.s) /\ {a`1 where a is Element of rng t: a`2 = s} by A3
.= (X.s) /\ ((S variables_in t).s) by A4,Def2;
end;
hence thesis by PBOOLE:def 5;
end;
theorem Th10:
for S being ManySortedSign, s,x being object holds (s in the
carrier of S implies (S variables_in root-tree [x,s]).s = {x}) &
for s9 being object st s9 <> s or not s in the carrier of S
holds (S variables_in root-tree [x,s]).s9 = {}
proof
let S be ManySortedSign, s,x be object;
reconsider t = root-tree [x,s] as DecoratedTree;
A1: [x,s]`2 = s;
t = {[{},[x,s]]} by TREES_4:6;
then
A2: rng t = {[x,s]} by RELAT_1:9;
A3: [x,s]`1 = x;
hereby
assume s in the carrier of S;
then
A4: (S variables_in t).s = {a`1 where a is Element of rng t: a`2 = s} by Def2;
thus (S variables_in root-tree [x,s]).s = {x}
proof
hereby
let y be object;
assume y in (S variables_in root-tree [x,s]).s;
then consider a being Element of rng t such that
A5: y = a`1 and
a`2 = s by A4;
a = [x,s] by A2,TARSKI:def 1;
hence y in {x} by A5,TARSKI:def 1;
end;
[x,s] in rng t by A2,TARSKI:def 1;
then x in {a`1 where a is Element of rng t: a`2 = s} by A3,A1;
hence thesis by A4,ZFMISC_1:31;
end;
end;
let s9 be object such that
A6: s9 <> s or not s in the carrier of S;
set y = the Element of (S variables_in root-tree [x,s]).s9;
assume
A7: (S variables_in root-tree [x,s]).s9 <> {};
then
A8: y in (S variables_in t).s9;
dom (S variables_in t) = the carrier of S by PARTFUN1:def 2;
then
A9: s9 in the carrier of S by A7,FUNCT_1:def 2;
then (S variables_in t).s9 = {a`1 where a is Element of rng t:a`2 = s9} by
Def2;
then ex a being Element of rng t st y = a`1 & a`2 = s9 by A8;
hence thesis by A2,A1,A6,A9,TARSKI:def 1;
end;
theorem Th11:
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
proof
let S be ManySortedSign, s be set such that
A1: s in the carrier of S;
let p be DTree-yielding FinSequence;
reconsider q = [z, the carrier of S]-tree p as DecoratedTree;
A2: (S variables_in q).s = {a`1 where a is Element of rng q: a`2 = s} by A1
,Def2;
A3: dom q = tree doms p by TREES_4:10;
A4: dom doms p = dom p by TREES_3:37;
then
A5: len p = len doms p by FINSEQ_3:29;
hereby
assume x in (S variables_in ([z, the carrier of S]-tree p)).s;
then consider a being Element of rng q such that
A6: x = a`1 and
A7: a`2 = s by A2;
consider y being object such that
A8: y in dom q and
A9: a = q.y by FUNCT_1:def 3;
reconsider y as Element of dom q by A8;
q.{} = [z, the carrier of S] & s <> the carrier of S by A1,TREES_4:def 4;
then y <> {} by A7,A9;
then consider n being Nat, r being FinSequence such that
A10: n < len doms p and
A11: r in (doms p).(n+1) and
A12: y = <*n*>^r by A3,TREES_3:def 15;
1 <= n+1 & n+1 <= len doms p by A10,NAT_1:11,13;
then
A13: n+1 in dom doms p by FINSEQ_3:25;
then reconsider t = p.(n+1) as DecoratedTree by A4,TREES_3:24;
reconsider r as FinSequence of NAT by A12,FINSEQ_1:36;
take t;
thus t in rng p by A4,A13,FUNCT_1:def 3;
A14: (doms p).(n+1) = dom t by A4,A13,FUNCT_6:22;
reconsider n as Element of NAT by ORDINAL1:def 12;
A15: t = q|<*n*> by A5,A10,TREES_4:def 4;
then dom t = (dom q)|<*n*> by TREES_2:def 10;
then a = t.r by A9,A11,A12,A15,A14,TREES_2:def 10;
then a in rng t by A11,A14,FUNCT_1:def 3;
then x in {b`1 where b is Element of rng t: b`2 = s} by A6,A7;
hence x in (S variables_in t).s by A1,Def2;
end;
given t being DecoratedTree such that
A16: t in rng p and
A17: x in (S variables_in t).s;
consider y being object such that
A18: y in dom p and
A19: t = p.y by A16,FUNCT_1:def 3;
reconsider y as Element of NAT by A18;
y >= 1 by A18,FINSEQ_3:25;
then consider n being Nat such that
A20: y = 1+n by NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
y <= len p by A18,FINSEQ_3:25;
then
A21: n < len p by A20,NAT_1:13;
then
A22: t = q|<*n*> by A19,A20,TREES_4:def 4;
A23: {} in dom t & <*n*>^{} = <*n*> by FINSEQ_1:34,TREES_1:22;
dom t = (doms p).(n+1) by A18,A19,A20,FUNCT_6:22;
then <*n*> in dom q by A3,A5,A21,A23,TREES_3:def 15;
then
A24: rng t c= rng q by A22,TREES_2:32;
x in {b`1 where b is Element of rng t: b`2 = s} by A1,A17,Def2;
then consider b being Element of rng t such that
A25: x = b`1 & b`2 = s;
b in rng t;
hence thesis by A2,A25,A24;
end;
theorem Th12:
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 s9 being set st s9 <> s or not x in X.s holds (
X variables_in root-tree [x,s]).s9 = {}
proof
let S be ManySortedSign, X be ManySortedSet of the carrier of S;
let s,x be set;
reconsider t = root-tree [x,s] as DecoratedTree;
hereby
assume
A1: x in X.s;
then
A2: {x} c= X.s by ZFMISC_1:31;
dom X = the carrier of S by PARTFUN1:def 2;
then
A3: s in the carrier of S by A1,FUNCT_1:def 2;
then (S variables_in root-tree [x,s]).s = {x} by Th10;
then (X.s) /\ ((S variables_in root-tree [x,s]).s) = {x} by A2,XBOOLE_1:28;
hence (X variables_in root-tree [x,s]).s = {x} by A3,PBOOLE:def 5;
end;
let s9 be set such that
A4: s9 <> s or not x in X.s;
set y = the Element of (X variables_in root-tree [x,s]).s9;
assume
A5: (X variables_in root-tree [x,s]).s9 <> {};
dom (X variables_in t) = the carrier of S by PARTFUN1:def 2;
then s9 in the carrier of S by A5,FUNCT_1:def 2;
then
A6: (X variables_in t).s9 = (X.s9) /\ {a`1 where a is Element of rng t:a`2
= s9} by Th9;
then y in {a`1 where a is Element of rng t: a`2 = s9} by A5,XBOOLE_0:def 4;
then consider a being Element of rng t such that
A7: y = a`1 & a`2 = s9;
t = {[{},[x,s]]} by TREES_4:6;
then rng t = {[x,s]} by RELAT_1:9;
then a = [x,s] by TARSKI:def 1;
hence thesis by A4,A5,A6,A7,XBOOLE_0:def 4;
end;
theorem Th13:
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
proof
let S be ManySortedSign, X be ManySortedSet of the carrier of S;
let s be set such that
A1: s in the carrier of S;
let p be DTree-yielding FinSequence;
reconsider q = [z, the carrier of S]-tree p as DecoratedTree;
(X variables_in q).s = (X.s) /\ ((S variables_in q).s) by A1,PBOOLE:def 5;
then
A2: x in (X variables_in ([z, the carrier of S]-tree p)).s iff x in X.s & x
in (S variables_in ([z, the carrier of S]-tree p)).s by XBOOLE_0:def 4;
then
A3: x in (X variables_in ([z, the carrier of S]-tree p)).s iff x in X.s & ex
t being DecoratedTree st t in rng p & x in (S variables_in t).s by A1,Th11;
hereby
assume x in (X variables_in ([z, the carrier of S]-tree p)).s;
then consider t being DecoratedTree such that
A4: t in rng p and
A5: x in X.s & x in (S variables_in t).s by A3;
take t;
thus t in rng p by A4;
x in (X.s) /\ ((S variables_in t).s) by A5,XBOOLE_0:def 4;
hence x in (X variables_in t).s by A1,PBOOLE:def 5;
end;
given t being DecoratedTree such that
A6: t in rng p and
A7: x in (X variables_in t).s;
A8: (X variables_in t).s = (X.s) /\ ((S variables_in t).s) by A1,PBOOLE:def 5;
then x in (S variables_in t).s by A7,XBOOLE_0:def 4;
hence thesis by A1,A2,A6,A7,A8,Th11,XBOOLE_0:def 4;
end;
theorem Th14:
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
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
defpred P[DecoratedTree] means S variables_in $1 c= X;
A1: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st for t
being Term of S,X st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X) such that
A2: for t being Term of S,X st t in rng p holds S variables_in t c= X;
set q = [o, the carrier of S]-tree p;
thus S variables_in q c= X
proof
let s9 be object;
assume s9 in the carrier of S;
then reconsider z = s9 as SortSymbol of S;
let x be object;
assume x in (S variables_in q).s9;
then consider t being DecoratedTree such that
A3: t in rng p and
A4: x in (S variables_in t).z by Th11;
consider i being object such that
A5: i in dom p and
A6: t = p.i by A3,FUNCT_1:def 3;
reconsider i as Nat by A5;
reconsider t = p.i as Term of S,X by A5,MSATERM:22;
S variables_in t c= X by A2,A3,A6;
then (S variables_in t).z c= X.z;
hence thesis by A4,A6;
end;
end;
A7: for s being SortSymbol of S, v being Element of X.s holds P[root-tree [v
,s]]
proof
let s be SortSymbol of S, v be Element of X.s;
thus S variables_in root-tree [v,s] c= X
proof
let s9 be object;
assume s9 in the carrier of S;
then reconsider z = s9 as SortSymbol of S;
let x be object;
assume
A8: x in (S variables_in root-tree [v,s]).s9;
then
A9: s <> z implies x in {} by Th10;
s = z implies x in {v} by A8,Th10;
hence thesis by A9;
end;
end;
for t being Term of S,X holds P[t] from MSATERM:sch 1(A7,A1);
hence thesis;
end;
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
S variables_in t;
correctness
proof
S variables_in t c= X by Th14;
then S variables_in t = X variables_in t by PBOOLE:23;
hence thesis;
end;
end;
theorem Th15:
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 by Th14,PBOOLE:23;
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
: Def5:
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};
existence
proof
deffunc F(SortSymbol of S) = {t where t is Term of S,Y: the_sort_of t = $1
& variables_in t c= X};
consider T being ManySortedSet of the carrier of S such that
A1: for s being SortSymbol of S holds T.s = F(s) from PBOOLE:sch 5;
T c= the Sorts of FreeMSA Y
proof
let s be object;
assume s in the carrier of S;
then reconsider s9 = s as SortSymbol of S;
let x be object;
assume
A2: x in T.s;
T.s9 = {t where t is Term of S,Y: the_sort_of t = s9 & variables_in
t c= X} by A1;
then
ex t being Term of S, Y st x = t & the_sort_of t = s9 & variables_in
t c= X by A2;
hence thesis by Th7;
end;
then reconsider T as MSSubset of FreeMSA Y by PBOOLE:def 18;
take T;
thus thesis by A1;
end;
correctness
proof
let T1, T2 be MSSubset of FreeMSA Y such that
A3: for s being SortSymbol of S holds T1.s = {t where t is Term of S,Y
: the_sort_of t = s & variables_in t c= X} and
A4: for s being SortSymbol of S holds T2.s = {t where t is Term of S,Y
: the_sort_of t = s & variables_in t c= X};
now
let s be object;
assume
A5: s in the carrier of S;
hence T1.s = {t where t is Term of S,Y: the_sort_of t = s & variables_in
t c= X} by A3
.= T2.s by A4,A5;
end;
hence thesis;
end;
end;
theorem Th16:
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
proof
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;
let s be SortSymbol of S;
assume x in S-Terms(X,Y).s;
then
x in {t where t is Term of S,Y: the_sort_of t = s & variables_in t c= X}
by Def5;
then
ex t being Term of S,Y st x = t & the_sort_of t = s & variables_in t c= X;
hence thesis;
end;
theorem Th17:
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
proof
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;
let q be Term of S,Y, s be SortSymbol of S such that
A1: q in S-Terms(X,Y).s;
S-Terms(X,Y).s = {t where t is Term of S,Y: the_sort_of t = s &
variables_in t c= X} by Def5;
then
ex t being Term of S,Y st q = t & the_sort_of t = s & variables_in t c=
X by A1;
hence thesis;
end;
theorem Th18:
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
proof
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;
let s be SortSymbol of S;
A1: (S-Terms(X,Y)).s = {t where t is Term of S,Y: the_sort_of t = s &
variables_in t c= X} by Def5;
hereby
assume root-tree [x,s] in (S-Terms(X,Y)).s;
then consider t being Term of S,Y such that
A2: root-tree [x,s] = t and
the_sort_of t = s and
A3: variables_in t c= X by A1;
A4: t.{} = [x,s] by A2,TREES_4:3;
s in the carrier of S;
then s <> the carrier of S;
then not s in {the carrier of S} by TARSKI:def 1;
then not t.{} in [:the carrier' of S,{the carrier of S}:] by A4,ZFMISC_1:87
;
then consider s9 being SortSymbol of S, v being Element of Y.s9 such that
A5: t.{} = [v,s9] by MSATERM:2;
A6: s = s9 & x = v by A4,A5,XTUPLE_0:1;
(S variables_in t).s = {x} & (variables_in t).s c= X.s by A2,A3,Th10;
hence x in X.s & x in Y.s by A6,ZFMISC_1:31;
end;
assume that
A7: x in X.s and
A8: x in Y.s;
reconsider t = root-tree [x,s] as Term of S,Y by A8,MSATERM:4;
A9: variables_in t c= X
proof
let i be object;
assume i in the carrier of S;
A10: (S variables_in t).s = { x } by Th10;
i <> s implies (S variables_in t).i = {} by Th10;
hence thesis by A7,A10,ZFMISC_1:31;
end;
the_sort_of t = s by A8,MSATERM:14;
hence thesis by A1,A9;
end;
theorem Th19:
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)
)
proof
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;
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,Y);
set s = the_result_sort_of o;
A1: dom (S-Terms(X,Y)) = the carrier of S by PARTFUN1:def 2;
A2: Sym(o,Y) = [o,the carrier of S] by MSAFREE:def 9;
A3: (S-Terms(X,Y)).s = {t where t is Term of S,Y: the_sort_of t = s &
variables_in t c= X} by Def5;
hereby
assume Sym(o,Y)-tree p in (S-Terms(X,Y)).s;
then consider t being Term of S,Y such that
A4: [o,the carrier of S]-tree p = t and
the_sort_of t = s and
A5: variables_in t c= X by A3,A2;
thus rng p c= Union (S-Terms(X,Y))
proof
let y be object;
assume
A6: y in rng p;
then consider x being object such that
A7: x in dom p and
A8: y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A7;
reconsider q = p.x as Term of S,Y by A7,MSATERM:22;
A9: variables_in q c= X
proof
let z be object;
assume
A10: z in the carrier of S;
let a be object;
assume a in (variables_in q).z;
then
A11: a in (variables_in t).z by A4,A6,A8,A10,Th11;
(variables_in t).z c= X.z by A5,A10;
hence thesis by A11;
end;
set sq = the_sort_of q;
(S-Terms(X,Y)).sq = {t9 where t9 is Term of S,Y: the_sort_of t9 =
sq & variables_in t9 c= X} by Def5;
then q in (S-Terms(X,Y)).sq by A9;
hence thesis by A1,A8,CARD_5:2;
end;
end;
set t = Sym(o,Y)-tree p;
assume
A12: rng p c= Union (S-Terms(X,Y));
A13: variables_in t c= X
proof
let z be object;
assume
A14: z in the carrier of S;
let x be object;
assume x in (variables_in t).z;
then consider q being DecoratedTree such that
A15: q in rng p and
A16: x in (S variables_in q).z by A2,A14,Th11;
consider y being object such that
A17: y in the carrier of S and
A18: q in (S-Terms(X,Y)).y by A1,A12,A15,CARD_5:2;
(S-Terms(X,Y)).y = {t9 where t9 is Term of S,Y: the_sort_of t9 = y &
variables_in t9 c= X} by A17,Def5;
then consider t9 being Term of S,Y such that
A19: q = t9 and
the_sort_of t9 = y and
A20: variables_in t9 c= X by A18;
(variables_in t9).z c= X.z by A14,A20;
hence thesis by A16,A19;
end;
the_sort_of t = s by MSATERM:20;
hence thesis by A3,A13;
end;
theorem Th20:
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
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
set A = FreeMSA X;
let T be MSSubset of FreeMSA X;
hereby
assume
A1: T is opers_closed;
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X);
T is_closed_on o by A1;
then
A2: rng ((Den(o,A))|((T# * the Arity of S).o)) c= (T * the ResultSort of S
).o;
A3: p is Element of Args(o, A) by INSTALG1:1;
A4: dom p = dom the_arity_of o by MSATERM:22;
A5: dom T = the carrier of S by PARTFUN1:def 2;
assume
A6: rng p c= Union T;
A7: now
let x be object;
assume
A8: x in dom the_arity_of o;
then reconsider i = x as Nat;
reconsider t = p.i as Term of S,X by A4,A8,MSATERM:22;
A9: the_sort_of t = (the_arity_of o).x & (T*the_arity_of o).x = T.((
the_arity_of o).x) by A4,A8,FUNCT_1:13,MSATERM:23;
p.x in rng p by A4,A8,FUNCT_1:def 3;
then consider y being object such that
A10: y in dom T and
A11: p.x in T.y by A6,CARD_5:2;
T c= the Sorts of A by PBOOLE:def 18;
then T.y c= (the Sorts of A).y by A10;
hence p.x in (T*the_arity_of o).x by A10,A11,A9,Th7;
end;
rng the_arity_of o c= dom T by A5;
then dom (T*the_arity_of o) = dom the_arity_of o by RELAT_1:27;
then
A12: p in product (T*the_arity_of o) by A4,A7,CARD_3:9;
A13: (T# * the Arity of S).o = T#.((the Arity of S).o) by FUNCT_2:15
.= T#.the_arity_of o by MSUALG_1:def 1
.= product (T*the_arity_of o) by FINSEQ_2:def 5;
then
A14: ((Den(o,A))|((T# * the Arity of S).o)).p = Den(o,A).p by A12,FUNCT_1:49;
dom Den(o,A) = Args(o, A) by FUNCT_2:def 1;
then p in dom ((Den(o,A))|((T# * the Arity of S).o)) by A13,A3,A12,
RELAT_1:57;
then
A15: Den(o,A).p in rng ((Den(o,A))|((T# * the Arity of S).o)) by A14,
FUNCT_1:def 3;
(T * the ResultSort of S).o = T.((the ResultSort of S).o) by FUNCT_2:15
.= T.the_result_sort_of o by MSUALG_1:def 2;
then
[o,the carrier of S] = Sym(o, X) & Den(o,A).p in T.the_result_sort_of
o by A2,A15,MSAFREE:def 9;
hence Sym(o,X)-tree p in T.the_result_sort_of o by A3,INSTALG1:3;
end;
assume
A16: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st rng
p c= Union T holds Sym(o,X)-tree p in T.the_result_sort_of o;
let o be OperSymbol of S;
let x be object;
A17: (T * the ResultSort of S).o = T.((the ResultSort of S).o) by FUNCT_2:15
.= T.the_result_sort_of o by MSUALG_1:def 2;
assume x in rng ((Den(o,A))|((T# * the Arity of S).o));
then consider y being object such that
A18: y in dom ((Den(o,A))|((T# * the Arity of S).o)) and
A19: x = ((Den(o,A))|((T# * the Arity of S).o)).y by FUNCT_1:def 3;
y in dom Den(o,A) by A18,RELAT_1:57;
then reconsider y as Element of Args(o, A);
reconsider p = y as ArgumentSeq of Sym(o, X) by INSTALG1:1;
A20: (T# * the Arity of S).o = T#.((the Arity of S).o) by FUNCT_2:15
.= T#.the_arity_of o by MSUALG_1:def 1
.= product (T*the_arity_of o) by FINSEQ_2:def 5;
A21: rng p c= Union T
proof
let z be object;
A22: dom T = the carrier of S by PARTFUN1:def 2;
assume z in rng p;
then consider a being object such that
A23: a in dom p and
A24: z = p.a by FUNCT_1:def 3;
A25: dom p = dom (T*the_arity_of o) by A18,A20,CARD_3:9;
then
A26: z in (T*the_arity_of o).a & (T*the_arity_of o).a = T.((the_arity_of o
).a) by A18,A20,A23,A24,CARD_3:9,FUNCT_1:12;
rng the_arity_of o c= the carrier of S;
then dom (T*the_arity_of o) = dom the_arity_of o by A22,RELAT_1:27;
then (the_arity_of o).a in rng the_arity_of o by A23,A25,FUNCT_1:def 3;
hence thesis by A22,A26,CARD_5:2;
end;
x = Den(o, A).y by A18,A19,FUNCT_1:47
.= [o,the carrier of S]-tree y by INSTALG1:3
.= Sym(o, X)-tree p by MSAFREE:def 9;
hence thesis by A16,A17,A21;
end;
theorem Th21:
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
proof
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;
for o being OperSymbol of S for p being ArgumentSeq of Sym(o,Y) st rng p
c= Union (S-Terms(X,Y)) holds Sym(o,Y)-tree p in (S-Terms(X,Y)).
the_result_sort_of o by Th19;
hence thesis by Th20;
end;
theorem Th22:
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)
proof
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;
let s be object;
assume s in the carrier of S;
then reconsider s9 = s as SortSymbol of S;
let x be object;
assume x in ((Reverse Y)""X).s;
then
A1: x in ((Reverse Y).s9)"(X.s9) by EQUATION:def 1;
then
A2: x in dom ((Reverse Y).s) by FUNCT_1:def 7;
A3: ((Reverse Y).s).x in X.s by A1,FUNCT_1:def 7;
A4: (Reverse Y).s = Reverse(s9, Y) by MSAFREE:def 18;
then
A5: dom ((Reverse Y).s) = FreeGen(s9, Y) by FUNCT_2:def 1;
then consider b being set such that
A6: b in Y.s9 and
A7: x = root-tree [b,s9] by A2,MSAFREE:def 15;
FreeGen(s9, Y) = {root-tree t where t is Symbol of DTConMSA(Y): t in
Terminals DTConMSA(Y) & t`2 = s} by MSAFREE:13;
then consider a being Symbol of DTConMSA(Y) such that
A8: x = root-tree a and
a in Terminals DTConMSA(Y) and
a`2 = s by A2,A5;
Reverse(s9, Y).x = a`1 by A2,A5,A8,MSAFREE:def 17
.= [b,s]`1 by A8,A7,TREES_4:4
.= b;
hence thesis by A3,A4,A6,A7,Th18;
end;
theorem Th23:
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
proof
let S be non void non empty ManySortedSign;
let X be ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S)-->{0});
set T = the Sorts of Free(S, X);
defpred P[set] means for s being SortSymbol of S st $1 in S-Terms(X, Y).s
holds $1 in T.s;
A1: ex A being MSSubset of FreeMSA Y st Free(S, X) = GenMSAlg A & A = (
Reverse Y)""X by Def1;
then reconsider TT = T as MSSubset of FreeMSA Y by MSUALG_2:def 9;
A2: now
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,Y) such that
A3: for t being Term of S,Y st t in rng p holds P[t];
thus P[[o,the carrier of S]-tree p]
proof
let s be SortSymbol of S;
assume
A4: [o, the carrier of S]-tree p in S-Terms(X, Y).s;
A5: Sym(o,Y) = [o, the carrier of S] by MSAFREE:def 9;
the_sort_of (Sym(o,Y)-tree p) = the_result_sort_of o by MSATERM:20;
then
A6: s = the_result_sort_of o by A4,A5,Th17;
then
A7: rng p c= Union (S-Terms(X,Y)) by A4,A5,Th19;
A8: rng p c= Union TT
proof
let x be object;
assume
A9: x in rng p;
then consider y being object such that
A10: y in dom (S-Terms(X,Y)) and
A11: x in (S-Terms(X,Y)).y by A7,CARD_5:2;
reconsider y as SortSymbol of S by A10;
S-Terms(X, Y).y = S-Terms(X, Y).y;
then reconsider x as Term of S,Y by A11,Th16;
dom T = the carrier of S & x in T.y by A3,A9,A11,PARTFUN1:def 2;
hence thesis by CARD_5:2;
end;
TT is opers_closed by A1,MSUALG_2:def 9;
hence thesis by A5,A6,A8,Th20;
end;
end;
A12: S-Terms(X, Y) c= the Sorts of FreeMSA Y by PBOOLE:def 18;
A13: now
let s1 be SortSymbol of S, v be Element of Y.s1;
thus P[root-tree [v,s1]]
proof
reconsider t = root-tree [v,s1] as Term of S,Y by MSATERM:4;
let s be SortSymbol of S;
assume
A14: root-tree [v,s1] in S-Terms(X, Y).s;
S-Terms(X, Y).s c= (the Sorts of FreeMSA Y).s by A12;
then
A15: the_sort_of t = s by A14,Th7;
A16: the_sort_of t = s1 by MSATERM:14;
then v in X.s by A14,A15,Th18;
hence thesis by A15,A16,Th4;
end;
end;
thus for t being Term of S,Y holds P[t] from MSATERM:sch 1(A13,A2);
end;
theorem Th24:
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}))
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S)-->{0});
set B = MSAlgebra(# S-Terms(X, Y), Opers(FreeMSA Y, S-Terms(X, Y)) #);
for Z being MSSubset of FreeMSA Y st Z = the Sorts of B holds Z is
opers_closed & the Charact of B = Opers(FreeMSA Y, Z) by Th21;
then reconsider B as MSSubAlgebra of FreeMSA Y by MSUALG_2:def 9;
A1: FreeMSA Y = MSAlgebra(#FreeSort Y, FreeOper Y#) & dom FreeSort Y = the
carrier of S by MSAFREE:def 14,PARTFUN1:def 2;
(Reverse Y)""X c= S-Terms(X, Y) by Th22;
then
A2: (Reverse Y)""X is MSSubset of B by PBOOLE:def 18;
let s be Element of S;
ex A being MSSubset of FreeMSA Y st Free(S, X) = GenMSAlg A & A = (
Reverse Y)""X by Def1;
then Free(S, X) is MSSubAlgebra of B by A2,MSUALG_2:def 17;
then the Sorts of Free(S, X) is MSSubset of B by MSUALG_2:def 9;
then the Sorts of Free(S, X) c= S-Terms(X, Y) by PBOOLE:def 18;
hence (the Sorts of Free(S, X)).s c= S-Terms(X, Y).s;
let x be object;
assume
A3: x in S-Terms(X, Y).s;
S-Terms(X, Y) c= the Sorts of FreeMSA Y by PBOOLE:def 18;
then (S-Terms(X, Y)).s c= (the Sorts of FreeMSA Y).s;
then x in Union FreeSort Y by A3,A1,CARD_5:2;
then x is Term of S,Y by MSATERM:13;
hence thesis by A3,Th23;
end;
theorem
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)
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S)-->{0});
(FreeMSA Y)|(S-Terms(X, Y)) = MSAlgebra(#S-Terms(X, Y), Opers(FreeMSA Y,
S -Terms(X, Y))#) & ex A being MSSubset of FreeMSA Y st Free(S, X) = GenMSAlg A
& A = (Reverse Y)""X by Def1,Th21,MSUALG_2:def 15;
hence thesis by Th24,MSUALG_2:9;
end;
theorem Th26:
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
proof
let S be non void Signature;
let X,Y be non-empty ManySortedSet of the carrier of S;
let A be MSSubAlgebra of FreeMSA X;
let B be MSSubAlgebra of FreeMSA Y such that
A1: the Sorts of A = the Sorts of B;
reconsider SB = the Sorts of B as MSSubset of FreeMSA Y by MSUALG_2:def 9;
reconsider SA = the Sorts of A as MSSubset of FreeMSA X by MSUALG_2:def 9;
A2: SA is opers_closed by MSUALG_2:def 9;
A3: SB is opers_closed by MSUALG_2:def 9;
now
let x be object;
A4: SA c= the Sorts of FreeMSA X & the Sorts of FreeMSA X is MSSubset of
FreeMSA X by PBOOLE:def 18;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
A5: SA is_closed_on o by A2;
A6: (the Charact of A).o = Opers(FreeMSA X, SA).o by MSUALG_2:def 9
.= o /. SA by MSUALG_2:def 8
.= (Den(o, FreeMSA X))|((SA# * the Arity of S).o) by A5,MSUALG_2:def 7;
Args(o, FreeMSA X) = ((the Sorts of FreeMSA X)#*the Arity of S).o by
MSUALG_1:def 4;
then dom Den(o,FreeMSA X) = ((the Sorts of FreeMSA X)#*the Arity of S).o
by FUNCT_2:def 1;
then
A7: dom ((the Charact of A).o) = (SA#*the Arity of S).o by A6,A4,MSUALG_2:2
,RELAT_1:62;
A8: SB c= the Sorts of FreeMSA Y & the Sorts of FreeMSA Y is MSSubset of
FreeMSA Y by PBOOLE:def 18;
then
A9: (SB#*the Arity of S).o c= ((the Sorts of FreeMSA Y)#*the Arity of S).
o by MSUALG_2:2;
A10: SB is_closed_on o by A3;
A11: (the Charact of B).o = Opers(FreeMSA Y, SB).o by MSUALG_2:def 9
.= o /. SB by MSUALG_2:def 8
.= (Den(o, FreeMSA Y))|((SB# * the Arity of S).o) by A10,MSUALG_2:def 7;
Args(o, FreeMSA Y) = ((the Sorts of FreeMSA Y)#*the Arity of S).o by
MSUALG_1:def 4;
then dom Den(o,FreeMSA Y) = ((the Sorts of FreeMSA Y)#*the Arity of S).o
by FUNCT_2:def 1;
then
A12: dom ((the Charact of B).o) = (SB#*the Arity of S).o by A11,A8,MSUALG_2:2
,RELAT_1:62;
A13: (SA#*the Arity of S).o c= ((the Sorts of FreeMSA X)#*the Arity of S)
.o by A4,MSUALG_2:2;
now
let x be object;
assume
A14: x in (SA#*the Arity of S).o;
then reconsider p1 = x as Element of Args(o, FreeMSA X) by A13,
MSUALG_1:def 4;
reconsider p2 = x as Element of Args(o, FreeMSA Y) by A1,A9,A14,
MSUALG_1:def 4;
thus ((the Charact of A).o).x = Den(o, FreeMSA X).p1 by A6,A7,A14,
FUNCT_1:47
.= [o, the carrier of S]-tree p1 by INSTALG1:3
.= Den(o, FreeMSA Y).p2 by INSTALG1:3
.= ((the Charact of B).o).x by A1,A11,A12,A14,FUNCT_1:47;
end;
hence (the Charact of A).x = (the Charact of B).x by A1,A7,A12,FUNCT_1:2;
end;
hence thesis by A1,PBOOLE:3;
end;
theorem Th27:
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
proof
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let Y be ManySortedSet of the carrier of S;
let t be Element of Free(S, X);
set Z = X (\/) ((the carrier of S)-->{0});
reconsider t as Term of S,Z by Th8;
t in Union the Sorts of Free(S, X);
then
A1: t in Union (S-Terms(X,Z)) by Th24;
dom (S-Terms(X,Z)) = the carrier of S by PARTFUN1:def 2;
then ex s being object st s in the carrier of S & t in S-Terms(X,Z).s by A1,
CARD_5:2;
then variables_in t c= X by Th17;
hence thesis;
end;
theorem Th28:
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
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
defpred P[DecoratedTree] means S variables_in $1 c= X;
let t be Term of S,X;
A1: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st for t
being Term of S,X st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S, p be ArgumentSeq of Sym(o, X) such that
A2: for t being Term of S,X st t in rng p holds S variables_in t c= X;
thus S variables_in ([o, the carrier of S]-tree p) c= X
proof
let s be object;
assume
A3: s in the carrier of S;
let x be object;
assume x in (S variables_in ([o, the carrier of S]-tree p)).s;
then consider t being DecoratedTree such that
A4: t in rng p and
A5: x in (S variables_in t).s by A3,Th11;
consider i being object such that
A6: i in dom p and
A7: t = p.i by A4,FUNCT_1:def 3;
reconsider i as Nat by A6;
reconsider t = p.i as Term of S,X by A6,MSATERM:22;
S variables_in t c= X by A2,A4,A7;
then (S variables_in t).s c= X.s by A3;
hence thesis by A5,A7;
end;
end;
A8: for s being SortSymbol of S, v being Element of X.s holds P[root-tree [v
,s]]
proof
let s be SortSymbol of S, x be Element of X.s;
thus S variables_in root-tree [x,s] c= X
proof
let y be object;
assume y in the carrier of S;
A9: y <> s implies (S variables_in root-tree [x,s]).y = {} by Th10;
(S variables_in root-tree [x,s]).s = {x} by Th10;
hence thesis by A9;
end;
end;
for t being Term of S,X holds P[t] from MSATERM:sch 1(A8,A1);
hence thesis;
end;
theorem Th29:
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
proof
let S be non void Signature;
let X,Y be non-empty ManySortedSet of the carrier of S;
let t1 be Term of S,X, t2 be Term of S,Y such that
A1: t1 = t2;
per cases by MSATERM:2;
suppose
ex s being SortSymbol of S, v being Element of X.s st t1.{} = [v,s ];
then consider s being SortSymbol of S, x be Element of X.s such that
A2: t1.{} = [x,s];
s in the carrier of S;
then s <> the carrier of S;
then not s in {the carrier of S} by TARSKI:def 1;
then not [x,s] in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1:87;
then consider s9 being SortSymbol of S, y be Element of Y.s9 such that
A3: t2.{} = [y,s9] by A1,A2,MSATERM:2;
t1 = root-tree [x,s] by A2,MSATERM:5;
then
A4: the_sort_of t1 = s by MSATERM:14;
t2 = root-tree [y,s9] by A3,MSATERM:5;
then the_sort_of t2 = s9 by MSATERM:14;
hence thesis by A1,A2,A3,A4,XTUPLE_0:1;
end;
suppose
t1.{} in [:the carrier' of S,{the carrier of S}:];
then consider o,z being object such that
A5: o in the carrier' of S and
A6: z in {the carrier of S} and
A7: t1.{} = [o,z] by ZFMISC_1:def 2;
reconsider o as OperSymbol of S by A5;
A8: z = the carrier of S by A6,TARSKI:def 1;
then the_sort_of t1 = the_result_sort_of o by A7,MSATERM:17;
hence thesis by A1,A7,A8,MSATERM:17;
end;
end;
theorem Th30:
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
proof
let S be non void Signature;
let X,Y be non-empty ManySortedSet of the carrier of S;
defpred P[DecoratedTree] means Y variables_in $1 c= X implies $1 is Term of
S,X;
let t be Term of S,Y;
A1: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,Y) st for t
being Term of S,Y st t in rng p holds P[t] holds P[[o, the carrier of S]-tree p
]
proof
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,Y) such that
A2: for t being Term of S,Y st t in rng p & Y variables_in t c= X
holds t is Term of S,X and
A3: Y variables_in ([o, the carrier of S]-tree p) c= X;
A4: now
let i be Nat;
assume
A5: i in dom p;
then reconsider t = p.i as Term of S,Y by MSATERM:22;
A6: t in rng p by A5,FUNCT_1:def 3;
Y variables_in t c= X
proof
let y be object;
assume y in the carrier of S;
then reconsider s = y as SortSymbol of S;
let x be object;
assume x in (Y variables_in t).y;
then
A7: x in (Y variables_in ([o, the carrier of S]-tree p)).s by A6,Th13;
(Y variables_in ([o, the carrier of S]-tree p)).s c= X.s by A3;
hence thesis by A7;
end;
then reconsider t9 = t as Term of S,X by A2,A6;
take t9;
thus t9 = p.i;
the_sort_of t = (the_arity_of o).i by A5,MSATERM:23;
hence the_sort_of t9 = (the_arity_of o).i by Th29;
end;
len p = len the_arity_of o by MSATERM:22;
then reconsider p as ArgumentSeq of Sym(o,X) by A4,MSATERM:24;
Sym(o,X)-tree p is Term of S,X;
hence thesis by MSAFREE:def 9;
end;
assume variables_in t c= X;
then
A8: Y variables_in t c= X by Th15;
A9: for s being SortSymbol of S, x being Element of Y.s holds P[root-tree [x
,s]]
proof
let s be SortSymbol of S, x be Element of Y.s;
assume Y variables_in root-tree [x,s] c= X;
then
A10: (Y variables_in root-tree [x,s]).s c= X.s;
(Y variables_in root-tree [x,s]).s = {x} by Th12;
then x in X.s by A10,ZFMISC_1:31;
hence thesis by MSATERM:4;
end;
for t being Term of S,Y holds P[t] from MSATERM:sch 1(A9,A1);
hence thesis by A8;
end;
theorem
for S being non void Signature for X being non-empty ManySortedSet of
the carrier of S holds Free(S, X) = FreeMSA X
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S)-->{0});
A1: the Sorts of Free(S, X) = S-Terms(X,Y) by Th24;
A2: FreeMSA X = MSAlgebra(#FreeSort X, FreeOper X#) by MSAFREE:def 14;
A3: the Sorts of Free(S, X) = the Sorts of FreeMSA X
proof
let s be Element of S;
reconsider s9 = s as SortSymbol of S;
thus (the Sorts of Free(S, X)).s c= (the Sorts of FreeMSA X).s
proof
let x be object;
assume
A4: x in (the Sorts of Free(S, X)).s;
then reconsider t = x as Term of S, Y by A1,Th16;
variables_in t c= X by A1,A4,Th17;
then reconsider t9 = t as Term of S,X by Th30;
the_sort_of t = s by A1,A4,Th17;
then the_sort_of t9 = s by Th29;
then x in FreeSort(X, s9) by MSATERM:def 5;
hence thesis by A2,MSAFREE:def 11;
end;
reconsider s9 = s as SortSymbol of S;
let x be object;
assume x in (the Sorts of FreeMSA X).s;
then
A5: x in FreeSort(X, s9) by A2,MSAFREE:def 11;
FreeSort(X, s9) c= S-Terms X by MSATERM:12;
then reconsider t = x as Term of S,X by A5;
X c= Y by PBOOLE:14;
then reconsider t9 = t as Term of S,Y by MSATERM:26;
variables_in t = S variables_in t;
then
A6: variables_in t9 c= X by Th28;
the_sort_of t = s by A5,MSATERM:def 5;
then the_sort_of t9 = s by Th29;
then
t in {q where q is Term of S,Y: the_sort_of q = s9 & variables_in q
c= X} by A6;
hence thesis by A1,Def5;
end;
FreeMSA X is MSSubAlgebra of FreeMSA X & ex A being MSSubset of FreeMSA
Y st Free(S, X) = GenMSAlg A & A = (Reverse Y)""X by Def1,MSUALG_2:5;
hence thesis by A3,Th26;
end;
theorem Th32:
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
proof
let S be non void Signature;
let Y be non-empty ManySortedSet of the carrier of S;
let t be Term of S,Y;
let p be Element of dom t;
reconsider q = t|p as Term of S,Y;
let s be object;
assume
A1: s in the carrier of S;
let x be object;
assume x in (variables_in (t|p)).s;
then x in {a`1 where a is Element of rng q: a`2 = s} by A1,Def2;
then consider a being Element of rng (t|p) such that
A2: x = a`1 & a`2 = s;
rng (t|p) c= rng t & a in rng (t|p) by TREES_2:32;
then x in {b`1 where b is Element of rng t: b`2 = s} by A2;
hence thesis by A1,Def2;
end;
theorem Th33:
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)
proof
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S, X);
let p be Element of dom t;
set Y = X (\/) ((the carrier of S) --> {0});
reconsider t as Term of S,Y by Th8;
reconsider p as Element of dom t;
A1: variables_in (t|p) c= variables_in t by Th32;
A2: the Sorts of Free(S, X) = S-Terms(X, Y) & dom (S-Terms(X, Y)) = the
carrier of S by Th24,PARTFUN1:def 2;
then ex x being object st x in the carrier of S & t in (S-Terms(X, Y)).x
by CARD_5:2;
then variables_in t c= X by Th17;
then variables_in (t|p) c= X by A1,PBOOLE:13;
then t|p in {q where q is Term of S,Y: the_sort_of q = the_sort_of (t|p) &
variables_in q c= X};
then t|p in S-Terms(X,Y).the_sort_of (t|p) by Def5;
hence thesis by A2,CARD_5:2;
end;
theorem Th34:
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]
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
let t be Term of S,X;
let a be Element of rng t;
consider x being object such that
A1: x in dom t and
A2: a = t.x by FUNCT_1:def 3;
reconsider x as Element of dom t by A1;
a = (t|x).{} by A2,TREES_9:35;
then (ex s being SortSymbol of S, v being Element of X.s st a = [v,s]) or a
in [:the carrier' of S,{the carrier of S}:] by MSATERM:2;
hence thesis by MCART_1:21;
end;
theorem
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)
proof
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S, X);
let s be SortSymbol of S;
set Y = X (\/) ((the carrier of S) --> {0});
hereby
assume x in (S variables_in t).s;
then x in {a`1 where a is Element of rng t: a`2 = s} by Def2;
then consider a being Element of rng t such that
A1: x = a`1 & a`2 = s;
t is Term of S,Y & a in rng t by Th8;
hence [x,s] in rng t by A1,Th34;
end;
assume
A2: [x,s] in rng t;
then consider z being object such that
A3: z in dom t and
A4: [x,s] = t.z by FUNCT_1:def 3;
reconsider z as Element of dom t by A3;
reconsider q = t|z as Element of Free(S, X) by Th33;
A5: [x,s] = q.{} by A4,TREES_9:35;
[x,s]`1 = x & [x,s]`2 = s;
then
A6: x in {a`1 where a is Element of rng t: a`2 = s} by A2;
A7: q is Term of S,Y by Th8;
s in the carrier of S;
then s <> the carrier of S;
then not s in {the carrier of S} by TARSKI:def 1;
then not [x,s] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
then consider s9 being SortSymbol of S, v being Element of Y.s9 such that
A8: [x,s] = [v,s9] by A5,A7,MSATERM:2;
S variables_in q c= X by Th27;
then
A9: (S variables_in q).s9 c= X.s9;
q = root-tree [v,s9] by A5,A7,A8,MSATERM:5;
then (S variables_in q).s9 = {v} by Th10;
then
A10: v in X.s9 by A9,ZFMISC_1:31;
x = v by A8,XTUPLE_0:1;
hence thesis by A8,A10,A6,Def2,XTUPLE_0:1;
end;
theorem
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
proof
let C be non void Signature;
let X be ManySortedSet of the carrier of C such that
A1: for s being SortSymbol of C st X.s = {} ex o being OperSymbol of C
st the_result_sort_of o = s & the_arity_of o = {};
now
assume {} in rng the Sorts of Free(C, X);
then consider s being object such that
A2: s in dom the Sorts of Free(C, X) and
A3: {} = (the Sorts of Free(C, X)).s by FUNCT_1:def 3;
reconsider s as SortSymbol of C by A2;
set x = the Element of X.s;
per cases;
suppose
X.s = {};
then
ex m being OperSymbol of C st the_result_sort_of m = s & the_arity_of
m = {} by A1;
hence contradiction by A3,Th5;
end;
suppose
X.s <> {};
then root-tree [x, s] in (the Sorts of Free(C, X)).s by Th4;
hence contradiction by A3;
end;
end;
then the Sorts of Free(C, X) is non-empty by RELAT_1:def 9;
hence thesis by MSUALG_1:def 3;
end;
theorem Th37:
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)
proof
let S be non void non empty ManySortedSign;
let A be MSAlgebra over S;
let B be MSSubAlgebra of A;
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
let o be OperSymbol of S;
reconsider SA = the Sorts of A as MSSubset of A by PBOOLE:def 18;
A1: Args(o,B) = (SB# * the Arity of S).o by MSUALG_1:def 4;
SB c= SA & Args(o,A) = (SA# * the Arity of S).o by MSUALG_1:def 4
,PBOOLE:def 18;
hence thesis by A1,MSUALG_2:2;
end;
theorem Th38:
for S being non void Signature for A being feasible MSAlgebra
over S for B being MSSubAlgebra of A holds B is feasible
proof
let S be non void Signature;
let A be feasible MSAlgebra over S;
let B be MSSubAlgebra of A;
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
let o be OperSymbol of S;
set a = the Element of Args(o,B);
assume Args(o,B) <> {};
then
A1: a in Args(o,B);
A2: Args(o,B) c= Args(o,A) by Th37;
then Result(o,A) <> {} by A1,MSUALG_6:def 1;
then dom Den(o,A) = Args(o,A) by FUNCT_2:def 1;
then a in dom (Den(o,A)|Args(o,B)) by A1,A2,RELAT_1:57;
then
A3: Result(o,B) = (SB * the ResultSort of S).o & (Den(o,A)|Args(o,B)).a in
rng ( Den(o,A)|Args(o,B)) by FUNCT_1:def 3,MSUALG_1:def 5;
SB is opers_closed by MSUALG_2:def 9;
then SB is_closed_on o;
then
rng ((Den(o,A))|((SB# * the Arity of S).o)) c= (SB * the ResultSort of S
).o;
hence thesis by A3,MSUALG_1:def 4;
end;
registration
let S be non void Signature, A be feasible MSAlgebra over S;
cluster -> feasible for MSSubAlgebra of A;
coherence by Th38;
end;
theorem Th39:
for S being non void Signature for X being ManySortedSet of the
carrier of S holds Free(S, X) is feasible free
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
set Y = X (\/) ((the carrier of S) --> {0});
consider A being MSSubset of FreeMSA Y such that
A1: Free(S, X) = GenMSAlg A and
A2: A = (Reverse Y)"" X by Def1;
thus Free(S, X) is feasible by A1;
A is ManySortedSubset of FreeGen Y by A2,EQUATION:8;
then A c= FreeGen Y by PBOOLE:def 18;
hence thesis by A1,EQUATION:28;
end;
registration
let S be non void Signature, X be ManySortedSet of the carrier of S;
cluster Free(S, X) -> feasible free;
coherence by Th39;
end;