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 l1 being Instruction-Location of S
for F being non empty programmed FinPartState of S st l1 in dom F holds
FirstLoc F <= l1
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l1 being Instruction-Location of S
for F being non empty programmed FinPartState of S st l1 in dom F holds
FirstLoc F <= l1
let l1 be Instruction-Location of S; :: thesis: for F being non empty programmed FinPartState of S st l1 in dom F holds
FirstLoc F <= l1
let F be non empty programmed FinPartState of S; :: thesis: ( l1 in dom F implies FirstLoc F <= l1 )
assume A1: l1 in dom F ; :: thesis: FirstLoc F <= l1
consider M being non empty Subset of NAT such that
A2: M = { (locnum w) where w is Instruction-Location of S : w in dom F } and
A3: FirstLoc F = il. S,(min M) by Def2;
A4: locnum (FirstLoc F) = min M by A3, AMISTD_1:def 13;
locnum l1 in M by A1, A2;
then min M <= locnum l1 by XXREAL_2:def 7;
hence FirstLoc F <= l1 by A4, AMISTD_1:29; :: thesis: verum