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 the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P )
thus ( I is parahalting implies for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P ) :: thesis: ( ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P
let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: I is_halting_on s,P
A2: Initialize I c= s +* (Initialize I) by FUNCT_4:26;
ProgramPart (Initialize I) = (ProgramPart I) +* (ProgramPart (Start-At (0,SCM+FSA))) by FUNCT_4:75
.= (ProgramPart I) +* {} by COMPOS_1:27
.= ProgramPart I by FUNCT_4:22 ;
then A3: ProgramPart (Initialize I) c= P +* (ProgramPart I) by FUNCT_4:26;
Initialize I is halting by A1, SCMFSA6B:def 3;
hence P +* (ProgramPart I) halts_on s +* (Initialize I) by A2, A3, EXTPRO_1:def 10; :: according to SCMFSA7B:def 8 :: thesis: verum

end;

assume A4: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P ; :: thesis: I is parahalting
let s be State of SCM+FSA; :: according to SCMFSA6B:def 3,EXTPRO_1:def 10 :: thesis: ( not Initialize I c= s or for b₁ being set holds
( not ProgramPart (Initialize I) c= b₁ or b₁ halts_on s ) )
assume A5: Initialize I c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize I) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize I) c= P or P halts_on s )
assume A6: ProgramPart (Initialize I) c= P ; :: thesis: P halts_on s
ProgramPart (Initialize I) = (ProgramPart I) +* (ProgramPart (Start-At (0,SCM+FSA))) by FUNCT_4:75
.= (ProgramPart I) +* {} by COMPOS_1:27
.= ProgramPart I by FUNCT_4:22 ;
then A7: P = P +* (ProgramPart I) by A6, FUNCT_4:79;
A8: s +* (Initialize I) = s by A5, FUNCT_4:79;
I is_halting_on s,P by A4;
hence P halts_on s by A7, A8, Def8; :: thesis: verum