[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification MAKS-BSD-unwinding
enrich eventfuns with
   constants 
      osc : bool; comment: output step consistency.;
      lrf : bool; comment: locally-respects forwards.;
   functions 
      view : event → viewstate;
   predicates 
      eqstate : state × state;
   
   axioms 
      osc-def
      : ⊦ 
          osc
        ↔ (∀ s1, s11, s22. 
            ∀ ev. 
               view(ev) ≠ C ∧ reachable(s1) ∧ reachable(s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1)
             → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(s1, tr, s2) ∧ eqstate(s22, s2)));
      lrf-def :  ⊦ lrf ↔ (∀ s, s0. ∀ ev. view(ev) = C → (reachable(s) ∧ trans(s, ev, s0) → eqstate(s0, s)));
end enrich