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 ) )
A1: ( 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;
assume A2: 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
A3: f = x `3_3 and
A4: x const_address = f /. 1 by Def7;
f = <*mk,r*> by A2, A3;
hence x const_address = mk by A4, A1, FINSEQ_4:17; :: thesis: x const_value = r
consider f being FinSequence of SCM-Data-Loc \/ the carrier of S such that
A5: f = x `3_3 and
A6: x const_value = f /. 2 by A2, Def8;
f = <*mk,r*> by A2, A5;
hence x const_value = r by A1, A6, FINSEQ_4:17; :: thesis: verum