let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of IL,N
for I being IL -defined FinPartState of S
for x being set st x in dom I holds
I . x is Instruction of S
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of IL,N
for I being IL -defined FinPartState of S
for x being set st x in dom I holds
I . x is Instruction of S
let S be non empty stored-program definite AMI-Struct of IL,N; :: thesis: for I being IL -defined FinPartState of S
for x being set st x in dom I holds
I . x is Instruction of S
let I be IL -defined FinPartState of S; :: thesis: for x being set st x in dom I holds
I . x is Instruction of S
let x be set ; :: thesis: ( x in dom I implies I . x is Instruction of S )
assume A1: x in dom I ; :: thesis: I . x is Instruction of S
dom I c= IL by RELAT_1:def 18;
then reconsider ll = x as Instruction-Location of S by A1, Def4;
consider s being State of S;
(s +* I) . ll = I . x by A1, FUNCT_4:14;
hence I . x is Instruction of S ; :: thesis: verum