let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being empty FinPartState of S holds F is lower
let IL be non empty set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for F being empty FinPartState of S holds F is lower
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for F being empty FinPartState of S holds F is lower
let F be empty FinPartState of S; :: thesis: F is lower
let l be Instruction-Location of S; :: according to AMISTD_1:def 20 :: thesis: ( l in dom F implies for m being Instruction-Location of S st m <= l holds
m in dom F )
assume l in dom F ; :: thesis: for m being Instruction-Location of S st m <= l holds
m in dom F
hence for m being Instruction-Location of S st m <= l holds
m in dom F ; :: thesis: verum