let C be initialized standardized ConstructorSignature; for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) or ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
let e be expression of C; ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) or ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
set X = MSVars C;
set Y = (MSVars C) \/ (the carrier of C --> {0 });
reconsider q = e as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
per cases
( ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ (the carrier of C --> {0 })) . s st q . {} = [v,s] or q . {} in [:the carrier' of C,{the carrier of C}:] )
by MSATERM:2;
suppose
ex
s being
SortSymbol of
C ex
v being
Element of
((MSVars C) \/ (the carrier of C --> {0 })) . s st
q . {} = [v,s]
;
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term ] ) or ex o being OperSymbol of C st
( e . {} = [o,the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )then consider s being
SortSymbol of
C,
v being
Element of
((MSVars C) \/ (the carrier of C --> {0 })) . s such that A1:
q . {} = [v,s]
;
consider z being
set such that A4:
(
z in dom the
Sorts of
(Free C,(MSVars C)) &
e in the
Sorts of
(Free C,(MSVars C)) . z )
by CARD_5:10;
reconsider z =
z as
SortSymbol of
C by A4, PARTFUN1:def 4;
the
carrier of
C = {a_Type ,an_Adj ,a_Term }
by ABCMIZ_1:def 9;
then A5:
(
z = a_Type or
z = an_Adj or
z = a_Term )
by ENUMSET1:def 1;
A3:
q = root-tree [v,s]
by A1, MSATERM:5;
then A6:
the_sort_of q = s
by MSATERM:14;
A7:
the
Sorts of
(Free C,(MSVars C)) = C -Terms (MSVars C),
((MSVars C) \/ (the carrier of C --> {0 }))
by MSAFREE3:25;
then
the
Sorts of
(Free C,(MSVars C)) c= the
Sorts of
(FreeMSA ((MSVars C) \/ (the carrier of C --> {0 })))
by PBOOLE:def 23;
then
( the
Sorts of
(Free C,(MSVars C)) . z c= the
Sorts of
(FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . z &
FreeMSA ((MSVars C) \/ (the carrier of C --> {0 })) = MSAlgebra(#
(FreeSort ((MSVars C) \/ (the carrier of C --> {0 }))),
(FreeOper ((MSVars C) \/ (the carrier of C --> {0 }))) #) )
by PBOOLE:def 5;
then
(
q in the
Sorts of
(FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . z & the
Sorts of
(FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . z = FreeSort ((MSVars C) \/ (the carrier of C --> {0 })),
z )
by A4, MSAFREE:def 13;
then A8:
s = z
by A6, MSATERM:def 5;
then
v in (MSVars C) . z
by A3, A4, A7, MSAFREE3:19;
then A9:
(
v in Vars &
z = a_Term )
by A5, ABCMIZ_1:def 25;
then reconsider x =
v as
Element of
Vars ;
e = x -term C
by A1, MSATERM:5, A8, A9;
hence
( ex
x being
Element of
Vars st
(
e = x -term C &
e . {} = [x,a_Term ] ) or ex
o being
OperSymbol of
C st
(
e . {} = [o,the carrier of C] & (
o in Constructors or
o = * or
o = non_op ) ) )
by A1, A8, A9;
verum end;