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 SCM-Data-Loc 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 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 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 SCM-Data-Loc : 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 SCM-Data-Loc : verum } by XBOOLE_0:def 3;
hence [x,{} ,<*d1,d2*>] in SCM-Instr S by XBOOLE_0:def 3; :: thesis: verum