IIIR: trait
  % Integration of Internet Information Resources
  % We define the basic information object to be an octet stream
  % subject to some interpretation, called the content type
  % (c.f. MIME).  (Note that this parallels the SGML and HyTime usage
  % of the term /entity/)

  includes
    IntCycle (0 for first, 255 for last, Octet for N),
    String (Octet for E, OctetSeq for C),
    PartialOrder(Time for T),
    Set(Entity, Entities),
    MediaType(MType, MBase)

  introduces

    type: Entity -> MType
    body: Entity -> OctetSeq

    make: MType, OctetSeq -> Entity

    immutable: URI -> Bool

    represent : URI, Time -> Entities
    lastMod : URI, Time -> Time
    expires : URI, Time -> Time


  asserts
    forall u: URI, t, t1, t2: Time
      immutable(u) => represent(u, t1) = represent(u, t2);

      lastMod(u,t) <= t;
      t1 >= lastMod(u, t) /\ t2 >= lastMod(u, t) =>
        represent(u, t1) = represent(u, t2);

      expires(u, t) >= t;
      t <= t1 /\ t1 <= expires(u, t) /\ t <= t2 /\ t2 <= expires(u, t) =>
	represent(u, t1) = represent(u, t2);