let I be Element of Segm 15; :: thesis: for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let x be Element of SCMPDS-Instr ; :: thesis: for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let d1, d2 be Element of SCM-Data-Loc ; :: thesis: for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let k1, k2 be Integer; :: thesis: ( x = [I,{},<*d1,d2,k1,k2*>] implies ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) )
A1: ( d1 is Element of SCM-Data-Loc \/ INT & d2 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;
k1 in INT by INT_1:def 2;
then A2: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
k2 in INT by INT_1:def 2;
then A3: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
assume A4: x = [I,{},<*d1,d2,k1,k2*>] ; :: thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
then consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: f = x `3_3 and
A6: x P41address = f /. 1 by Def9;
f = <*d1,d2,k1,k2*> by A4, A5;
hence x P41address = d1 by A1, A2, A3, A6, FINSEQ_4:80; :: thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A7: f = x `3_3 and
A8: x P42address = f /. 2 by A4, Def10;
f = <*d1,d2,k1,k2*> by A4, A7;
hence x P42address = d2 by A1, A2, A3, A8, FINSEQ_4:80; :: thesis: ( x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A9: f = x `3_3 and
A10: x P43const = f /. 3 by A4, Def11;
f = <*d1,d2,k1,k2*> by A4, A9;
hence x P43const = k1 by A1, A2, A3, A10, FINSEQ_4:80; :: thesis: x P44const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A11: f = x `3_3 and
A12: x P44const = f /. 4 by A4, Def12;
f = <*d1,d2,k1,k2*> by A4, A11;
hence x P44const = k2 by A1, A2, A3, A12, FINSEQ_4:80; :: thesis: verum