let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for L being Instruction-Location of S
for J being Instruction of S st S is realistic & J is halting holds
LocNums (NIC J,L) = {(locnum L)}
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for L being Instruction-Location of S
for J being Instruction of S st S is realistic & J is halting holds
LocNums (NIC J,L) = {(locnum L)}
let L be Instruction-Location of S; :: thesis: for J being Instruction of S st S is realistic & J is halting holds
LocNums (NIC J,L) = {(locnum L)}
let J be Instruction of S; :: thesis: ( S is realistic & J is halting implies LocNums (NIC J,L) = {(locnum L)} )
assume ( S is realistic & J is halting ) ; :: thesis: LocNums (NIC J,L) = {(locnum L)}
then NIC J,L = {L} by AMISTD_1:15
.= {(il. S,(locnum L))} by AMISTD_1:def 13 ;
hence LocNums (NIC J,L) = {(locnum L)} by Th26; :: thesis: verum