[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 termfuns
enrich term_or_none with
   functions 
      # : term_or_none → nat;
      ks : nat → term;
   predicates 
      hasS : term_or_none;
      hasS : term;
   
   axioms 
      ks-zero :  ⊦ ks(0) = K;
      used for : s, ls;
       
      ks-rec :  ⊦ ks(n + 1) = ks(n) _ K;
      used for : s, ls;
       
      hasS-none :  ⊦ ¬ hasS(none);
      used for : s, ls;
       
      hasS-some :  ⊦ hasS(some(t)) ↔ hasS(t);
      used for : s, ls;
       
      hasS-K :  ⊦ ¬ hasS(K);
      used for : s, ls;
       
      hasS-S :  ⊦ hasS(S);
      used for : s, ls;
       
      hasS-A :  ⊦ hasS(t _ t0) ↔ hasS(t) ∨ hasS(t0);
      used for : s, ls;
       
      size-none :  ⊦ #(none) = 0;
      used for : s, ls;
       
      size-some :  ⊦ #(some(t)) = #(t);
      used for : s, ls;
       
end enrich