take Macro (halt SCM+FSA) ; :: thesis: ( Macro (halt SCM+FSA) is parahalting & Macro (halt SCM+FSA) is keeping_0 )
thus Macro (halt SCM+FSA) is parahalting :: thesis: Macro (halt SCM+FSA) is keeping_0

proof

let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11 :: thesis: for b₁ being set holds
( not Macro (halt SCM+FSA) c= b₁ or b₁ halts_on s )
set m = Macro (halt SCM+FSA);
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro (halt SCM+FSA) c= P or P halts_on s )
assume A2: Macro (halt SCM+FSA) c= P ; :: thesis: P halts_on s
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
take 0 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,0)) in proj1 P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A11: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A13: Comput (P,s,0) = s by EXTPRO_1:2;
dom P = NAT by PARTFUN1:def 2;
hence IC (Comput (P,s,0)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
dom P = NAT by PARTFUN1:def 2;
then CurInstr (P,(Comput (P,s,0))) = P . (IC s) by A13, PARTFUN1:def 6
.= P . (IC (Start-At (0,SCM+FSA))) by A1, A4, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Macro (halt SCM+FSA)) . 0 by A2, A11, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum

end;

set Mi = Macro (halt SCM+FSA);
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A1: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: for P being Instruction-Sequence of SCM+FSA st Macro (halt SCM+FSA) c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A2: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Macro (halt SCM+FSA) c= P implies for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A3: Macro (halt SCM+FSA) c= P ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A4: s = Comput (P,s,0) by EXTPRO_1:2;
dom P = NAT by PARTFUN1:def 2;
then A5: P /. (IC s) = P . (IC s) by PARTFUN1:def 6;
CurInstr (P,s) = P . 0 by A2, A5, MEMSTR_0:39
.= (Macro (halt SCM+FSA)) . 0 by A1, A3, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A4, EXTPRO_1:5; :: thesis: verum