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