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
B1: [T,y] in proj1 the Instructions of (SCM R) by RELAT_1:def 4;
consider x being set such that
A1: [[T,y],x] in the Instructions of (SCM R) by B1, RELAT_1:def 4;
[T,y,x] in SCM-Instr R by A1, SCMRING2:def 1;
then ( [T,y,x] 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,x] 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,x] 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,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y,x] 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,x] 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,x] in { [6,<*i*>,{} ] where i is Element of NAT : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y,x] 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,x] in {[0 ,{} ,{} ]} or [T,y,x] 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,x] in { [6,<*i*>,{} ] where i is Element of NAT : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or [T,y,x] 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,x] 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,x] = [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 MCART_1:28; :: thesis: verum

end;

suppose [T,y,x] 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,x] = [I,{} ,<*a,b*>] & I in {1,2,3,4} ) ;
then T in {1,2,3,4} by MCART_1:28;
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,x] 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,x] = [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 MCART_1:28; :: thesis: verum

end;

suppose [T,y,x] 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,x] = [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 MCART_1:28; :: thesis: verum

end;

suppose [T,y,x] 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,x] = [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 MCART_1:28; :: thesis: verum

end;

end;