[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 abs-FLIT-FLITPSCweak
enrich
   FLITPSCweak, 
   FLIT
with
   functions 
       propFOs : T × L × List(Bevent) → List(FOW);
   
   predicates 
       reorder : (L → List(FOW)) × (L → List(FOW)) × (T → List(Bevent));
       reorder : L × List(FOW) × List(FOW) × (T → List(Bevent));
   
   variables 
       be : Bevent;
       bel : List(Bevent);
       bq : T → List(Bevent);
       rfo : T → List(Bevent);
       l : L;
       v : V;
       t : T;
       p : L → List(FOW);
       pq : L → List(FOW);
       writers : L → Set(T);
       ws : Set(T);
       m : Nat;
       n : Nat;
       fowl : List(FOW);
       fow : FOW;
       pmem : L → V;
       mem : L → V;
       bv : Bool;
   
   
   axioms 
      reorder-def: reorder(p, pq, rfo) ↔ (∀ l. reorder(l, p(l), pq(l), rfo));
      used for: ls;
      
      reorder-base: reorder(l, [], fowl0, rfo) ↔ fowl0 = [] ∧ (∀ t. propFOs(t, l, rfo(t)) = []);
      used for: s, ls;
      
      reorder-rec-FO: 
        reorder(l, FO(t) ' + fowl, fowl0, rfo)
      ↔   (∃ fowl1, fowl2. fowl0 = fowl1 + FO(t) ' + fowl2 ∧ fowl1 | t = [] ∧ reorder(l, fowl, fowl1 + fowl2, rfo))
        ∨ fowl0 | t = [] ∧ FO(l) ∈ rfo(t) ∧ reorder(l, fowl, fowl0, rfo(t := rfo(t) -1l FO(l)));
      used for: s, ls;
      
      reorder-rec-W: reorder(l, W(v, t) ' + fowl0, fowl1, rfo) ↔ fowl1 ≠ [] ∧ fowl1.head = W(v, t) ∧ reorder(l, fowl0, fowl1.tail, rfo);
      used for: s, ls;
      
      propFOs-base: propFOs(t, l, []) = [];
      used for: s, ls;
      
      propFOs-SF: propFOs(t, l, SF ' + bel) = propFOs(t, l, bel);
      used for: s, ls;
      
      propFOs-FO-same: propFOs(t, l, FO(l) ' + bel) = FO(t) + propFOs(t, l, bel);
      used for: s, ls;
      
      propFOs-FO-other: l ≠ l0 → propFOs(t, l, FO(l0) ' + bel) = propFOs(t, l, bel);
      used for: s, ls, lc;
      
      propFOs-W: propFOs(t, l, W(l0, v) ' + bel) = propFOs(t, l, bel);
      used for: s, ls;
   
   
end enrich