theorem Th8: :: SCMPDS_I:8

for x being Element of SCMPDS-Instr holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) )