let x be Element of SCM-Instr ; for mk being Nat
for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Nat; for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds
x jump_address = mk
let I be Element of Segm 9; ( x = [I,<*mk*>,{}] implies x jump_address = mk )
assume A1:
x = [I,<*mk*>,{}]
; x jump_address = mk
then consider f being FinSequence of NAT such that
A2:
f = x `2_3
and
A3:
x jump_address = f /. 1
by Def5;
reconsider mk = mk as Element of NAT by ORDINAL1:def 12;
f = <*mk*>
by A1, A2;
hence
x jump_address = mk
by A3, FINSEQ_4:16; verum