let term be bin-term; ( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )
root-label term in the carrier of SCM-AE
;
then
term . {} in the carrier of SCM-AE
by BINTREE1:def 1;
then A1:
term . {} in (Terminals SCM-AE) \/ (NonTerminals SCM-AE)
by LANG1:1;
per cases
( term . {} in Terminals SCM-AE or term . {} in NonTerminals SCM-AE )
by A1, XBOOLE_0:def 3;
suppose
term . {} in NonTerminals SCM-AE
;
( ex t being Terminal of SCM-AE st term = root-tree t or ex tl, tr being bin-term st
( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )then reconsider nt =
term . {} as
NonTerminal of
SCM-AE ;
consider ts being
FinSequence of
TS SCM-AE such that A2:
term = nt -tree ts
and A3:
nt ==> roots ts
by DTCONSTR:10;
ex
x1,
x2 being
Symbol of
SCM-AE st
roots ts = <*x1,x2*>
by A3, BINTREE1:def 4;
then
len (roots ts) = 2
by FINSEQ_1:44;
then A4:
(
dom (roots ts) = dom ts &
dom (roots ts) = Seg 2 )
by FINSEQ_1:def 3, TREES_3:def 18;
A5:
2
in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
then consider tr being
DecoratedTree such that A6:
tr = ts . 2
and
(roots ts) . 2
= tr . {}
by A4, TREES_3:def 18;
A7:
1
in Seg 2
by FINSEQ_1:2, TARSKI:def 2;
then consider tl being
DecoratedTree such that A8:
tl = ts . 1
and
(roots ts) . 1
= tl . {}
by A4, TREES_3:def 18;
reconsider tl =
tl,
tr =
tr as
bin-term by A4, A7, A5, A8, A6, FINSEQ_2:11;
A9:
not not
nt = [0,0] & ... & not
nt = [0,4]
by Th1;
len ts = 2
by A4, FINSEQ_1:def 3;
then
ts = <*tl,tr*>
by A8, A6, FINSEQ_1:44;
then
term = nt -tree (
tl,
tr)
by A2, TREES_4:def 6;
then
(
term = tl + tr or
term = tl - tr or
term = tl * tr or
term = tl div tr or
term = tl mod tr )
by A9;
hence
( ex
t being
Terminal of
SCM-AE st
term = root-tree t or ex
tl,
tr being
bin-term st
(
term = tl + tr or
term = tl - tr or
term = tl * tr or
term = tl div tr or
term = tl mod tr ) )
;
verum end;