let T be InsType of SCM ; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
consider y being set such that
A1: [T,y] in the Instructions of SCM by RELAT_1:def 4;
reconsider I = [T,y] as Instruction of SCM by A1;
T = InsCode I by MCART_1:7;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by AMI_5:36, NAT_1:33; :: thesis: verum