let S be non empty 1-sorted ; :: thesis: for x being set
for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let x be set ; :: thesis: for d1, d2 being Element of SCM-Data-Loc st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let d1, d2 be Element of SCM-Data-Loc ; :: thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
reconsider D1 = d1, D2 = d2 as Element of SCM-Data-Loc ;
assume A1: x in {1,2,3,4} ; :: thesis: [x,{},<*d1,d2*>] in SCM-Instr S
then ( x = 1 or x = 2 or x = 3 or x = 4 ) by ENUMSET1:def 2;
then reconsider x = x as Element of Segm 8 by NAT_1:44;
[x,{},<*D1,D2*>] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by A1;
then [x,{},<*D1,D2*>] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } by XBOOLE_0:def 3;
then [x,{},<*D1,D2*>] in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } by XBOOLE_0:def 3;
then [x,{},<*D1,D2*>] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } by XBOOLE_0:def 3;
hence [x,{},<*d1,d2*>] in SCM-Instr S by XBOOLE_0:def 3; :: thesis: verum