let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: thesis: ( Initialize ((intloc 0) .--> 1) 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 = Initialized (Macro (halt SCM+FSA));
assume A1: Initialize ((intloc 0) .--> 1) 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
B6: IC in dom (Initialize ((intloc 0) .--> 1)) by COMPOS_1:225;
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 )
IC (Comput (p,s,0)) in NAT ;
hence IC (Comput (p,s,0)) in dom p by PARTFUN1:def 4; :: thesis: CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA
A8: ( (Macro (halt SCM+FSA)) . 0 = halt SCM+FSA & Macro (halt SCM+FSA) c= Initialized (Macro (halt SCM+FSA)) ) by FUNCT_4:66, SCMFSA6A:26;
dom (Macro (halt SCM+FSA)) = {0,1} by FUNCT_4:65;
then A9: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A10: p /. (IC s) = p . (IC s) by PBOOLE:158;
CurInstr (p,(Comput (p,s,0))) = CurInstr (p,s) by EXTPRO_1:3
.= p . 0 by ICiS, A1, A10, B6, GRFUNC_1:8
.= halt SCM+FSA by A8, A2, A9, GRFUNC_1:8 ;
hence CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA ; :: thesis: verum