let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( <%(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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: Result (F,s) = s
IC s = 0 by MEMSTR_0:def 11;
hence Result (F,s) = s by A2, A3, EXTPRO_1:7; :: thesis: verum