let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA holds (IExec (I,P,s)) . (intloc 0) = 1
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA holds (IExec (I,P,s)) . (intloc 0) = 1
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: (IExec (I,P,s)) . (intloc 0) = 1
A1: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
A2: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
A3: I c= P +* I by FUNCT_4:26;
P +* I halts_on s +* (Initialized I) by Th19, A3, A2;
then A4: ex n being Element of NAT st
( Result ((P +* I),(s +* (Initialized I))) = Comput ((P +* I),(s +* (Initialized I)),n) & CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialized I))))) = halt SCM+FSA ) by EXTPRO_1:def 8;
A5: not intloc 0 in NAT

proof

A6: intloc 0 in Int-Locations by SCMFSA_2:9;
assume intloc 0 in NAT ; :: thesis: contradiction
hence contradiction by A6, SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum

end;

A7: Initialize I c= Initialized I by Lm4;
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then A8: Initialize I c= s +* (Initialized I) by A7, XBOOLE_1:1;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then not intloc 0 in dom (s | NAT) by A5;
hence (IExec (I,P,s)) . (intloc 0) = (Result ((P +* I),(s +* (Initialized I)))) . (intloc 0) by FUNCT_4:12
.= (s +* (Initialized I)) . (intloc 0) by A4, Def4, FUNCT_4:26, A8
.= (Initialized I) . (intloc 0) by A1, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: verum