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

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