let I be Instruction of SCM; :: thesis: for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 holds
IncAddr (I,k) = I
let k be Element of NAT ; :: thesis: ( not not InsCode I = 0 & ... & not InsCode I = 5 implies IncAddr (I,k) = I )
assume A1: not not InsCode I = 0 & ... & not InsCode I = 5 ; :: thesis: IncAddr (I,k) = 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 ) by A1;

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

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

end;

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

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: verum

end;

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

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: verum

end;

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

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: verum

end;

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

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: verum

end;

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

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: verum

end;

end;