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
A2: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
A3: I c= P +* I by FUNCT_4:26;
P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th19, A3, A2;
then A4: ex n being Element of NAT st
( Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),n) & CurInstr ((P +* I),(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) = 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;

B7: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then B8: Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1)) by B7, XBOOLE_1:1;
X9: Initialize ((intloc 0) .--> 1) c= Initialized I by FUNCT_4:26;
dom (ProgramPart s) = NAT by COMPOS_1:34;
hence (IExec (I,P,s)) . (intloc 0) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . (intloc 0) by A5, FUNCT_4:12
.= (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A4, Def4, B8, FUNCT_4:26
.= (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:14, SCMFSA6A:86
.= (Initialized I) . (intloc 0) by X9, GRFUNC_1:8, SCMFSA6A:86
.= 1 by SCMFSA6A:46 ;
:: thesis: verum