set FM = FreeMSA X;
set D = DTConMSA X;
deffunc H1( Element of S) -> Subset of ((FreeSort X) . $1) = FreeGen $1,X;
consider f being Function such that
A1:
( dom f = the carrier of S & ( for s being Element of S holds f . s = H1(s) ) )
from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of by A1, PARTFUN1:def 4, RELAT_1:def 18;
f c= the Sorts of (FreeMSA X)
then reconsider f = f as MSSubset of (FreeMSA X) by PBOOLE:def 23;
the Sorts of (GenMSAlg f) = the Sorts of (FreeMSA X)
proof
the
Sorts of
(GenMSAlg f) is
MSSubset of
(FreeMSA X)
by MSUALG_2:def 10;
hence A2:
the
Sorts of
(GenMSAlg f) c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 23;
:: according to PBOOLE:def 13 :: thesis: the Sorts of (FreeMSA X) c= the Sorts of (GenMSAlg f)
defpred S1[
set ]
means $1
in union (rng the Sorts of (GenMSAlg f));
A3:
for
s being
Symbol of
(DTConMSA X) st
s in Terminals (DTConMSA X) holds
S1[
root-tree s]
proof
let t be
Symbol of
(DTConMSA X);
:: thesis: ( t in Terminals (DTConMSA X) implies S1[ root-tree t] )
assume
t in Terminals (DTConMSA X)
;
:: thesis: S1[ root-tree t]
then
t in Union (coprod X)
by Th6;
then
t in union (rng (coprod X))
by CARD_3:def 4;
then consider A being
set such that A4:
(
t in A &
A in rng (coprod X) )
by TARSKI:def 4;
consider s being
set such that A5:
(
s in dom (coprod X) &
(coprod X) . s = A )
by A4, FUNCT_1:def 5;
reconsider s =
s as
SortSymbol of
S by A5, PARTFUN1:def 4;
A = coprod s,
X
by A5, Def3;
then consider a being
set such that A6:
(
a in X . s &
t = [a,s] )
by A4, Def2;
f is
MSSubset of
(GenMSAlg f)
by MSUALG_2:def 18;
then
f c= the
Sorts of
(GenMSAlg f)
by PBOOLE:def 23;
then
f . s c= the
Sorts of
(GenMSAlg f) . s
by PBOOLE:def 5;
then A7:
FreeGen s,
X c= the
Sorts of
(GenMSAlg f) . s
by A1;
A8:
root-tree t in FreeGen s,
X
by A6, Def17;
dom the
Sorts of
(GenMSAlg f) = the
carrier of
S
by PARTFUN1:def 4;
then
the
Sorts of
(GenMSAlg f) . s in rng the
Sorts of
(GenMSAlg f)
by FUNCT_1:def 5;
hence
S1[
root-tree t]
by A7, A8, TARSKI:def 4;
:: thesis: verum
end;
A9:
for
nt being
Symbol of
(DTConMSA X) for
ts being
FinSequence of
TS (DTConMSA X) st
nt ==> roots ts & ( for
t being
DecoratedTree of st
t in rng ts holds
S1[
t] ) holds
S1[
nt -tree ts]
proof
let nt be
Symbol of
(DTConMSA X);
:: thesis: for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA X);
:: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume A10:
(
nt ==> roots ts & ( for
t being
DecoratedTree of st
t in rng ts holds
S1[
t] ) )
;
:: thesis: S1[nt -tree ts]
set G =
GenMSAlg f;
set OU =
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
reconsider B = the
Sorts of
(GenMSAlg f) as
MSSubset of
(FreeMSA X) by MSUALG_2:def 10;
set AR = the
Arity of
S;
set RS = the
ResultSort of
S;
set BH =
(B # ) * the
Arity of
S;
set O = the
carrier' of
S;
A11:
B is
opers_closed
by MSUALG_2:def 10;
A12:
[nt,(roots ts)] in the
Rules of
(DTConMSA X)
by A10, LANG1:def 1;
A13:
[nt,(roots ts)] in REL X
by A10, LANG1:def 1;
reconsider sy =
nt as
Element of
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
reconsider rt =
roots ts as
Element of
([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A12, ZFMISC_1:106;
[sy,rt] in REL X
by A10, LANG1:def 1;
then
sy in [:the carrier' of S,{the carrier of S}:]
by Def9;
then consider o being
OperSymbol of
S,
x2 being
Element of
{the carrier of S} such that A14:
sy = [o,x2]
by DOMAIN_1:9;
A15:
x2 = the
carrier of
S
by TARSKI:def 1;
set ar =
the_arity_of o;
set rs =
the_result_sort_of o;
B is_closed_on o
by A11, MSUALG_2:def 7;
then A16:
rng ((Den o,(FreeMSA X)) | (((B # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
by MSUALG_2:def 6;
A17:
(
Sym o,
X = [o,the carrier of S] &
nt = [o,the carrier of S] )
by A14, TARSKI:def 1;
A18:
Den o,
(FreeMSA X) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp o,
X
by Def15
;
A19:
(
dom (FreeSort X) = the
carrier of
S &
o in the
carrier' of
S &
dom B = the
carrier of
S &
dom the
ResultSort of
S = the
carrier' of
S &
rng the
ResultSort of
S c= the
carrier of
S & the
Arity of
S . o = the_arity_of o & the
ResultSort of
S . o = the_result_sort_of o )
by MSUALG_1:def 6, MSUALG_1:def 7, PARTFUN1:def 4, RELAT_1:def 19;
dom (DenOp o,X) = (((FreeSort X) # ) * the Arity of S) . o
by FUNCT_2:def 1;
then A20:
ts in dom (DenOp o,X)
by A10, A17, Th10;
A21:
((B # ) * the Arity of S) . o = product (B * (the_arity_of o))
by A19, Th1;
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then A22:
dom (B * (the_arity_of o)) = dom (the_arity_of o)
by A19, RELAT_1:46;
A23:
dom (roots ts) = dom ts
by TREES_3:def 18;
A24:
(
len rt = len (the_arity_of o) & ( for
x being
set st
x in dom rt holds
( (
rt . x in [:the carrier' of S,{the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1,the carrier of S] = rt . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & (
rt . x in Union (coprod X) implies
rt . x in coprod ((the_arity_of o) . x),
X ) ) ) )
by A13, A14, A15, Th5;
A25:
(
Seg (len rt) = dom rt &
Seg (len (the_arity_of o)) = dom (the_arity_of o) )
by FINSEQ_1:def 3;
then A26:
dom ts = dom (the_arity_of o)
by A12, A14, A15, A23, Th5;
for
x being
set st
x in dom (B * (the_arity_of o)) holds
ts . x in (B * (the_arity_of o)) . x
proof
let x be
set ;
:: thesis: ( x in dom (B * (the_arity_of o)) implies ts . x in (B * (the_arity_of o)) . x )
assume A27:
x in dom (B * (the_arity_of o))
;
:: thesis: ts . x in (B * (the_arity_of o)) . x
then reconsider n =
x as
Nat by A22;
A28:
rng ts c= TS (DTConMSA X)
by FINSEQ_1:def 4;
A29:
ts . n in rng ts
by A22, A23, A24, A25, A27, FUNCT_1:def 5;
then reconsider T =
ts . x as
Element of
TS (DTConMSA X) by A28;
S1[
T]
by A10, A29;
then consider A being
set such that A30:
(
T in A &
A in rng the
Sorts of
(GenMSAlg f) )
by TARSKI:def 4;
consider s being
set such that A31:
(
s in dom the
Sorts of
(GenMSAlg f) & the
Sorts of
(GenMSAlg f) . s = A )
by A30, FUNCT_1:def 5;
reconsider s =
s as
SortSymbol of
S by A31, PARTFUN1:def 4;
A32:
(B * (the_arity_of o)) . x =
B . ((the_arity_of o) . n)
by A27, FUNCT_1:22
.=
B . ((the_arity_of o) /. n)
by A22, A27, PARTFUN1:def 8
;
set b =
(the_arity_of o) /. n;
set A1 =
{ a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } ;
A33:
{ a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } =
FreeSort X,
((the_arity_of o) /. n)
.=
(FreeSort X) . ((the_arity_of o) /. n)
by Def13
;
consider t being
DecoratedTree such that A34:
(
t = ts . n &
rt . n = t . {} )
by A22, A23, A24, A25, A27, TREES_3:def 18;
A35:
rng rt c= [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))
by FINSEQ_1:def 4;
A36:
rt . n in rng rt
by A22, A24, A25, A27, FUNCT_1:def 5;
A37:
now per cases
( rt . n in [:the carrier' of S,{the carrier of S}:] or rt . n in Union (coprod X) )
by A35, A36, XBOOLE_0:def 3;
suppose A38:
rt . n in [:the carrier' of S,{the carrier of S}:]
;
:: thesis: T in (FreeSort X) . ((the_arity_of o) /. n)then consider o1 being
OperSymbol of
S,
x2 being
Element of
{the carrier of S} such that A39:
rt . n = [o1,x2]
by DOMAIN_1:9;
A40:
x2 = the
carrier of
S
by TARSKI:def 1;
then the_result_sort_of o1 =
(the_arity_of o) . n
by A12, A14, A15, A22, A23, A26, A27, A38, A39, Th5
.=
(the_arity_of o) /. n
by A22, A27, PARTFUN1:def 8
;
hence
T in (FreeSort X) . ((the_arity_of o) /. n)
by A33, A34, A39, A40;
:: thesis: verum end; suppose A41:
rt . n in Union (coprod X)
;
:: thesis: T in (FreeSort X) . ((the_arity_of o) /. n)then
rt . n in coprod ((the_arity_of o) . n),
X
by A12, A14, A15, A22, A23, A26, A27, Th5;
then
rt . n in coprod ((the_arity_of o) /. n),
X
by A22, A27, PARTFUN1:def 8;
then consider a being
set such that A42:
(
a in X . ((the_arity_of o) /. n) &
rt . n = [a,((the_arity_of o) /. n)] )
by Def2;
reconsider tt =
rt . n as
Terminal of
(DTConMSA X) by A41, Th6;
T = root-tree tt
by A34, DTCONSTR:9;
hence
T in (FreeSort X) . ((the_arity_of o) /. n)
by A33, A42;
:: thesis: verum end;
hence
ts . x in (B * (the_arity_of o)) . x
by A30, A31, A32;
:: thesis: verum
end;
then
ts in ((B # ) * the Arity of S) . o
by A21, A22, A23, A24, A25, CARD_3:18;
then
ts in (dom (DenOp o,X)) /\ (((B # ) * the Arity of S) . o)
by A20, XBOOLE_0:def 4;
then A44:
ts in dom ((DenOp o,X) | (((B # ) * the Arity of S) . o))
by RELAT_1:90;
then ((DenOp o,X) | (((B # ) * the Arity of S) . o)) . ts =
(DenOp o,X) . ts
by FUNCT_1:70
.=
nt -tree ts
by A10, A17, Def14
;
then A45:
nt -tree ts in rng ((Den o,(FreeMSA X)) | (((B # ) * the Arity of S) . o))
by A18, A44, FUNCT_1:def 5;
dom (B * the ResultSort of S) = the
carrier' of
S
by PARTFUN1:def 4;
then
(
(B * the ResultSort of S) . o = B . (the_result_sort_of o) &
B . (the_result_sort_of o) in rng B )
by A19, FUNCT_1:22, FUNCT_1:def 5;
hence
S1[
nt -tree ts]
by A16, A45, TARSKI:def 4;
:: thesis: verum
end;
A46:
for
t being
DecoratedTree of st
t in TS (DTConMSA X) holds
S1[
t]
from DTCONSTR:sch 7(A3, A9);
A47:
union (rng the Sorts of (FreeMSA X)) c= union (rng the Sorts of (GenMSAlg f))
let x be
set ;
:: according to PBOOLE:def 5 :: thesis: ( not x in the carrier of S or the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x )
assume
x in the
carrier of
S
;
:: thesis: the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x
then reconsider s =
x as
SortSymbol of
S ;
the
Sorts of
(FreeMSA X) . s c= the
Sorts of
(GenMSAlg f) . s
hence
the
Sorts of
(FreeMSA X) . x c= the
Sorts of
(GenMSAlg f) . x
;
:: thesis: verum
end;
then reconsider f = f as GeneratorSet of FreeMSA X by Def4;
take
f
; :: thesis: for s being SortSymbol of S holds f . s = FreeGen s,X
thus
for s being SortSymbol of S holds f . s = FreeGen s,X
by A1; :: thesis: verum