let R be good Ring; :: thesis: for T being InsType of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
let T be InsType of (SCM R); :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
consider y being set such that
A1: [T,y] in the Instructions of (SCM R) by RELAT_1:def 4;
[T,y] in SCM-Instr R by A1, SCMRING2:def 1;
then ( [T,y] 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 } or [T,y] in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } ) by XBOOLE_0:def 3;
then ( [T,y] 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 } or [T,y] in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y] in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } ) by XBOOLE_0:def 3;
then A2: ( [T,y] 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} } or [T,y] in { [6,<*i*>] where i is Element of NAT : verum } or [T,y] in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y] in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } ) by XBOOLE_0:def 3;

per cases ( [T,y] in {[0 ,{} ]} or [T,y] 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} } or [T,y] in { [6,<*i*>] where i is Element of NAT : verum } or [T,y] in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y] in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } ) by A2, XBOOLE_0:def 3;

suppose [T,y] in {[0 ,{} ]} ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

then [T,y] = [0 ,{} ] by TARSKI:def 1;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ZFMISC_1:33; :: thesis: verum

end;

suppose [T,y] 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} } ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

then ex I being Element of Segm 8 ex a, b being Element of SCM-Data-Loc st
( [T,y] = [I,<*a,b*>] & I in {1,2,3,4} ) ;
then T in {1,2,3,4} by ZFMISC_1:33;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ENUMSET1:def 2; :: thesis: verum

end;

suppose [T,y] in { [6,<*i*>] where i is Element of NAT : verum } ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

then ex i being Element of NAT st [T,y] = [6,<*i*>] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ZFMISC_1:33; :: thesis: verum

end;

suppose [T,y] in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

then ex i being Element of NAT ex a being Element of SCM-Data-Loc st [T,y] = [7,<*i,a*>] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ZFMISC_1:33; :: thesis: verum

end;

suppose [T,y] in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

then ex a being Element of SCM-Data-Loc ex r being Element of R st [T,y] = [5,<*a,r*>] ;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by ZFMISC_1:33; :: thesis: verum

end;

end;