theorem Th5: :: SCM_COMP:5

for s being State of SCM
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))