set D = DTConMSA X;

set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

A1: Terminals (DTConMSA X) = Union (coprod X) by Th6;

A2: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;

A3: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;

for nt being Symbol of (DTConMSA X) st nt in NonTerminals (DTConMSA X) holds

ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p

set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

A1: Terminals (DTConMSA X) = Union (coprod X) by Th6;

A2: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;

A3: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;

for nt being Symbol of (DTConMSA X) st nt in NonTerminals (DTConMSA X) holds

ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p

proof

hence
( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals )
by A1, A2, DTCONSTR:def 3, DTCONSTR:def 4, DTCONSTR:def 5; :: thesis: verum
let nt be Symbol of (DTConMSA X); :: thesis: ( nt in NonTerminals (DTConMSA X) implies ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p )

assume nt in NonTerminals (DTConMSA X) ; :: thesis: ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p

then consider o being OperSymbol 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;

defpred S_{1}[ object , object ] means X in coprod (((the_arity_of o) . S),X);

A5: for a being object st a in Seg (len (the_arity_of o)) holds

ex b being object st S_{1}[a,b]

A9: ( dom b = Seg (len (the_arity_of o)) & ( for a being object st a in Seg (len (the_arity_of o)) holds

S_{1}[a,b . a] ) )
from CLASSES1:sch 1(A5);

reconsider b = b as FinSequence by A9, FINSEQ_1:def 2;

A10: rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;

deffunc H_{1}( 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 = H_{1}(x) ) )
from FUNCT_1:sch 3();

reconsider f = f as FinSequence by A9, A16, FINSEQ_1:def 2;

rng f c= TS (DTConMSA X)

A23: for x being object st x in dom b holds

(roots f) . x = b . x

then [nt,b] in REL X by A4, A25, Th5;

then A30: nt ==> b by LANG1:def 1;

take f ; :: thesis: nt ==> roots f

dom (roots f) = dom f by TREES_3:def 18;

hence nt ==> roots f by A30, A16, A23, FUNCT_1:2; :: thesis: verum

end;assume nt in NonTerminals (DTConMSA X) ; :: thesis: ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p

then consider o being OperSymbol 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;

defpred S

A5: for a being object st a in Seg (len (the_arity_of o)) holds

ex b being object st S

proof

consider b being Function such that
let a be object ; :: thesis: ( a in Seg (len (the_arity_of o)) implies ex b being object st S_{1}[a,b] )

assume a in Seg (len (the_arity_of o)) ; :: thesis: ex b being object st S_{1}[a,b]

then a in dom (the_arity_of o) by FINSEQ_1:def 3;

then A6: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;

A7: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then consider x being object such that

A8: x in X . ((the_arity_of o) . a) by A6, XBOOLE_0:def 1;

take [x,((the_arity_of o) . a)] ; :: thesis: S_{1}[a,[x,((the_arity_of o) . a)]]

thus S_{1}[a,[x,((the_arity_of o) . a)]]
by A6, A7, A8, Def2; :: thesis: verum

end;assume a in Seg (len (the_arity_of o)) ; :: thesis: ex b being object st S

then a in dom (the_arity_of o) by FINSEQ_1:def 3;

then A6: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def 3;

A7: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then consider x being object such that

A8: x in X . ((the_arity_of o) . a) by A6, XBOOLE_0:def 1;

take [x,((the_arity_of o) . a)] ; :: thesis: S

thus S

A9: ( dom b = Seg (len (the_arity_of o)) & ( for a being object st a in Seg (len (the_arity_of o)) holds

S

reconsider b = b as FinSequence by A9, FINSEQ_1:def 2;

A10: rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

proof

then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng b or a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) )

A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

assume a in rng b ; :: thesis: a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

then consider c being object such that

A12: c in dom b and

A13: b . c = a by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A14: (the_arity_of o) . c in rng (the_arity_of o) by A9, A12, FUNCT_1:def 3;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A14, A11, FUNCT_1:def 3;

then A15: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A14, A11, Def3;

a in coprod (((the_arity_of o) . c),X) by A9, A12, A13;

then a in union (rng (coprod X)) by A15, TARSKI:def 4;

then a in Union (coprod X) by CARD_3:def 4;

hence a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def 3; :: thesis: verum

end;A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

assume a in rng b ; :: thesis: a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

then consider c being object such that

A12: c in dom b and

A13: b . c = a by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A14: (the_arity_of o) . c in rng (the_arity_of o) by A9, A12, FUNCT_1:def 3;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A14, A11, FUNCT_1:def 3;

then A15: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A14, A11, Def3;

a in coprod (((the_arity_of o) . c),X) by A9, A12, A13;

then a in union (rng (coprod X)) by A15, TARSKI:def 4;

then a in Union (coprod X) by CARD_3:def 4;

hence a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def 3; :: thesis: verum

reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;

deffunc H

consider f being Function such that

A16: ( dom f = dom b & ( for x being object st x in dom b holds

f . x = H

reconsider f = f as FinSequence by A9, A16, FINSEQ_1:def 2;

rng f c= TS (DTConMSA X)

proof

then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in TS (DTConMSA X) )

A17: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

assume x in rng f ; :: thesis: x in TS (DTConMSA X)

then consider y being object such that

A18: y in dom f and

A19: f . y = x by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A20: (the_arity_of o) . y in rng (the_arity_of o) by A9, A16, A18, FUNCT_1:def 3;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . y) in rng (coprod X) by A20, A17, FUNCT_1:def 3;

then A21: coprod (((the_arity_of o) . y),X) in rng (coprod X) by A20, A17, Def3;

b . y in rng b by A16, A18, FUNCT_1:def 3;

then reconsider a = b . y as Symbol of (DTConMSA X) by A10;

S_{1}[y,b . y]
by A9, A16, A18;

then b . y in union (rng (coprod X)) by A21, TARSKI:def 4;

then A22: a in Terminals (DTConMSA X) by A1, CARD_3:def 4;

x = root-tree (b . y) by A16, A18, A19;

hence x in TS (DTConMSA X) by A22, DTCONSTR:def 1; :: thesis: verum

end;A17: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

assume x in rng f ; :: thesis: x in TS (DTConMSA X)

then consider y being object such that

A18: y in dom f and

A19: f . y = x by FUNCT_1:def 3;

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A20: (the_arity_of o) . y in rng (the_arity_of o) by A9, A16, A18, FUNCT_1:def 3;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . y) in rng (coprod X) by A20, A17, FUNCT_1:def 3;

then A21: coprod (((the_arity_of o) . y),X) in rng (coprod X) by A20, A17, Def3;

b . y in rng b by A16, A18, FUNCT_1:def 3;

then reconsider a = b . y as Symbol of (DTConMSA X) by A10;

S

then b . y in union (rng (coprod X)) by A21, TARSKI:def 4;

then A22: a in Terminals (DTConMSA X) by A1, CARD_3:def 4;

x = root-tree (b . y) by A16, A18, A19;

hence x in TS (DTConMSA X) by A22, DTCONSTR:def 1; :: thesis: verum

A23: for x being object st x in dom b holds

(roots f) . x = b . x

proof

let x be object ; :: thesis: ( x in dom b implies (roots f) . x = b . x )

assume A24: x in dom b ; :: thesis: (roots f) . x = b . x

then reconsider i = x as Nat ;

( f . x = root-tree (b . x) & ex T being DecoratedTree st

( T = f . i & (roots f) . i = T . {} ) ) by A16, A24, TREES_3:def 18;

hence (roots f) . x = b . x by TREES_4:3; :: thesis: verum

end;assume A24: x in dom b ; :: thesis: (roots f) . x = b . x

then reconsider i = x as Nat ;

( f . x = root-tree (b . x) & ex T being DecoratedTree st

( T = f . i & (roots f) . i = T . {} ) ) by A16, A24, TREES_3:def 18;

hence (roots f) . x = b . x by TREES_4:3; :: thesis: verum

A25: now :: thesis: 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 b . c in coprod (((the_arity_of o) . c),X) ) )

( the carrier of S = x2 & len b = len (the_arity_of o) )
by A9, FINSEQ_1:def 3, TARSKI:def 1;( ( 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 b . c in coprod (((the_arity_of o) . c),X) ) )

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 b . c in coprod (((the_arity_of o) . c),X) ) ) )

assume A26: 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 b . c in coprod (((the_arity_of o) . c),X) ) )

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A27: (the_arity_of o) . c in rng (the_arity_of o) by A9, A26, FUNCT_1:def 3;

A28: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A27, A28, FUNCT_1:def 3;

then A29: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A27, A28, Def3;

S_{1}[c,b . c]
by A9, A26;

then b . c in union (rng (coprod X)) by A29, 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; :: thesis: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )

assume b . c in Union (coprod X) ; :: thesis: b . c in coprod (((the_arity_of o) . c),X)

thus b . c in coprod (((the_arity_of o) . c),X) by A9, A26; :: thesis: verum

end;the_result_sort_of o1 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) ) )

assume A26: 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 b . c in coprod (((the_arity_of o) . c),X) ) )

dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

then A27: (the_arity_of o) . c in rng (the_arity_of o) by A9, A26, FUNCT_1:def 3;

A28: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

dom (coprod X) = the carrier of S by PARTFUN1:def 2;

then (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A27, A28, FUNCT_1:def 3;

then A29: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A27, A28, Def3;

S

then b . c in union (rng (coprod X)) by A29, 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; :: thesis: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )

assume b . c in Union (coprod X) ; :: thesis: b . c in coprod (((the_arity_of o) . c),X)

thus b . c in coprod (((the_arity_of o) . c),X) by A9, A26; :: thesis: verum

then [nt,b] in REL X by A4, A25, Th5;

then A30: nt ==> b by LANG1:def 1;

take f ; :: thesis: nt ==> roots f

dom (roots f) = dom f by TREES_3:def 18;

hence nt ==> roots f by A30, A16, A23, FUNCT_1:2; :: thesis: verum