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 SCM-Data-Loc
for r being Element of S st x = [I,<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let S be non empty 1-sorted ; :: thesis: for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let x be Element of SCM-Instr S; :: thesis: for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let mk be Element of SCM-Data-Loc ; :: thesis: for r being Element of S st x = [I,<*mk,r*>] holds
( x const_address = mk & x const_value = r )
let r be Element of S; :: thesis: ( x = [I,<*mk,r*>] implies ( x const_address = mk & x const_value = r ) )
assume A1: x = [I,<*mk,r*>] ; :: thesis: ( x const_address = mk & x const_value = r )
then consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A2: ( f = x `2 & x const_address = f /. 1 ) by Def12;
A3: f = <*mk,r*> by A1, A2, MCART_1:7;
A4: ( mk is Element of SCM-Data-Loc \/ the carrier of S & r is Element of SCM-Data-Loc \/ the carrier of S ) by XBOOLE_0:def 3;
hence x const_address = mk by A2, A3, FINSEQ_4:26; :: thesis: x const_value = r
consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A5: ( f = x `2 & x const_value = f /. 2 ) by A1, Def13;
f = <*mk,r*> by A1, A5, MCART_1:7;
hence x const_value = r by A4, A5, FINSEQ_4:26; :: thesis: verum