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