:: deftheorem Def1 defines SCM-AE SCM_COMP:def 1 :
for b₁ being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr holds
( b₁ = SCM-AE iff ( Terminals b₁ = SCM-Data-Loc & NonTerminals b₁ = [:1,5:] & ( for x, y, z being Symbol of b₁ holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) ) );