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

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