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