let I be Element of Segm 14; :: thesis: for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let x be Element of SCMPDS-Instr ; :: thesis: for mk being Element of SCM-Data-Loc
for r being Integer st x = [I,<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let mk be Element of SCM-Data-Loc ; :: thesis: for r being Integer st x = [I,<*mk,r*>] holds
( x P21address = mk & x P22const = r )
let r be Integer; :: thesis: ( x = [I,<*mk,r*>] implies ( x P21address = mk & x P22const = r ) )
assume A1: x = [I,<*mk,r*>] ; :: thesis: ( x P21address = mk & x P22const = r )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A2: ( f = x `2 & x P21address = f /. 1 ) by Def12;
A3: f = <*mk,r*> by A1, A2, MCART_1:7;
r in INT by INT_1:def 2;
then A4: ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;
hence x P21address = mk by A2, A3, FINSEQ_4:26; :: thesis: x P22const = r
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: ( f = x `2 & x P22const = f /. 2 ) by A1, Def13;
f = <*mk,r*> by A1, A5, MCART_1:7;
hence x P22const = r by A4, A5, FINSEQ_4:26; :: thesis: verum