:: deftheorem defines SCM-Instr SCMRINGI:def 1 :
for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;