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