set A = DTConUA f,D;
A1:
NonTerminals (DTConUA f,D) = dom f
by Th2;
A2:
Terminals (DTConUA f,D) = D
by Th3;
DTConUA f,D is with_useful_nonterminals
proof
consider d being
Element of
D;
let s be
Symbol of
(DTConUA f,D);
DTCONSTR:def 8 ( not s in NonTerminals (DTConUA f,D) or ex b1 being FinSequence of TS (DTConUA f,D) st s ==> roots b1 )
reconsider sd =
d as
Symbol of
(DTConUA f,D) by XBOOLE_0:def 3;
A3:
rng f c= NAT
by FINSEQ_1:def 4;
assume A4:
s in NonTerminals (DTConUA f,D)
;
ex b1 being FinSequence of TS (DTConUA f,D) st s ==> roots b1
then
f . s in rng f
by A1, FUNCT_1:def 5;
then reconsider fs =
f . s as
Element of
NAT by A3;
reconsider sdd =
s as
Element of
(dom f) \/ D ;
set p =
fs |-> (root-tree sd);
A5:
len (fs |-> (root-tree sd)) = fs
by FINSEQ_1:def 18;
A6:
root-tree sd in TS (DTConUA f,D)
by A2, DTCONSTR:def 4;
A7:
rng (fs |-> (root-tree sd)) c= TS (DTConUA f,D)
dom (roots (fs |-> (root-tree sd))) =
dom (fs |-> (root-tree sd))
by TREES_3:def 18
.=
Seg (len (fs |-> (root-tree sd)))
by FINSEQ_1:def 3
;
then A10:
len (roots (fs |-> (root-tree sd))) = fs
by A5, FINSEQ_1:def 3;
reconsider p =
fs |-> (root-tree sd) as
FinSequence of
TS (DTConUA f,D) by A7, FINSEQ_1:def 4;
take
p
;
s ==> roots p
reconsider p =
p as
FinSequence of
FinTrees the
carrier of
(DTConUA f,D) ;
reconsider rp =
roots p as
Element of
((dom f) \/ D) * by FINSEQ_1:def 11;
[sdd,rp] in REL f,
D
by A1, A4, A10, Def8;
hence
s ==> roots p
by LANG1:def 1;
verum
end;
hence
( DTConUA f,D is with_terminals & DTConUA f,D is with_nonterminals & DTConUA f,D is with_useful_nonterminals )
by A2, DTCONSTR:def 6; verum