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

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