let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: 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; :: thesis: ( 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 ; :: thesis: P halts_on s
A2: IC s = 0 by MEMSTR_0:def 11;
take 0 ; :: according to EXTPRO_1:def 8 :: thesis: ( 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; :: thesis: 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 ; :: thesis: verum