[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 caterpillar-refines-tree-buffer
asm refinement
   

   export caterpillar-asm


   import tree-buffer-asm


   using tree-buffer-asm
, 
         caterpillar-asm


   

   by mapping tree_buffer_init# → caterpillar_init#, tree_buffer_add# → caterpillar_add#, tree_buffer_get# → caterpillar_get#

   abstraction λ h, xs, xs_len, ys, h0, xs0. prefixn(h0, xs + ys) = prefixn(h0, xs0) ∧ #(xs + ys) ≤ # xs0 ∧ h0 = h;

   
end asm refinement