let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput p,s,m )
let S be non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput p,s,m )
let p be NAT -defined the Instructions of S -valued Function; :: thesis: for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput p,s,m )
let s be State of S; :: thesis: for m being Element of NAT holds
( p halts_on s iff p halts_on Comput p,s,m )
let m be Element of NAT ; :: thesis: ( p halts_on s iff p halts_on Comput p,s,m )

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

assume p halts_on s ; :: thesis: p halts_on Comput p,s,m
then consider n being Nat such that
W0: IC (Comput p,s,n) in dom p and
W: CurInstr p,(Comput p,s,n) = halt S by Def20;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A1: CurInstr p,(Comput p,s,n) = halt S by W;

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

suppose n <= m ; :: thesis: p halts_on Comput p,s,m

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

end;

suppose n >= m ; :: thesis: p halts_on Comput p,s,m

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

end;

end;

end;

given n being Nat such that W1: IC (Comput p,(Comput p,s,m),n) in dom p and
W2: CurInstr p,(Comput p,(Comput p,s,m),n) = halt S ; :: according to AMI_1:def 20 :: thesis: p halts_on s
reconsider nn = n as Element of NAT by ORDINAL1:def 13;
take m + nn ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput p,s,(m + nn)) in dom p & CurInstr p,(Comput p,s,(m + nn)) = halt S )
thus ( IC (Comput p,s,(m + nn)) in dom p & CurInstr p,(Comput p,s,(m + nn)) = halt S ) by W1, W2, Th51; :: thesis: verum