let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . (intloc 0) = 1
let p be Instruction-Sequence of SCM+FSA; :: 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
A1: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
A2: I c= p +* I by FUNCT_4:25;
then p +* I halts_on Initialized s by Def1, A1;
then A3: ( Initialize ((intloc 0) .--> 1) c= Initialized s & ex n being Nat st
( Result ((p +* I),(Initialized s)) = Comput ((p +* I),(Initialized s),n) & CurInstr ((p +* I),(Result ((p +* I),(Initialized s)))) = halt SCM+FSA ) ) by EXTPRO_1:def 9, FUNCT_4:25;
thus (IExec (I,p,s)) . (intloc 0) = (Result ((p +* I),(Initialized s))) . (intloc 0) by SCMFSA6B:def 1
.= 1 by A3, A2, Def2 ; :: thesis: verum