Picture Omitted
slide
:
Abstraction function and representation invariant