let R be Ring; :: thesis: for I being Instruction of (SCM R) holds InsCode I <= 7

let I be Instruction of (SCM R); :: thesis: InsCode I <= 7

set T = InsCode I;

( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 ) by Lm2;

hence InsCode I <= 7 ; :: thesis: verum

let I be Instruction of (SCM R); :: thesis: InsCode I <= 7

set T = InsCode I;

( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 ) by Lm2;

hence InsCode I <= 7 ; :: thesis: verum