let s be State of SCM+FSA; :: according to SCMFSA6B:def 3 :: thesis: ( not Start-At (0,SCM+FSA) c= s or 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 = Initialize (Macro (halt SCM+FSA));
assume A1: Start-At (0,SCM+FSA) c= s ; :: thesis: for b₁ being set holds
( not Macro (halt SCM+FSA) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 COMPOS_1:52;
take 0 ; :: according to EXTPRO_1:def 7 :: 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 4;
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 FUNCT_4:65;
then A7: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A8: Macro (halt SCM+FSA) c= P by A2;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s) by EXTPRO_1:3
.= P . (IC s) by A6, PARTFUN1:def 8
.= P . (IC (Start-At (0,SCM+FSA))) by A1, GRFUNC_1:8, B4
.= P . 0 by COMPOS_1:64
.= (Macro (halt SCM+FSA)) . 0 by GRFUNC_1:8, A8, A7
.= halt SCM+FSA by FUNCT_4:66 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum