set Ma = Macro (AddTo a,b);
let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not (Macro (AddTo a,b)) +* (Start-At (insloc 0 )) c= s or s is halting )
assume A8: (Macro (AddTo a,b)) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
A9: Macro (AddTo a,b) c= s by A8, SCMFSA6B:5;
take 1 ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,1) = halt SCM+FSA
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A10: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
Start-At (insloc 0 ) c= (Macro (AddTo a,b)) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then Start-At (insloc 0 ) c= s by A8, XBOOLE_1:1;
then A11: IC s = (Start-At (insloc 0 )) . (IC SCM+FSA ) by A10, GRFUNC_1:8
.= insloc 0 by FUNCOP_1:87 ;
then A12: IC (Exec (AddTo a,b),s) = Next (insloc 0 ) by SCMFSA_2:90
.= insloc (0 + 1) ;
insloc 1 in dom (Macro (AddTo a,b)) by SCMFSA6B:32;
then (Macro (AddTo a,b)) . (insloc 1) = s . (insloc 1) by A9, GRFUNC_1:8;
then A13: s . (insloc 1) = halt SCM+FSA by SCMFSA6B:33;
insloc 0 in dom (Macro (AddTo a,b)) by SCMFSA6B:32;
then A14: (Macro (AddTo a,b)) . (insloc 0 ) = s . (insloc 0 ) by A9, GRFUNC_1:8;
Computation s,(0 + 1) = Following (Computation s,0 ) by AMI_1:14
.= Following s by AMI_1:13
.= Exec (AddTo a,b),s by A11, A14, SCMFSA6B:33 ;
hence CurInstr (Computation s,1) = halt SCM+FSA by A13, A12, AMI_1:def 13; :: thesis: verum