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 F being NAT -defined lower FinPartState of S
for f being Instruction-Location of S st f in dom F holds
locnum f < card F
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being NAT -defined lower FinPartState of S
for f being Instruction-Location of S st f in dom F holds
locnum f < card F
let F be NAT -defined lower FinPartState of S; :: thesis: for f being Instruction-Location of S st f in dom F holds
locnum f < card F
let f be Instruction-Location of S; :: thesis: ( f in dom F implies locnum f < card F )
assume A1: f in dom F ; :: thesis: locnum f < card F
f = il. S,(locnum f) by AMISTD_1:def 13;
hence locnum f < card F by A1, AMISTD_1:50; :: thesis: verum