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
for ml being Element of SCM-Data-Loc st x = [I,<*mk,ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let S be non empty 1-sorted ; :: thesis: for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk,ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let x be Element of SCM-Instr S; :: thesis: for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk,ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let mk be Element of NAT ; :: thesis: for ml being Element of SCM-Data-Loc st x = [I,<*mk,ml*>] holds
( x cjump_address = mk & x cond_address = ml )
let ml be Element of SCM-Data-Loc ; :: thesis: ( x = [I,<*mk,ml*>] implies ( x cjump_address = mk & x cond_address = ml ) )
assume A1: x = [I,<*mk,ml*>] ; :: thesis: ( x cjump_address = mk & x cond_address = ml )
then consider mk' being Element of NAT , ml' being Element of SCM-Data-Loc such that
A2: <*mk',ml'*> = x `2 and
A3: x cjump_address = <*mk',ml'*> /. 1 by Def10;
<*mk',ml'*> = <*mk,ml*> by A1, A2, MCART_1:7;
hence x cjump_address = mk by A3, FINSEQ_4:26; :: thesis: x cond_address = ml
consider mk' being Element of NAT , ml' being Element of SCM-Data-Loc such that
A4: <*mk',ml'*> = x `2 and
A5: x cond_address = <*mk',ml'*> /. 2 by A1, Def11;
<*mk',ml'*> = <*mk,ml*> by A1, A4, MCART_1:7;
hence x cond_address = ml by A5, FINSEQ_4:26; :: thesis: verum