let S be non empty 1-sorted ; :: thesis: for R being good Ring
for d1 being Data-Location of R
for i1 being Instruction-Location of SCM R holds [7,<*i1,d1*>] in SCM-Instr S
let R be good Ring; :: thesis: for d1 being Data-Location of R
for i1 being Instruction-Location of SCM R holds [7,<*i1,d1*>] in SCM-Instr S
let d1 be Data-Location of R; :: thesis: for i1 being Instruction-Location of SCM R holds [7,<*i1,d1*>] in SCM-Instr S
let i1 be Instruction-Location of SCM R; :: thesis: [7,<*i1,d1*>] in SCM-Instr S
reconsider I1 = i1 as Element of NAT by AMI_1:def 4;
reconsider D1 = d1 as Element of SCM-Data-Loc by Th1;
[7,<*I1,D1*>] in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ;
then [7,<*I1,D1*>] 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 [7,<*i1,d1*>] in SCM-Instr S by XBOOLE_0:def 3; :: thesis: verum