let s be 0 -started State of SCMPDS; SCMPDS_4:def 7 for P being Instruction-Sequence of SCMPDS st stop (Load (halt SCMPDS)) c= P holds
P halts_on s
let P be Instruction-Sequence of SCMPDS; ( stop (Load (halt SCMPDS)) c= P implies P halts_on s )
set m = Load (halt SCMPDS);
set m0 = stop (Load (halt SCMPDS));
assume A1:
stop (Load (halt SCMPDS)) c= P
; P halts_on s
A2:
IC s = 0
by MEMSTR_0:def 11;
take
0
; EXTPRO_1:def 8 ( IC (Comput (P,s,0)) in proj1 P & CurInstr (P,(Comput (P,s,0))) = halt SCMPDS )
IC (Comput (P,s,0)) in NAT
;
hence
IC (Comput (P,s,0)) in dom P
by PARTFUN1:def 2; CurInstr (P,(Comput (P,s,0))) = halt SCMPDS
A3:
(Load (halt SCMPDS)) . 0 = halt SCMPDS
;
dom (Load (halt SCMPDS)) = {0}
by FUNCOP_1:13;
then A4:
0 in dom (Load (halt SCMPDS))
by TARSKI:def 1;
then A5:
0 in dom (stop (Load (halt SCMPDS)))
by FUNCT_4:12;
A6:
P /. (IC s) = P . (IC s)
by PBOOLE:143;
CurInstr (P,(Comput (P,s,0))) =
(stop (Load (halt SCMPDS))) . 0
by A1, A5, A2, A6, GRFUNC_1:2
.=
halt SCMPDS
by A3, A4, AFINSQ_1:def 3
;
hence
CurInstr (P,(Comput (P,s,0))) = halt SCMPDS
; verum