let C be initialized standardized ConstructorSignature; for t being quasi-term of C holds
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
set X = MSVars C;
set V = (MSVars C) (\/) ( the carrier of C --> {0});
let t be quasi-term of C; ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
( C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) & the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) )
by MSAFREE3:24, PBOOLE:def 18;
then A1:
( 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}))) #) & (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) & t in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C) )
by ABCMIZ_1:def 28;
then
t in (FreeSort ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C)
;
then A2:
t in FreeSort (((MSVars C) (\/) ( the carrier of C --> {0})),(a_Term C))
by MSAFREE:def 11;
A3:
( (MSVars C) . a_Term = Vars & a_Term C = a_Term & a_Term = 2 )
by ABCMIZ_1:def 25;
reconsider q = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
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]
;
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )then consider s being
SortSymbol of
C,
v being
Element of
((MSVars C) (\/) ( the carrier of C --> {0})) . s such that A4:
t . {} = [v,s]
;
A5:
(
q = root-tree [v,s] &
the_sort_of q = a_Term C )
by A2, A4, MSATERM:5, MSATERM:def 5;
then A6:
(
a_Term C = s &
(t . {}) `1 = v )
by A4, MSATERM:14;
then reconsider x =
v as
Element of
Vars by A3, A5, A1, MSAFREE3:18;
(
q = x -term C &
vars x <> 2 )
by A5, A6, Th7;
hence
(
t is
compound iff (
(t . {}) `1 in Constructors &
((t . {}) `1) `1 = a_Term ) )
by A6;
verum end; suppose
q . {} in [: the carrier' of C,{ the carrier of C}:]
;
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )then consider o,
k being
object such that A7:
(
o in the
carrier' of
C &
k in { the carrier of C} &
q . {} = [o,k] )
by ZFMISC_1:def 2;
reconsider o =
o as
OperSymbol of
C by A7;
k = the
carrier of
C
by A7, TARSKI:def 1;
then A8:
the_result_sort_of o =
the_sort_of q
by A7, MSATERM:17
.=
a_Term C
by A1, MSAFREE3:17
;
then
(
o <> ast C &
o <> non_op C )
by ABCMIZ_1:38;
then A9:
o is
constructor
;
then A10:
a_Term C =
o `1
by A8, Def1
.=
((q . {}) `1) `1
by A7
;
A11:
(q . {}) `1 = o
by A7;
hence
(
t is
compound iff (
(t . {}) `1 in Constructors &
((t . {}) `1) `1 = a_Term ) )
by A9, A10, A11, Th3, Def1;
verum end;