let l be Instruction of SCM ; :: thesis: InsCode l <= 8
( l in ({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or l in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;
then A1: ( l in {[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } or l in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or l in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

per cases ( l in {[SCM-Halt ,{} ]} or l in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } or l in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or l in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by A1, XBOOLE_0:def 3;

suppose l in {[SCM-Halt ,{} ]} ; :: thesis: InsCode l <= 8

then l = [SCM-Halt ,{} ] by TARSKI:def 1;
then l `1 = 0 by MCART_1:7;
hence InsCode l <= 8 ; :: thesis: verum

end;

suppose l in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; :: thesis: InsCode l <= 8

then ex J being Element of Segm 9 ex a being Element of NAT st
( l = [J,<*a*>] & J = 6 ) ;
then l `1 = 6 by MCART_1:7;
hence InsCode l <= 8 ; :: thesis: verum

end;

suppose l in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ; :: thesis: InsCode l <= 8

then ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of SCM-Data-Loc st
( l = [K,<*a1,b1*>] & K in {7,8} ) ;
then l `1 in {7,8} by MCART_1:7;
then ( l `1 = 7 or l `1 = 8 ) by TARSKI:def 2;
hence InsCode l <= 8 ; :: thesis: verum

end;

suppose l in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ; :: thesis: InsCode l <= 8

then ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( l = [I,<*b,c*>] & I in {1,2,3,4,5} ) ;
then l `1 in {1,2,3,4,5} by MCART_1:7;
then ( l `1 = 1 or l `1 = 2 or l `1 = 3 or l `1 = 4 or l `1 = 5 ) by ENUMSET1:def 3;
hence InsCode l <= 8 ; :: thesis: verum

end;

end;