Specification buffer-inf-conv

[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
   buffer, 
   buffer-inf
with
   

   
   constants  σ⊥ : buffer-inf;
   functions  ⌜ . ⌝ : buffer → buffer-inf;
              . .buf : buffer-inf → buffer;
   
   
   
   
   

   

   axioms emptystream :  ⊦ σ⊥ = ⌜λ n. zero⌝ ;
          tostream-size :  ⊦ # ⌜buf⌝  = ⌜# buf⌝ ;
          used for: s, ls;
          tostream-at :  ⊦ n < # buf → ⌜buf⌝ [n] = buf[n];
          used for: s, ls;
          tobuf-size : finp(σ) ⊦ # σ.buf = (# σ).n;
          used for: s, ls;
          tobuf-at : finp(σ), ⌜n⌝  < # σ ⊦ σ.buf[n] = σ[n];
          used for: s, ls;

   

   
end enrich