let I be Instruction of SCM; :: thesis:
let k be Element of NAT ; :: thesis:
assume A1: not not InsCode I = 0 & ... & not InsCode I = 5 ; :: thesis:

per cases by A1;

suppose InsCode I = 0 ; :: thesis:

then I = halt SCM by AMI_5:7;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

suppose InsCode I = 1 ; :: thesis:

then ex da, db being Data-Location st I = da := db by AMI_5:8;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

suppose InsCode I = 2 ; :: thesis:

then ex da, db being Data-Location st I = AddTo (da,db) by AMI_5:9;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

suppose InsCode I = 3 ; :: thesis:

then ex da, db being Data-Location st I = SubFrom (da,db) by AMI_5:10;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

suppose InsCode I = 4 ; :: thesis:

then ex da, db being Data-Location st I = MultBy (da,db) by AMI_5:11;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

suppose InsCode I = 5 ; :: thesis:

then ex da, db being Data-Location st I = Divide (da,db) by AMI_5:12;
hence IncAddr (I,k) = I by COMPOS_0:4; :: thesis:

end;

end;