set m = Stop SCM+FSA;
A1:
0 in dom (Stop SCM+FSA)
by COMPOS_1:3;
thus
Stop SCM+FSA is parahalting
Stop SCM+FSA is keeping_0 proof
let s be
0 -started State of
SCM+FSA;
AMISTD_1:def 10 for b1 being set holds
( not Stop SCM+FSA c= b1 or b1 halts_on s )
A2:
Start-At (
0,
SCM+FSA)
c= s
by MEMSTR_0:29;
let P be
Instruction-Sequence of
SCM+FSA;
( not Stop SCM+FSA c= P or P halts_on s )
assume A3:
Stop SCM+FSA c= P
;
P halts_on s
A4:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
take
0
;
EXTPRO_1:def 8 ( IC (Comput (P,s,0)) in dom P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
A5:
dom P = NAT
by PARTFUN1:def 2;
hence
IC (Comput (P,s,0)) in dom P
;
CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
CurInstr (
P,
(Comput (P,s,0))) =
P . (IC s)
by A5, PARTFUN1:def 6
.=
P . (IC (Start-At (0,SCM+FSA)))
by A2, A4, GRFUNC_1:2
.=
P . 0
by FUNCOP_1:72
.=
(Stop SCM+FSA) . 0
by A3, A1, GRFUNC_1:2
.=
halt SCM+FSA
;
hence
CurInstr (
P,
(Comput (P,s,0)))
= halt SCM+FSA
;
verum
end;
let s be 0 -started State of SCM+FSA; SCMFSA6B:def 4 for P being Instruction-Sequence of SCM+FSA st Stop SCM+FSA c= P holds
for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A6:
Start-At (0,SCM+FSA) c= s
by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; ( Stop SCM+FSA c= P implies for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A7:
Stop SCM+FSA c= P
; for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Nat; (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A8:
s = Comput (P,s,0)
;
dom P = NAT
by PARTFUN1:def 2;
then A9:
P /. (IC s) = P . (IC s)
by PARTFUN1:def 6;
CurInstr (P,s) =
P . 0
by A6, A9, MEMSTR_0:39
.=
(Stop SCM+FSA) . 0
by A1, A7, GRFUNC_1:2
.=
halt SCM+FSA
;
hence
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
by A8, EXTPRO_1:5; verum