let s be State of ; :: according to AMI_1:def 26,SCM_HALT:def 2 :: thesis: ( 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 ; :: thesis: ProgramPart s halts_on s
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A2: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
then A3: IC SCM+FSA in dom (Initialized (Macro (halt SCM+FSA ))) by FUNCT_4:13;
then A4: IC (Initialized (Macro (halt SCM+FSA ))) = (Initialized (Macro (halt SCM+FSA ))) . (IC SCM+FSA ) by AMI_1:def 43
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
take 0 ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,0 ) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA )
IC (Computation s,0 ) in NAT by AMI_1:def 4;
hence IC (Computation s,0 ) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA
A5: ( (Macro (halt SCM+FSA )) . (insloc 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 )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;
then A6: insloc 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 (insloc 0 ))) by FUNCT_4:15;
then A7: insloc 0 in dom (Initialized (Macro (halt SCM+FSA ))) by A6, FUNCT_4:13;
CurInstr (Computation s,0 ) = CurInstr s by AMI_1:13
.= s . (IC (Initialized (Macro (halt SCM+FSA )))) by A1, A3, AMI_1:97
.= (Initialized (Macro (halt SCM+FSA ))) . (insloc 0 ) by A1, A7, A4, GRFUNC_1:8
.= halt SCM+FSA by A5, A6, GRFUNC_1:8 ;
hence (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA by AMI_1:145; :: thesis: verum