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, 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; :: thesis: 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; :: thesis: ( F c= G implies LastLoc F <= LastLoc G,T )
assume A1: F c= G ; :: thesis: 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
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in M or a in N )
assume a in M ; :: thesis: a in N
then A6: ex l being Element of NAT st
( a = locnum (l,T) & l in dom F ) by A4;
dom F c= dom G by A1, GRFUNC_1:2;
hence a in N by A2, A6; :: thesis: verum
end;
then max MM <= max NN by XXREAL_2:59;
hence LastLoc F <= LastLoc G,T by A5, A3, Th8; :: thesis: verum