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

proof

A1: 0 in dom (Stop SCM+FSA) by AFINSQ_1:69;
B2: IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 3 :: thesis: ( not Start-At (0,SCM+FSA) c= s or for b₁ being set holds
( not Stop SCM+FSA c= b₁ or b₁ halts_on s ) )
assume A3: Start-At (0,SCM+FSA) c= s ; :: thesis: for b₁ being set holds
( not Stop SCM+FSA c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not Stop SCM+FSA c= P or P halts_on s )
assume A4: Stop SCM+FSA c= P ; :: thesis: P halts_on s
A5: Stop SCM+FSA c= P by A4;
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 (Start-At (0,SCM+FSA))) by A3, B2, GRFUNC_1:8
.= P . 0 by COMPOS_1:64
.= (Stop SCM+FSA) . 0 by A1, A5, GRFUNC_1:8
.= halt SCM+FSA by AFINSQ_1:38 ;
then P halts_on s by EXTPRO_1:30;
hence P halts_on s ; :: 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;