let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting 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 IC-Ins-separated halting 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
A1: IC (Comput (p,s,n)) in dom p and
A2: CurInstr (p,(Comput (p,s,n))) = halt S by Def7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;

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 A2, Th6
.= Comput (p,(Comput (p,s,m)),0) by Th5 ;
hence p halts_on Comput (p,s,m) by Def7, A2, A1; :: 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:5;
Comput (p,(Comput (p,s,m)),k) = Comput (p,s,(m + k)) by Th5
.= Comput (p,s,n) ;
hence p halts_on Comput (p,s,m) by Def7, A1, A2; :: thesis: verum

end;

end;

end;

given n being Nat such that A3: IC (Comput (p,(Comput (p,s,m)),n)) in dom p and
A4: CurInstr (p,(Comput (p,(Comput (p,s,m)),n))) = halt S ; :: according to EXTPRO_1:def 8 :: thesis: p halts_on s
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
take m + nn ; :: according to EXTPRO_1:def 8 :: 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 A3, A4, Th5; :: thesis: verum