let N be with_zero set ; for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for F, G being NAT -defined the InstructionsF of b1 -valued non empty finite Function st F c= G holds
LastLoc F <= LastLoc G,T
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; for F, G being NAT -defined the InstructionsF of T -valued non empty finite Function st F c= G holds
LastLoc F <= LastLoc G,T
let F, G be NAT -defined the InstructionsF of T -valued non empty finite Function; ( F c= G implies LastLoc F <= LastLoc G,T )
assume A1:
F c= G
; LastLoc F <= LastLoc G,T
consider N being non empty finite natural-membered set such that
A2:
N = { (locnum (l,T)) where l is Element of NAT : l in dom G }
and
A3:
LastLoc G = il. (T,(max N))
by Def11;
consider M being non empty finite natural-membered set such that
A4:
M = { (locnum (l,T)) where l is Element of NAT : l in dom F }
and
A5:
LastLoc F = il. (T,(max M))
by Def11;
reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED:3;
M c= N
then
max MM <= max NN
by XXREAL_2:59;
hence
LastLoc F <= LastLoc G,T
by A5, A3, Th8; verum