let i be Element of SCM+FSA-Instr ; :: thesis: ( ( InsCode i = 11 or InsCode i = 12 ) implies JumpPart i = {} )
assume ( InsCode i = 11 or InsCode i = 12 ) ; :: thesis: JumpPart i = {}
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 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 = {} by RECDEF_2:def 2; :: thesis: verum