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;
consider P being the Instructions of SCMPDS -valued ManySortedSet of NAT ;
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;
set P1 = P +* (stop Li);
(Initialize s) . (DataLoc (((Initialize s) . a),RetIC)) =
s . (DataLoc (((Initialize s) . a),RetIC))
by Th19
.=
2
by A1
;
then A4: (Exec (i,(Initialize s))) . (IC ) =
(abs 2) + 2
by A2, SCMPDS_2:70
.=
2 + 2
by ABSVALUE:def 1
.=
4
;
set C1 = Comput ((P +* (stop Li)),(Initialize s),1);
A5:
IC (Comput ((P +* (stop Li)),(Initialize s),1)) in dom (stop Li)
by FUNCT_4:26, SCMPDS_4:def 9;
0 in dom (stop Li)
by Th9;
then A6: (P +* (stop Li)) . 0 =
(stop Li) . 0
by FUNCT_4:14
.=
i
by Th10
;
A7:
card (stop Li) = 2
by Th8;
A8:
(P +* (stop Li)) /. (IC (Initialize s)) = (P +* (stop Li)) . (IC (Initialize s))
by PBOOLE:158;
Comput ((P +* (stop Li)),(Initialize s),(0 + 1)) =
Following ((P +* (stop Li)),(Comput ((P +* (stop Li)),(Initialize s),0)))
by EXTPRO_1:4
.=
Following ((P +* (stop Li)),(Initialize s))
by EXTPRO_1:3
.=
Exec (i,(Initialize s))
by A6, A8, COMPOS_1:223
;
hence
contradiction
by A4, A5, A7, AFINSQ_1:70; verum