let I be Program of SCMPDS; :: thesis: ( I is parahalting iff for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P )

hereby :: thesis: ( ( for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P ) implies I is parahalting )

assume A1: I is parahalting ; :: thesis: for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P
let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: I is_halting_on s,P
P +* (stop I) halts_on Initialize s by A1, FUNCT_4:26, SCMPDS_4:def 10;
hence I is_halting_on s,P by Def3; :: thesis: verum

end;

assume A2: for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P ; :: thesis: I is parahalting
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 10 :: thesis: for b₁ being set holds
( not stop I c= b₁ or b₁ halts_on s )
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( not stop I c= P or P halts_on s )
A3: Initialize s = s by COMPOS_1:78;
assume stop I c= P ; :: thesis: P halts_on s
then A4: P = P +* (stop I) by FUNCT_4:104;
I is_halting_on s,P by A2;
hence P halts_on s by A4, Def3, A3; :: thesis: verum