let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F implies for i1, i2 being Integer
for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) ) )
assume A1: <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F ; :: thesis: for i1, i2 being Integer
for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
let i1, i2 be Integer; :: thesis: for s being 0 -started State-consisting of <%i1,i2%> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
let s be 0 -started State-consisting of <%i1,i2%>; :: thesis: ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A2: s = Comput (F,s,0) by EXTPRO_1:2;
A3: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) by Th2;
A4: IC s = 0 by MEMSTR_0:def 11;
A5: F . 0 = AddTo ((dl. 0),(dl. 1)) by A1, Th3;
then A6: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A4, A2, Th5;
A7: F . 1 = halt SCM by A1, Th3;
hence F halts_on s by A6, EXTPRO_1:30; :: thesis: ( LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
thus LifeSpan (F,s) = 1 by A4, A7, A2, A6, EXTPRO_1:33; :: thesis: ( (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
(Comput (F,s,(0 + 1))) . (dl. 0) = ((Comput (F,s,0)) . (dl. 0)) + ((Comput (F,s,0)) . (dl. 1)) by A4, A5, A2, Th5;
hence (Result (F,s)) . (dl. 0) = i1 + i2 by A7, A3, A2, A6, EXTPRO_1:7; :: thesis: for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d
let d be Data-Location; :: thesis: ( d <> dl. 0 implies (Result (F,s)) . d = s . d )
assume A8: d <> dl. 0 ; :: thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A7, A6, EXTPRO_1:7
.= s . d by A4, A5, A2, A8, Th5 ; :: thesis: verum