set Ma = Macro (SubFrom (a,b));
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11,SCMFSA6C:def 1 :: thesis: for b₁ being set holds
( not Macro (SubFrom (a,b)) c= b₁ or b₁ halts_on s )
A23: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro (SubFrom (a,b)) c= P or P halts_on s )
assume A24: Macro (SubFrom (a,b)) c= P ; :: thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A26: dom P = NAT by PARTFUN1:def 2;
thus IC (Comput (P,s,1)) in dom P by A26; :: thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A27: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A28: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A27, A23, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A29: IC (Exec ((SubFrom (a,b)),s)) = succ 0 by SCMFSA_2:65
.= 0 + 1 ;
A30: 1 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
A31: 0 in dom (Macro (SubFrom (a,b))) by COMPOS_1:60;
A32: P . 0 = (Macro (SubFrom (a,b))) . 0 by A24, A31, GRFUNC_1:2
.= SubFrom (a,b) by COMPOS_1:58 ;
A33: P . 1 = (Macro (SubFrom (a,b))) . 1 by A24, A30, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec ((SubFrom (a,b)),s) by A28, A26, A32, PARTFUN1:def 6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A29, A26, A33, PARTFUN1:def 6; :: thesis: verum