let I be Instruction of SCM+FSA ; :: thesis: for k being Element of NAT holds InsCode (IncAddr I,k) = InsCode I
let k be Element of NAT ; :: thesis: InsCode (IncAddr I,k) = InsCode I
A1: InsCode I <= 11 + 1 by SCMFSA_2:35;
A2: ( not InsCode I <= 10 + 1 or InsCode I <= 10 or InsCode I = 11 ) by NAT_1:8;
A3: ( not InsCode I <= 9 + 1 or InsCode I <= 8 + 1 or InsCode I = 10 ) by NAT_1:8;

per cases ( InsCode I <= 8 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 ) by A1, A2, A3, NAT_1:8;

suppose InsCode I <= 8 ; :: thesis: InsCode (IncAddr I,k) = InsCode I

then reconsider i = I as Instruction of SCM by SCMFSA_2:34;
IncAddr I,k = IncAddr i,k by Th21;
hence InsCode (IncAddr I,k) = InsCode I by RELOC:13; :: thesis: verum

end;

suppose ( InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 ) ; :: thesis: InsCode (IncAddr I,k) = InsCode I

then not InsCode I in {6,7,8} by ENUMSET1:def 1;
hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

end;