let k be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds
IncAddr i,k = i
let i be Instruction of SCM+FSA ; :: thesis: ( not InsCode i in {6,7,8} implies IncAddr i,k = i )
assume not InsCode i in {6,7,8} ; :: thesis: IncAddr i,k = i
then Z: ( InsCode i <> 6 & InsCode i <> 7 & InsCode i <> 8 ) by ENUMSET1:def 1;
A4: InsCode i <= 12 by SCMFSA_2:35;

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 = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by Z, A4, NAT_1:37;

suppose InsCode i = 0 ; :: thesis: IncAddr i,k = i

then i = halt SCM+FSA by SCMFSA_2:122;
hence IncAddr i,k = i by AMISTD_2:30; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: IncAddr i,k = i

then consider da, db being Int-Location such that
A8: i = da := db by SCMFSA_2:54;
thus IncAddr i,k = i by A8, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: IncAddr i,k = i

then consider da, db being Int-Location such that
A14: i = AddTo da,db by SCMFSA_2:55;
thus IncAddr i,k = i by A14, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: IncAddr i,k = i

then consider da, db being Int-Location such that
A20: i = SubFrom da,db by SCMFSA_2:56;
thus IncAddr i,k = i by A20, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: IncAddr i,k = i

then consider da, db being Int-Location such that
A26: i = MultBy da,db by SCMFSA_2:57;
thus IncAddr i,k = i by A26, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: IncAddr i,k = i

then consider da, db being Int-Location such that
A32: i = Divide da,db by SCMFSA_2:58;
thus IncAddr i,k = i by A32, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: IncAddr i,k = i

then consider db, da being Int-Location , f being FinSeq-Location such that
A70: i = da := f,db by SCMFSA_2:62;
thus IncAddr i,k = i by A70, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: IncAddr i,k = i

then consider db, da being Int-Location , f being FinSeq-Location such that
A79: i = f,db := da by SCMFSA_2:63;
thus IncAddr i,k = i by A79, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: IncAddr i,k = i

then consider da being Int-Location , f being FinSeq-Location such that
A88: i = da :=len f by SCMFSA_2:64;
thus IncAddr i,k = i by A88, AMISTD_2:29; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: IncAddr i,k = i

then consider da being Int-Location , f being FinSeq-Location such that
A94: i = f :=<0,...,0> da by SCMFSA_2:65;
thus IncAddr i,k = i by A94, AMISTD_2:29; :: thesis: verum

end;

end;