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 sequential holds
LocNums (NIC J,L) = {(locnum (NextLoc 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 sequential holds
LocNums (NIC J,L) = {(locnum (NextLoc L))}
let L be Instruction-Location of S; :: thesis: for J being Instruction of S st S is realistic & J is sequential holds
LocNums (NIC J,L) = {(locnum (NextLoc L))}
let J be Instruction of S; :: thesis: ( S is realistic & J is sequential implies LocNums (NIC J,L) = {(locnum (NextLoc L))} )
assume ( S is realistic & J is sequential ) ; :: thesis: LocNums (NIC J,L) = {(locnum (NextLoc L))}
then NIC J,L = {(NextLoc L)} by AMISTD_1:41
.= {(il. S,(locnum (NextLoc L)))} by AMISTD_1:def 13 ;
hence LocNums (NIC J,L) = {(locnum (NextLoc L))} by Th26; :: thesis: verum