Example -- $IntSet \not<= FatSet$
  • FatSet -- insert, select, size
  • IntSet -- insert, delete, select, size

History property -- not satisfied by $IntSet$

post( push(i) ) ⇒ post( put(i) )[ b : = α(s) ]
slide: History properties -- example