let s be State-consisting of 0 , 0 , 0 ,<%(halt SCM )%>, <*> INT ; :: thesis: ( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = 0 & Result (ProgramPart s),s = s )
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;
s . (IC s) = halt SCM by A1, Def1;
hence A3: ProgramPart s halts_on s by Th3, A2; :: thesis: ( LifeSpan (ProgramPart s),s = 0 & Result (ProgramPart s),s = s )
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
CurInstr (ProgramPart s),s = halt SCM by A1, Def1, Y;
hence LifeSpan (ProgramPart s),s = 0 by A3, A2, AMI_1:def 46; :: thesis: Result (ProgramPart s),s = s
IC s = 0 by Def1;
hence Result (ProgramPart s),s = s by A1, A2, Th4; :: thesis: verum