let I be Instruction of SCM; :: thesis: for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) holds
IncAddr (I,k) = I
let k be Element of NAT ; :: thesis: ( ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) implies IncAddr (I,k) = I )
assume A1: ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or 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:46;
hence IncAddr (I,k) = I by COMPOS_1:93; :: 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:47;
hence IncAddr (I,k) = I by COMPOS_1:92; :: 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:48;
hence IncAddr (I,k) = I by COMPOS_1:92; :: 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:49;
hence IncAddr (I,k) = I by COMPOS_1:92; :: 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:50;
hence IncAddr (I,k) = I by COMPOS_1:92; :: 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:51;
hence IncAddr (I,k) = I by COMPOS_1:92; :: thesis: verum

end;

end;