let I be Instruction of SCM ; :: 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

per cases ( 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 ) by AMI_5:36, NAT_1:33;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

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

hence InsCode (IncAddr I,k) = InsCode I by Def3; :: thesis: verum

end;

suppose A1: InsCode I = 6 ; :: thesis: InsCode (IncAddr I,k) = InsCode I

then consider loc being Instruction-Location of SCM such that
A2: I = goto loc by AMI_5:52;
IncAddr (goto loc),k = goto (loc + k) by Th10;
hence InsCode (IncAddr I,k) = InsCode I by A1, A2, MCART_1:7; :: thesis: verum

end;

suppose A3: InsCode I = 7 ; :: thesis: InsCode (IncAddr I,k) = InsCode I

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A4: I = da =0_goto loc by AMI_5:53;
IncAddr (da =0_goto loc),k = da =0_goto (loc + k) by Th11;
hence InsCode (IncAddr I,k) = InsCode I by A3, A4, MCART_1:7; :: thesis: verum

end;

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

then consider loc being Instruction-Location of SCM , da being Data-Location such that
A6: I = da >0_goto loc by AMI_5:54;
IncAddr (da >0_goto loc),k = da >0_goto (loc + k) by Th12;
hence InsCode (IncAddr I,k) = InsCode I by A5, A6, MCART_1:7; :: thesis: verum

end;

end;