let I be Instruction of SCMPDS; :: thesis: InsCode I <= 14
( 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 or InsCode I = 8 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 or InsCode I = 14 ) by SCMPDS_I:8;
hence InsCode I <= 14 ; :: thesis: verum