set fgs = FreeGenSetNSG f,D;
set fua = FreeUnivAlgNSG f,D;
A1:
the carrier of (GenUnivAlg (FreeGenSetNSG f,D)) = the carrier of (FreeUnivAlgNSG f,D)
proof
set A =
DTConUA f,
D;
defpred S1[
DecoratedTree of the
carrier of
(DTConUA f,D)]
means $1
in the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D));
the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D)) is
Subset of
(FreeUnivAlgNSG f,D)
by UNIALG_2:def 8;
hence
the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D)) c= the
carrier of
(FreeUnivAlgNSG f,D)
;
XBOOLE_0:def 10 the carrier of (FreeUnivAlgNSG f,D) c= the carrier of (GenUnivAlg (FreeGenSetNSG f,D))
A2:
for
nt being
Symbol of
(DTConUA f,D) for
ts being
FinSequence of
TS (DTConUA f,D) st
nt ==> roots ts & ( for
t being
DecoratedTree of the
carrier of
(DTConUA f,D) st
t in rng ts holds
S1[
t] ) holds
S1[
nt -tree ts]
proof
reconsider B = the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D)) as
Subset of
(FreeUnivAlgNSG f,D) by UNIALG_2:def 8;
let s be
Symbol of
(DTConUA f,D);
for ts being FinSequence of TS (DTConUA f,D) st s ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConUA f,D) st t in rng ts holds
S1[t] ) holds
S1[s -tree ts]let p be
FinSequence of
TS (DTConUA f,D);
( s ==> roots p & ( for t being DecoratedTree of the carrier of (DTConUA f,D) st t in rng p holds
S1[t] ) implies S1[s -tree p] )
assume that A3:
s ==> roots p
and A4:
for
t being
DecoratedTree of the
carrier of
(DTConUA f,D) st
t in rng p holds
t in the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D))
;
S1[s -tree p]
rng p c= the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D))
then reconsider cp =
p as
FinSequence of the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D)) by FINSEQ_1:def 4;
reconsider tp =
p as
Element of
(TS (DTConUA f,D)) * by FINSEQ_1:def 11;
[s,(roots p)] in the
Rules of
(DTConUA f,D)
by A3, LANG1:def 1;
then reconsider rp =
roots p as
Element of
((dom f) \/ D) * by ZFMISC_1:106;
reconsider s0 =
s as
Element of
(dom f) \/ D ;
A6:
[s0,rp] in REL f,
D
by A3, LANG1:def 1;
then A7:
s0 in dom f
by Def8;
then reconsider ns =
s as
Element of
NAT ;
A8:
f . s0 = len rp
by A6, Def8;
len (FreeOpSeqNSG f,D) = len f
by Def12;
then A9:
dom (FreeOpSeqNSG f,D) =
Seg (len f)
by FINSEQ_1:def 3
.=
dom f
by FINSEQ_1:def 3
;
then
(FreeOpSeqNSG f,D) . ns in rng (FreeOpSeqNSG f,D)
by A7, FUNCT_1:def 5;
then reconsider o =
FreeOpNSG ns,
f,
D as
operation of
(FreeUnivAlgNSG f,D) by A7, A9, Def12;
B is
opers_closed
by UNIALG_2:def 8;
then A10:
B is_closed_on o
by UNIALG_2:def 5;
A11:
dom (FreeOpNSG ns,f,D) = (f /. ns) -tuples_on (TS (DTConUA f,D))
by A7, Def11;
dom o = (arity o) -tuples_on the
carrier of
(FreeUnivAlgNSG f,D)
by MARGREL1:58;
then A12:
arity o = f /. ns
by A11, FINSEQ_2:130;
dom (roots p) =
dom p
by TREES_3:def 18
.=
Seg (len p)
by FINSEQ_1:def 3
;
then A13:
len p =
len rp
by FINSEQ_1:def 3
.=
f /. ns
by A7, A8, PARTFUN1:def 8
;
then
tp in { w where w is Element of (TS (DTConUA f,D)) * : len w = f /. ns }
;
then o . cp =
(Sym ns,f,D) -tree p
by A7, A11, Def11
.=
s -tree p
by A7, Def10
;
hence
S1[
s -tree p]
by A10, A13, A12, UNIALG_2:def 4;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (FreeUnivAlgNSG f,D) or x in the carrier of (GenUnivAlg (FreeGenSetNSG f,D)) )
assume A14:
x in the
carrier of
(FreeUnivAlgNSG f,D)
;
x in the carrier of (GenUnivAlg (FreeGenSetNSG f,D))
then reconsider x1 =
x as
Element of
FinTrees the
carrier of
(DTConUA f,D) ;
A15:
x1 in TS (DTConUA f,D)
by A14;
A16:
for
s being
Symbol of
(DTConUA f,D) st
s in Terminals (DTConUA f,D) holds
S1[
root-tree s]
for
t being
DecoratedTree of the
carrier of
(DTConUA f,D) st
t in TS (DTConUA f,D) holds
S1[
t]
from DTCONSTR:sch 7(A16, A2);
hence
x in the
carrier of
(GenUnivAlg (FreeGenSetNSG f,D))
by A15;
verum
end;
FreeGenSetNSG f,D <> {}
by Th5;
hence
FreeGenSetNSG f,D is GeneratorSet of FreeUnivAlgNSG f,D
by A1, Lm3; verum