let f be FinSeq-Location ; for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let P be Instruction-Sequence of SCM+FSA; for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
let I be parahalting Program of ; ( not f in UsedInt*Loc I implies (IExec (I,P,s)) . f = s . f )
assume A1:
not f in UsedInt*Loc I
; (IExec (I,P,s)) . f = s . f
A2:
I c= P +* I
by FUNCT_4:25;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:25;
then
P +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th19, A2;
then consider n being Element of NAT such that
A3:
Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),n)
and
CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = halt SCM+FSA
by EXTPRO_1:def 9;
XX:
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA)))
by FUNCT_4:def 1;
YY:
not f in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:103;
f <> intloc 0
by SCMFSA_2:58;
then
not f in {(intloc 0)}
by TARSKI:def 1;
then
not f in dom ((intloc 0) .--> 1)
by FUNCOP_1:13;
then A4:
not f in dom (Initialize ((intloc 0) .--> 1))
by XX, YY, XBOOLE_0:def 3;
for m being Element of NAT st m < n holds
IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),m)) in dom I
by A2, AMISTD_1:def 10;
hence (IExec (I,P,s)) . f =
(s +* (Initialize ((intloc 0) .--> 1))) . f
by A1, A3, FUNCT_4:25, SF_MASTR:63
.=
s . f
by A4, FUNCT_4:11
;
verum