[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 infgraph-gen-basic
specification
   sorts Graph('a);
   functions 
       dom : Graph('a) → 'a → Bool;
       edge : Graph('a) → 'a × 'a → Bool;
       . × . : ('a → Bool) × ('a × 'a → Bool) → Graph('a);
   
   variables 
       g : Graph('a);
       g1 : Graph('a);
       g2 : Graph('a);
       vs : 'a → Bool;
       es : 'a × 'a → Bool;
       a : 'a;
       b : 'a;
   
   
   induction 
      Graph('a) generated by ×;
   
   axioms 
      dom-def: dom(vs × es) = vs;
      
      edge-def: edge(vs × es)(a, b) ↔ es(a, b) ∧ vs(a) ∧ vs(b);
      
      extensionality: g1 = g2 ↔ dom(g1) = dom(g2) ∧ edge(g1) = edge(g2);
   
   end specification