Specification infgraph-gen

[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
   infgraph-gen-basic, 
   stream, 
   set-union
with
   functions 
       isroot : Graph('a) → 'a → Bool;
       pathp : Graph('a) → Stream('a) → Bool;
       path : Graph('a) → 'a × 'a → Bool;
   
   variables 
       strP : Stream('a) → Bool;
       eP : 'a → Bool;
       g : Graph('a);
       σ : Stream('a);
       a : 'a;
       b : 'a;
       n : Nat;
       x : List('a);
   
   
   axioms 
      isroot-def: isroot(g)(b) ↔ dom(g)(b) ∧ (∀ a. ¬ edge(g)(a, b));
      
      pathp-def: pathp(g)(σ) ↔ (∀ n. ⌜n⌝  < # σ → dom(g)(σ[n])) ∧ (∀ n. ⌜n + 1⌝  < # σ → edge(g)(σ[n], σ[n + 1]));
      
      path-def: path(g)(a, b) ↔ (∃ x. pathp(g)(⌜x⌝ ) ∧ x ≠ [] ∧ a = x.head ∧ b = x.last);
   
   
end enrich