Specification Koenigs-Lemma-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
with
   functions 
       reach : Graph('a) → Set('a) × Nat → 'a → Bool;
       reach≤ : Graph('a) → Set('a) × Nat → 'a → Bool;
       . ^ . : (List('a) → List('a)) × Nat → List('a) → List('a) prio 12 right;
       haspathanylength : Graph('a) → 'a → Bool;
   
   predicates 
       finout : Graph('a);
       finroot : Graph('a);
       allreachable : Graph('a);
       infgraph : Graph('a);
   
   variables 
       eP : 'a → Bool;
       cf : List('a) → List('a);
       rf : Set('a) × Nat → 'a → Bool;
       x : List('a);
       s : Set('a);
       m : Nat;
       n : Nat;
       a : 'a;
       b : 'a;
       g : Graph('a);
   
   
   axioms 
      it-zero: ((cf ^ 0))(x) = x;
      
      it-succ: ((cf ^ (n + 1)))(x) = cf(((cf ^ n))(x));
      
      infgraph-def: infgraph(g) ↔ (∀ s. ∃ a. dom(g)(a) ∧ ¬ a ∈ s);
      used for: ls;
      
      finroot-def: finroot(g) ↔ (∃ s. ∀ a. isroot(g)(a) ↔ a ∈ s);
      used for: ls;
      
      finout-def: finout(g) ↔ (∀ a. ∃ s. ∀ b. edge(g)(a, b) ↔ b ∈ s);
      used for: ls;
      
      allreachable-def: allreachable(g) ↔ (∀ b. dom(g)(b) → (∃ a. isroot(g)(a) ∧ path(g)(a, b)));
      used for: ls;
      
      reach-def: reach(g)(s, n)(b) ↔ (∃ x. x ≠ [] ∧ x.head ∈ s ∧ pathp(g)(⌜x⌝ ) ∧ b = x.last ∧ # x = n + 1);
      used for: ls;
      
      reachle-def: reach≤(g)(s, n)(b) ↔ (∃ m. m ≤ n ∧ reach(g)(s, m)(b));
      
      haspathanylength-def: haspathanylength(g)(a) ↔ (∀ n. ∃ x. x.head = a ∧ # x = n + 1 ∧ pathp(g)(⌜x⌝ ));
   
   
end enrich