[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 BSPs
enrich eventfunsHO with
   predicates 
      BSP_SR : (event → viewstate) × (state × event × state → bool);
      comment: strict remove (all C occurrences). This is purge.;
       
      BSP_D : (event → viewstate) × (state × event × state → bool);
      comment: delete (with past and future ajustments) last C event.;
       
      BSP_SD : (event → viewstate) × (state × event × state → bool);
      comment: strict delete (without adjustments) last C event.;
       
      BSP_BSD : (event → viewstate) × (state × event × state → bool);
      comment: backward strict delete (with future, but not past adjustments) last C event.;
       
      BSP_RA : xview × (state × event × state → bool);
      comment: replace with all (with past and future ajustments) one C event.;
       
      BSP_BSRA : xview × (state × event × state → bool);
      comment: backward strict replace with all (with future ajustments) one C event.;
       
   
   axioms 
      BSP_SR-def :  ⊦ BSP_SR(view, trans) ↔ (∀ tr. tr ∈TR trans → proj(tr, VNview(view)) ∈TR trans);
      comment: strict remove (all C occurrences). This is purge.;
       
      BSP_D-def
      : ⊦ 
          BSP_D(view, trans)
        ↔ (∀ tr, tr0, ev. 
              view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = []
            → (∃ tr1, tr2. 
                  tr2 + tr1 ∈TR trans ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = []
                ∧ proj(tr2, VCview(view)) = proj(tr0, VCview(view))));
      comment: delete (with past and future ajustments) last C event.;
       
      BSP_SD-def
      :  ⊦ BSP_SD(view, trans) ↔ (∀ tr, tr0, ev. view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = [] → tr0 + tr ∈TR trans);
      comment: strict delete (without adjustments) last C event.;
       
      BSP_BSD-def
      : ⊦ 
          BSP_BSD(view, trans)
        ↔ (∀ tr, tr0, ev. 
              view(ev) = C ∧ tr0 + (ev + tr) ∈TR trans ∧ proj(tr, Cview(view)) = []
            → (∃ tr1. tr0 + tr1 ∈TR trans ∧ proj(tr1, Vview(view)) = proj(tr, Vview(view)) ∧ proj(tr1, Cview(view)) = []));
      comment: backward strict delete (with future, but not past adjustments) last C event.;
       
      BSP_RA-def
      : ⊦ 
          BSP_RA(mkxview(view, eqrel), trans)
        ↔ (∀ tr, tr0, ev, ev0. 
              view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ tr0 + (ev + tr) ∈TR trans
            → (∃ tr1, tr2. 
                tr2 + (ev0 + tr1) ∈TR trans ∧ proj(tr0, VCview(view)) = proj(tr2, VCview(view)) ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view))));
      comment: replace with all (with past and future ajustments) one C event.;
       
      BSP_BSRA-def
      : ⊦ 
          BSP_BSRA(mkxview(view, eqrel), trans)
        ↔ (∀ tr, tr0, ev, ev0. 
              view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ tr0 + (ev + tr) ∈TR trans
            → (∃ tr1. tr0 + (ev0 + tr1) ∈TR trans ∧ proj(tr, VCview(view)) = proj(tr1, VCview(view))));
      comment: backward strict replace with all (with future ajustments) one C event.;
       
end enrich