set SAt = Start-At (0,SCM+FSA);

let I be Program of ; :: 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 ) by FUNCT_4:25; :: 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 )

assume A1: 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 10 :: thesis: for b_{1} being set holds

( not I c= b_{1} or b_{1} halts_on s )

A2: 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 A3: I c= P ; :: thesis: P halts_on s

A4: P = P +* I by A3, FUNCT_4:98;

A5: Initialize s = s by A2, FUNCT_4:98;

I is_halting_on s,P by A1;

hence P halts_on s by A4, A5; :: thesis: verum

let I be Program of ; :: 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 ) by FUNCT_4:25; :: 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 )

assume A1: 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 10 :: thesis: for b

( not I c= b

A2: 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 A3: I c= P ; :: thesis: P halts_on s

A4: P = P +* I by A3, FUNCT_4:98;

A5: Initialize s = s by A2, FUNCT_4:98;

I is_halting_on s,P by A1;

hence P halts_on s by A4, A5; :: thesis: verum