set SAt = Start-At (0,SCM+FSA);
let I be Program of SCM+FSA; :: thesis: ( I is parahalting iff for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P )
thus ( I is parahalting implies for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) :: thesis: ( ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) implies I is parahalting )

proof

assume A1: I is parahalting ; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P
let P be Instruction-Sequence of SCM+FSA; :: thesis: I is_halting_on s,P
I c= P +* I by FUNCT_4:25;
hence P +* I halts_on Initialize s by A1, AMISTD_1:def 11; :: according to SCMFSA7B:def 7 :: thesis: verum

end;

assume A4: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ; :: thesis: I is parahalting
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11 :: thesis: for b₁ being set holds
( not I c= b₁ or b₁ halts_on s )
A5: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not I c= P or P halts_on s )
assume A6: I c= P ; :: thesis: P halts_on s
A7: P = P +* I by A6, FUNCT_4:98;
A8: Initialize s = s by A5, FUNCT_4:98;
I is_halting_on s,P by A4;
hence P halts_on s by A7, A8, Def8; :: thesis: verum