[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-BSRA
enrich MAKS-BSRA-unwinding
 with
   constants 
      BSP_BSRA : bool; comment: backward strict replace with all (with future ajustments) one C event.;
   
   axioms 
      BSP_BSRA-def
      : ⊦ 
          BSP_BSRA
        ↔ (∀ tr, tr0, ev, ev0. 
              view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ (tr0 + (ev + tr)) ∈TR
            → (∃ tr1. (tr0 + (ev0 + tr1)) ∈TR ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view))));
      comment: backward strict replace with all (with future ajustments) one C event.;
       
end enrich