let C be initialized standardized ConstructorSignature; for t being expression of C holds
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
set X = MSVars C;
set V = (MSVars C) (\/) ( the carrier of C --> {0});
let t be expression of C; ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
consider A being MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) such that
A1:
( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) (\/) ( the carrier of C --> {0}))) "" (MSVars C) )
by MSAFREE3:def 1;
the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by A1, MSUALG_2:def 9;
then
the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by PBOOLE:def 18;
then A2:
the Sorts of (Free (C,(MSVars C))) . (a_Type C) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Type C)
;
per cases
( ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op )
by Th14;
suppose that A3:
(t . {}) `2 = the
carrier of
C
and A4:
(t . {}) `1 in Constructors
and A5:
(t . {}) `1 in the
carrier' of
C
;
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )reconsider o =
(t . {}) `1 as
OperSymbol of
C by A5;
reconsider tt =
t as
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
not
o in {*,non_op}
by A4, ABCMIZ_1:39, XBOOLE_0:3;
then
(
o <> * &
o <> non_op )
by TARSKI:def 2;
then
o is
constructor
;
then A6:
o `1 = the_result_sort_of o
by Def1;
A7:
t . {} = [o,((t . {}) `2)]
;
then A8:
the_sort_of tt = the_result_sort_of o
by A3, MSATERM:17;
assume
(t . {}) `1 in Constructors
;
( not ((t . {}) `1) `1 = a_Type or t is pure expression of C, a_Type C )assume
((t . {}) `1) `1 = a_Type
;
t is pure expression of C, a_Type Cthen reconsider t =
t as
expression of
C,
a_Type C by A3, A7, Th12, A6;
t is
pure
proof
given a being
expression of
C,
an_Adj C,
q being
expression of
C,
a_Type C such that A10:
t = (ast C) term (
a,
q)
;
ABCMIZ_1:def 41 contradiction
t = [*, the carrier of C] -tree <*a,q*>
by A10, ABCMIZ_1:46;
then
t . {} = [*, the carrier of C]
by TREES_4:def 4;
then
(t . {}) `1 = *
;
then
(t . {}) `1 in {*,non_op}
by TARSKI:def 2;
hence
contradiction
by A4, ABCMIZ_1:39, XBOOLE_0:3;
verum
end; hence
t is
pure expression of
C,
a_Type C
;
verum end; suppose A11:
(t . {}) `1 = *
;
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )then
(t . {}) `1 in {*,non_op}
by TARSKI:def 2;
then A12:
not
(t . {}) `1 in Constructors
by ABCMIZ_1:39, XBOOLE_0:3;
consider a being
expression of
C,
an_Adj C,
q being
expression of
C,
a_Type C such that A13:
t = [*,3] -tree (
a,
q)
by A11, Th18;
t =
[*,3] -tree <*a,q*>
by A13, TREES_4:def 6
.=
[*, the carrier of C] -tree <*a,q*>
by ABCMIZ_1:def 9, YELLOW11:1
.=
(ast C) term (
a,
q)
by ABCMIZ_1:46
;
hence
(
t is
pure expression of
C,
a_Type C iff (
(t . {}) `1 in Constructors &
((t . {}) `1) `1 = a_Type ) )
by A12, ABCMIZ_1:def 41;
verum end; suppose A14:
(t . {}) `1 = non_op
;
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )then
(t . {}) `1 in {*,non_op}
by TARSKI:def 2;
then A15:
not
(t . {}) `1 in Constructors
by ABCMIZ_1:39, XBOOLE_0:3;
consider a being
expression of
C,
an_Adj C such that A16:
t = [non_op,3] -tree a
by A14, Th19;
t = [non_op,3] -tree <*a*>
by A16, TREES_4:def 5;
then
t . {} = [non_op,3]
by TREES_4:def 4;
then
(t . {}) `1 = non_op
;
then
t is
expression of
C,
an_Adj C
by Th13;
hence
(
t is
pure expression of
C,
a_Type C iff (
(t . {}) `1 in Constructors &
((t . {}) `1) `1 = a_Type ) )
by A15, ABCMIZ_1:48;
verum end; end;