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:24;
A2:
dom the Sorts of (Free (S,X)) = the carrier of S
by PARTFUN1:def 2;
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
object 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:2;
reconsider s1 =
s1 as
SortSymbol of
S by A4;
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 5;
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:10;
then
{v} c= X . s
by A7;
then
v in X . s
by ZFMISC_1:31;
then
[v,s] in Terminals (DTConMSA X)
by MSAFREE:7;
hence
root-tree [v,s] in TS (DTConMSA X)
by DTCONSTR:def 1;
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
object 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:2;
reconsider s =
s as
SortSymbol of
S by A11;
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 5;
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:19;
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:106;
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 1;
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:22;
A23:
s `1 in X . (s `2)
by A19, A21, CARD_3:22;
A24:
s = [(s `1),(s `2)]
by A19, A21, CARD_3:22;
A25:
dom the
Sorts of
(Free (S,X)) = the
carrier of
S
by PARTFUN1:def 2;
root-tree s in the
Sorts of
(Free (S,X)) . (s `2)
by A22, A23, A24, MSAFREE3:4;
hence
S2[
root-tree s]
by A22, A25, CARD_5:2;
verum
end;
A26:
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 A27:
nt ==> roots ts
and A28:
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 A27;
then consider o,
z being
object such that A29:
o in the
carrier' of
S
and A30:
z in { the carrier of S}
and A31:
nt = [o,z]
by A18, ZFMISC_1:def 2;
reconsider o =
o as
OperSymbol of
S by A29;
A32:
rng ts c= Union the
Sorts of
(Free (S,X))
by A28;
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;
A34:
z = the
carrier of
S
by A30, TARSKI:def 1;
then
Sym (
o,
(X (\/) ( the carrier of S --> {0})))
==> roots p
by A27, A31, 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, A32, MSAFREE3:19;
hence
S2[
nt -tree ts]
by A2, A31, A34, CARD_5:2;
verum
end;
A35:
for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S2[t]
from DTCONSTR:sch 7(A20, A26);
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 object ; TARSKI:def 3 ( not x in TS (DTConMSA X) or x in Union the Sorts of (Free (S,X)) )
assume A39:
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 A39;
hence
x in Union the Sorts of (Free (S,X))
by A35; verum