let N be non empty with_non-empty_elements set ; :: thesis: for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for I being Instruction of S st IncAddr (I,k) = halt S holds
I = halt S
let k be natural number ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-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 standard-ins homogeneous regular J/A-independent proper-halt COM-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 Th92;
hence I = halt S by Th95; :: thesis: verum