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 COMPOS_1:93; :: 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, COMPOS_1:92; :: 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, COMPOS_1:92; :: 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, COMPOS_1:92; :: 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, COMPOS_1:92; :: 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, 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
A70: i = da := (f,db) by SCMFSA_2:62;
thus IncAddr (i,k) = i by A70, 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
A79: i = (f,db) := da by SCMFSA_2:63;
thus IncAddr (i,k) = i by A79, 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
A88: i = da :=len f by SCMFSA_2:64;
thus IncAddr (i,k) = i by A88, 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
A94: i = f :=<0,...,0> da by SCMFSA_2:65;
thus IncAddr (i,k) = i by A94, COMPOS_1:92; :: thesis: verum

end;

end;