let k be 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;
not not InsCode i = 0 & ... & not InsCode i = 12 by SCMFSA_2:16;

per cases then ( 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 A1;

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

then i = halt SCM+FSA by SCMFSA_2:95;
hence IncAddr (i,k) = i by COMPOS_0:4; :: 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:30;
thus IncAddr (i,k) = i by A2, COMPOS_0:4; :: 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:31;
thus IncAddr (i,k) = i by A3, COMPOS_0:4; :: 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:32;
thus IncAddr (i,k) = i by A4, COMPOS_0:4; :: 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:33;
thus IncAddr (i,k) = i by A5, COMPOS_0:4; :: 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:34;
thus IncAddr (i,k) = i by A6, COMPOS_0:4; :: 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:38;
thus IncAddr (i,k) = i by A7, COMPOS_0:4; :: 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:39;
thus IncAddr (i,k) = i by A8, COMPOS_0:4; :: 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:40;
thus IncAddr (i,k) = i by A9, COMPOS_0:4; :: 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:41;
thus IncAddr (i,k) = i by A10, COMPOS_0:4; :: thesis: verum

end;

end;