:: deftheorem Def2 defines SCM-OK AMI_2:def 4 :
for b₁ being Function of SCM-Memory,(Segm 2) holds
( b₁ = SCM-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = 0 ) & ( k in SCM-Data-Loc implies b₁ . k = 1 ) ) );