enrich trace , 
       xview , 
       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;
      N2Vview : (event → viewstate) → event → viewstate;
      comment: all Ns become Vs.;
       
   predicates 
      isInput : event;
      isOutput : event;
      validx : xview;
       . ∈TR . : trace × (state × event × state → bool);
      isTransition : (state × event × state → bool);
      trans∃ : (state × event × state → bool) × state × trace × state;
      reachable : (state × event × state → bool) × state;
      enabled : (state × event × state → bool) × state × trace;
   variables 
      view : event → viewstate;  comment: This guarantees that V, C, N are a disjoint partion 
                                             of all events.;
      adm, inevs : event → bool; 
      trans : state × event × state → bool; 
   
   axioms 
      input-output-disjoint :  ⊦ ¬ (isInput(ev) ∧ isOutput(ev));
      validx-def
      : ⊦ 
          validx(mkxview(view, eqrel))
        ↔   (∀ ev. view(ev) = C → eqrel(ev, ev)) ∧ (∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) → eqrel(ev0, ev))
          ∧ (∀ ev, ev0, ev1. view(ev) = C ∧ view(ev0) = C ∧ view(ev1) = C ∧ eqrel(ev, ev0) ∧ eqrel(ev0, ev1) → eqrel(ev, ev1))
          ∧ (∀ ev, ev0. view(ev) = C ∧ eqrel(ev, ev0) → view(ev0) = C) ∧ (∀ ev, ev0. view(ev0) = C ∧ eqrel(ev, ev0) → view(ev) = C);
      comment: eqrel is an equivalence relation on C, and Cs are related only to other Cs.;
       
      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(view) = (λ ev. view(ev) = V);
      Cview-def :  ⊦ Cview(view) = (λ ev. view(ev) = C);
      Nview-def :  ⊦ Nview(view) = (λ ev. view(ev) = N);
      VCview-def :  ⊦ VCview(view) = (λ ev. view(ev) = V ∨ view(ev) = C);
      VNview-def :  ⊦ VNview(view) = (λ ev. view(ev) = V ∨ view(ev) = N);
      N2Vview-def :  ⊦ N2Vview(view) = (λ ev. view(ev) = C ⊃ C ; V);
      isTransition-def :  ⊦ isTransition(trans) ↔ (∀ s, s0, s1, ev. trans(s, ev, s0) ∧ trans(s, ev, s1) → s0 = s1);
      transex-empty :  ⊦ trans∃(trans, s, [], s0) ↔ s = s0;
      used for : s, ls;
       
      transex-rec :  ⊦ trans∃(trans, s, ev ' + tr, s0) ↔ (∃ s1. trans(s, ev, s1) ∧ trans∃(trans, s1, tr, s0));
      reachable-def :  ⊦ reachable(trans, s) ↔ (∃ tr. trans∃(trans, S0, tr, s));
      enabled-def :  ⊦ enabled(trans, s, tr) ↔ (∃ s0. trans∃(trans, s, tr, s0));
      in-trace-def :  ⊦ tr ∈TR trans ↔ enabled(trans, S0, tr);
end enrich