let N be non empty with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued Function
for s being State of S
for m being Nat holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; for p being NAT -defined the InstructionsF of S -valued Function
for s being State of S
for m being Nat holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let p be NAT -defined the InstructionsF of S -valued Function; for s being State of S
for m being Nat holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let s be State of S; for m being Nat holds
( p halts_on s iff p halts_on Comput (p,s,m) )
let m be Nat; ( p halts_on s iff p halts_on Comput (p,s,m) )
hereby ( p halts_on Comput (p,s,m) implies p halts_on s )
assume
p halts_on s
;
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
;
reconsider n =
n as
Nat ;
per cases
( n <= m or n >= m )
;
suppose
n <= m
;
p halts_on Comput (p,s,m)then Comput (
p,
s,
n) =
Comput (
p,
s,
(m + 0))
by A2, Th5
.=
Comput (
p,
(Comput (p,s,m)),
0)
;
hence
p halts_on Comput (
p,
s,
m)
by A2, A1;
verum end; suppose
n >= m
;
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 Th4
.=
Comput (
p,
s,
n)
;
hence
p halts_on Comput (
p,
s,
m)
by A1, A2;
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
; EXTPRO_1:def 8 p halts_on s
reconsider nn = n as Nat ;
take
m + nn
; EXTPRO_1:def 8 ( 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, Th4; verum