Specification MAKS-BSD

[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,

enrich MAKS-BSD-unwinding
 with
   constants 
      BSP_BSD : bool;
   
   axioms 
      BSP_BSD-def
      : ⊦ 
          BSP_BSD
        ↔ (∀ tr, tr0, ev. 
              view(ev) = C ∧ (tr0 + (ev + tr)) ∈TR ∧ proj(tr, Cview(view)) = []
            → (∃ tr1. (tr0 + tr1) ∈TR ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = []));
end enrich