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 F being programmed lower FinPartState of S
for G being programmed FinPartState of S st dom F = dom G holds
G is lower
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being programmed lower FinPartState of S
for G being programmed FinPartState of S st dom F = dom G holds
G is lower
let F be programmed lower FinPartState of S; :: thesis: for G being programmed FinPartState of S st dom F = dom G holds
G is lower
let G be programmed FinPartState of S; :: thesis: ( dom F = dom G implies G is lower )
assume dom F = dom G ; :: thesis: G is lower
hence for l being Instruction-Location of S st l in dom G holds
for m being Instruction-Location of S st m <= l holds
m in dom G by AMISTD_1:def 20; :: according to AMISTD_1:def 20 :: thesis: verum