let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting keepInt0_1 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 InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . (intloc 0) = 1
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: (IExec (I,p,s)) . (intloc 0) = 1
not intloc 0 in NAT

proof

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

end;

then A2: not intloc 0 in dom (s | NAT) by RELAT_1:86;
A3: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
A4: I c= p +* I by FUNCT_4:26;
then p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th5, A3;
then A5: ( Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) & 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, FUNCT_4:26;
thus (IExec (I,p,s)) . (intloc 0) = ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) . (intloc 0) by SCMFSA6B:def 1
.= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . (intloc 0) by A2, FUNCT_4:12
.= 1 by A5, A4, Def3 ; :: thesis: verum