let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-Struct of N
for I being NAT -defined FinPartState of
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 N; :: thesis: for I being NAT -defined FinPartState of
for x being set st x in dom I holds
I . x is Instruction of S
let I be NAT -defined FinPartState of ; :: 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= NAT by RELAT_1:def 18;
then reconsider ll = x as Element of NAT by A1;
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