let s be State of ; AMI_1:def 26,SCMPDS_4:def 10 ( not Initialized (stop (Load (halt SCMPDS ))) c= s or ProgramPart s halts_on s )
set m = Load (halt SCMPDS );
set m0 = stop (Load (halt SCMPDS ));
set m1 = Initialized (stop (Load (halt SCMPDS )));
assume A1:
Initialized (stop (Load (halt SCMPDS ))) c= s
; ProgramPart s halts_on s
dom (Start-At (inspos 0 )) = {(IC SCMPDS )}
by FUNCOP_1:19;
then A2:
IC SCMPDS in dom (Start-At (inspos 0 ))
by TARSKI:def 1;
then A3:
IC SCMPDS in dom (Initialized (stop (Load (halt SCMPDS ))))
by FUNCT_4:13;
then A4: IC (Initialized (stop (Load (halt SCMPDS )))) =
(Initialized (stop (Load (halt SCMPDS )))) . (IC SCMPDS )
by AMI_1:def 43
.=
(Start-At (inspos 0 )) . (IC SCMPDS )
by A2, FUNCT_4:14
.=
inspos 0
by FUNCOP_1:87
;
take
0
; AMI_1:def 20 ( IC (Computation s,0 ) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,0 )) = halt SCMPDS )
IC (Computation s,0 ) in NAT
by AMI_1:def 4;
hence
IC (Computation s,0 ) in dom (ProgramPart s)
by AMI_1:143; (ProgramPart s) . (IC (Computation s,0 )) = halt SCMPDS
A5:
(Load (halt SCMPDS )) . (inspos 0 ) = halt SCMPDS
by FUNCOP_1:87;
dom (stop (Load (halt SCMPDS ))) misses dom (Start-At (inspos 0 ))
by Th54;
then A6:
stop (Load (halt SCMPDS )) c= Initialized (stop (Load (halt SCMPDS )))
by FUNCT_4:33;
dom (Load (halt SCMPDS )) = {(inspos 0 )}
by FUNCOP_1:19;
then A7:
inspos 0 in dom (Load (halt SCMPDS ))
by TARSKI:def 1;
then A8:
inspos 0 in dom (stop (Load (halt SCMPDS )))
by FUNCT_4:13;
then A9:
inspos 0 in dom (Initialized (stop (Load (halt SCMPDS ))))
by FUNCT_4:13;
CurInstr (Computation s,0 ) =
CurInstr s
by AMI_1:13
.=
s . (IC (Initialized (stop (Load (halt SCMPDS )))))
by A1, A3, AMI_1:97
.=
(Initialized (stop (Load (halt SCMPDS )))) . (inspos 0 )
by A1, A9, A4, GRFUNC_1:8
.=
(stop (Load (halt SCMPDS ))) . (inspos 0 )
by A6, A8, GRFUNC_1:8
.=
halt SCMPDS
by A5, A7, Th37
;
hence
(ProgramPart s) . (IC (Computation s,0 )) = halt SCMPDS
by AMI_1:145; verum