Specification reachable

[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
   relops, 
   polyref, 
   set-union
with
   functions 
       reach : Ref[A] × (Ref[A] × Ref[A] → Bool) → Set[Ref[A]];
   
   variables 
       rrp : Ref[A] × Ref[A] → Bool;
       r : Ref[A];
   
   
   axioms 
      reachset: r1 ∈ reach(r0, rrp) ↔ rrp.^*(r0, r1);
      used for: s, ls;
   
   
end enrich