let F be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( F is parahalting implies F is 0 -halting )
assume A1: F is parahalting ; :: thesis: F is 0 -halting
let s be 0 -started State of S; :: according to AMISTD_5:def 7 :: thesis: for P being Instruction-Sequence of S st F c= P holds
P halts_on s
thus for P being Instruction-Sequence of S st F c= P holds
P halts_on s by A1, AMISTD_1:def 11; :: thesis: verum