let i be Element of SCMPDS-Instr ; :: thesis: ( ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) implies JumpPart i = {} )
assume ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; :: thesis: JumpPart i = {}
then i in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } by Th8;
then ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st
( i = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ;
hence JumpPart i = {} ; :: thesis: verum