let I be Element of Segm 8; 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 ; 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; 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 ; 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; ( 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*>]
; ( 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; 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; verum