:: deftheorem Def1 defines SCM SCMRING2:def 1 :
for R being Ring
for b₂ being strict AMI-Struct over Segm 2 holds
( b₂ = SCM R iff ( the carrier of b₂ = SCM-Memory & the ZeroF of b₂ = NAT & the InstructionsF of b₂ = SCM-Instr R & the Object-Kind of b₂ = SCM-OK & the ValuesF of b₂ = SCM-VAL R & the Execution of b₂ = SCM-Exec R ) );