[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 graph
enrich set-union
 , 
       list-last
 with
comment: successor function succ, paths, reachability.;
   functions 
      succ : elem → set;
   predicates 
      path : list;
      reach : elem × elem × nat;
      comment: reach(a,b,n) = there is a path from a to b of length n.;
       
      reach< : elem × elem × nat;
      comment: reach<(a,b,n) = there is a path with length less than n.;
       
      reachS : elem × set × nat;
      comment: reach(a,S,n) = all of S are reachable in n steps, but none in fewer.;
       
   variables 
      S : set; 
   
   axioms 
      reach-zero :  ⊦ reach(a, b, 0) ↔ a = b;
      used for : s, ls;
       
      reach-succ :  ⊦ reach(a, b, n + 1) ↔ (∃ c. reach(a, c, n) ∧ b ∈ succ(c));
      used for : s, ls;
       
      reachls-def :  ⊦ reach<(a, b, n) ↔ (∃ m. m < n ∧ reach(a, b, m));
      reachset-def :  ⊦ reachS(a, S, n) ↔ (∀ b. b ∈ S → reach(a, b, n) ∧ ¬ reach<(a, b, n));
      path-base :  ⊦ ¬ path([]);
      used for : s, ls;
       
      path-one :  ⊦ path(a ');
      used for : s, ls;
       
      path-rec :  ⊦ path(x + a ' + b ') ↔ b ∈ succ(a) ∧ path(x + a ');
      used for : s, ls;
       
end enrich