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 proj1 the Instructions of (SCM R) by RELAT_1:def 4;
consider x being set such that
A2: [[T,y],x] in the Instructions of (SCM R) by A1, RELAT_1:def 4;
[T,y,x] in SCM-Instr R by A2, SCMRING2:def 1;
then ( [T,y,x] in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : 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 : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by AMI_3:27, 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 Data-Locations : 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 Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by XBOOLE_0:def 3;
then A3: ( [T,y,x] in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : 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 Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , 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 Data-Locations : 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 Data-Locations : verum } or [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } ) by A3, 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:25; :: thesis: verum

end;

suppose [T,y,x] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : 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 Data-Locations st
( [T,y,x] = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;
then T in {1,2,3,4} by MCART_1:25;
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:25; :: thesis: verum

end;

suppose [T,y,x] in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of Data-Locations : 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 Data-Locations 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:25; :: thesis: verum

end;

suppose [T,y,x] in { [5,{},<*a,r*>] where a is Element of Data-Locations , 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 Data-Locations 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:25; :: thesis: verum

end;

end;