let S be non empty 1-sorted ; :: thesis: for i being Element of SCM-Instr S st not not InsCode i = 1 & ... & not InsCode i = 4 holds
JumpPart i = {}
let i be Element of SCM-Instr S; :: thesis: ( not not InsCode i = 1 & ... & not InsCode i = 4 implies JumpPart i = {} )
assume not not InsCode i = 1 & ... & not 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 = {} ; :: thesis: verum