Auth: trait
  introduces
    __ \says __ : P, Bool -> Bool
    __ \speaksFor __ : P, P -> Bool

  asserts
    forall s, s2: Bool, a: P
      % S1, S2 are built in to Larch

      % S3
      (a \says s) /\ (a \says (s => s2)) => (a \says s2)

      % S4
      s => (a \says s)

  implies
    forall s, s2: Bool, a: P
      % s5
      (a says (s /\ s2)) = ((a \says s) /\ (a \says s2))