set D = DTConOSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1:
Terminals (DTConOSA X) = Union (coprod X)
by Th3;
A2:
NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:]
by Th3;
A3:
Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:4;
for nt being Symbol of (DTConOSA X) st nt in NonTerminals (DTConOSA X) holds
ex p being FinSequence of TS (DTConOSA X) st nt ==> roots p
proof
let nt be
Symbol of
(DTConOSA X);
( nt in NonTerminals (DTConOSA X) implies ex p being FinSequence of TS (DTConOSA X) st nt ==> roots p )
assume
nt in NonTerminals (DTConOSA X)
;
ex p being FinSequence of TS (DTConOSA X) st nt ==> roots p
then consider o being
Element of the
carrier' of
S,
x2 being
Element of
{ the carrier of S} such that A4:
nt = [o,x2]
by A2, DOMAIN_1:1;
set O =
the_arity_of o;
A5:
the
carrier of
S = x2
by TARSKI:def 1;
defpred S1[
object ,
object ]
means ex
i being
Element of
S st
(
i <= (the_arity_of o) /. S &
X in coprod (
i,
X) );
A6:
for
a being
object st
a in Seg (len (the_arity_of o)) holds
ex
b being
object st
S1[
a,
b]
proof
let a be
object ;
( a in Seg (len (the_arity_of o)) implies ex b being object st S1[a,b] )
assume
a in Seg (len (the_arity_of o))
;
ex b being object st S1[a,b]
then A7:
a in dom (the_arity_of o)
by FINSEQ_1:def 3;
then A8:
(the_arity_of o) . a in rng (the_arity_of o)
by FUNCT_1:def 3;
A9:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then consider x being
object such that A10:
x in X . ((the_arity_of o) . a)
by A8, XBOOLE_0:def 1;
take y =
[x,((the_arity_of o) . a)];
S1[a,y]
take
(the_arity_of o) /. a
;
( (the_arity_of o) /. a <= (the_arity_of o) /. a & y in coprod (((the_arity_of o) /. a),X) )
y in coprod (
((the_arity_of o) . a),
X)
by A8, A9, A10, MSAFREE:def 2;
hence
(
(the_arity_of o) /. a <= (the_arity_of o) /. a &
y in coprod (
((the_arity_of o) /. a),
X) )
by A7, PARTFUN1:def 6;
verum
end;
consider b being
Function such that A11:
(
dom b = Seg (len (the_arity_of o)) & ( for
a being
object st
a in Seg (len (the_arity_of o)) holds
S1[
a,
b . a] ) )
from CLASSES1:sch 1(A6);
reconsider b =
b as
FinSequence by A11, FINSEQ_1:def 2;
A12:
rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
then reconsider b =
b as
FinSequence of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
reconsider b =
b as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
deffunc H1(
object )
-> set =
root-tree (b . S);
consider f being
Function such that A16:
(
dom f = dom b & ( for
x being
object st
x in dom b holds
f . x = H1(
x) ) )
from FUNCT_1:sch 3();
reconsider f =
f as
FinSequence by A11, A16, FINSEQ_1:def 2;
rng f c= TS (DTConOSA X)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in TS (DTConOSA X) )
assume
x in rng f
;
x in TS (DTConOSA X)
then consider y being
object such that A17:
y in dom f
and A18:
f . y = x
by FUNCT_1:def 3;
b . y in rng b
by A16, A17, FUNCT_1:def 3;
then reconsider a =
b . y as
Symbol of
(DTConOSA X) by A12;
consider i being
Element of
S such that
i <= (the_arity_of o) /. y
and A19:
b . y in coprod (
i,
X)
by A11, A16, A17;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . i in rng (coprod X)
by FUNCT_1:def 3;
then
coprod (
i,
X)
in rng (coprod X)
by MSAFREE:def 3;
then
b . y in union (rng (coprod X))
by A19, TARSKI:def 4;
then A20:
a in Terminals (DTConOSA X)
by A1, CARD_3:def 4;
x = root-tree (b . y)
by A16, A17, A18;
hence
x in TS (DTConOSA X)
by A20, DTCONSTR:def 1;
verum
end;
then reconsider f =
f as
FinSequence of
TS (DTConOSA X) by FINSEQ_1:def 4;
A21:
for
x being
object st
x in dom b holds
(roots f) . x = b . x
A24:
now for c being set st c in dom b holds
( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) )let c be
set ;
( c in dom b implies ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) ) )assume
c in dom b
;
( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c ) & ( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) ) )then consider i being
Element of
S such that A25:
i <= (the_arity_of o) /. c
and A26:
b . c in coprod (
i,
X)
by A11;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . i in rng (coprod X)
by FUNCT_1:def 3;
then
coprod (
i,
X)
in rng (coprod X)
by MSAFREE:def 3;
then
b . c in union (rng (coprod X))
by A26, TARSKI:def 4;
then
b . c in Union (coprod X)
by CARD_3:def 4;
hence
(
b . c in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = b . c holds
the_result_sort_of o1 <= (the_arity_of o) /. c )
by A3, XBOOLE_0:3;
( b . c in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) ) )assume
b . c in Union (coprod X)
;
ex i being Element of S st
( i <= (the_arity_of o) /. c & b . c in coprod (i,X) )thus
ex
i being
Element of
S st
(
i <= (the_arity_of o) /. c &
b . c in coprod (
i,
X) )
by A25, A26;
verum end;
len b = len (the_arity_of o)
by A11, FINSEQ_1:def 3;
then
[nt,b] in OSREL X
by A4, A5, A24, Th2;
then A27:
nt ==> b
by LANG1:def 1;
take
f
;
nt ==> roots f
dom (roots f) = dom f
by TREES_3:def 18;
hence
nt ==> roots f
by A27, A16, A21, FUNCT_1:2;
verum
end;
hence
( DTConOSA X is with_terminals & DTConOSA X is with_nonterminals & DTConOSA X is with_useful_nonterminals )
by A1, A2, DTCONSTR:def 3, DTCONSTR:def 4, DTCONSTR:def 5; verum