let s be State of SCM+FSA; EXTPRO_1:def 10,SCM_HALT:def 2 ( not Initialized (Macro (halt SCM+FSA)) c= s or for b1 being set holds
( not ProgramPart (Initialized (Macro (halt SCM+FSA))) c= b1 or b1 halts_on s ) )
set m = Macro (halt SCM+FSA);
set m1 = Initialized (Macro (halt SCM+FSA));
assume A1:
Initialized (Macro (halt SCM+FSA)) c= s
; for b1 being set holds
( not ProgramPart (Initialized (Macro (halt SCM+FSA))) c= b1 or b1 halts_on s )
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; ( not ProgramPart (Initialized (Macro (halt SCM+FSA))) c= p or p halts_on s )
assume A2:
ProgramPart (Initialized (Macro (halt SCM+FSA))) c= p
; p halts_on s
A3:
ProgramPart (Initialized (Macro (halt SCM+FSA))) = Macro (halt SCM+FSA)
by SCMFSA6A:33;
A4:
Initialized (Macro (halt SCM+FSA)) = Initialize ((Macro (halt SCM+FSA)) +* ((intloc 0) .--> 1))
by FUNCT_4:15;
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
then A5:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
then A6:
IC in dom (Initialized (Macro (halt SCM+FSA)))
by FUNCT_4:13, A4;
A7: IC (Initialized (Macro (halt SCM+FSA))) =
(Start-At (0,SCM+FSA)) . (IC )
by A5, FUNCT_4:14, A4
.=
0
by FUNCOP_1:87
;
take
0
; EXTPRO_1:def 7 ( IC (Comput (p,s,0)) in proj1 p & CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA )
IC (Comput (p,s,0)) in NAT
;
hence
IC (Comput (p,s,0)) in dom p
by PARTFUN1:def 4; CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA
A8:
( (Macro (halt SCM+FSA)) . 0 = halt SCM+FSA & Macro (halt SCM+FSA) c= Initialized (Macro (halt SCM+FSA)) )
by FUNCT_4:66, SCMFSA6A:26;
dom (Macro (halt SCM+FSA)) = {0,1}
by FUNCT_4:65;
then A9:
0 in dom (Macro (halt SCM+FSA))
by TARSKI:def 2;
A10:
p /. (IC s) = p . (IC s)
by PBOOLE:158;
CurInstr (p,(Comput (p,s,0))) =
CurInstr (p,s)
by EXTPRO_1:3
.=
p . (IC (Initialized (Macro (halt SCM+FSA))))
by A1, A6, A10, GRFUNC_1:8
.=
(Macro (halt SCM+FSA)) . 0
by A7, GRFUNC_1:8, A2, A3, A9
.=
halt SCM+FSA
by A8
;
hence
CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA
; verum