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