let I be Element of Segm 15; 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 ; 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 ; 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; ( 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*>]
; ( 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; ( 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; 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; verum