for x being Element of SCM+FSA-Instr holds
( ( x in SCM-Instr & not not InsCode x = 0 & ... & not InsCode x = 8 ) or ( x in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } & ( InsCode x = 9 or InsCode x = 10 ) ) or ( x in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } & ( InsCode x = 11 or InsCode x = 12 ) ) )