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 = {} ; :: thesis: verum

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 = {} ; :: thesis: verum