consider k being Element of NAT such that
IC (Comput (ProgramPart s),s,k) in dom (ProgramPart s) and
W: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = halt S by A1, Def20;
(ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by LmX;
hence ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput (ProgramPart s),s,k & CurInstr (ProgramPart b₁),b₁ = halt S ) by W; :: thesis: verum