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:73;
assume
InsCode i = 1
; not i is parahalting
then consider a being Int_position such that
A2:
i = return a
by SCMPDS_2:36;
assume
i is parahalting
; 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 COMPOS_1:125;
((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);
A4:
IC (Comput ((ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)),1)) in dom (stop Li)
by FUNCT_4:26, SCMPDS_4:def 9;
0 in dom (stop Li)
by Th9;
then A5: ((Initialize s) +* (stop Li)) . 0 =
(stop Li) . 0
by FUNCT_4:14
.=
i
by Th10
;
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 EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize s) +* (stop Li))),((Initialize s) +* (stop Li)))
by EXTPRO_1:3
.=
Exec (i,((Initialize s) +* (stop Li)))
by A5, Th18, Y, I1, FUNCT_4:26
;
hence
contradiction
by A3, A4, A6, AFINSQ_1:70; verum