set fgs = FreeGenSetZAO (f,D);
set fua = FreeUnivAlgZAO (f,D);
A1:
the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) = the carrier of (FreeUnivAlgZAO (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 (FreeGenSetZAO (f,D)));
the
carrier of
(GenUnivAlg (FreeGenSetZAO (f,D))) is
Subset of
(FreeUnivAlgZAO (f,D))
by UNIALG_2:def 7;
hence
the
carrier of
(GenUnivAlg (FreeGenSetZAO (f,D))) c= the
carrier of
(FreeUnivAlgZAO (f,D))
;
XBOOLE_0:def 10 the carrier of (FreeUnivAlgZAO (f,D)) c= the carrier of (GenUnivAlg (FreeGenSetZAO (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 (FreeGenSetZAO (f,D))) as
Subset of
(FreeUnivAlgZAO (f,D)) by UNIALG_2:def 7;
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 (FreeGenSetZAO (f,D)))
;
S1[s -tree p]
rng p c= the
carrier of
(GenUnivAlg (FreeGenSetZAO (f,D)))
then reconsider cp =
p as
FinSequence of the
carrier of
(GenUnivAlg (FreeGenSetZAO (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:87;
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 Def7;
then reconsider ns =
s as
Nat ;
A8:
f . s0 = len rp
by A6, Def7;
len (FreeOpSeqZAO (f,D)) = len f
by Def17;
then A9:
dom (FreeOpSeqZAO (f,D)) =
Seg (len f)
by FINSEQ_1:def 3
.=
dom f
by FINSEQ_1:def 3
;
then
(FreeOpSeqZAO (f,D)) . ns in rng (FreeOpSeqZAO (f,D))
by A7, FUNCT_1:def 3;
then reconsider o =
FreeOpZAO (
ns,
f,
D) as
operation of
(FreeUnivAlgZAO (f,D)) by A7, A9, Def17;
B is
opers_closed
by UNIALG_2:def 7;
then A10:
B is_closed_on o
;
A11:
dom (FreeOpZAO (ns,f,D)) = (f /. ns) -tuples_on (TS (DTConUA (f,D)))
by A7, Def16;
dom o = (arity o) -tuples_on the
carrier of
(FreeUnivAlgZAO (f,D))
by MARGREL1:22;
then A12:
arity o = f /. ns
by A11, FINSEQ_2:110;
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 6
;
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, Def16
.=
s -tree p
by A7, Def9
;
hence
S1[
s -tree p]
by A10, A13, A12;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (FreeUnivAlgZAO (f,D)) or x in the carrier of (GenUnivAlg (FreeGenSetZAO (f,D))) )
assume A14:
x in the
carrier of
(FreeUnivAlgZAO (f,D))
;
x in the carrier of (GenUnivAlg (FreeGenSetZAO (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 (FreeGenSetZAO (f,D)))
by A15;
verum
end;
Constants (FreeUnivAlgZAO (f,D)) <> {}
by Th9;
hence
FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D)
by A1, Lm3; verum