let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: ( <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F implies for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) ) )
assume Z: <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F ; :: thesis: for i1, i2 being Integer
for s being 0 -started State-consisting of 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = 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 0 ,<*i1*> ^ <*i2*> holds
( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = 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 0 ,<*i1*> ^ <*i2*>; :: thesis: ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
set s1 = Comput (F,s,(0 + 1));
A1: s . (dl. 1) = i2 by Th15;
A2: ( IC s = 0 & s = Comput (F,s,0) ) by COMPOS_1:def 16, EXTPRO_1:3;
A3: F . 0 = (dl. 0) := (dl. 1) by Z, Th15A;
then A4: IC (Comput (F,s,(0 + 1))) = 0 + 1 by A2, Th18;
A5: F . 1 = halt SCM by Z, Th15A;
hence F halts_on s by A4, EXTPRO_1:31; :: thesis: ( LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
thus LifeSpan (F,s) = 1 by A5, A2, A4, EXTPRO_1:34; :: thesis: ( (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )
(Comput (F,s,(0 + 1))) . (dl. 0) = s . (dl. 1) by A3, A2, Th18;
hence (Result (F,s)) . (dl. 0) = i2 by A5, A1, A4, EXTPRO_1:32; :: 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 A6: d <> dl. 0 ; :: thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by A5, A4, EXTPRO_1:32
.= s . d by A3, A2, A6, Th18 ; :: thesis: verum