Inductive evaluationOfRule : Set :=
  | ERuleMatched     : halt -> access -> evaluationOfRule
  | ERuleDidNotMatch : evaluationOfRule
  .
