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 = Computation s,0 ;
1 = len <%(halt SCM )%> by AFINSQ_1:38;
then A1: s . (il. (0 + 0 )) = <%(halt SCM )%> . 0 by Def1
.= halt SCM by AFINSQ_1:38 ;
A2: s = Computation s,0 by AMI_1:13;
then s . (IC (Computation s,0 )) = halt SCM by A1, Def1;
hence A3: ProgramPart s halts_on s by Th3; :: thesis: ( LifeSpan s = 0 & Result s = s )
CurInstr (Computation s,0 ) = halt SCM by A1, A2, Def1;
hence LifeSpan s = 0 by A3, AMI_1:def 46; :: thesis: Result s = s
IC s = il. 0 by Def1;
hence Result s = s by A1, A2, Th4; :: thesis: verum