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