deffunc H1( Element of S) -> Subset of ((FreeSort X) . $1) = FreeGen ($1,X);
set FM = FreeMSA X;
set D = DTConMSA 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 the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
f c= the Sorts of (FreeMSA X)
then reconsider f = f as MSSubset of (FreeMSA X) by PBOOLE:def 18;
the Sorts of (GenMSAlg f) = the Sorts of (FreeMSA X)
proof
defpred S1[
set ]
means $1
in union (rng the Sorts of (GenMSAlg f));
the
Sorts of
(GenMSAlg f) is
MSSubset of
(FreeMSA X)
by MSUALG_2:def 9;
then A2:
the
Sorts of
(GenMSAlg f) c= the
Sorts of
(FreeMSA X)
by PBOOLE:def 18;
A3:
for
nt being
Symbol of
(DTConMSA X) for
ts being
FinSequence of
TS (DTConMSA X) st
nt ==> roots ts & ( for
t being
DecoratedTree of the
carrier of
(DTConMSA X) st
t in rng ts holds
S1[
t] ) holds
S1[
nt -tree ts]
proof
set G =
GenMSAlg f;
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
let nt be
Symbol of
(DTConMSA X);
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A4:
nt ==> roots ts
and A5:
for
t being
DecoratedTree of the
carrier of
(DTConMSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
reconsider sy =
nt as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
A6:
[nt,(roots ts)] in the
Rules of
(DTConMSA X)
by A4, LANG1:def 1;
then reconsider rt =
roots ts as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
[sy,rt] in REL X
by A4, LANG1:def 1;
then
sy in [: the carrier' of S,{ the carrier of S}:]
by Def7;
then consider o being
OperSymbol of
S,
x2 being
Element of
{ the carrier of S} such that A7:
sy = [o,x2]
by DOMAIN_1:1;
set ar =
the_arity_of o;
set rs =
the_result_sort_of o;
A8:
x2 = the
carrier of
S
by TARSKI:def 1;
[nt,(roots ts)] in REL X
by A4, LANG1:def 1;
then A9:
len rt = len (the_arity_of o)
by A7, A8, Th5;
reconsider B = the
Sorts of
(GenMSAlg f) as
MSSubset of
(FreeMSA X) by MSUALG_2:def 9;
A10:
dom B = the
carrier of
S
by PARTFUN1:def 2;
A11:
dom (roots ts) = dom ts
by TREES_3:def 18;
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then A12:
dom (B * (the_arity_of o)) = dom (the_arity_of o)
by A10, RELAT_1:27;
A13:
(
Seg (len rt) = dom rt &
Seg (len (the_arity_of o)) = dom (the_arity_of o) )
by FINSEQ_1:def 3;
then A14:
dom ts = dom (the_arity_of o)
by A6, A7, A8, A11, Th5;
A15:
for
x being
object st
x in dom (B * (the_arity_of o)) holds
ts . x in (B * (the_arity_of o)) . x
proof
let x be
object ;
( x in dom (B * (the_arity_of o)) implies ts . x in (B * (the_arity_of o)) . x )
assume A16:
x in dom (B * (the_arity_of o))
;
ts . x in (B * (the_arity_of o)) . x
then reconsider n =
x as
Nat ;
A17:
ts . n in rng ts
by A12, A11, A9, A13, A16, FUNCT_1:def 3;
rng ts c= TS (DTConMSA X)
by FINSEQ_1:def 4;
then reconsider T =
ts . x as
Element of
TS (DTConMSA X) by A17;
S1[
T]
by A5, A17;
then consider A being
set such that A18:
T in A
and A19:
A in rng the
Sorts of
(GenMSAlg f)
by TARSKI:def 4;
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 ) ) } ;
A20:
{ 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 Def11
;
A21:
ex
t being
DecoratedTree st
(
t = ts . n &
rt . n = t . {} )
by A12, A11, A9, A13, A16, TREES_3:def 18;
consider s being
object such that A22:
s in dom the
Sorts of
(GenMSAlg f)
and A23:
the
Sorts of
(GenMSAlg f) . s = A
by A19, FUNCT_1:def 3;
reconsider s =
s as
SortSymbol of
S by A22;
A24:
(
rng rt c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) &
rt . n in rng rt )
by A12, A9, A13, A16, FINSEQ_1:def 4, FUNCT_1:def 3;
A25:
now T in (FreeSort X) . ((the_arity_of o) /. n)per cases
( rt . n in [: the carrier' of S,{ the carrier of S}:] or rt . n in Union (coprod X) )
by A24, XBOOLE_0:def 3;
suppose A26:
rt . n in [: the carrier' of S,{ the carrier of S}:]
;
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 A27:
rt . n = [o1,x2]
by DOMAIN_1:1;
A28:
x2 = the
carrier of
S
by TARSKI:def 1;
then the_result_sort_of o1 =
(the_arity_of o) . n
by A6, A7, A8, A12, A11, A14, A16, A26, A27, Th5
.=
(the_arity_of o) /. n
by A12, A16, PARTFUN1:def 6
;
hence
T in (FreeSort X) . ((the_arity_of o) /. n)
by A20, A21, A27, A28;
verum end; suppose A29:
rt . n in Union (coprod X)
;
T in (FreeSort X) . ((the_arity_of o) /. n)then
rt . n in coprod (
((the_arity_of o) . n),
X)
by A6, A7, A8, A12, A11, A14, A16, Th5;
then
rt . n in coprod (
((the_arity_of o) /. n),
X)
by A12, A16, PARTFUN1:def 6;
then A30:
ex
a being
set st
(
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 A29, Th6;
T = root-tree tt
by A21, DTCONSTR:9;
hence
T in (FreeSort X) . ((the_arity_of o) /. n)
by A20, A30;
verum end;
(B * (the_arity_of o)) . x =
B . ((the_arity_of o) . n)
by A16, FUNCT_1:12
.=
B . ((the_arity_of o) /. n)
by A12, A16, PARTFUN1:def 6
;
hence
ts . x in (B * (the_arity_of o)) . x
by A18, A23, A31;
verum
end;
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;
A33:
Den (
o,
(FreeMSA X)) =
(FreeOper X) . o
by MSUALG_1:def 6
.=
DenOp (
o,
X)
by Def13
;
A34:
(
Sym (
o,
X)
= [o, the carrier of S] &
nt = [o, the carrier of S] )
by A7, TARSKI:def 1;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 1;
then
((B #) * the Arity of S) . o = product (B * (the_arity_of o))
by Th1;
then A35:
ts in ((B #) * the Arity of S) . o
by A12, A11, A9, A13, A15, CARD_3:9;
dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o
by FUNCT_2:def 1;
then
ts in dom (DenOp (o,X))
by A4, A34, Th10;
then
ts in (dom (DenOp (o,X))) /\ (((B #) * the Arity of S) . o)
by A35, XBOOLE_0:def 4;
then A36:
ts in dom ((DenOp (o,X)) | (((B #) * the Arity of S) . o))
by RELAT_1:61;
then ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) . ts =
(DenOp (o,X)) . ts
by FUNCT_1:47
.=
nt -tree ts
by A4, A34, Def12
;
then A37:
nt -tree ts in rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o))
by A33, A36, FUNCT_1:def 3;
( the
ResultSort of
S . o = the_result_sort_of o &
dom (B * the ResultSort of S) = the
carrier' of
S )
by MSUALG_1:def 2, PARTFUN1:def 2;
then A38:
(B * the ResultSort of S) . o = B . (the_result_sort_of o)
by FUNCT_1:12;
B is
opers_closed
by MSUALG_2:def 9;
then
B is_closed_on o
by MSUALG_2:def 6;
then A39:
rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
by MSUALG_2:def 5;
B . (the_result_sort_of o) in rng B
by A10, FUNCT_1:def 3;
hence
S1[
nt -tree ts]
by A39, A37, A38, TARSKI:def 4;
verum
end;
A40:
for
s being
Symbol of
(DTConMSA X) st
s in Terminals (DTConMSA X) holds
S1[
root-tree s]
A47:
for
t being
DecoratedTree of the
carrier of
(DTConMSA X) st
t in TS (DTConMSA X) holds
S1[
t]
from DTCONSTR:sch 7(A40, A3);
A48:
union (rng the Sorts of (FreeMSA X)) c= union (rng the Sorts of (GenMSAlg f))
let x be
Element of
S;
PBOOLE:def 21 the Sorts of (GenMSAlg f) . x = the Sorts of (FreeMSA X) . x
reconsider s =
x as
SortSymbol of
S ;
thus
the
Sorts of
(GenMSAlg f) . x c= the
Sorts of
(FreeMSA X) . x
by A2;
XBOOLE_0:def 10 the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x
let a be
object ;
TARSKI:def 3 ( not a in the Sorts of (FreeMSA X) . x or a in the Sorts of (GenMSAlg f) . x )
assume A53:
a in the
Sorts of
(FreeMSA X) . x
;
a in the Sorts of (GenMSAlg f) . x
the
carrier of
S = dom the
Sorts of
(FreeMSA X)
by PARTFUN1:def 2;
then
the
Sorts of
(FreeMSA X) . s in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 3;
then
a in union (rng the Sorts of (FreeMSA X))
by A53, TARSKI:def 4;
then consider A being
set such that A54:
a in A
and A55:
A in rng the
Sorts of
(GenMSAlg f)
by A48, TARSKI:def 4;
consider b being
object such that A56:
b in dom the
Sorts of
(GenMSAlg f)
and A57:
the
Sorts of
(GenMSAlg f) . b = A
by A55, FUNCT_1:def 3;
reconsider b =
b as
SortSymbol of
S by A56;
hence
a in the
Sorts of
(GenMSAlg f) . x
by A54, A57;
verum
end;
then reconsider f = f as GeneratorSet of FreeMSA X by Def4;
take
f
; 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; verum