[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 split-finalzeros
enrich nat-even
 , 
       nat-pot
 with
   functions 
      #fz : nat → nat;
      lead : nat → nat;
   
   axioms 
      lead-even : ⊦ 
                  lead(2 * n) = 2 * n + 1;
      used for : s, ls;
       
      finz-even : ⊦ 
                  #fz(2 * n) = 0;
      used for : s, ls;
       
      lead-odd : ⊦ 
                 lead(2 * n + 1) = lead(n);
      used for : s, ls;
       
      finz-odd : ⊦ 
                 #fz(2 * n + 1) = #fz(n) + 1;
      used for : s, ls;
       
end enrich