let I be Element of Segm 15; :: 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 ) )
k1 in INT by INT_1:def 2;
then A1: ( d1 is Element of SCM-Data-Loc \/ INT & k1 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;
k2 in INT by INT_1:def 2;
then A2: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
assume A3: x = [I,{},<*d1,k1,k2*>] ; :: thesis: ( x P31address = d1 & x P32const = k1 & x P33const = k2 )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A4: f = x `3_3 and
A5: x P31address = f /. 1 by Def6;
f = <*d1,k1,k2*> by A3, A4;
hence x P31address = d1 by A1, A2, A5, FINSEQ_4:18; :: thesis: ( x P32const = k1 & x P33const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A6: f = x `3_3 and
A7: x P32const = f /. 2 by A3, Def7;
f = <*d1,k1,k2*> by A3, A6;
hence x P32const = k1 by A1, A2, A7, FINSEQ_4:18; :: thesis: x P33const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A8: f = x `3_3 and
A9: x P33const = f /. 3 by A3, Def8;
f = <*d1,k1,k2*> by A3, A8;
hence x P33const = k2 by A1, A2, A9, FINSEQ_4:18; :: thesis: verum