let s be State-consisting of 0 , 0 , 0 ,<%(halt SCM )%>, <*> INT ; :: thesis: ( ProgramPart s halts_on s & LifeSpan s = 0 & Result s = s )
set s0 = Comput (ProgramPart s),s,0 ;
1 = len <%(halt SCM )%> by AFINSQ_1:38;
then A1: s . (0 + 0 ) = <%(halt SCM )%> . 0 by Def1
.= halt SCM by AFINSQ_1:38 ;
A2: s = Comput (ProgramPart s),s,0 by AMI_1:13;
then s . (IC (Comput (ProgramPart s),s,0 )) = halt SCM by A1, Def1;
hence A3: ProgramPart s halts_on s by Th3; :: thesis: ( LifeSpan s = 0 & Result s = s )
Y: (ProgramPart (Comput (ProgramPart s),s,0 )) /. (IC (Comput (ProgramPart s),s,0 )) = (Comput (ProgramPart s),s,0 ) . (IC (Comput (ProgramPart s),s,0 )) by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s),s,0 )),(Comput (ProgramPart s),s,0 ) = halt SCM by A1, A2, Def1, Y;
hence LifeSpan s = 0 by A3, AMI_1:def 46; :: thesis: Result s = s
IC s = 0 by Def1;
hence Result s = s by A1, A2, Th4; :: thesis: verum