let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: ( <%(halt SCM)%> c= F implies for s being 0 -started State-consisting of 0 , <*> 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 0 , <*> INT holds
( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
let s be 0 -started State-consisting of 0 , <*> INT; :: thesis: ( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s )
1 = dom <%(halt SCM)%> by AFINSQ_1:36;
then 0 in dom <%(halt SCM)%> by CARD_1:87, TARSKI:def 1;
then A2: F . (0 + 0) = <%(halt SCM)%> . 0 by A1, GRFUNC_1:8
.= halt SCM by AFINSQ_1:38 ;
A3: s = Comput (F,s,0) by EXTPRO_1:3;
F . (IC s) = halt SCM by A2, COMPOS_1:def 16;
hence A4: F halts_on s by A3, EXTPRO_1:31; :: thesis: ( LifeSpan (F,s) = 0 & Result (F,s) = s )
dom F = NAT by PARTFUN1:def 4;
then CurInstr (F,s) = F . (IC s) by PARTFUN1:def 8
.= halt SCM by A2, COMPOS_1:def 16 ;
hence LifeSpan (F,s) = 0 by A4, A3, EXTPRO_1:def 14; :: thesis: Result (F,s) = s
IC s = 0 by COMPOS_1:def 16;
hence Result (F,s) = s by A2, A3, EXTPRO_1:32; :: thesis: verum