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