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