let s be State of SCM+FSA; :: according to SCM_HALT:def 1 :: 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
A3: 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 dom 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
A4: (Macro (halt SCM+FSA)) . 0 = halt SCM+FSA by COMPOS_1:58;
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:61;
then A5: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
A6: p /. (IC s) = p . (IC s) by PBOOLE:143;
CurInstr (p,(Comput (p,s,0))) = CurInstr (p,s)
.= p . 0 by Lm1, A1, A6, A3, GRFUNC_1:2
.= halt SCM+FSA by A4, A2, A5, GRFUNC_1:2 ;
hence CurInstr (p,(Comput (p,s,0))) = halt SCM+FSA ; :: thesis: verum