let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of T
for l being Instruction-Location of T st l in dom F holds
l <= LastLoc F
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being non empty programmed FinPartState of T
for l being Instruction-Location of T st l in dom F holds
l <= LastLoc F
let F be non empty programmed FinPartState of T; :: thesis: for l being Instruction-Location of T st l in dom F holds
l <= LastLoc F
let l be Instruction-Location of T; :: thesis: ( l in dom F implies l <= LastLoc F )
assume A1: l in dom F ; :: thesis: l <= LastLoc F
consider M being non empty finite natural-membered set such that
A2: M = { (locnum w) where w is Instruction-Location of T : w in dom F } and
A3: LastLoc F = il. T,(max M) by Def21;
A4: locnum (LastLoc F) = max M by A3, Def13;
locnum l in M by A1, A2;
then locnum l <= max M by XXREAL_2:def 8;
hence l <= LastLoc F by A4, Th29; :: thesis: verum