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 Z: <%(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 A1: F . (0 + 0) = <%(halt SCM)%> . 0 by Z, GRFUNC_1:8
.= halt SCM by AFINSQ_1:38 ;
A2: s = Comput (F,s,0) by EXTPRO_1:3;
F . (IC s) = halt SCM by A1, COMPOS_1:def 16;
hence A3: F halts_on s by EXTPRO_1:31, A2; :: 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 A1, COMPOS_1:def 16 ;
hence LifeSpan (F,s) = 0 by A3, A2, EXTPRO_1:def 14; :: thesis: Result (F,s) = s
IC s = 0 by COMPOS_1:def 16;
hence Result (F,s) = s by A1, A2, EXTPRO_1:32; :: thesis: verum