set A = DTConUA (f,X);
set D = (dom f) \/ X;
DTConUA (f,X) is with_useful_nonterminals
proof
set e =
<*> (TS (DTConUA (f,X)));
let s be
Symbol of
(DTConUA (f,X));
DTCONSTR:def 5 ( 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))
;
ex b1 being FinSequence of TS (DTConUA (f,X)) st s ==> roots b1
A2:
rng f c= NAT
by FINSEQ_1:def 4;
NonTerminals (DTConUA (f,X)) = dom f
by Th2;
then
f . s in rng f
by A1, FUNCT_1:def 3;
then reconsider fs =
f . s as
Nat by A2;
reconsider sd =
s as
Element of
(dom f) \/ X ;
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) * ;
0 in rng f
by Def2;
then consider x being
object such that A3:
x in dom f
and A4:
f . x = 0
by FUNCT_1:def 3;
A5:
NonTerminals (DTConUA (f,X)) = dom f
by Th2;
then reconsider s0 =
x as
Symbol of
(DTConUA (f,X)) by A3;
set p =
fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))));
A6:
len (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) = fs
by CARD_1:def 7;
len re = 0
by DTCONSTR:3;
then
[s0,(roots (<*> (TS (DTConUA (f,X)))))] in the
Rules of
(DTConUA (f,X))
by A3, A4, Def7;
then
s0 ==> roots (<*> (TS (DTConUA (f,X))))
by LANG1:def 1;
then A7:
s0 -tree (<*> (TS (DTConUA (f,X)))) in TS (DTConUA (f,X))
by DTCONSTR:def 1;
A8:
rng (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) c= TS (DTConUA (f,X))
proof
let y be
object ;
TARSKI:def 3 ( 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))))))
;
y in TS (DTConUA (f,X))
then A9:
ex
n being
Nat st
(
n in dom (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) &
(fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) . n = y )
by FINSEQ_2:10;
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 A7, A6, A9, FUNCOP_1:7;
verum
end;
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 A10:
len (roots (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))))) = fs
by A6, FINSEQ_1:def 3;
reconsider p =
fs |-> (s0 -tree (<*> (TS (DTConUA (f,X))))) as
FinSequence of
TS (DTConUA (f,X)) by A8, FINSEQ_1:def 4;
take
p
;
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, A5, A10, Def7;
hence
s ==> roots p
by LANG1:def 1;
verum
end;
hence
( DTConUA (f,X) is with_nonterminals & DTConUA (f,X) is with_useful_nonterminals )
; verum