let i1, i2 be Integer; :: thesis: for s being State-consisting of 0 , 0 , 0 ,<%(goto (il. 1))%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*> holds
( ProgramPart s halts_on s & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )
let s be State-consisting of 0 , 0 , 0 ,<%(goto (il. 1))%> ^ <%(halt SCM )%>,<*i1*> ^ <*i2*>; :: thesis: ( ProgramPart s halts_on s & LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )
set s1 = Computation s,(0 + 1);
A1: ( IC s = il. 0 & s = Computation s,0 ) by Th15, AMI_1:13;
A2: s . (il. 0 ) = goto (il. 1) by Th15;
then A3: IC (Computation s,(0 + 1)) = il. (0 + 1) by A1, Th23;
A4: s . (il. 1) = halt SCM by Th15;
hence ProgramPart s halts_on s by A3, Th3; :: thesis: ( LifeSpan s = 1 & ( for d being Data-Location holds (Result s) . d = s . d ) )
thus LifeSpan s = 1 by A4, A1, A3, Th17; :: thesis: for d being Data-Location holds (Result s) . d = s . d
let d be Data-Location ; :: thesis: (Result s) . d = s . d
thus (Result s) . d = (Computation s,(0 + 1)) . d by A4, A3, Th4
.= s . d by A2, A1, Th23 ; :: thesis: verum