thus Stop SCM+FSA is parahalting :: thesis: Stop SCM+FSA is good

proof

Initialize (Stop SCM+FSA) is halting

proof

A1: 0 in dom (Stop SCM+FSA) by AFINSQ_1:69;
A2: IC in dom (Initialize (Stop SCM+FSA)) by COMPOS_1:141;
let s be State of SCM+FSA; :: according to EXTPRO_1:def 10 :: thesis: ( not Initialize (Stop SCM+FSA) c= s or for b₁ being set holds
( not ProgramPart (Initialize (Stop SCM+FSA)) c= b₁ or b₁ halts_on s ) )
assume A3: Initialize (Stop SCM+FSA) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (Stop SCM+FSA)) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize (Stop SCM+FSA)) c= P or P halts_on s )
assume A4: ProgramPart (Initialize (Stop SCM+FSA)) c= P ; :: thesis: P halts_on s
A5: Stop SCM+FSA c= P by A4, COMPOS_1:144;
A6: dom P = NAT by PARTFUN1:def 4;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s) by EXTPRO_1:3
.= P . (IC s) by A6, PARTFUN1:def 8
.= P . (IC (Initialize (Stop SCM+FSA))) by A3, A2, GRFUNC_1:8
.= P . 0 by COMPOS_1:142
.= (Stop SCM+FSA) . 0 by A1, GRFUNC_1:8, A5
.= halt SCM+FSA by AFINSQ_1:38 ;
hence P halts_on s by EXTPRO_1:30; :: thesis: verum

end;

hence Stop SCM+FSA is parahalting by SCMFSA6B:def 3; :: thesis: verum

end;

thus not Stop SCM+FSA destroys intloc 0 :: according to SCMFSA7B:def 5 :: thesis: verum

proof

now

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Stop SCM+FSA) implies not i destroys intloc 0 )
A7: rng (Stop SCM+FSA) = {(halt SCM+FSA)} by AFINSQ_1:36;
assume i in rng (Stop SCM+FSA) ; :: thesis: not i destroys intloc 0
then i = halt SCM+FSA by A7, TARSKI:def 1;
hence not i destroys intloc 0 by Th11; :: thesis: verum

end;

hence not Stop SCM+FSA destroys intloc 0 by Def4; :: thesis: verum

end;