let s be State of SCM+FSA ; AMI_1:def 26,SCM_HALT:def 2 ( not Initialized (Macro (halt SCM+FSA )) c= s or ProgramPart s halts_on s )
set m = Macro (halt SCM+FSA );
set m1 = Initialized (Macro (halt SCM+FSA ));
assume A1:
Initialized (Macro (halt SCM+FSA )) c= s
; ProgramPart s halts_on s
dom (Start-At 0 ,SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A2:
IC SCM+FSA in dom (Start-At 0 ,SCM+FSA )
by TARSKI:def 1;
then A3:
IC SCM+FSA in dom (Initialized (Macro (halt SCM+FSA )))
by FUNCT_4:13;
A4: IC (Initialized (Macro (halt SCM+FSA ))) =
(Initialized (Macro (halt SCM+FSA ))) . (IC SCM+FSA )
.=
(Start-At 0 ,SCM+FSA ) . (IC SCM+FSA )
by A2, FUNCT_4:14
.=
0
by FUNCOP_1:87
;
take
0
; AMI_1:def 20 ( IC (Comput (ProgramPart s),s,0 ) in proj1 (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt SCM+FSA )
IC (Comput (ProgramPart s),s,0 ) in NAT
;
hence
IC (Comput (ProgramPart s),s,0 ) in dom (ProgramPart s)
by AMI_1:143; (ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt SCM+FSA
A5:
( (Macro (halt SCM+FSA )) . 0 = halt SCM+FSA & Macro (halt SCM+FSA ) c= Initialized (Macro (halt SCM+FSA )) )
by FUNCT_4:66, SCMFSA6A:26;
dom (Macro (halt SCM+FSA )) = {0 ,1}
by FUNCT_4:65;
then A6:
0 in dom (Macro (halt SCM+FSA ))
by TARSKI:def 2;
Initialized (Macro (halt SCM+FSA )) = (Macro (halt SCM+FSA )) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15;
then A7:
0 in dom (Initialized (Macro (halt SCM+FSA )))
by A6, FUNCT_4:13;
u:
Comput (ProgramPart s),s,0 = s
by AMI_1:13;
Y:
(ProgramPart s) /. (IC s) = s . (IC s)
by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s),s,0 )),(Comput (ProgramPart s),s,0 ) =
CurInstr (ProgramPart s),s
by u
.=
s . (IC (Initialized (Macro (halt SCM+FSA ))))
by A1, A3, GRFUNC_1:8, Y
.=
(Initialized (Macro (halt SCM+FSA ))) . 0
by A1, A7, A4, GRFUNC_1:8
.=
halt SCM+FSA
by A5, A6, GRFUNC_1:8
;
hence
(ProgramPart s) /. (IC (Comput (ProgramPart s),s,0 )) = halt SCM+FSA
by AMI_1:145; verum