let I be Program of SCM+FSA ; :: thesis: ( I is parahalting implies not I is empty )
assume that
A1: I is parahalting and
A2: I is empty ; :: thesis: contradiction
reconsider I = I as parahalting Program of SCM+FSA by A1;
deffunc H₁( set ) -> Element of the Instructions of SCM+FSA = goto (insloc 0 );
deffunc H₂( set ) -> Element of K327() = 1;
deffunc H₃( set ) -> FinSequence of INT = <*> INT ;
consider S being State of SCM+FSA such that
A3: IC S = insloc 0 and
A4: for i being Element of NAT holds
( S . (insloc i) = H₁(i) & S . (intloc i) = H₂(i) & S . (fsloc i) = H₃(i) ) from SCMFSA6A:sch 1();
A5: I c= S by A2, XBOOLE_1:2;
A6: intloc 0 in dom S by SCMFSA_2:66;
S . (intloc 0 ) = 1 by A4;
then (intloc 0 ) .--> 1 c= S by A6, FUNCOP_1:88;
then A7: I +* ((intloc 0 ) .--> 1) c= S by A5, FUNCT_4:92;
IC SCM+FSA in dom S by AMI_1:94;
then A8: (IC SCM+FSA ) .--> (insloc 0 ) c= S by A3, FUNCOP_1:88;
Initialized I c= S by A7, A8, FUNCT_4:92;
then A9: S is halting by AMI_1:def 26;
S . (insloc 0 ) = goto (insloc 0 ) by A4;
hence contradiction by A3, A9, Th24; :: thesis: verum