let s be State of SCM+FSA ; :: thesis: for I being parahalting Program of SCM+FSA st I +* (Start-At (insloc 0 )) c= s holds
s is halting
let I be parahalting Program of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s implies s is halting )
assume A1: I +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
I +* (Start-At (insloc 0 )) is halting by Def3;
hence s is halting by A1, AMI_1:def 26; :: thesis: verum