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

( 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