let I be Element of Segm 8; :: thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>] holds
x jump_address = mk
let S be non empty 1-sorted ; :: thesis: for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>] holds
x jump_address = mk
let x be Element of SCM-Instr S; :: thesis: for mk being Element of NAT st x = [I,<*mk*>] holds
x jump_address = mk
let mk be Element of NAT ; :: thesis: ( x = [I,<*mk*>] implies x jump_address = mk )
assume A1: x = [I,<*mk*>] ; :: thesis: x jump_address = mk
then consider f being FinSequence of NAT such that
A2: ( f = x `2 & x jump_address = f /. 1 ) by Def9;
f = <*mk*> by A1, A2, MCART_1:7;
hence x jump_address = mk by A2, FINSEQ_4:25; :: thesis: verum