defpred S₁[ Nat] means CurInstr (ProgramPart (Comput (ProgramPart s),s,$1)),(Comput (ProgramPart s),s,$1) = halt S;
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;
then A2: ex k being Nat st S₁[k] by W;
consider k being Nat such that
A3: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A2);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
take k ; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
k <= k ) )
thus ( CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
k <= k ) ) by A3; :: thesis: verum