set m = Stop SCM+FSA;
A1: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
thus Stop SCM+FSA is parahalting :: thesis: Stop SCM+FSA is keeping_0
proof
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b1 being set holds
( not Stop SCM+FSA c= b1 or b1 halts_on s )
A2: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Stop SCM+FSA c= P or P halts_on s )
assume A3: Stop SCM+FSA c= P ; :: thesis: P halts_on s
A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
take 0 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
A5: dom P = NAT by PARTFUN1:def 2;
hence IC (Comput (P,s,0)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
CurInstr (P,(Comput (P,s,0))) = P . (IC s) by A5, PARTFUN1:def 6
.= P . (IC (Start-At (0,SCM+FSA))) by A2, A4, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Stop SCM+FSA) . 0 by A3, A1, GRFUNC_1:2
.= halt SCM+FSA ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum
end;
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: for P being Instruction-Sequence of SCM+FSA st Stop SCM+FSA c= P holds
for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A6: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Stop SCM+FSA c= P implies for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A7: Stop SCM+FSA c= P ; :: thesis: for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Nat; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A8: s = Comput (P,s,0) ;
dom P = NAT by PARTFUN1:def 2;
then A9: P /. (IC s) = P . (IC s) by PARTFUN1:def 6;
CurInstr (P,s) = P . 0 by A6, A9, MEMSTR_0:39
.= (Stop SCM+FSA) . 0 by A1, A7, GRFUNC_1:2
.= halt SCM+FSA ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A8, EXTPRO_1:5; :: thesis: verum