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;
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;
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;
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;
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;
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;
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;
end;