let x be Element of SCM-Instr ; :: thesis: for mk being Nat

for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let mk be Nat; :: thesis: for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let ml be Element of SCM-Data-Loc ; :: thesis: for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let I be Element of Segm 9; :: thesis: ( x = [I,<*mk*>,<*ml*>] implies ( x cjump_address = mk & x cond_address = ml ) )

reconsider mkk = mk as Element of NAT by ORDINAL1:def 12;

assume A1: x = [I,<*mk*>,<*ml*>] ; :: thesis: ( x cjump_address = mk & x cond_address = ml )

then consider mk9 being Element of NAT such that

A2: <*mk9*> = x `2_3 and

A3: x cjump_address = <*mk9*> /. 1 by Def6;

<*mk9*> = <*mkk*> by A1, A2;

hence x cjump_address = mk by A3, FINSEQ_4:16; :: thesis: x cond_address = ml

consider ml9 being Element of SCM-Data-Loc such that

A4: <*ml9*> = x `3_3 and

A5: x cond_address = <*ml9*> /. 1 by A1, Def7;

<*ml9*> = <*ml*> by A1, A4;

hence x cond_address = ml by A5, FINSEQ_4:16; :: thesis: verum

for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let mk be Nat; :: thesis: for ml being Element of SCM-Data-Loc

for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let ml be Element of SCM-Data-Loc ; :: thesis: for I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds

( x cjump_address = mk & x cond_address = ml )

let I be Element of Segm 9; :: thesis: ( x = [I,<*mk*>,<*ml*>] implies ( x cjump_address = mk & x cond_address = ml ) )

reconsider mkk = mk as Element of NAT by ORDINAL1:def 12;

assume A1: x = [I,<*mk*>,<*ml*>] ; :: thesis: ( x cjump_address = mk & x cond_address = ml )

then consider mk9 being Element of NAT such that

A2: <*mk9*> = x `2_3 and

A3: x cjump_address = <*mk9*> /. 1 by Def6;

<*mk9*> = <*mkk*> by A1, A2;

hence x cjump_address = mk by A3, FINSEQ_4:16; :: thesis: x cond_address = ml

consider ml9 being Element of SCM-Data-Loc such that

A4: <*ml9*> = x `3_3 and

A5: x cond_address = <*ml9*> /. 1 by A1, Def7;

<*ml9*> = <*ml*> by A1, A4;

hence x cond_address = ml by A5, FINSEQ_4:16; :: thesis: verum