let k be natural number ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct
for I being Instruction of S st IncAddr (I,k) = halt S holds
I = halt S
let S be standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ; :: 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