let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 10 :: thesis: for b₁ being set holds
( not Macro i c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro i c= P or P halts_on s )
assume A1: Macro i c= P ; :: thesis: P halts_on s
dom P = NAT by PARTFUN1:def 2;
then A2: 0 in dom P ;
A3: ( 0 in dom (Macro i) & 1 in dom (Macro i) ) by COMPOS_1:57;
A4: IC s = 0 by MEMSTR_0:def 11;
A5: P . 0 = (Macro i) . 0 by A1, GRFUNC_1:2, A3
.= i by COMPOS_1:58 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Exec (i,s) by A5, A2, A4, PARTFUN1:def 6 ;
then A6: IC (Comput (P,s,1)) = 0 + 1 by AMISTD_1:def 8, A4;
then (Macro i) . (IC (Comput (P,s,1))) = halt SCM+FSA by COMPOS_1:59;
then P . (IC (Comput (P,s,1))) = halt SCM+FSA by A3, A1, GRFUNC_1:2, A6;
hence P halts_on s by EXTPRO_1:30; :: thesis: verum