let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N
for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N
for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S
let S be non empty stored-program halting IC-Ins-separated definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of NAT ,N; :: thesis: for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S
let I be Instruction of S; :: thesis: ( IncAddr I,k = halt S implies I = halt S )
assume IncAddr I,k = halt S ; :: thesis: I = halt S
then IncAddr I,k = IncAddr (halt S),k by Th29;
hence I = halt S by Th34; :: thesis: verum