set Ma = Macro (SubFrom a,b);
let s be State of SCM+FSA ; AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 ( not (Macro (SubFrom a,b)) +* (Start-At 0 ,SCM+FSA ) c= s or ProgramPart s halts_on s )
assume A15:
(Macro (SubFrom a,b)) +* (Start-At 0 ,SCM+FSA ) c= s
; ProgramPart s halts_on s
A16:
Macro (SubFrom a,b) c= s
by A15, 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 A17:
IC SCM+FSA in dom (Start-At 0 ,SCM+FSA )
by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (SubFrom a,b)) +* (Start-At 0 ,SCM+FSA )
by FUNCT_4:26;
then
Start-At 0 ,SCM+FSA c= s
by A15, XBOOLE_1:1;
then A18: IC s =
(Start-At 0 ,SCM+FSA ) . (IC SCM+FSA )
by A17, GRFUNC_1:8
.=
0
by FUNCOP_1:87
;
then A19: IC (Exec (SubFrom a,b),s) =
succ 0
by SCMFSA_2:91
.=
0 + 1
;
1 in dom (Macro (SubFrom a,b))
by SCMFSA6B:32;
then
(Macro (SubFrom a,b)) . 1 = s . 1
by A16, GRFUNC_1:8;
then A20:
s . 1 = halt SCM+FSA
by SCMFSA6B:33;
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;
0 in dom (Macro (SubFrom a,b))
by SCMFSA6B:32;
then A21:
(Macro (SubFrom a,b)) . 0 = s . 0
by A16, GRFUNC_1:8;
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 (SubFrom a,b),s
by A18, A21, SCMFSA6B:33, Y
;
then
CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = halt SCM+FSA
by A20, A19, AMI_1:def 13, Z;
hence
(ProgramPart s) /. (IC (Comput (ProgramPart s),s,1)) = halt SCM+FSA
by AMI_1:145; verum