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