let S be non void Signature; for X being with_missing_variables ManySortedSet of the carrier of S holds Union the Sorts of (Free S,X) = TS (DTConMSA X)
let X be with_missing_variables ManySortedSet of the carrier of S; Union the Sorts of (Free S,X) = TS (DTConMSA X)
set V = X \/ (the carrier of S --> {0 });
set A = Free S,X;
set U = the Sorts of (Free S,X);
set G = DTConMSA X;
A1:
the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 }))
by MSAFREE3:25;
A2:
dom the Sorts of (Free S,X) = the carrier of S
by PARTFUN1:def 4;
defpred S1[ set ] means ( $1 in Union the Sorts of (Free S,X) implies $1 in TS (DTConMSA X) );
A3:
for s being SortSymbol of S
for v being Element of (X \/ (the carrier of S --> {0 })) . s holds S1[ root-tree [v,s]]
proof
let s be
SortSymbol of
S;
for v being Element of (X \/ (the carrier of S --> {0 })) . s holds S1[ root-tree [v,s]]let v be
Element of
(X \/ (the carrier of S --> {0 })) . s;
S1[ root-tree [v,s]]
assume
root-tree [v,s] in Union the
Sorts of
(Free S,X)
;
root-tree [v,s] in TS (DTConMSA X)
then consider s1 being
set such that A4:
s1 in dom the
Sorts of
(Free S,X)
and A5:
root-tree [v,s] in the
Sorts of
(Free S,X) . s1
by CARD_5:10;
reconsider s1 =
s1 as
SortSymbol of
S by A4, PARTFUN1:def 4;
the
Sorts of
(Free S,X) . s1 = { t where t is Term of S,(X \/ (the carrier of S --> {0 })) : ( the_sort_of t = s1 & variables_in t c= X ) }
by A1, MSAFREE3:def 6;
then consider t being
Term of
S,
(X \/ (the carrier of S --> {0 })) such that A6:
root-tree [v,s] = t
and
the_sort_of t = s1
and A7:
variables_in t c= X
by A5;
(variables_in t) . s = {v}
by A6, MSAFREE3:11;
then
{v} c= X . s
by A7, PBOOLE:def 5;
then
v in X . s
by ZFMISC_1:37;
then
[v,s] in Terminals (DTConMSA X)
by MSAFREE:7;
hence
root-tree [v,s] in TS (DTConMSA X)
by DTCONSTR:def 4;
verum
end;
A8:
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) st ( for t being Term of S,(X \/ (the carrier of S --> {0 })) st t in rng p holds
S1[t] ) holds
S1[[o,the carrier of S] -tree p]
proof
let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) st ( for t being Term of S,(X \/ (the carrier of S --> {0 })) st t in rng p holds
S1[t] ) holds
S1[[o,the carrier of S] -tree p]let p be
ArgumentSeq of
Sym o,
(X \/ (the carrier of S --> {0 }));
( ( for t being Term of S,(X \/ (the carrier of S --> {0 })) st t in rng p holds
S1[t] ) implies S1[[o,the carrier of S] -tree p] )
assume that A9:
for
t being
Term of
S,
(X \/ (the carrier of S --> {0 })) st
t in rng p holds
S1[
t]
and A10:
[o,the carrier of S] -tree p in Union the
Sorts of
(Free S,X)
;
[o,the carrier of S] -tree p in TS (DTConMSA X)
consider s being
set such that A11:
s in dom the
Sorts of
(Free S,X)
and A12:
[o,the carrier of S] -tree p in the
Sorts of
(Free S,X) . s
by A10, CARD_5:10;
reconsider s =
s as
SortSymbol of
S by A11, PARTFUN1:def 4;
the
Sorts of
(Free S,X) . s = { t where t is Term of S,(X \/ (the carrier of S --> {0 })) : ( the_sort_of t = s & variables_in t c= X ) }
by A1, MSAFREE3:def 6;
then consider t being
Term of
S,
(X \/ (the carrier of S --> {0 })) such that A13:
[o,the carrier of S] -tree p = t
and A14:
the_sort_of t = s
and
variables_in t c= X
by A12;
t . {} = [o,the carrier of S]
by A13, TREES_4:def 4;
then
the_result_sort_of o = s
by A14, MSATERM:17;
then A15:
rng p c= Union the
Sorts of
(Free S,X)
by A1, A12, MSAFREE3:20;
rng p c= TS (DTConMSA X)
then reconsider q =
p as
FinSequence of
TS (DTConMSA X) by FINSEQ_1:def 4;
NonTerminals (DTConMSA X) = [:the carrier' of S,{the carrier of S}:]
by Th120;
then
[o,the carrier of S] in NonTerminals (DTConMSA X)
by ZFMISC_1:129;
then reconsider oo =
[o,the carrier of S] as
Symbol of
(DTConMSA X) ;
Sym o,
(X \/ (the carrier of S --> {0 })) ==> roots p
by MSATERM:21;
then
oo ==> roots q
by Th127;
hence
[o,the carrier of S] -tree p in TS (DTConMSA X)
by DTCONSTR:def 4;
verum
end;
A17:
for t being Term of S,(X \/ (the carrier of S --> {0 })) holds S1[t]
from MSATERM:sch 1(A3, A8);
A18:
NonTerminals (DTConMSA X) = [:the carrier' of S,{the carrier of S}:]
by Th120;
A19:
Terminals (DTConMSA X) = Union (coprod X)
by Th120;
defpred S2[ set ] means $1 in Union the Sorts of (Free S,X);
A20:
for s being Symbol of (DTConMSA X) st s in Terminals (DTConMSA X) holds
S2[ root-tree s]
proof
let s be
Symbol of
(DTConMSA X);
( s in Terminals (DTConMSA X) implies S2[ root-tree s] )
assume A21:
s in Terminals (DTConMSA X)
;
S2[ root-tree s]
then A22:
s `2 in dom X
by A19, CARD_3:33;
A23:
s `1 in X . (s `2 )
by A19, A21, CARD_3:33;
A24:
s = [(s `1 ),(s `2 )]
by A19, A21, CARD_3:33;
A25:
dom X = the
carrier of
S
by PARTFUN1:def 4;
A26:
dom the
Sorts of
(Free S,X) = the
carrier of
S
by PARTFUN1:def 4;
root-tree s in the
Sorts of
(Free S,X) . (s `2 )
by A22, A23, A24, A25, MSAFREE3:5;
hence
S2[
root-tree s]
by A22, A25, A26, CARD_5:10;
verum
end;
A27:
for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]
proof
let nt be
Symbol of
(DTConMSA X);
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S2[t] ) holds
S2[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S2[t] ) implies S2[nt -tree ts] )
assume that A28:
nt ==> roots ts
and A29:
for
t being
DecoratedTree of the
carrier of
(DTConMSA X) st
t in rng ts holds
S2[
t]
;
S2[nt -tree ts]
nt in NonTerminals (DTConMSA X)
by A28;
then consider o,
z being
set such that A30:
o in the
carrier' of
S
and A31:
z in {the carrier of S}
and A32:
nt = [o,z]
by A18, ZFMISC_1:def 2;
reconsider o =
o as
OperSymbol of
S by A30;
A33:
rng ts c= Union the
Sorts of
(Free S,X)
rng ts c= TS (DTConMSA (X \/ (the carrier of S --> {0 })))
then reconsider p =
ts as
FinSequence of
TS (DTConMSA (X \/ (the carrier of S --> {0 }))) by FINSEQ_1:def 4;
reconsider q =
p as
FinSequence of
S -Terms (X \/ (the carrier of S --> {0 })) by MSATERM:def 1;
A36:
z = the
carrier of
S
by A31, TARSKI:def 1;
then
Sym o,
(X \/ (the carrier of S --> {0 })) ==> roots p
by A28, A32, Th127;
then reconsider q =
q as
ArgumentSeq of
Sym o,
(X \/ (the carrier of S --> {0 })) by MSATERM:21;
set t =
(Sym o,(X \/ (the carrier of S --> {0 }))) -tree q;
(Sym o,(X \/ (the carrier of S --> {0 }))) -tree q in the
Sorts of
(Free S,X) . (the_result_sort_of o)
by A1, A33, MSAFREE3:20;
hence
S2[
nt -tree ts]
by A2, A32, A36, CARD_5:10;
verum
end;
A37:
for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S2[t]
from DTCONSTR:sch 7(A20, A27);
thus
Union the Sorts of (Free S,X) c= TS (DTConMSA X)
XBOOLE_0:def 10 TS (DTConMSA X) c= Union the Sorts of (Free S,X)
let x be set ; TARSKI:def 3 ( not x in TS (DTConMSA X) or x in Union the Sorts of (Free S,X) )
assume A41:
x in TS (DTConMSA X)
; x in Union the Sorts of (Free S,X)
then reconsider TG = TS (DTConMSA X) as non empty Subset of (FinTrees the carrier of (DTConMSA X)) ;
x is Element of TG
by A41;
hence
x in Union the Sorts of (Free S,X)
by A37; verum