let s be State of SCM+FSA; :: according to SCMFSA6B:def 3 :: thesis: ( Start-At (0,SCM+FSA) c= s implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Macro (halt SCM+FSA) c= P holds
P 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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Macro (halt SCM+FSA) c= P holds
P halts_on s
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( Macro (halt SCM+FSA) c= P implies P halts_on s )
assume A2: Macro (halt SCM+FSA) c= P ; :: thesis: P halts_on s
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
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 )
dom (Macro (halt SCM+FSA)) = {0,1} by FUNCT_4:65;
then A11: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A13: Comput (P,s,0) = s by EXTPRO_1:3;
dom P = NAT by PARTFUN1:def 4;
hence IC (Comput (P,s,0)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
dom P = NAT by PARTFUN1:def 4;
then CurInstr (P,(Comput (P,s,0))) = P . (IC s) by A13, PARTFUN1:def 8
.= P . (IC (Start-At (0,SCM+FSA))) by A1, A4, GRFUNC_1:8
.= P . 0 by COMPOS_1:64
.= (Macro (halt SCM+FSA)) . 0 by A2, A11, GRFUNC_1:8
.= halt SCM+FSA by FUNCT_4:66 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum