let x be set ; :: thesis: for d3 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,<*d3,k3,k4*>] in SCMPDS-Instr
let d3 be Element of SCM-Data-Loc ; :: thesis: for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,<*d3,k3,k4*>] in SCMPDS-Instr
let k3, k4 be Integer; :: thesis: ( x in {4,5,6,7,8} implies [x,<*d3,k3,k4*>] in SCMPDS-Instr )
assume A1: x in {4,5,6,7,8} ; :: thesis: [x,<*d3,k3,k4*>] in SCMPDS-Instr
then ( x = 4 or x = 5 or x = 6 or x = 7 or x = 8 ) by ENUMSET1:def 3;
then reconsider x = x as Element of Segm 14 by GR_CY_1:10;
( k3 is Element of INT & k4 is Element of INT ) by INT_1:def 2;
then [x,<*d3,k3,k4*>] in { [I2,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by A1;
then [x,<*d3,k3,k4*>] in (({ [0 ,<*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 14, 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 14, 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,<*d3,k3,k4*>] in SCMPDS-Instr by XBOOLE_0:def 3; :: thesis: verum