let term be bin-term; :: thesis: ( 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;

( 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;

end;

suppose
term . {} in Terminals SCM-AE
; :: thesis: ( 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 ) )

( term = tl + tr or term = tl - tr or term = tl * tr or term = tl div tr or term = tl mod tr ) )

then reconsider t = term . {} as Terminal of SCM-AE ;

term = root-tree t by DTCONSTR:9;

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 ) ) ; :: thesis: verum

end;term = root-tree t by DTCONSTR:9;

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 ) ) ; :: thesis: verum

suppose
term . {} in NonTerminals SCM-AE
; :: thesis: ( 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 ) )

( 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 ) ) ; :: thesis: verum

end;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 ) ) ; :: thesis: verum