let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
let I be parahalting keeping_0 Program of ; :: thesis: (IExec (I,P,s)) . (intloc 0) = 1
A1: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A2: I c= P +* I by FUNCT_4:25;
P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by Th2, A2, A1;
then A3: 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 9;
thus (IExec (I,P,s)) . (intloc 0) = (Initialized s) . (intloc 0) by A3, Def4, A2
.= 1 by SCMFSA_M:9 ; :: thesis: verum