:: deftheorem Def14 defines max_Data-Loc_in SCM_COMP:def 14 :
for term being bin-term
for b₂ being Element of NAT holds
( b₂ = max_Data-Loc_in term iff ex f being Function of (TS SCM-AE),NAT st
( b₂ = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". 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 NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) );