set Ma = Macro (MultBy a,b);
let s be State of SCM+FSA ; AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 ( not (Macro (MultBy a,b)) +* (Start-At 0 ,SCM+FSA ) c= s or ProgramPart s halts_on s )
assume A22:
(Macro (MultBy a,b)) +* (Start-At 0 ,SCM+FSA ) c= s
; ProgramPart s halts_on s
A23:
Macro (MultBy a,b) c= s
by A22, SCMFSA6B:5;
take
1
; AMI_1:def 20 ( IC (Comput (ProgramPart s),s,1) in proj1 (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,1)) = halt SCM+FSA )
IC (Comput (ProgramPart s),s,1) in NAT
;
hence
IC (Comput (ProgramPart s),s,1) in dom (ProgramPart s)
by AMI_1:143; (ProgramPart s) /. (IC (Comput (ProgramPart s),s,1)) = halt SCM+FSA
dom (Start-At 0 ,SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A24:
IC SCM+FSA in dom (Start-At 0 ,SCM+FSA )
by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (MultBy a,b)) +* (Start-At 0 ,SCM+FSA )
by FUNCT_4:26;
then
Start-At 0 ,SCM+FSA c= s
by A22, XBOOLE_1:1;
then A25: IC s =
(Start-At 0 ,SCM+FSA ) . (IC SCM+FSA )
by A24, GRFUNC_1:8
.=
0
by FUNCOP_1:87
;
then A26: IC (Exec (MultBy a,b),s) =
succ 0
by SCMFSA_2:92
.=
0 + 1
;
1 in dom (Macro (MultBy a,b))
by SCMFSA6B:32;
then
(Macro (MultBy a,b)) . 1 = s . 1
by A23, GRFUNC_1:8;
then A27:
s . 1 = halt SCM+FSA
by SCMFSA6B:33;
0 in dom (Macro (MultBy a,b))
by SCMFSA6B:32;
then A28:
(Macro (MultBy a,b)) . 0 = s . 0
by A23, 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 (MultBy a,b),s
by A25, A28, SCMFSA6B:33, Y
;
then
CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = halt SCM+FSA
by A27, A26, AMI_1:def 13, Z;
hence
(ProgramPart s) /. (IC (Comput (ProgramPart s),s,1)) = halt SCM+FSA
by AMI_1:145; verum