set m = Macro (halt SCM+FSA );
set m1 = Initialized (Macro (halt SCM+FSA ));
let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCM_HALT:def 2 :: thesis: ( not Initialized (Macro (halt SCM+FSA )) c= s or s is halting )
assume A1: Initialized (Macro (halt SCM+FSA )) c= s ; :: thesis: s is halting
A3: Initialized (Macro (halt SCM+FSA )) = (Macro (halt SCM+FSA )) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A4: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
then A5: IC SCM+FSA in dom (Initialized (Macro (halt SCM+FSA ))) by FUNCT_4:13;
A7: (Macro (halt SCM+FSA )) . (insloc 0 ) = halt SCM+FSA by FUNCT_4:66;
A8: Macro (halt SCM+FSA ) c= Initialized (Macro (halt SCM+FSA )) by SCMFSA6A:26;
dom (Macro (halt SCM+FSA )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;
then A9: insloc 0 in dom (Macro (halt SCM+FSA )) by TARSKI:def 2;
then A10: insloc 0 in dom (Initialized (Macro (halt SCM+FSA ))) by A3, FUNCT_4:13;
A11: IC (Initialized (Macro (halt SCM+FSA ))) = (Initialized (Macro (halt SCM+FSA ))) . (IC SCM+FSA ) by A5, AMI_1:def 43
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
take 0 ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,0 ) = halt SCM+FSA
thus CurInstr (Computation s,0 ) = CurInstr s by AMI_1:13
.= s . (IC (Initialized (Macro (halt SCM+FSA )))) by A1, A5, AMI_1:97
.= (Initialized (Macro (halt SCM+FSA ))) . (insloc 0 ) by A1, A10, A11, GRFUNC_1:8
.= halt SCM+FSA by A7, A8, A9, GRFUNC_1:8 ; :: thesis: verum