let S be non empty 1-sorted ; :: thesis: for x being set
for R being good Ring
for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let x be set ; :: thesis: for R being good Ring
for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let R be good Ring; :: thesis: for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let d1, d2 be Data-Location of R; :: thesis: ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
reconsider D1 = d1, D2 = d2 as Element of Data-Locations SCM by Th1;
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:45;
[x,{},<*D1,D2*>] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations SCM : 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 Data-Locations SCM : 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 Data-Locations SCM : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of 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 Data-Locations SCM : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations SCM : verum } by XBOOLE_0:def 3;
hence [x,{},<*d1,d2*>] in SCM-Instr S by AMI_3:72, XBOOLE_0:def 3; :: thesis: verum