let C be initialized standardized ConstructorSignature; for e being expression of C st (e . {}) `1 = * holds
ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
let e be expression of C; ( (e . {}) `1 = * implies ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) )
assume A1:
(e . {}) `1 = *
; ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
for x being Element of Vars holds
( not e = x -term C or not e . {} = [x,a_Term] )
by A1;
then consider o being OperSymbol of C such that
A2:
e . {} = [o, the carrier of C]
and
( o in Constructors or o = * or o = non_op )
by Th11;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
consider aa being ArgumentSeq of Sym (o,((MSVars C) (\/) ( the carrier of C --> {0}))) such that
A3:
t = [o, the carrier of C] -tree aa
by A2, MSATERM:10;
A4: * =
[o, the carrier of C] `1
by A1, A3, TREES_4:def 4
.=
o
;
A5:
the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*>
by ABCMIZ_1:38;
A6: len aa =
len (the_arity_of o)
by MSATERM:22
.=
2
by A4, A5, FINSEQ_1:44
;
then
dom aa = Seg 2
by FINSEQ_1:def 3;
then A7:
( 1 in dom aa & 2 in dom aa )
;
then reconsider t1 = aa . 1, t2 = aa . 2 as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSATERM:22;
A8:
len (doms aa) = len aa
by TREES_3:38;
( (doms aa) . 1 = dom t1 & (doms aa) . 2 = dom t2 )
by A7, FUNCT_6:22;
then A9:
( 0 < 2 & 0 + 1 = 1 & 1 < 2 & 1 + 1 = 2 & {} in (doms aa) . 1 & {} in (doms aa) . 2 & <*0*> ^ (<*> NAT) = <*0*> & <*1*> ^ (<*> NAT) = <*1*> )
by FINSEQ_1:34, TREES_1:22;
dom t = tree (doms aa)
by A3, TREES_4:10;
then reconsider 00 = <*0*>, 01 = <*1*> as Element of dom t by A6, A8, A9, TREES_3:def 15;
( 0 < 2 & 1 = 0 + 1 & 1 < 2 & 2 = 1 + 1 & aa is DTree-yielding )
;
then
( t1 = t | 00 & t2 = t | 01 )
by A3, A6, TREES_4:def 4;
then A10:
( t1 is expression of C & t2 is expression of C & variables_in t1 c= variables_in t & variables_in t2 c= variables_in t )
by MSAFREE3:32, MSAFREE3:33;
then A11:
( variables_in t1 c= MSVars C & variables_in t2 c= MSVars C )
by MSAFREE3:27;
the_sort_of t1 =
(the_arity_of o) . 1
by A7, MSATERM:23
.=
an_Adj C
by A4, A5, FINSEQ_1:44
;
then
t1 in { s where s is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) }
by A11;
then
t1 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (an_Adj C)
by MSAFREE3:def 5;
then
t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C)
by MSAFREE3:24;
then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def 28;
the_sort_of t2 =
(the_arity_of o) . 2
by A7, MSATERM:23
.=
a_Type C
by A4, A5, FINSEQ_1:44
;
then
t2 in { s where s is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of s = a_Type C & variables_in s c= MSVars C ) }
by A11;
then
t2 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Type C)
by MSAFREE3:def 5;
then
t2 in the Sorts of (Free (C,(MSVars C))) . (a_Type C)
by MSAFREE3:24;
then reconsider q = t2 as expression of C, a_Type C by A10, ABCMIZ_1:def 28;
take
a
; ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
take
q
; e = [*,3] -tree (a,q)
A12:
the carrier of C = 3
by ABCMIZ_1:def 9, YELLOW11:1;
aa = <*a,q*>
by A6, FINSEQ_1:44;
hence
e = [*,3] -tree (a,q)
by A3, A4, A12, TREES_4:def 6; verum