webarch: trait
  % World Wide Web

  includes
    PartialOrder(Time for T)

  introduces

    identify   : URI -> Resource
    represent  : Entity, Resource, Time, Time -> Bool
    repr       : Entity, URI, Time, Time -> Bool

    combine    : URI, URI -> URI
    abs        : URI -> bool

    link       : Anchor, Anchor, Time, Time -> Bool
    addr       : URI, Fragment -> Anchor

    id         : Fragment, Element, Entity -> Bool
    linkmarkup : Entity, Element, URI, Fragment -> Bool
    basemarkup : Entity, URI

  asserts
    forall e: Entity, el: Element, fh, ft: Fragment,
           i, ih, it: URI, t1, t2, t3, t4: Time

      repr(e, i, t1, t2) == represent(e, identify(i), t1, t2);

      repr(e, i, t1, t2) /\ t1 <= t3 /\ t3 <= t4 /\ t4 <= t2 =>
		repr(e, i, t3, t4)

      abs(i) => combine(it, i) = i

      repr(e, it, t1, t2) /\ linkmarkup(e, el, ih, fh) /\ id(ft, el, e) =>
          link(addr(it, ft), addr(combine(it, ih), fh), t1, t2)

      basemarkup(e, it) /\ repr(e, i, t1, t2) => repr(e, it, t1, t2)