let S be non empty 1-sorted ; :: thesis: for i being Element of SCM-Instr S st ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) holds
JumpPart i = {}
let i be Element of SCM-Instr S; :: thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) implies JumpPart i = {} )
assume ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 ) ; :: thesis: JumpPart i = {}
then i in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by Th7;
then ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( i = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
hence JumpPart i = {} by RECDEF_2:def 2; :: thesis: verum