let R be Ring; :: thesis: for T being InsType of the InstructionsF 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 the InstructionsF 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 object such that

A1: [T,y] in proj1 the InstructionsF of (SCM R) by XTUPLE_0:def 12;

consider x being object such that

A2: [[T,y],x] in the InstructionsF of (SCM R) by A1, XTUPLE_0:def 12;

[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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is 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 Nat : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is 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 Nat : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is 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;

( 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 the InstructionsF 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 object such that

A1: [T,y] in proj1 the InstructionsF of (SCM R) by XTUPLE_0:def 12;

consider x being object such that

A2: [[T,y],x] in the InstructionsF of (SCM R) by A1, XTUPLE_0:def 12;

[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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is 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 Nat : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is 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 Nat : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is 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 Nat : verum } or [T,y,x] in { [7,<*i*>,<*a*>] where i is 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;

end;

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 XTUPLE_0:3; :: thesis: verum

end;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 XTUPLE_0:3; :: thesis: verum

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 XTUPLE_0:3;

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;( [T,y,x] = [I,{},<*a,b*>] & I in {1,2,3,4} ) ;

then T in {1,2,3,4} by XTUPLE_0:3;

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

suppose
[T,y,x] in { [6,<*i*>,{}] where i is 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 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 XTUPLE_0:3; :: thesis: verum

end;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 XTUPLE_0:3; :: thesis: verum

suppose
[T,y,x] in { [7,<*i*>,<*a*>] where i is 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 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 XTUPLE_0:3; :: thesis: verum

end;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 XTUPLE_0:3; :: thesis: verum

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 XTUPLE_0:3; :: thesis: verum

end;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 XTUPLE_0:3; :: thesis: verum