let s be State of SCM; :: thesis: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term holds (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
let tl, tr be bin-term; :: thesis: (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s))
consider f being Function of (TS SCM-AE),INT such that
A1: (nt -tree (tl,tr)) @ s = f . (nt -tree (tl,tr)) and
A2: for t being Terminal of SCM-AE holds f . (root-tree t) = s . t and
A3: 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;
A4: nt ==> <*(root-label tl),(root-label tr)*> by Def1, Lm3;
( tl @ s = f . tl & tr @ s = f . tr ) by A2, A3, Def9;
hence (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s)) by A1, A3, A4; :: thesis: verum