now

let s be State of SCM+FSA ; :: thesis: ( (a := k) +* (Start-At (insloc 0 )) c= s implies s is halting )
assume A1: (a := k) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
A2: IC SCM+FSA in dom ((a := k) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
IC s = s . (IC SCM+FSA ) by AMI_1:def 15
.= ((a := k) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A2, GRFUNC_1:8
.= insloc 0 by SF_MASTR:66 ;
hence s is halting by A1, Lm1, SCMFSA6B:5; :: thesis: verum

end;

then (a := k) +* (Start-At (insloc 0 )) is halting by AMI_1:def 26;
hence a := k is parahalting by SCMFSA6B:def 3; :: thesis: verum