let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₁ -valued non empty finite Function
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for F being NAT -defined the InstructionsF of T -valued non empty finite Function
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let F be NAT -defined the InstructionsF of T -valued non empty finite Function; :: thesis: for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let l be Element of NAT ; :: thesis: ( l in dom F implies l <= LastLoc F,T )
assume A1: l in dom F ; :: thesis: l <= LastLoc F,T
consider M being non empty finite natural-membered set such that
A2: M = { (locnum (w,T)) where w is Element of NAT : w in dom F } and
A3: LastLoc F = il. (T,(max M)) by Def11;
locnum (l,T) in M by A1, A2;
then A4: locnum (l,T) <= max M by XXREAL_2:def 8;
max M is Nat by TARSKI:1;
then locnum ((LastLoc F),T) = max M by A3, Def5;
hence l <= LastLoc F,T by A4, Th9; :: thesis: verum