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 Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ) by AMI_3:27, XBOOLE_0:def 3;
then A1: ( l in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } or l in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : 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 Nat : J = 6 } or l in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : 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_3 = 0 ;
hence InsCode l <= 8 ; :: thesis: verum

end;

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

then ex J being Element of Segm 9 ex a being Nat st
( l = [J,<*a*>,{}] & J = 6 ) ;
then l `1_3 = 6 ;
hence InsCode l <= 8 ; :: thesis: verum

end;

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

then ex K being Element of Segm 9 ex a1 being Nat ex b1 being Element of Data-Locations st
( l = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
then l `1_3 in {7,8} ;
then ( l `1_3 = 7 or l `1_3 = 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 Data-Locations : 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 Data-Locations st
( l = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
then l `1_3 in {1,2,3,4,5} ;
then ( l `1_3 = 1 or l `1_3 = 2 or l `1_3 = 3 or l `1_3 = 4 or l `1_3 = 5 ) by ENUMSET1:def 3;
hence InsCode l <= 8 ; :: thesis: verum

end;

end;