:: deftheorem Def11 defines SCM-Compile SCM_COMP:def 11 :
for b₁ being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) holds
( b₁ = SCM-Compile iff ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
( g = b₁ . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = b₁ . (nt -tree (t1,t2)) & f1 = b₁ . t1 & f2 = b₁ . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) );