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