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 A1: ( InsCode i <> 6 & InsCode i <> 7 & InsCode i <> 8 ) by ENUMSET1:def 1;

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 or InsCode i = 13 ) by A1, SCMFSA_2:35, NAT_1:38;

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

then i = halt SCM+FSA by SCMFSA_2:122;
hence IncAddr (i,k) = i by COMPOS_1:93; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A2: i = da := db by SCMFSA_2:54;
thus IncAddr (i,k) = i by A2, COMPOS_1:92; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A3: i = AddTo (da,db) by SCMFSA_2:55;
thus IncAddr (i,k) = i by A3, COMPOS_1:92; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A4: i = SubFrom (da,db) by SCMFSA_2:56;
thus IncAddr (i,k) = i by A4, COMPOS_1:92; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A5: i = MultBy (da,db) by SCMFSA_2:57;
thus IncAddr (i,k) = i by A5, COMPOS_1:92; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A6: i = Divide (da,db) by SCMFSA_2:58;
thus IncAddr (i,k) = i by A6, COMPOS_1:92; :: 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
A7: i = da := (f,db) by SCMFSA_2:62;
thus IncAddr (i,k) = i by A7, COMPOS_1:92; :: 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
A8: i = (f,db) := da by SCMFSA_2:63;
thus IncAddr (i,k) = i by A8, COMPOS_1:92; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A9: i = da :=len f by SCMFSA_2:64;
thus IncAddr (i,k) = i by A9, COMPOS_1:92; :: thesis: verum

end;

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

then consider da being Int-Location , f being FinSeq-Location such that
A10: i = f :=<0,...,0> da by SCMFSA_2:65;
thus IncAddr (i,k) = i by A10, COMPOS_1:92; :: thesis: verum

end;

suppose InsCode i = 13 ; :: thesis: IncAddr (i,k) = i

then consider da being Int-Location such that
A10: i = da :==1 by SCMFSA_2:134;
thus IncAddr (i,k) = i by A10, COMPOS_1:92; :: thesis: verum

end;

end;