let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,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 (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 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,0)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(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 COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(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 EXTPRO_1:3;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = CurInstr ((ProgramPart s),s) by u
.= s . (IC (Initialized (Macro (halt SCM+FSA)))) by A1, A3, Y, GRFUNC_1:8
.= (Initialized (Macro (halt SCM+FSA))) . 0 by A1, A7, A4, GRFUNC_1:8
.= halt SCM+FSA by A5, A6, GRFUNC_1:8 ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt SCM+FSA ; :: thesis: verum