let s be State of SCM+FSA; :: thesis: for I being parahalting Program of SCM+FSA st Initialized I c= s holds
ProgramPart s halts_on s
let I be parahalting Program of SCM+FSA; :: thesis: ( Initialized I c= s implies ProgramPart s halts_on s )
A1: I +* (Start-At (0,SCM+FSA)) is halting by Def3;
( Start-At (0,SCM+FSA) c= Initialized I & I c= Initialized I ) by FUNCT_4:26, SCMFSA6A:26;
then ( I +* (Start-At (0,SCM+FSA)) c= I \/ (Start-At (0,SCM+FSA)) & I \/ (Start-At (0,SCM+FSA)) c= Initialized I ) by FUNCT_4:30, XBOOLE_1:8;
then A2: I +* (Start-At (0,SCM+FSA)) c= Initialized I by XBOOLE_1:1;
assume Initialized I c= s ; :: thesis: ProgramPart s halts_on s
then I +* (Start-At (0,SCM+FSA)) c= s by A2, XBOOLE_1:1;
hence ProgramPart s halts_on s by A1, EXTPRO_1:def 10; :: thesis: verum