set Ma = Macro (b := f,a);
let s be State of SCM+FSA ; AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 ( not (Macro (b := f,a)) +* (Start-At 0 ,SCM+FSA ) c= s or ProgramPart s halts_on s )
assume A36:
(Macro (b := f,a)) +* (Start-At 0 ,SCM+FSA ) c= s
; ProgramPart s halts_on s
A37:
Macro (b := f,a) c= s
by A36, SCMFSA6B:5;
take
1
; AMI_1:def 20 ( IC (Comput (ProgramPart s),s,1) in proj1 (ProgramPart s) & CurInstr (ProgramPart s),(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 COMPOS_1:34; CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCM+FSA
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 COMPOS_1:38;
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 COMPOS_1:38;
NX:
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,1)
by AMI_1:123;
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, Y, SCMFSA6B:33
;
then
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCM+FSA
by A41, A40, Z, NX, AMI_1:def 13;
hence
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCM+FSA
; verum