enrich BSPs with
   predicates 
      osc : (event → viewstate) × (state × event × state → bool) × (state × state → bool);
      comment: output step consistency.;
       
      xosc : xview × (state × event × state → bool) × (state × state → bool);
      comment: output step consistency for extended views (for RA, RAE, RS).;
       
      lrf : (event → viewstate) × (state × event × state → bool) × (state × state → bool);
      comment: locally-respects forwards.;
       
      xlrf : xview × (state × event × state → bool) × (state × state → bool);
      comment: locally-respects forwards for extended views (for RA, RAE, RS).;
       
      isEqRel : (state × state → bool);
      comment: true if eqstate is an equivalence relation.;
       
   variables 
      eqstate : state × state → bool; 
   
   axioms 
      isEqRel-def
      : ⊦ 
          isEqRel(eqstate)
        ↔ (∀ s. eqstate(s, s)) ∧ (∀ s, s0. eqstate(s, s0) → eqstate(s0, s)) ∧ (∀ s, s0, s1. eqstate(s, s0) ∧ eqstate(s0, s1) → eqstate(s, s1));
      comment: equivalence relation: reflexive, symmetric, transitive.;
       
      osc-def
      : ⊦ 
          osc(view, trans, eqstate)
        ↔ (∀ s1, s11, s22. 
            ∀ ev. 
               view(ev) ≠ C ∧ reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1)
             → (∃ s2. 
                 ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s22, s2)));
      comment: output step consistency.
                             view(ev) = N → tr can contain only N events, possibly tr = [].
                             view(ev) = V → tr must contain ev and possibly N events.;
       
      xosc-def
      : ⊦ 
          xosc(mkxview(view, eqrel), trans, eqstate)
        ↔ (∀ s1, s11, s22. 
            ∀ ev. 
               view(ev) ≠ C ∧ reachable(trans, s1) ∧ reachable(trans, s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1)
             → (∃ s2. 
                 ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(trans, s1, tr, s2) ∧ eqstate(s22, s2)));
      comment: identical to osc.;
       
      lrf-def :  ⊦ lrf(view, trans, eqstate) ↔ (∀ s, s0. ∀ ev. view(ev) = C → (reachable(trans, s) ∧ trans(s, ev, s0) → eqstate(s0, s)));
      xlrf-def
      : ⊦ 
          xlrf(mkxview(view, eqrel), trans, eqstate)
        ↔ (∀ s, s0, s1. 
            ∀ ev, ev0. 
               view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ reachable(trans, s) ∧ trans(s, ev, s0) ∧ eqstate(s, s1) ∧ reachable(trans, s1)
             → (∃ s2. trans(s1, ev0, s2) ∧ eqstate(s0, s2)));
end enrich