let i be Element of SCM+FSA-Instr ; :: thesis: ( ( InsCode i = 11 or InsCode i = 12 ) implies JumpPart i = {} )
assume A1: ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis: JumpPart i = {}
then not InsCode i = 0 & ... & not InsCode i = 8 ;
then i 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} } by A1, Th7;
then ex K being Element of Segm 13 ex c1 being Element of SCM-Data-Loc ex f1 being Element of SCM+FSA-Data*-Loc st
( i = [K,{},<*c1,f1*>] & K in {11,12} ) ;
hence JumpPart i = {} ; :: thesis: verum