set Ma = Macro (b := f,a);
let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis:
assume A36: (Macro (b := f,a)) +* (Start-At 0 ,SCM+FSA ) c= s ; :: thesis:
A37: Macro (b := f,a) c= s by A36, SCMFSA6B:5;
take 1 ; :: according to AMI_1:def 20 :: thesis:
IC (Comput (ProgramPart s),s,1) in NAT ;
hence IC (Comput (ProgramPart s),s,1) in dom (ProgramPart s) by AMI_1:143; :: thesis:
dom (Start-At 0 ,SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A38: IC SCM+FSA in dom (Start-At 0 ,SCM+FSA ) by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (b := f,a)) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:26;
then Start-At 0 ,SCM+FSA c= s by A36, XBOOLE_1:1;
then A39: IC s = (Start-At 0 ,SCM+FSA ) . (IC SCM+FSA ) by A38, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
then A40: IC (Exec (b := f,a),s) = succ 0 by SCMFSA_2:98
.= 0 + 1 ;
1 in dom (Macro (b := f,a)) by SCMFSA6B:32;
then (Macro (b := f,a)) . 1 = s . 1 by A37, GRFUNC_1:8;
then A41: s . 1 = halt SCM+FSA by SCMFSA6B:33;
0 in dom (Macro (b := f,a)) by SCMFSA6B:32;
then A42: (Macro (b := f,a)) . 0 = s . 0 by A37, GRFUNC_1:8;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by AMI_1:150;
Z: (ProgramPart (Comput (ProgramPart s),s,1)) /. (IC (Comput (ProgramPart s),s,1)) = (Comput (ProgramPart s),s,1) . (IC (Comput (ProgramPart s),s,1)) by AMI_1:150;
Comput (ProgramPart s),s,(0 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,0 ) by AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= Exec (b := f,a),s by A39, A42, SCMFSA6B:33, Y ;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = halt SCM+FSA by A41, A40, AMI_1:def 13, Z;
hence (ProgramPart s) /. (IC (Comput (ProgramPart s),s,1)) = halt SCM+FSA by AMI_1:145; :: thesis: