let F be NAT -defined the InstructionsF of SCM -valued total Function; ( <%(halt SCM)%> c= F implies for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s ) )
assume A1:
<%(halt SCM)%> c= F
; for s being 0 -started State-consisting of <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
let s be 0 -started State-consisting of <*> INT; ( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
1 = len <%(halt SCM)%>
by AFINSQ_1:34;
then
0 in dom <%(halt SCM)%>
by CARD_1:49, TARSKI:def 1;
then A2: F . (0 + 0) =
<%(halt SCM)%> . 0
by A1, GRFUNC_1:2
.=
halt SCM
;
A3:
s = Comput (F,s,0)
by EXTPRO_1:2;
F . (IC s) = halt SCM
by A2, MEMSTR_0:def 11;
hence A4:
F halts_on s
by A3, EXTPRO_1:30; ( LifeSpan (F,s) = 0 & Result (F,s) = s )
dom F = NAT
by PARTFUN1:def 2;
then CurInstr (F,s) =
F . (IC s)
by PARTFUN1:def 6
.=
halt SCM
by A2, MEMSTR_0:def 11
;
hence
LifeSpan (F,s) = 0
by A4, A3, EXTPRO_1:def 15; Result (F,s) = s
IC s = 0
by MEMSTR_0:def 11;
hence
Result (F,s) = s
by A2, A3, EXTPRO_1:7; verum