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
.= inspos 4 ;
set C1 = Computation (s +* (Initialized (stop Li))),1;
Initialized (stop Li) c= s +* (Initialized (stop Li)) by FUNCT_4:26;
then A4: IC (Computation (s +* (Initialized (stop Li))),1) in dom (stop Li) by SCMPDS_4:def 9;
inspos 0 in dom (Initialized (stop Li)) by Th13;
then A5: (s +* (Initialized (stop Li))) . (inspos 0 ) = (Initialized (stop Li)) . (inspos 0 ) by FUNCT_4:14
.= i by Th13 ;
A6: card (stop Li) = 2 by Th8;
Computation (s +* (Initialized (stop Li))),(0 + 1) = Following (Computation (s +* (Initialized (stop Li))),0 ) by AMI_1:14
.= Following (s +* (Initialized (stop Li))) by AMI_1:13
.= Exec i,(s +* (Initialized (stop Li))) by A5, Th18, FUNCT_4:26 ;
hence contradiction by A3, A4, A6, SCMPDS_4:1; :: thesis: verum