let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3 :: thesis: ( not Initialize (Macro (halt SCM+FSA)) c= s or for b₁ being set holds
( not ProgramPart (Initialize (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: Initialize (Macro (halt SCM+FSA)) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (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 ProgramPart (Initialize (Macro (halt SCM+FSA))) c= P or P halts_on s )
assume A2: ProgramPart (Initialize (Macro (halt SCM+FSA))) c= P ; :: thesis: P halts_on s
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
then A4: IC in dom (Initialize (Macro (halt SCM+FSA))) by FUNCT_4:13;
A5: IC (Initialize (Macro (halt SCM+FSA))) = (Start-At (0,SCM+FSA)) . (IC ) by A3, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
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, COMPOS_1:144;
CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s) by EXTPRO_1:3
.= P . (IC s) by A6, PARTFUN1:def 8
.= P . (IC (Initialize (Macro (halt SCM+FSA)))) by A1, A4, GRFUNC_1:8
.= (Macro (halt SCM+FSA)) . 0 by A5, GRFUNC_1:8, A8, A7
.= halt SCM+FSA by FUNCT_4:66 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum