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 Ii = Initialized (stop Li);
set s1 = s +* (Initialized (stop Li));
(s +* (Initialized (stop Li))) . (DataLoc ((s +* (Initialized (stop Li))) . a),RetIC ) = s . (DataLoc ((s +* (Initialized (stop Li))) . a),RetIC ) by Th19
.= 2 by A1 ;
then A3: (Exec i,(s +* (Initialized (stop Li)))) . (IC SCMPDS ) = (abs 2) + 2 by A2, SCMPDS_2:70
.= 2 + 2 by ABSVALUE:def 1
.= 4 ;
set C1 = Comput (ProgramPart (s +* (Initialized (stop Li)))),(s +* (Initialized (stop Li))),1;
Initialized (stop Li) c= s +* (Initialized (stop Li)) by FUNCT_4:26;
then A4: IC (Comput (ProgramPart (s +* (Initialized (stop Li)))),(s +* (Initialized (stop Li))),1) in dom (stop Li) by SCMPDS_4:def 9;
0 in dom (Initialized (stop Li)) by Th13;
then A5: (s +* (Initialized (stop Li))) . 0 = (Initialized (stop Li)) . 0 by FUNCT_4:14
.= i by Th13 ;
A6: card (stop Li) = 2 by Th8;
Y: (ProgramPart (s +* (Initialized (stop Li)))) /. (IC (s +* (Initialized (stop Li)))) = (s +* (Initialized (stop Li))) . (IC (s +* (Initialized (stop Li)))) by AMI_1:150;
Comput (ProgramPart (s +* (Initialized (stop Li)))),(s +* (Initialized (stop Li))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop Li)))),(Comput (ProgramPart (s +* (Initialized (stop Li)))),(s +* (Initialized (stop Li))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop Li)))),(s +* (Initialized (stop Li))) by AMI_1:13
.= Exec i,(s +* (Initialized (stop Li))) by A5, Th18, FUNCT_4:26, Y ;
hence contradiction by A3, A4, A6, SCMPDS_4:1; :: thesis: verum