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