let i be Element of SCM+FSA-Instr ; :: thesis: ( ( InsCode i = 9 or InsCode i = 10 ) implies JumpPart i = {} )

assume A1: ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis: JumpPart i = {}

then not InsCode i = 0 & ... & not InsCode i = 8 ;

then i 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} } by A1, Th7;

then ex J being Element of Segm 13 ex b, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( i = [J,{},<*c,f,b*>] & J in {9,10} ) ;

hence JumpPart i = {} ; :: thesis: verum

assume A1: ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis: JumpPart i = {}

then not InsCode i = 0 & ... & not InsCode i = 8 ;

then i 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} } by A1, Th7;

then ex J being Element of Segm 13 ex b, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st

( i = [J,{},<*c,f,b*>] & J in {9,10} ) ;

hence JumpPart i = {} ; :: thesis: verum