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
A2: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A3: I c= P +* I by FUNCT_4:25;
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 9;
thus (IExec (I,P,s)) . (intloc 0) = (Initialized s) . (intloc 0) by A4, Def4, A3
.= 1 by SCMFSA6A:38 ; :: thesis: verum