let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for P being Instruction-Sequence of SCM+FSA st Macro (halt SCM+FSA) c= P holds
P halts_on s )
set m = Macro (halt SCM+FSA);
set m1 = Macro (halt SCM+FSA);
assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for P being Instruction-Sequence of SCM+FSA st Macro (halt SCM+FSA) c= P holds
P halts_on s
let p be Instruction-Sequence of SCM+FSA; :: 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 MEMSTR_0:48;
take 0 ; :: according to EXTPRO_1:def 8 :: 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 2; :: thesis: CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA
A8: (Macro (halt SCM+FSA)) . 0 = halt SCM+FSA by COMPOS_1:58;
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A9: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A10: p /. (IC s) = p . (IC s) by PBOOLE:143;
CurInstr (p,(Comput (p,s,0))) = CurInstr (p,s) by EXTPRO_1:2
.= p . 0 by ICiS, A1, A10, B6, GRFUNC_1:2
.= halt SCM+FSA by A8, A2, A9, GRFUNC_1:2 ;
hence CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA ; :: thesis: verum