set ii = (DataLoc (0,0)) := 0;
set m0 = stop (Load ((DataLoc (0,0)) := 0));
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 7 :: thesis: for b₁ being set holds
( not stop (Load ((DataLoc (0,0)) := 0)) c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop (Load ((DataLoc (0,0)) := 0)) c= P or P halts_on s )
assume A1: stop (Load ((DataLoc (0,0)) := 0)) c= P ; :: thesis: P halts_on s
XX: stop (Load ((DataLoc (0,0)) := 0)) = Macro ((DataLoc (0,0)) := 0) ;
take 1 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCMPDS )
IC (Comput (P,s,1)) in NAT ;
hence IC (Comput (P,s,1)) in dom P by PARTFUN1:def 2; :: thesis: CurInstr (P,(Comput (P,s,1))) = halt SCMPDS
A2: IC s = 0 by MEMSTR_0:def 8;
then A3: IC (Exec (((DataLoc (0,0)) := 0),s)) = succ 0 by SCMPDS_2:45
.= 0 + 1 ;
1 in dom (stop (Load ((DataLoc (0,0)) := 0))) by COMPOS_1:57, XX;
then (stop (Load ((DataLoc (0,0)) := 0))) . 1 = P . 1 by A1, GRFUNC_1:2;
then A4: P . 1 = halt SCMPDS by COMPOS_1:59, XX;
0 in dom (stop (Load ((DataLoc (0,0)) := 0))) by COMPOS_1:57, XX;
then A5: (stop (Load ((DataLoc (0,0)) := 0))) . 0 = P . 0 by A1, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec (((DataLoc (0,0)) := 0),s) by A2, A5, COMPOS_1:58, A6, XX ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCMPDS by A4, A3, PBOOLE:143; :: thesis: verum