theorem Th9: :: SCM_INST:9

for x being Element of SCM-Instr holds
( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } & InsCode x = 6 ) or ( x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) ) )