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);
set m1 = 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
B4: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
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 )
A6: dom P = NAT by PARTFUN1:def 2;
thus IC (Comput (P,s,0)) in dom P by A6; :: thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A7: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s) by EXTPRO_1:2
.= P . (IC s) by A6, PARTFUN1:def 6
.= P . (IC (Start-At (0,SCM+FSA))) by A1, B4, GRFUNC_1:2
.= P . 0 by FUNCOP_1:72
.= (Macro (halt SCM+FSA)) . 0 by A2, A7, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:58 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum