set A = DTConUA f,X;
set D = (dom f) \/ X;
DTConUA f,X is with_useful_nonterminals
proof
let s be
Symbol of
(DTConUA f,X);
:: according to DTCONSTR:def 8 :: thesis: ( not s in NonTerminals (DTConUA f,X) or ex b1 being FinSequence of TS (DTConUA f,X) st s ==> roots b1 )
assume A1:
s in NonTerminals (DTConUA f,X)
;
:: thesis: ex b1 being FinSequence of TS (DTConUA f,X) st s ==> roots b1
set e =
<*> (TS (DTConUA f,X));
0 in rng f
by Def2;
then consider x being
set such that A2:
(
x in dom f &
f . x = 0 )
by FUNCT_1:def 5;
A3:
(
NonTerminals (DTConUA f,X) = dom f & the
carrier of
(DTConUA f,X) = (Terminals (DTConUA f,X)) \/ (NonTerminals (DTConUA f,X)) )
by Th2, LANG1:1;
then reconsider s0 =
x as
Symbol of
(DTConUA f,X) by A2;
roots (<*> (TS (DTConUA f,X))) = <*> ((dom f) \/ X)
by DTCONSTR:3;
then reconsider re =
roots (<*> (TS (DTConUA f,X))) as
Element of
((dom f) \/ X) * ;
len re = 0
by DTCONSTR:3;
then
[s0,(roots (<*> (TS (DTConUA f,X))))] in the
Rules of
(DTConUA f,X)
by A2, Def8;
then
s0 ==> roots (<*> (TS (DTConUA f,X)))
by LANG1:def 1;
then A4:
s0 -tree (<*> (TS (DTConUA f,X))) in TS (DTConUA f,X)
by DTCONSTR:def 4;
NonTerminals (DTConUA f,X) = dom f
by Th2;
then
(
f . s in rng f &
rng f c= NAT )
by A1, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider fs =
f . s as
Element of
NAT ;
set p =
fs |-> (s0 -tree (<*> (TS (DTConUA f,X))));
A5:
len (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) = fs
by FINSEQ_1:def 18;
dom (roots (fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))))) =
dom (fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))))
by TREES_3:def 18
.=
Seg (len (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))))
by FINSEQ_1:def 3
;
then A6:
len (roots (fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))))) = fs
by A5, FINSEQ_1:def 3;
reconsider sd =
s as
Element of
(dom f) \/ X ;
rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) c= TS (DTConUA f,X)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) or y in TS (DTConUA f,X) )
assume
y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))))
;
:: thesis: y in TS (DTConUA f,X)
then consider n being
Nat such that A7:
(
n in dom (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) &
(fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) . n = y )
by FINSEQ_2:11;
dom (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) = Seg (len (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))))
by FINSEQ_1:def 3;
hence
y in TS (DTConUA f,X)
by A4, A5, A7, FUNCOP_1:13;
:: thesis: verum
end;
then reconsider p =
fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))) as
FinSequence of
TS (DTConUA f,X) by FINSEQ_1:def 4;
take
p
;
:: thesis: s ==> roots p
reconsider p =
p as
FinSequence of
FinTrees the
carrier of
(DTConUA f,X) ;
reconsider rp =
roots p as
Element of
((dom f) \/ X) * by FINSEQ_1:def 11;
[sd,rp] in REL f,
X
by A1, A3, A6, Def8;
hence
s ==> roots p
by LANG1:def 1;
:: thesis: verum
end;
hence
( DTConUA f,X is with_nonterminals & DTConUA f,X is with_useful_nonterminals )
; :: thesis: verum