let x be set ; for d2 being Element of SCM-Data-Loc
for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr
let d2 be Element of SCM-Data-Loc ; for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr
let k2 be Integer; ( x in {2,3} implies [x,{},<*d2,k2*>] in SCMPDS-Instr )
assume A1:
x in {2,3}
; [x,{},<*d2,k2*>] in SCMPDS-Instr
then
( x = 2 or x = 3 )
by TARSKI:def 2;
then reconsider x = x as Element of Segm 15 by NAT_1:44;
k2 is Element of INT
by INT_1:def 2;
then
[x,{},<*d2,k2*>] in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} }
by A1;
then
[x,{},<*d2,k2*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} }
by XBOOLE_0:def 3;
then
[x,{},<*d2,k2*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} }
by XBOOLE_0:def 3;
hence
[x,{},<*d2,k2*>] in SCMPDS-Instr
by XBOOLE_0:def 3; verum