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