let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%(() := (dl. 1))%> ^ <%()%> 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)) . () = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) ) )

assume A1: <%(() := (dl. 1))%> ^ <%()%> 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)) . () = 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)) . () = 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)) . () = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )

set s1 = Comput (F,s,(0 + 1));
A2: s . (dl. 1) = i2 by Th2;
A3: ( IC s = 0 & s = Comput (F,s,0) ) by ;
A4: F . 0 = () := (dl. 1) by ;
then A5: IC (Comput (F,s,(0 + 1))) = 0 + 1 by ;
A6: F . 1 = halt SCM by ;
hence F halts_on s by ; :: thesis: ( LifeSpan (F,s) = 1 & (Result (F,s)) . () = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )

thus LifeSpan (F,s) = 1 by ; :: thesis: ( (Result (F,s)) . () = i2 & ( for d being Data-Location st d <> dl. 0 holds
(Result (F,s)) . d = s . d ) )

(Comput (F,s,(0 + 1))) . () = s . (dl. 1) by A4, A3, Th4;
hence (Result (F,s)) . () = i2 by ; :: 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 A7: d <> dl. 0 ; :: thesis: (Result (F,s)) . d = s . d
thus (Result (F,s)) . d = (Comput (F,s,(0 + 1))) . d by
.= s . d by A4, A3, A7, Th4 ; :: thesis: verum