(reset)
(
knowledge: type.
msg <: knowledge.
I: knowledge -> state. --- intruder memory predicate

dolevyao: {
  INT: forall t: msg.
    N(t) => I(t).
}
)