:: deftheorem Def9 defines @ SCM_COMP:def 9 :
for s being State of SCM
for term being bin-term
for b₃ being Integer holds
( b₃ = term @ s iff ex f being Function of (TS SCM-AE),INT st
( b₃ = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of INT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = nt -Meaning_on (xl,xr) ) ) );