let i be Instruction of SCMPDS ; :: thesis: ( InsCode i = 1 implies not i is parahalting )
assume A1: InsCode i = 1 ; :: thesis: not i is parahalting
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);
consider s being State of SCMPDS such that
A2: for a being Int_position holds s . a = 2 by SCMPDS_2:73;
set s1 = s +* (Initialized (stop Li));
A3: Initialized (stop Li) c= s +* (Initialized (stop Li)) by FUNCT_4:26;
inspos 0 in dom (Initialized (stop Li)) by Th13;
then A4: (s +* (Initialized (stop Li))) . (inspos 0 ) = (Initialized (stop Li)) . (inspos 0 ) by FUNCT_4:14
.= i by Th13 ;
A5: 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 A4, Th18, FUNCT_4:26 ;
consider a being Int_position such that
A6: i = return a by A1, SCMPDS_2:36;
(s +* (Initialized (stop Li))) . (DataLoc ((s +* (Initialized (stop Li))) . a),RetIC ) = s . (DataLoc ((s +* (Initialized (stop Li))) . a),RetIC ) by Th19
.= 2 by A2 ;
then A7: (Exec i,(s +* (Initialized (stop Li)))) . (IC SCMPDS ) = (abs 2) + 2 by A6, SCMPDS_2:70
.= 2 + 2 by ABSVALUE:def 1
.= inspos 4 ;
set C1 = Computation (s +* (Initialized (stop Li))),1;
A8: IC (Computation (s +* (Initialized (stop Li))),1) in dom (stop Li) by A3, SCMPDS_4:def 9;
card (stop Li) = 2 by Th8;
hence contradiction by A5, A7, A8, SCMPDS_4:1; :: thesis: verum