let I be Element of Segm 14; :: thesis: for x being Element of SCMPDS-Instr
for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let x be Element of SCMPDS-Instr ; :: thesis: for d1 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let d1 be Element of SCM-Data-Loc ; :: thesis: for k1, k2 being Integer st x = [I,<*d1,k1,k2*>] holds
( x P31address = d1 & x P32const = k1 & x P33const = k2 )
let k1, k2 be Integer; :: thesis: ( x = [I,<*d1,k1,k2*>] implies ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) )
assume A1: x = [I,<*d1,k1,k2*>] ; :: thesis: ( x P31address = d1 & x P32const = k1 & x P33const = k2 )
A2: d1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
k1 in INT by INT_1:def 2;
then A3: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
k2 in INT by INT_1:def 2;
then A4: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: ( f = x `2 & x P31address = f /. 1 ) by A1, Def14;
f = <*d1,k1,k2*> by A1, A5, MCART_1:7;
hence x P31address = d1 by A2, A3, A4, A5, FINSEQ_4:27; :: thesis: ( x P32const = k1 & x P33const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A6: ( f = x `2 & x P32const = f /. 2 ) by A1, Def15;
f = <*d1,k1,k2*> by A1, A6, MCART_1:7;
hence x P32const = k1 by A2, A3, A4, A6, FINSEQ_4:27; :: thesis: x P33const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A7: ( f = x `2 & x P33const = f /. 3 ) by A1, Def16;
f = <*d1,k1,k2*> by A1, A7, MCART_1:7;
hence x P33const = k2 by A2, A3, A4, A7, FINSEQ_4:27; :: thesis: verum