let i be Instruction of SCMPDS; ( 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:61;
set P = the Instruction-Sequence of SCMPDS;
assume
InsCode i = 1
; not i is parahalting
then consider a being Int_position such that
A2:
i = return a
by SCMPDS_2:27;
assume
i is parahalting
; contradiction
then reconsider Li = Load i as parahalting Program of ;
set pi = Macro i;
set s1 = Initialize s;
set P1 = the Instruction-Sequence of SCMPDS +* (Macro i);
(Initialize s) . (DataLoc (((Initialize s) . a),RetIC)) =
s . (DataLoc (((Initialize s) . a),RetIC))
by Th4
.=
2
by A1
;
then A3: (Exec (i,(Initialize s))) . (IC ) =
|.2.| + 2
by A2, SCMPDS_2:58
.=
2 + 2
by ABSVALUE:def 1
.=
4
;
set C1 = Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),1);
stop Li c= the Instruction-Sequence of SCMPDS +* (Macro i)
by FUNCT_4:25;
then A4:
IC (Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),1)) in dom (Macro i)
by SCMPDS_4:def 6;
0 in dom (Macro i)
by COMPOS_1:57;
then A5: ( the Instruction-Sequence of SCMPDS +* (Macro i)) . 0 =
(Macro i) . 0
by FUNCT_4:13
.=
i
by COMPOS_1:58
;
A6:
card (Macro i) = 2
by COMPOS_1:56;
A7:
( the Instruction-Sequence of SCMPDS +* (Macro i)) /. (IC (Initialize s)) = ( the Instruction-Sequence of SCMPDS +* (Macro i)) . (IC (Initialize s))
by PBOOLE:143;
Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),(0 + 1)) =
Following (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),0)))
by EXTPRO_1:3
.=
Following (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s))
.=
Exec (i,(Initialize s))
by A5, A7, MEMSTR_0:47
;
hence
contradiction
by A3, A4, A6, AFINSQ_1:66; verum