let s be State-consisting of 0 , 0 , 0 ,<*(halt SCM )*>, <*> INT ; :: thesis: ( s is halting & LifeSpan s = 0 & Result s = s )
set s0 = Computation s,0 ;
1 = len <*(halt SCM )*> by FINSEQ_1:57;
then A1: s . (il. (0 + 0 )) = <*(halt SCM )*> . (0 + 1) by Def1
.= halt SCM by FINSEQ_1:57 ;
A2: s = Computation s,0 by AMI_1:13;
then s . (IC (Computation s,0 )) = halt SCM by A1, Def1;
hence A3: s is halting 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