let s be State of SCM; :: thesis: for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t
let t be Terminal of SCM-AE; :: thesis: (root-tree t) @ s = s . t
ex f being Function of (TS SCM-AE),INT st
( (root-tree t) @ s = f . (root-tree t) & ( 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) ) ) by Def9;
hence (root-tree t) @ s = s . t ; :: thesis: verum