let i be Element of SCMPDS-Instr ; :: thesis: ( ( InsCode i = 2 or InsCode i = 3 ) implies JumpPart i = {} )
assume ( InsCode i = 2 or InsCode i = 3 ) ; :: thesis: JumpPart i = {}
then i 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} } by Th8;
then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st
( i = [I,{},<*v,c*>] & I in {2,3} ) ;
hence JumpPart i = {} ; :: thesis: verum