let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of N
for I being Instruction of S st IncAddr I,k = halt S holds
I = halt S
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting steady-programmed standard homogeneous without_implicit_jumps regular J/A-independent AMI-Struct of 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