enrich trace , 
       view , 
       state with
   functions 
      proj : trace × (event → bool) → trace;
      Vview : (event → viewstate) → event → bool;
      Cview : (event → viewstate) → event → bool;
      Nview : (event → viewstate) → event → bool;
      VCview : (event → viewstate) → event → bool;
      VNview : (event → viewstate) → event → bool;
   predicates 
      trans : state × event × state;
      isInput : event;
      isOutput : event;
       . ∈TR : trace;
      trans∃ : state × trace × state;
      reachable : state;
      enabled : state × trace;
   variables 
      viewvar : event → viewstate; 
      inevs : event → bool; 
   
   axioms 
      input-output-disjoint :  ⊦ ¬ (isInput(ev) ∧ isOutput(ev));
      projection-empty :  ⊦ proj([], inevs) = [];
      used for : s, ls;
       
      projection-remove :  ⊦ ¬ inevs(ev) → proj(ev ' + tr, inevs) = proj(tr, inevs);
      used for : s, ls;
       
      projection-keep :  ⊦ inevs(ev) → proj(ev ' + tr, inevs) = ev ' + proj(tr, inevs);
      used for : s, ls;
       
      Vview-def :  ⊦ Vview(viewvar) = (λ ev. viewvar(ev) = V);
      Cview-def :  ⊦ Cview(viewvar) = (λ ev. viewvar(ev) = C);
      Nview-def :  ⊦ Nview(viewvar) = (λ ev. viewvar(ev) = N);
      VCview-def :  ⊦ VCview(viewvar) = (λ ev. viewvar(ev) = V ∨ viewvar(ev) = C);
      VNview-def :  ⊦ VNview(viewvar) = (λ ev. viewvar(ev) = V ∨ viewvar(ev) = N);
      isTransition-def :  ⊦ ∀ s, s0, s1, ev. trans(s, ev, s0) ∧ trans(s, ev, s1) → s0 = s1;
      transex-empty :  ⊦ trans∃(s, [], s0) ↔ s = s0;
      used for : s, ls;
       
      transex-rec :  ⊦ trans∃(s, ev ' + tr, s0) ↔ (∃ s1. trans(s, ev, s1) ∧ trans∃(s1, tr, s0));
      reachable-def :  ⊦ reachable(s) ↔ (∃ tr. trans∃(S0, tr, s));
      enabled-def :  ⊦ enabled(s, tr) ↔ (∃ s0. trans∃(s, tr, s0));
      in-trace-def :  ⊦ tr ∈TR ↔ enabled(S0, tr);
end enrich