deffunc H₁( set ) -> FinSequence of INT = <*> INT ;
deffunc H₂( set ) -> Element of K314() = 1;
deffunc H₃( set ) -> Element of the Instructions of SCM+FSA = goto 0 ;
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;
consider S being State of SCM+FSA such that
A3: IC S = 0 and
A4: for i being Element of NAT holds
( S . i = H₃(i) & S . (intloc i) = H₂(i) & S . (fsloc i) = H₁(i) ) from SCMFSA6A:sch 1();
( intloc 0 in dom S & S . (intloc 0 ) = 1 ) by A4, SCMFSA_2:66;
then A5: (intloc 0 ) .--> 1 c= S by FUNCOP_1:88;
IC SCM+FSA in dom S by COMPOS_1:9;
then A6: (IC SCM+FSA ) .--> 0 c= S by A3, FUNCOP_1:88;
I c= S by A2, XBOOLE_1:2;
then I +* ((intloc 0 ) .--> 1) c= S by A5, FUNCT_4:92;
then Initialized I c= S by A6, FUNCT_4:92;
then A7: ProgramPart S halts_on S by AMI_1:def 26;
S . 0 = goto 0 by A4;
hence contradiction by A3, A7, Th24; :: thesis: verum