let i be Instruction of SCMPDS ; :: thesis: ( InsCode i = 1 implies not i is parahalting )
consider s being State of SCMPDS such that
A1: for a being Int_position holds s . a = 2 by SCMPDS_2:73;
assume InsCode i = 1 ; :: thesis: not i is parahalting
then consider a being Int_position such that
A2: i = return a by SCMPDS_2:36;
assume i is parahalting ; :: thesis: contradiction
then reconsider Li = Load i as parahalting Program of SCMPDS ;
set pi = stop Li;
set s1 = (Initialize s) +* (stop Li);
I1: s +* (Initialize (stop Li)) = (Initialize s) +* (stop Li) by SCMPDS_4:5;
((Initialize s) +* (stop Li)) . (DataLoc (((Initialize s) +* (stop Li)) . a),RetIC ) = s . (DataLoc (((Initialize s) +* (stop Li)) . a),RetIC ) by Th19
.= 2 by A1 ;
then A3: (Exec i,((Initialize s) +* (stop Li))) . (IC SCMPDS ) = (abs 2) + 2 by A2, SCMPDS_2:70
.= 2 + 2 by ABSVALUE:def 1
.= 4 ;
set C1 = Comput (ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)),1;
Initialize (stop Li) c= (Initialize s) +* (stop Li) by I1, FUNCT_4:26;
then A4: IC (Comput (ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)),1) in dom (stop Li) by SCMPDS_4:def 9;
0 in dom (Initialize (stop Li)) by Th13;
then A5: ((Initialize s) +* (stop Li)) . 0 = (Initialize (stop Li)) . 0 by I1, FUNCT_4:14
.= i by Th13 ;
A6: card (stop Li) = 2 by Th8;
Y: (ProgramPart ((Initialize s) +* (stop Li))) /. (IC ((Initialize s) +* (stop Li))) = ((Initialize s) +* (stop Li)) . (IC ((Initialize s) +* (stop Li))) by COMPOS_1:38;
Comput (ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop Li))),(Comput (ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)) by AMI_1:13
.= Exec i,((Initialize s) +* (stop Li)) by A5, Th18, Y, I1, FUNCT_4:26 ;
hence contradiction by A3, A4, A6, AFINSQ_1:70; :: thesis: verum