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