let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for m being Element of NAT holds
( ProgramPart s halts_on s iff ProgramPart s halts_on Comput (ProgramPart s),s,m )
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for s being State of S
for m being Element of NAT holds
( ProgramPart s halts_on s iff ProgramPart s halts_on Comput (ProgramPart s),s,m )
let s be State of S; :: thesis: for m being Element of NAT holds
( ProgramPart s halts_on s iff ProgramPart s halts_on Comput (ProgramPart s),s,m )
let m be Element of NAT ; :: thesis: ( ProgramPart s halts_on s iff ProgramPart s halts_on Comput (ProgramPart s),s,m )
Y: ProgramPart (Comput (ProgramPart s),s,m) = ProgramPart s by LmY;

hereby :: thesis: ( ProgramPart s halts_on Comput (ProgramPart s),s,m implies ProgramPart s halts_on s )

assume ProgramPart s halts_on s ; :: thesis: ProgramPart s halts_on Comput (ProgramPart s),s,m
then consider n being Element of NAT such that
W0: IC (Comput (ProgramPart s),s,n) in dom (ProgramPart s) and
W: (ProgramPart s) /. (IC (Comput (ProgramPart s),s,n)) = halt S by Def20;
X: ProgramPart (Comput (ProgramPart s),s,n) = ProgramPart s by LmY;
A1: CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = halt S by W, LmX;

per cases ( n <= m or n >= m ) ;

suppose n <= m ; :: thesis: ProgramPart s halts_on Comput (ProgramPart s),s,m

then Comput (ProgramPart s),s,n = Comput (ProgramPart s),s,(m + 0 ) by A1, Th52, X
.= Comput (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m),0 by Th51, Y ;
hence ProgramPart s halts_on Comput (ProgramPart s),s,m by Def20, W, W0; :: thesis: verum

end;

suppose n >= m ; :: thesis: ProgramPart s halts_on Comput (ProgramPart s),s,m

then reconsider k = n - m as Element of NAT by INT_1:18;
ProgramPart (Comput (ProgramPart s),s,m) = ProgramPart s by LmY;
then Comput (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m),k = Comput (ProgramPart s),s,(m + k) by Th51
.= Comput (ProgramPart s),s,n ;
hence ProgramPart s halts_on Comput (ProgramPart s),s,m by Def20, W0, W; :: thesis: verum

end;

end;

end;

given n being Element of NAT such that W1: IC (Comput (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m),n) in dom (ProgramPart s) and
W2: (ProgramPart s) /. (IC (Comput (ProgramPart (Comput (ProgramPart s),s,m)),(Comput (ProgramPart s),s,m),n)) = halt S ; :: according to AMI_1:def 20 :: thesis: ProgramPart s halts_on s
take m + n ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,(m + n)) in dom (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(m + n))) = halt S )
thus ( IC (Comput (ProgramPart s),s,(m + n)) in dom (ProgramPart s) & (ProgramPart s) /. (IC (Comput (ProgramPart s),s,(m + n))) = halt S ) by W1, W2, Th51, Y; :: thesis: verum